Cleanup a bit

1 files changed, 3 insertions, 178 deletions

diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index b7bc978f..5dba408e 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1173,183 +1173,6 @@ val vec_to_list_num_bounds =
   new_axiom ("vec_to_list_num_bounds",
     “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”)
 
-(*
-Theorem vec_to_list_int_bounds:
-  !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max
-Proof
-  gen_tac >>
-  assume_tac vec_to_list_num_bounds >>
-  pop_assum (qspec_assume ‘v’) >>
-  pop_assum mp_tac >>
-  pure_once_rewrite_tac [GSYM INT_LE] >>
-  sg ‘0 ≤ usize_max’ >- (assume_tac usize_bounds >> fs [u16_max_def] >> cooper_tac) >>
-  metis_tac [INT_OF_NUM]
-QED
-
-val vec_len_def = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’
-Theorem vec_len_spec:
-  ∀v.
-    vec_len v = int_to_usize (&(LENGTH (vec_to_list v))) ∧
-    0 ≤ &(LENGTH (vec_to_list v)) ∧ &(LENGTH (vec_to_list v)) ≤ usize_max
-Proof
-  gen_tac >> rw [vec_len_def] >>
-  qspec_assume ‘v’ vec_to_list_int_bounds >>
-  fs []
-QED
-
-val mk_vec_spec = new_axiom ("mk_vec_spec",
-  “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
-
-val vec_new_def = Define ‘vec_new = case mk_vec [] of Return v => v’
-Theorem vec_new_spec:
-  vec_to_list vec_new = []
-Proof
-  rw [vec_new_def] >>
-  qabbrev_tac ‘l = []’ >>
-  qspec_assume ‘l’ mk_vec_spec >>
-  Cases_on ‘mk_vec l’ >>
-  rfs [markerTheory.Abbrev_def, not_le_eq_gt] >> fs [] >>
-  assume_tac usize_bounds >> fs[u16_max_def] >> try_tac (exfalso >> cooper_tac) >>
-  sg ‘0 ≤ usize_max’ >- cooper_tac >>
-  fs []
-QED
-
-val vec_push_def = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’
-Theorem vec_push_spec:
-  ∀v x. usize_to_int (vec_len v) < usize_max ⇒
-    ∃vx. vec_push_back v x = Return vx ∧
-    vec_to_list vx = vec_to_list v ++ [x]
-Proof
-  rpt strip_tac >> fs [vec_push_def] >>
-  qspec_assume ‘v’ vec_len_spec >> rw [] >>
-  qspec_assume ‘vec_to_list v ++ [x]’ mk_vec_spec >>
-  fs [vec_len_def] >> rw [] >>
-  pop_assum irule >>
-  pop_last_assum mp_tac >>
-  dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >>
-  cooper_tac
-QED
-
-val update_def = Define ‘
-  update ([] : 'a list) (i : num) (y : 'a) : 'a list = [] ∧
-  update (_ :: ls) (0: num) y = y :: ls ∧
-  update (x :: ls) (SUC i) y = x :: update ls i y
-’
-
-Theorem update_length:
-  ∀ls i y. LENGTH (update ls i y) = LENGTH ls
-Proof
-  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def]
-QED
-
-Theorem update_spec:
-  ∀ls i y. i < LENGTH ls ==>
-    LENGTH (update ls i y) = LENGTH ls ∧
-    EL i (update ls i y) = y ∧
-    ∀j. j < LENGTH ls ⇒ j ≠ i ⇒ EL j (update ls i y) = EL j ls
-Proof
-  Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] >>
-  Cases_on ‘j’ >> fs []
-QED
-*)
-
-(*
-(* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *)
-val vec_index_def = Define ‘
-  vec_index i v =
-    if usize_to_int i ≤ usize_to_int (vec_len v)
-    then Return (EL (Num (usize_to_int i)) (vec_to_list v))
-    else Fail Failure’
-*)
-
-(* TODO: shortcut for qspec_then ... ASSUME_TAC *)
-(* TODO: use cooper_tac everywhere *)
-(* TODO: use pure_once_rewrite_tac everywhere *)
-
-(*
-Theorem usize_to_int_inj:
-  ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
-Proof
-  metis_tac [int_to_usize_usize_to_int]
-QED
-
-Theorem usize_to_int_neq_inj:
-  ∀i j. i <> j ==> usize_to_int i <> usize_to_int j
-Proof
-  metis_tac [usize_to_int_inj]
-QED
-*)
-
-Theorem int_of_num_neq_inj:
-  ∀n m. &n ≠ &m ⇒ n ≠ m
-Proof
-  metis_tac [int_of_num_inj]
-QED
-
-(* TODO: automate: take assumption, intro first premise as subgoal *)
-
-(* TODO: I think we should express as much as we could in terms of integers (not machine integers).
-
-   For instance:
-   - theorem below: ‘j <> i’ ~~> ‘usize_to_int j <> usize_to_int i’
-   - we should prove theorems like: ‘usize_eq i j <=> usize_to_int i = usize_to_int j’
-     (that we would automatically apply)
-*)
-
-(*
-  &(SUC n) = 1 + &n
-  n < m
-  &n < &m
-*)
-
-(*
-val vec_insert_back_def = Define ‘
-  vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’
-
-Theorem vec_insert_back_spec:
-  ∀v i x.
-    usize_to_int i < usize_to_int (vec_len v) ⇒
-    ∃nv. vec_insert_back v i x = Return nv ∧
-    vec_len v = vec_len nv ∧
-    vec_index i nv = Return x ∧
-    (* TODO: usize_to_int j ≠ usize_to_int i ? *)
-    (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ j ≠ i ⇒ vec_index j nv = vec_index j v)
-Proof
-  rpt strip_tac >> fs [vec_insert_back_def] >>
-  qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ mk_vec_spec >>
-  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_length >>
-  fs [] >>
-  qspec_assume ‘v’ vec_len_spec >>
-  rw [] >> gvs [] >>
-  fs [vec_len_def, vec_index_def] >>
-  sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’
-  >-(irule usize_to_int_int_to_usize >> cooper_tac) >>
-  fs [] >>
-  qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_spec >> rfs [] >>
-  sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-(
-    (* TODO: automate *)
-    pure_once_rewrite_tac [gsym INT_LT] >>
-    dep_pure_once_rewrite_tac [int_of_num_id] >>
-    qspec_assume ‘i’ usize_to_int_bounds >> fs []
-  ) >>
-  fs [] >>
-  (* Case: !j. j <> i ==> ... *)
-  rpt strip_tac >>
-  first_x_assum irule >>
-  rw [] >-(
-    (* TODO: automate *)
-    irule int_of_num_neq_inj >>
-    dep_pure_rewrite_tac [int_of_num_id] >>
-    rw [usize_to_int_bounds] >>
-    metis_tac [int_to_usize_usize_to_int]
-  ) >>
-  (* TODO: automate *)
-  pure_once_rewrite_tac [gsym INT_LT] >>
-  dep_pure_once_rewrite_tac [int_of_num_id] >>
-  qspec_assume ‘j’ usize_to_int_bounds >> fs []
-QED
-*)
-
 Theorem update_len:
   ∀ls i y. len (update ls i y) = len ls
 Proof
@@ -1440,7 +1263,9 @@ Theorem vec_insert_back_spec:
     ∃nv. vec_insert_back v i x = Return nv ∧
     vec_len v = vec_len nv ∧
     vec_index i nv = Return x ∧
-    (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ usize_to_int j ≠ usize_to_int i ⇒ vec_index j nv = vec_index j v)
+    (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒
+          usize_to_int j ≠ usize_to_int i ⇒
+          vec_index j nv = vec_index j v)
 Proof
   rpt strip_tac >> fs [vec_insert_back_def] >>
   (* TODO: improve this? *)