summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4')
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml22
-rw-r--r--backends/hol4/primitivesScript.sml181
-rw-r--r--backends/hol4/primitivesTheory.sig5
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]