Cleanup a bit

3 files changed, 17 insertions, 191 deletions

diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 75df3015..bff4f7c9 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -234,6 +234,8 @@ val th = SPEC_ALL NUM_SUB_1_EQ
    identifies this theorem (the lhs of the equality, if this is a rewriting
    theorem for instance - we use this to check for collisions, and discard
    redundant instantiations).
+   It takes as input the set of bound variables (it should not perform
+   substitutions with variables belonging to this set).
  *)
 fun inst_match_in_terms
   (try_match: string Redblackset.set -> term -> term * thm)
@@ -258,9 +260,10 @@ fun inst_match_in_terms
    instantiations of this theorem which make its conclusion match subterms
    in the provided list of term.
 
-   [ignore]: if the conclusion of a theorem matches a term in this set, ignore it.
+   [keep]: if this function returns false on an instantiated theorem, ignore
+   the theorem.
  *)
-fun inst_match_concl_in_terms (ignore : term Redblackset.set) (th : thm) (tl : term list) : thm list =
+fun inst_match_concl_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
   let
     val th = (UNDISCH_ALL o SPEC_ALL) th;
     fun try_match bvars t =
@@ -269,8 +272,8 @@ fun inst_match_concl_in_terms (ignore : term Redblackset.set) (th : thm) (tl : t
         val c = concl inst_th;
       in
         (* Check that we mustn't ignore the theorem *)
-        if Redblackset.member (ignore, c) then failwith "inst_match_concl_in_terms: already in the assumptions"
-        else (lhs (concl inst_th), inst_th)
+        if keep inst_th then (lhs (concl inst_th), inst_th)
+        else failwith "inst_match_concl_in_terms: ignore theorem"
       end;
   in
     inst_match_in_terms try_match tl
@@ -288,14 +291,15 @@ val thms = inst_match_concl_in_terms int_to_u32_id [t]
    instantiations of this theorem which make its first premise match subterms
    in the provided list of term.
  *)
-fun inst_match_first_premise_in_terms (th : thm) (tl : term list) : thm list =
+fun inst_match_first_premise_in_terms (keep : thm -> bool) (th : thm) (tl : term list) : thm list =
   let
     val th = SPEC_ALL th;
     fun try_match bvars t =
       let
         val inst_th = inst_match_first_premise bvars th t;
       in
-        ((fst o dest_imp o concl) inst_th, inst_th)
+        if keep inst_th then  ((fst o dest_imp o concl) inst_th, inst_th)
+        else failwith "inst_match_first_premise_in_terms: ignore theorem"
       end;
   in
     inst_match_in_terms try_match tl
@@ -318,8 +322,9 @@ fun apply_dep_rewrites_match_concl_with_terms_tac
   (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic =
   let
     val ignore = Redblackset.fromList Term.compare tl;
+    fun keep th = not (Redblackset.member (ignore, concl th));
     (* Discharge the assumptions so that the goal is one single term *)
-    val thms = inst_match_concl_in_terms ignore th tl;
+    val thms = inst_match_concl_in_terms keep th tl;
     val thms = map thm_to_conj_implies thms;
   in
     (* Apply each theorem *)
@@ -415,11 +420,12 @@ apply_dep_rewrites_match_concl_tac
    Leaves the premises as subgoals if [prove_premise] doesn't prove them.
  *)
 fun apply_dep_rewrites_match_first_premise_tac
+  (keep : thm -> bool)
   (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
   fn (asms, g) =>
     let
       (* Discharge the assumptions so that the goal is one single term *)
-      val thms = inst_match_first_premise_in_terms th (g :: asms);
+      val thms = inst_match_first_premise_in_terms keep th (g :: asms);
       val thms = map thm_to_conj_implies thms;
       fun apply_tac th =
         let
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? *)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 23846737..583f66bd 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -190,7 +190,6 @@ sig
     val i8_sub_eq : thm
     val index_update_diff : thm
     val index_update_same : thm
-    val int_of_num_neq_inj : thm
     val isize_add_eq : thm
     val isize_div_eq : thm
     val isize_mul_eq : thm
@@ -1320,10 +1319,6 @@ sig
           j ≠ i ⇒
           index j (update ls i y) = index j ls
    
-   [int_of_num_neq_inj]  Theorem
-      
-      ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m
-   
    [isize_add_eq]  Theorem
       
       [oracles: DISK_THM]