summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4')
-rw-r--r--backends/hol4/divDefLibTestTheory.sig5
-rw-r--r--backends/hol4/divDefNoFixLibTestTheory.sig51
-rw-r--r--backends/hol4/primitivesTheory.sig226
3 files changed, 137 insertions, 145 deletions
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index d8cc4ab5..2df28a2f 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -53,7 +53,6 @@ sig
val tree_distinct : thm
val tree_induction : thm
val tree_nchotomy : thm
- val tree_size_eq : thm
val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -434,10 +433,6 @@ sig
⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n
- [tree_size_eq] Theorem
-
- ⊢ tree1_size f = list_size (tree_size f)
-
*)
end
diff --git a/backends/hol4/divDefNoFixLibTestTheory.sig b/backends/hol4/divDefNoFixLibTestTheory.sig
index 999cf543..6c8f373c 100644
--- a/backends/hol4/divDefNoFixLibTestTheory.sig
+++ b/backends/hol4/divDefNoFixLibTestTheory.sig
@@ -5,12 +5,12 @@ sig
(* Definitions *)
val even___E_def : thm
val even___P_def : thm
- val even___fuel0_def_UNION_extract0 : thm
- val even___fuel0_def_UNION_extract1 : thm
- val even___fuel0_def_UNION_primitive : thm
- val even___fuel_def_UNION_extract0 : thm
- val even___fuel_def_UNION_extract1 : thm
- val even___fuel_def_UNION_primitive : thm
+ val even___fuel0_UNION_extract0_def : thm
+ val even___fuel0_UNION_extract1_def : thm
+ val even___fuel0_UNION_primitive_def : thm
+ val even___fuel_UNION_extract0_def : thm
+ val even___fuel_UNION_extract1_def : thm
+ val even___fuel_UNION_primitive_def : thm
val even_def : thm
val list_t_TY_DEF : thm
val list_t_case_def : thm
@@ -56,17 +56,17 @@ sig
⊢ ∀i $var$($n).
even___P i $var$($n) ⇔ ¬is_diverge (even___fuel0 $var$($n) i)
- [even___fuel0_def_UNION_extract0] Definition
+ [even___fuel0_UNION_extract0_def] Definition
- ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_def_UNION (INL (x,x0))
+ ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_UNION (INL (x,x0))
- [even___fuel0_def_UNION_extract1] Definition
+ [even___fuel0_UNION_extract1_def] Definition
- ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_def_UNION (INR (x,x0))
+ ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_UNION (INR (x,x0))
- [even___fuel0_def_UNION_primitive] Definition
+ [even___fuel0_UNION_primitive_def] Definition
- ⊢ even___fuel0_def_UNION =
+ ⊢ even___fuel0_UNION =
WFREC
(@R. WF R ∧
(∀i $var$($n) $var$($m).
@@ -75,7 +75,7 @@ sig
∀i $var$($n) $var$($m).
$var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
R (INL ($var$($m),i − 1)) (INR ($var$($n),i)))
- (λeven___fuel0_def_UNION a.
+ (λeven___fuel0_UNION a.
case a of
INL ($var$($n),i) =>
I
@@ -85,9 +85,7 @@ sig
if i = 0 then do b <- Return T; Return b od
else
do
- b <-
- even___fuel0_def_UNION
- (INR ($var$($m),i − 1));
+ b <- even___fuel0_UNION (INR ($var$($m),i − 1));
Return b
od)
| INR ($var$($n'),i') =>
@@ -98,22 +96,21 @@ sig
if i' = 0 then do b <- Return F; Return b od
else
do
- b <-
- even___fuel0_def_UNION (INL ($var$($m),i' − 1));
+ b <- even___fuel0_UNION (INL ($var$($m),i' − 1));
Return b
od))
- [even___fuel_def_UNION_extract0] Definition
+ [even___fuel_UNION_extract0_def] Definition
- ⊢ ∀x x0. even___fuel x x0 = even___fuel_def_UNION (INL (x,x0))
+ ⊢ ∀x x0. even___fuel x x0 = even___fuel_UNION (INL (x,x0))
- [even___fuel_def_UNION_extract1] Definition
+ [even___fuel_UNION_extract1_def] Definition
- ⊢ ∀x x0. odd___fuel x x0 = even___fuel_def_UNION (INR (x,x0))
+ ⊢ ∀x x0. odd___fuel x x0 = even___fuel_UNION (INR (x,x0))
- [even___fuel_def_UNION_primitive] Definition
+ [even___fuel_UNION_primitive_def] Definition
- ⊢ even___fuel_def_UNION =
+ ⊢ even___fuel_UNION =
WFREC
(@R. WF R ∧
(∀i $var$($n) $var$($m).
@@ -122,7 +119,7 @@ sig
∀i $var$($n) $var$($m).
$var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
R (INL ($var$($m),i − 1)) (INR ($var$($n),i)))
- (λeven___fuel_def_UNION a.
+ (λeven___fuel_UNION a.
case a of
INL ($var$($n),i) =>
I
@@ -130,14 +127,14 @@ sig
0 => Diverge
| SUC $var$($m) =>
if i = 0 then Return T
- else even___fuel_def_UNION (INR ($var$($m),i − 1)))
+ else even___fuel_UNION (INR ($var$($m),i − 1)))
| INR ($var$($n'),i') =>
I
(case $var$($n') of
0 => Diverge
| SUC $var$($m) =>
if i' = 0 then Return F
- else even___fuel_def_UNION (INL ($var$($m),i' − 1))))
+ else even___fuel_UNION (INL ($var$($m),i' − 1))))
[even_def] Definition
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index ae7f083d..6660b02d 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -359,195 +359,200 @@ sig
[string] Parent theory of "primitives"
- [isize_bounds] Axiom
-
- [oracles: ] [axioms: isize_bounds] []
- ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max
-
- [usize_bounds] Axiom
-
- [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max
-
- [isize_to_int_bounds] Axiom
+ [i128_to_int_bounds] Axiom
- [oracles: ] [axioms: isize_to_int_bounds] []
- ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
+ [oracles: ] [axioms: i128_to_int_bounds] []
+ ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
- [i8_to_int_bounds] Axiom
+ [i128_to_int_int_to_i128] Axiom
- [oracles: ] [axioms: i8_to_int_bounds] []
- ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
+ [oracles: ] [axioms: i128_to_int_int_to_i128] []
+ ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
[i16_to_int_bounds] Axiom
[oracles: ] [axioms: i16_to_int_bounds] []
⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
+ [i16_to_int_int_to_i16] Axiom
+
+ [oracles: ] [axioms: i16_to_int_int_to_i16] []
+ ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+
[i32_to_int_bounds] Axiom
[oracles: ] [axioms: i32_to_int_bounds] []
⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
+ [i32_to_int_int_to_i32] Axiom
+
+ [oracles: ] [axioms: i32_to_int_int_to_i32] []
+ ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+
[i64_to_int_bounds] Axiom
[oracles: ] [axioms: i64_to_int_bounds] []
⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
- [i128_to_int_bounds] Axiom
+ [i64_to_int_int_to_i64] Axiom
- [oracles: ] [axioms: i128_to_int_bounds] []
- ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
+ [oracles: ] [axioms: i64_to_int_int_to_i64] []
+ ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
- [usize_to_int_bounds] Axiom
+ [i8_to_int_bounds] Axiom
- [oracles: ] [axioms: usize_to_int_bounds] []
- ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+ [oracles: ] [axioms: i8_to_int_bounds] []
+ ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
- [u8_to_int_bounds] Axiom
+ [i8_to_int_int_to_i8] Axiom
- [oracles: ] [axioms: u8_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+ [oracles: ] [axioms: i8_to_int_int_to_i8] []
+ ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
- [u16_to_int_bounds] Axiom
+ [int_to_i128_i128_to_int] Axiom
- [oracles: ] [axioms: u16_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+ [oracles: ] [axioms: int_to_i128_i128_to_int] []
+ ⊢ ∀i. int_to_i128 (i128_to_int i) = i
- [u32_to_int_bounds] Axiom
+ [int_to_i16_i16_to_int] Axiom
- [oracles: ] [axioms: u32_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+ [oracles: ] [axioms: int_to_i16_i16_to_int] []
+ ⊢ ∀i. int_to_i16 (i16_to_int i) = i
- [u64_to_int_bounds] Axiom
+ [int_to_i32_i32_to_int] Axiom
- [oracles: ] [axioms: u64_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+ [oracles: ] [axioms: int_to_i32_i32_to_int] []
+ ⊢ ∀i. int_to_i32 (i32_to_int i) = i
- [u128_to_int_bounds] Axiom
+ [int_to_i64_i64_to_int] Axiom
- [oracles: ] [axioms: u128_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
+ [oracles: ] [axioms: int_to_i64_i64_to_int] []
+ ⊢ ∀i. int_to_i64 (i64_to_int i) = i
- [isize_to_int_int_to_isize] Axiom
+ [int_to_i8_i8_to_int] Axiom
- [oracles: ] [axioms: isize_to_int_int_to_isize] []
- ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
- isize_to_int (int_to_isize n) = n
+ [oracles: ] [axioms: int_to_i8_i8_to_int] []
+ ⊢ ∀i. int_to_i8 (i8_to_int i) = i
- [i8_to_int_int_to_i8] Axiom
+ [int_to_isize_isize_to_int] Axiom
- [oracles: ] [axioms: i8_to_int_int_to_i8] []
- ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
+ [oracles: ] [axioms: int_to_isize_isize_to_int] []
+ ⊢ ∀i. int_to_isize (isize_to_int i) = i
- [i16_to_int_int_to_i16] Axiom
+ [int_to_u128_u128_to_int] Axiom
- [oracles: ] [axioms: i16_to_int_int_to_i16] []
- ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+ [oracles: ] [axioms: int_to_u128_u128_to_int] []
+ ⊢ ∀i. int_to_u128 (u128_to_int i) = i
- [i32_to_int_int_to_i32] Axiom
+ [int_to_u16_u16_to_int] Axiom
- [oracles: ] [axioms: i32_to_int_int_to_i32] []
- ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+ [oracles: ] [axioms: int_to_u16_u16_to_int] []
+ ⊢ ∀i. int_to_u16 (u16_to_int i) = i
- [i64_to_int_int_to_i64] Axiom
+ [int_to_u32_u32_to_int] Axiom
- [oracles: ] [axioms: i64_to_int_int_to_i64] []
- ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
+ [oracles: ] [axioms: int_to_u32_u32_to_int] []
+ ⊢ ∀i. int_to_u32 (u32_to_int i) = i
- [i128_to_int_int_to_i128] Axiom
+ [int_to_u64_u64_to_int] Axiom
- [oracles: ] [axioms: i128_to_int_int_to_i128] []
- ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
+ [oracles: ] [axioms: int_to_u64_u64_to_int] []
+ ⊢ ∀i. int_to_u64 (u64_to_int i) = i
- [usize_to_int_int_to_usize] Axiom
+ [int_to_u8_u8_to_int] Axiom
- [oracles: ] [axioms: usize_to_int_int_to_usize] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n
+ [oracles: ] [axioms: int_to_u8_u8_to_int] []
+ ⊢ ∀i. int_to_u8 (u8_to_int i) = i
- [u8_to_int_int_to_u8] Axiom
+ [int_to_usize_usize_to_int] Axiom
- [oracles: ] [axioms: u8_to_int_int_to_u8] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
+ [oracles: ] [axioms: int_to_usize_usize_to_int] []
+ ⊢ ∀i. int_to_usize (usize_to_int i) = i
- [u16_to_int_int_to_u16] Axiom
+ [isize_bounds] Axiom
- [oracles: ] [axioms: u16_to_int_int_to_u16] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
+ [oracles: ] [axioms: isize_bounds] []
+ ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max
- [u32_to_int_int_to_u32] Axiom
+ [isize_to_int_bounds] Axiom
- [oracles: ] [axioms: u32_to_int_int_to_u32] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+ [oracles: ] [axioms: isize_to_int_bounds] []
+ ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
- [u64_to_int_int_to_u64] Axiom
+ [isize_to_int_int_to_isize] Axiom
- [oracles: ] [axioms: u64_to_int_int_to_u64] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
+ [oracles: ] [axioms: isize_to_int_int_to_isize] []
+ ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒
+ isize_to_int (int_to_isize n) = n
+
+ [mk_vec_axiom] Axiom
+
+ [oracles: ] [axioms: mk_vec_axiom] []
+ ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l
+
+ [u128_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u128_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
[u128_to_int_int_to_u128] Axiom
[oracles: ] [axioms: u128_to_int_int_to_u128] []
⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
- [int_to_i8_i8_to_int] Axiom
-
- [oracles: ] [axioms: int_to_i8_i8_to_int] []
- ⊢ ∀i. int_to_i8 (i8_to_int i) = i
-
- [int_to_i16_i16_to_int] Axiom
+ [u16_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i16_i16_to_int] []
- ⊢ ∀i. int_to_i16 (i16_to_int i) = i
+ [oracles: ] [axioms: u16_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
- [int_to_i32_i32_to_int] Axiom
+ [u16_to_int_int_to_u16] Axiom
- [oracles: ] [axioms: int_to_i32_i32_to_int] []
- ⊢ ∀i. int_to_i32 (i32_to_int i) = i
+ [oracles: ] [axioms: u16_to_int_int_to_u16] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
- [int_to_i64_i64_to_int] Axiom
+ [u32_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i64_i64_to_int] []
- ⊢ ∀i. int_to_i64 (i64_to_int i) = i
+ [oracles: ] [axioms: u32_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
- [int_to_i128_i128_to_int] Axiom
+ [u32_to_int_int_to_u32] Axiom
- [oracles: ] [axioms: int_to_i128_i128_to_int] []
- ⊢ ∀i. int_to_i128 (i128_to_int i) = i
+ [oracles: ] [axioms: u32_to_int_int_to_u32] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
- [int_to_isize_isize_to_int] Axiom
+ [u64_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_isize_isize_to_int] []
- ⊢ ∀i. int_to_isize (isize_to_int i) = i
+ [oracles: ] [axioms: u64_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
- [int_to_u8_u8_to_int] Axiom
+ [u64_to_int_int_to_u64] Axiom
- [oracles: ] [axioms: int_to_u8_u8_to_int] []
- ⊢ ∀i. int_to_u8 (u8_to_int i) = i
+ [oracles: ] [axioms: u64_to_int_int_to_u64] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
- [int_to_u16_u16_to_int] Axiom
+ [u8_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_u16_u16_to_int] []
- ⊢ ∀i. int_to_u16 (u16_to_int i) = i
+ [oracles: ] [axioms: u8_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
- [int_to_u32_u32_to_int] Axiom
+ [u8_to_int_int_to_u8] Axiom
- [oracles: ] [axioms: int_to_u32_u32_to_int] []
- ⊢ ∀i. int_to_u32 (u32_to_int i) = i
+ [oracles: ] [axioms: u8_to_int_int_to_u8] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
- [int_to_u64_u64_to_int] Axiom
+ [usize_bounds] Axiom
- [oracles: ] [axioms: int_to_u64_u64_to_int] []
- ⊢ ∀i. int_to_u64 (u64_to_int i) = i
+ [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max
- [int_to_u128_u128_to_int] Axiom
+ [usize_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_u128_u128_to_int] []
- ⊢ ∀i. int_to_u128 (u128_to_int i) = i
+ [oracles: ] [axioms: usize_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
- [int_to_usize_usize_to_int] Axiom
+ [usize_to_int_int_to_usize] Axiom
- [oracles: ] [axioms: int_to_usize_usize_to_int] []
- ⊢ ∀i. int_to_usize (usize_to_int i) = i
+ [oracles: ] [axioms: usize_to_int_int_to_usize] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n
[vec_to_list_num_bounds] Axiom
@@ -555,11 +560,6 @@ sig
⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧
LENGTH (vec_to_list v) ≤ Num usize_max
- [mk_vec_axiom] Axiom
-
- [oracles: ] [axioms: mk_vec_axiom] []
- ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l
-
[bind_def] Definition
⊢ ∀x f.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:16:40 +0000