diff options
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 22 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 181 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 5 |
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] |