Update the HOL4 proofs for the last *release* version of HOL4

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.