diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/primitivesBaseTacLib.sml | 399 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 177 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 393 | ||||
| -rw-r--r-- | backends/hol4/testScript.sml | 8 |
4 files changed, 890 insertions, 87 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml index b5d9918e..0368ee9a 100644 --- a/backends/hol4/primitivesBaseTacLib.sml +++ b/backends/hol4/primitivesBaseTacLib.sml @@ -13,6 +13,8 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC val pop_ignore_tac = pop_assum ignore_tac +val try_tac = TRY + (* TODO: no exfalso tactic?? *) val ex_falso : tactic = SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[]) @@ -22,13 +24,406 @@ fun qspecl_assume xl th = qspecl_then xl assume_tac th fun first_qspec_assume x = first_assum (qspec_assume x) fun first_qspecl_assume xl = first_assum (qspecl_assume xl) - - +val all_tac = all_tac val cooper_tac = COOPER_TAC +val pure_rewrite_tac = PURE_REWRITE_TAC val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC (* Dependent rewrites *) val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC + +(* Add a list of theorems in the assumptions *) +fun assume_tacl (thms : thm list) : tactic = + let + (* TODO: use MAP_EVERY *) + fun t thms = + case thms of + [] => all_tac + | thm :: thms => assume_tac thm >> t thms + in + t thms + end + +(* Given a theorem of the shape: + {[ + A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl + ]} + + Rewrite it so that it has the shape: + {[ + ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl + ]} + *) +fun thm_to_conj_implies (thm : thm) : thm = + let + (* Discharge all the assumptions *) + val thm = DISCH_ALL thm; + (* Rewrite the implications as one conjunction *) + val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm; + in thm end + +(* Like THEN1 and >-, but doesn't fail if the first subgoal is not completely + solved. + + TODO: how to get the notation right? + *) +fun op partial_then1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_GOAL tac2 1) + +(* If the current goal is [asms ⊢ g], and given a lemma of the form + [⊢ H ==> C], do the following: + - introduce [asms ⊢ H] as a subgoal and apply the given tactic on it + - also calls the theorem tactic with the theorem [asms ⊢ C] + + If the lemma is not an implication, we directly call the theorem tactic. + *) +fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = + let + val c = concl thm; + (* First case: there is a premise to prove *) + fun prove_premise_then (h : term) = + partial_then1 (SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm))) premise_tac; + (* Second case: no premise to prove *) + val no_prove_premise_then = then_tac thm; + in + if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then + end + +(* Add the first premise of the theorem as subgoal, and add the theorem without its + first premise as an assumption. + + For instance, if we have the goal: + asls + ==== + c + and the theorem: ⊢ H ==> G + + We generate: + asls asls + ==== G + H ==== + C + +*) +val sg_premise_tac = sg_premise_then all_tac assume_tac + +(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *) +fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = + sg_premise_then + (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise") + then_tac thm + +(* +val thm = th +*) + +(* Call a function on all the subterms of a term *) +fun dep_apply_in_subterms + (f : string Redblackset.set -> term -> unit) + (bound_vars : string Redblackset.set) + (t : term) : unit = + let + val dep = dep_apply_in_subterms f; + val _ = f bound_vars t; + in + case dest_term t of + VAR (name, ty) => () + | CONST {Name=name, Thy=thy, Ty=ty} => () + | COMB (app, arg) => + let + val _ = dep bound_vars app; + val _ = dep bound_vars arg; + in () end + | LAMB (bvar, body) => + let + val (varname, ty) = dest_var bvar; + val bound_vars = Redblackset.add (bound_vars, varname); + val _ = dep bound_vars body; + in () end + end + +(* Return the set of free variables appearing in the residues of a term substitution *) +fun free_vars_in_subst_residue (s: (term, term) Term.subst) : string Redblackset.set = + let + val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) s); + val free_vars = map (fst o dest_var) free_vars; + val free_vars = Redblackset.fromList String.compare free_vars; + in free_vars end + +(* Attempt to instantiate a rewrite theorem. + + Remark: this theorem should be of the form: + H ⊢ x = y + + (without quantified variables). + + **REMARK**: the function raises a HOL_ERR exception if it fails. + + [forbid_vars]: forbid substituting with those vars (typically because + we are maching in a subterm under lambdas, and some of those variables + are bounds in the outer lambdas). +*) +fun inst_match_concl (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = + let + (* Retrieve the lhs of the conclusion of the theorem *) + val l = lhs (concl th); + (* Match this lhs with the term *) + val (var_s, ty_s) = match_term l t; + (* Check that we are allowed to perform the substitution *) + val free_vars = free_vars_in_subst_residue var_s; + val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); + in + (* Perform the substitution *) + INST var_s (INST_TYPE ty_s th) + end + +(* +val forbid_vars = Redblackset.empty String.compare +val t = “u32_to_int (int_to_u32 x)” +val t = “u32_to_int (int_to_u32 3)” +val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id +*) + +(* Attempt to instantiate a theorem by matching its first premise. + + Note that we make the hypothesis tha all the free variables which need + to be instantiated appear in the first premise, of course (the caller should + enforce this). + + Remark: this theorem should be of the form: + ⊢ H0 ==> ... ==> Hn ==> H + + (without quantified variables). + + **REMARK**: the function raises a HOL_ERR exception if it fails. + + [forbid_vars]: see [inst_match_concl] +*) +fun inst_match_first_premise + (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = + let + (* Retrieve the first premise *) + val l = (fst o dest_imp o concl) th; + (* Match this with the term *) + val (var_s, ty_s) = match_term l t; + (* Check that we are allowed to perform the substitution *) + val free_vars = free_vars_in_subst_residue var_s; + val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); + in + (* Perform the substitution *) + INST var_s (INST_TYPE ty_s th) + end + +(* +val forbid_vars = Redblackset.empty String.compare +val t = “u32_to_int z = u32_to_int i − 1” +val th = SPEC_ALL NUM_SUB_1_EQ +*) + +(* Call a matching function on all the subterms in the provided list of term. + This is a generic function. + + [try_match] should return an instantiated theorem, as well as a term which + 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). + *) +fun inst_match_in_terms + (try_match: string Redblackset.set -> term -> term * thm) + (tl : term list) : thm list = + let + (* We use a map when storing the theorems, to avoid storing the same theorem twice *) + val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare); + fun try_instantiate bvars t = + let + val (inst_th_tm, inst_th) = try_match bvars t; + in + inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th) + end + handle HOL_ERR _ => (); + (* Explore the term *) + val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl; + in + map snd (Redblackmap.listItems (!inst_thms)) + end + +(* Given a rewriting theorem [th] which has premises, return all the + 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. + *) +fun inst_match_concl_in_terms (ignore : term Redblackset.set) (th : thm) (tl : term list) : thm list = + let + val th = (UNDISCH_ALL o SPEC_ALL) th; + fun try_match bvars t = + let + val inst_th = inst_match_concl bvars th 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) + end; + in + inst_match_in_terms try_match tl + end + +(* +val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)” +val th = int_to_u32_id + +val thms = inst_match_concl_in_terms int_to_u32_id [t] +*) + + +(* Given a theorem [th] which has premises, return all the + 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 = + 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) + end; + in + inst_match_in_terms try_match tl + end + +(* +val t = “x = y - 1 ==> T” +val th = SPEC_ALL NUM_SUB_1_EQ + +val thms = inst_match_first_premise_in_terms th [t] +*) + + +(* Attempt to apply dependent rewrites with a theorem by matching its + conclusion with subterms in the given list of terms. + + Leaves the premises as subgoals if [prove_premise] doesn't prove them. + *) +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; + (* Discharge the assumptions so that the goal is one single term *) + val thms = inst_match_concl_in_terms ignore th tl; + val thms = map thm_to_conj_implies thms; + in + (* Apply each theorem *) + MAP_EVERY (sg_premise_then prove_premise then_tac) thms + end + +(* Attempt to apply dependent rewrites with a theorem by matching its + conclusion with subterms of the goal (including the assumptions). + + Leaves the premises as subgoals if [prove_premise] doesn't prove them. + *) +fun apply_dep_rewrites_match_concl_with_all_tac + (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = + fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g) + +(* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the + conclusion of the goal. + *) +fun apply_dep_rewrites_match_concl_with_goal_tac + (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = + fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g) + +(* A theorem might be of the shape: [H => A = B /\ C = D], in which + case we can split it into: + [H => A = B] + [H => C = D] + + The theorem mustn't have assumptions. + *) +fun split_rewrite_thm (th : thm) : thm list = + let + val _ = null (hyp th); + val t = concl th; + val (vars, t) = strip_forall t; + val (impl, t) = strip_imp t; + val tl = strip_conj t; + fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t))) + val prove_tac = + rpt gen_tac >> rpt disch_tac >> + qspecl_assume (map (fn a => ‘^a’) vars) th >> + fs []; + fun mk_th (t : term) = prove (mk_goal t, prove_tac); + (* Change the shape of the theorem (one of the conjuncts may have + universally quantified variables) + *) + fun transform_th (th : thm) : thm = + (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th + in + map (transform_th o mk_th) tl + end + +(* A dependent rewrite tactic which introduces the premises in a new goal. + + We try to apply dependent rewrites to the whole goal, including its assumptions. + + TODO: this tactic sometimes introduces several times the same subgoal + (because we split theorems...). + *) +fun sg_dep_rewrite_all_tac (th : thm) = + let + (* Split the theorem *) + val thml = split_rewrite_thm th + in + MAP_EVERY (apply_dep_rewrites_match_concl_with_all_tac all_tac assume_tac) thml + end + +(* Same as {!sg_dep_rewrite_tac} but this time we apply rewrites only in the conclusion + of the goal (not the assumptions). + *) +fun sg_dep_rewrite_goal_tac (th : thm) = + let + (* Split the theorem *) + val thml = split_rewrite_thm th + in + MAP_EVERY (apply_dep_rewrites_match_concl_with_goal_tac all_tac assume_tac) thml + end + +(* +val (asms, g) = ([ + “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”, + “u32_to_int (int_to_u32 2) = 2” +], “T”) + +apply_dep_rewrites_match_concl_tac + (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC) + (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]) + int_to_u32_id +*) + +(* Attempt to apply dependent rewrites with a theorem by matching its + first premise with subterms of the goal. + + Leaves the premises as subgoals if [prove_premise] doesn't prove them. + *) +fun apply_dep_rewrites_match_first_premise_tac + (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 = map thm_to_conj_implies thms; + fun apply_tac th = + let + val th = thm_to_conj_implies th; + in + sg_premise_then prove_premise then_tac th + end; + in + (* Apply each theorem *) + MAP_EVERY apply_tac thms (asms, g) + end + end diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 85efeb61..2df3375a 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1389,8 +1389,23 @@ 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) ⇒ @@ -1433,4 +1448,166 @@ Proof qspec_assume ‘j’ usize_to_int_bounds >> fs [] QED +(* TODO: use lowercase everywhere for the theorem names *) + +(* We generate and save an induction theorem for positive integers *) +Theorem int_induction: + !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i +Proof + ntac 4 strip_tac >> + Induct_on ‘Num i’ >> rpt strip_tac + >-(sg ‘i = 0’ >- cooper_tac >> fs []) >> + last_assum (qspec_assume ‘i-1’) >> + fs [] >> pop_assum irule >> + rw [] >> try_tac cooper_tac >> + first_assum (qspec_assume ‘i - 1’) >> + pop_assum irule >> + rw [] >> try_tac cooper_tac +QED + +val _ = TypeBase.update_induction int_induction + +(* Small experiment: trying to redefine common functions with integers instead of nums *) +val index_def = Define ‘ + index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB) +’ + +val len_def = Define ‘ + len [] : int = 0 /\ + len (x :: ls) : int = 1 + len ls +’ + +val update_def = Define ‘ + update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧ + update (x :: ls) (i : int) y = if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls) +’ + +Theorem update_len: + ∀ls i y. len (update ls i y) = len ls +Proof + Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def, len_def] +QED + +Theorem update_spec: + ∀ls i y. + 0 <= i ==> + i < len ls ==> + len (update ls i y) = len ls ∧ + index i (update ls i y) = y ∧ + ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls +Proof + Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> try_tac (ex_falso >> cooper_tac) >> + try_tac ( + pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> + pop_assum sg_premise_tac >- cooper_tac >> + pop_assum sg_premise_tac >- cooper_tac >> + rw []) + >> ( + pop_assum (qspec_assume ‘j - 1’) >> + pop_assum sg_premise_tac >- cooper_tac >> + pop_assum sg_premise_tac >- cooper_tac >> + rw []) +QED + +Theorem index_update_same: + ∀ls i j y. + 0 <= i ==> + i < len ls ==> + j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls +Proof + rpt strip_tac >> + qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >> + rw [] +QED + +Theorem index_update_diff: + ∀ls i j y. + 0 <= i ==> + i < len ls ==> + index i (update ls i y) = y +Proof + rpt strip_tac >> + qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >> + rw [] +QED + +Theorem vec_to_list_int_bounds: + !v. 0 <= len (vec_to_list v) /\ len (vec_to_list v) <= usize_max +Proof + (* TODO *) + cheat +QED + +val vec_len_def = Define ‘vec_len v = int_to_usize (len (vec_to_list v))’ +Theorem vec_len_spec: + ∀v. + vec_len v = int_to_usize (len (vec_to_list v)) ∧ + 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max +Proof + gen_tac >> rw [vec_len_def] >> + qspec_assume ‘v’ vec_to_list_int_bounds >> + fs [] +QED + +val vec_index_def = Define ‘ + vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (index (usize_to_int i) (vec_to_list v)) else Fail Failure’ + +(* TODO: *) +val mk_vec_spec = new_axiom ("mk_vec_spec", “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) + +(* Redefining ‘vec_insert_back’ *) +val vec_insert_back_def = Define ‘ + vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (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 ∧ + (∀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? *) + qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_spec >> + sg_dep_rewrite_all_tac update_len >> fs [] >> + qspec_assume ‘v’ vec_len_spec >> + rw [] >> gvs [] >> + fs [vec_len_def, vec_index_def] >> + qspec_assume ‘i’ usize_to_int_bounds >> + sg_dep_rewrite_all_tac int_to_usize_id >- cooper_tac >> fs [] >> + sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >> + rw [] >> + irule index_update_same >> cooper_tac +QED + +(* TODO: add theorems to the rewriting theorems +from listSimps.sml: + +val LIST_ss = BasicProvers.thy_ssfrag "list" +val _ = BasicProvers.logged_addfrags {thyname="list"} [LIST_EQ_ss] + +val list_rws = computeLib.add_thms + [ + ALL_DISTINCT, APPEND, APPEND_NIL, CONS_11, DROP_compute, EL_restricted, + EL_simp_restricted, EVERY_DEF, EXISTS_DEF, FILTER, FIND_def, FLAT, FOLDL, + FOLDR, FRONT_DEF, GENLIST_AUX_compute, GENLIST_NUMERALS, HD, INDEX_FIND_def, + INDEX_OF_def, LAST_compute, LENGTH, LEN_DEF, LIST_APPLY_def, LIST_BIND_def, + LIST_IGNORE_BIND_def, LIST_LIFT2_def, LIST_TO_SET_THM, LLEX_def, LRC_def, + LUPDATE_compute, MAP, MAP2, NOT_CONS_NIL, NOT_NIL_CONS, NULL_DEF, oEL_def, + oHD_def, + PAD_LEFT, PAD_RIGHT, REVERSE_REV, REV_DEF, SHORTLEX_def, SNOC, SUM_ACC_DEF, + SUM_SUM_ACC, + TAKE_compute, TL, UNZIP, ZIP, computeLib.lazyfy_thm list_case_compute, + dropWhile_def, isPREFIX, list_size_def, nub_def, splitAtPki_def + ] + +fun list_compset () = + let + val base = reduceLib.num_compset() + in + list_rws base; base + end +*) + val _ = export_theory () diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index 75098bfe..cc2f3115 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -3,26 +3,40 @@ sig type thm = Thm.thm (* Axioms *) + val MK_VEC_SPEC : thm val VEC_TO_LIST_BOUNDS : thm val i128_to_int_bounds : thm val i16_to_int_bounds : thm val i32_to_int_bounds : thm val i64_to_int_bounds : thm val i8_to_int_bounds : thm + val int_to_i128_i128_to_int : thm val int_to_i128_id : thm + val int_to_i16_i16_to_int : thm val int_to_i16_id : thm + val int_to_i32_i32_to_int : thm val int_to_i32_id : thm + val int_to_i64_i64_to_int : thm val int_to_i64_id : thm + val int_to_i8_i8_to_int : thm val int_to_i8_id : thm val int_to_isize_id : thm + val int_to_isize_isize_to_int : thm val int_to_u128_id : thm + val int_to_u128_u128_to_int : thm val int_to_u16_id : thm + val int_to_u16_u16_to_int : thm val int_to_u32_id : thm + val int_to_u32_u32_to_int : thm val int_to_u64_id : thm + val int_to_u64_u64_to_int : thm val int_to_u8_id : thm + val int_to_u8_u8_to_int : thm val int_to_usize_id : thm + val int_to_usize_usize_to_int : thm val isize_bounds : thm val isize_to_int_bounds : thm + val mk_vec_spec : thm val u128_to_int_bounds : thm val u16_to_int_bounds : thm val u32_to_int_bounds : thm @@ -72,12 +86,14 @@ sig val i8_mul_def : thm val i8_rem_def : thm val i8_sub_def : thm + val index_def : thm val int_rem_def : thm val isize_add_def : thm val isize_div_def : thm val isize_mul_def : thm val isize_rem_def : thm val isize_sub_def : thm + val len_def : thm val massert_def : thm val mem_replace_back_def : thm val mem_replace_fwd_def : thm @@ -127,12 +143,17 @@ sig val u8_mul_def : thm val u8_rem_def : thm val u8_sub_def : thm + val update_def : thm val usize_add_def : thm val usize_div_def : thm val usize_mul_def : thm val usize_rem_def : thm val usize_sub_def : thm + val vec_index_def : thm + val vec_insert_back_def : thm val vec_len_def : thm + val vec_new_def : thm + val vec_push_back_def : thm (* Theorems *) val I128_ADD_EQ : thm @@ -159,6 +180,8 @@ sig val I8_MUL_EQ : thm val I8_REM_EQ : thm val I8_SUB_EQ : thm + val INT_OF_NUM : thm + val INT_OF_NUM_NEQ_INJ : thm val ISIZE_ADD_EQ : thm val ISIZE_DIV_EQ : thm val ISIZE_MUL_EQ : thm @@ -193,6 +216,9 @@ sig val USIZE_MUL_EQ : thm val USIZE_REM_EQ : thm val USIZE_SUB_EQ : thm + val USIZE_TO_INT_INJ : thm + val USIZE_TO_INT_NEQ_INJ : thm + val VEC_NEW_SPEC : thm val VEC_TO_LIST_INT_BOUNDS : thm val datatype_error : thm val datatype_result : thm @@ -207,6 +233,9 @@ sig val error_case_eq : thm val error_induction : thm val error_nchotomy : thm + val index_update_diff : thm + val index_update_same : thm + val int_induction : thm val num2error_11 : thm val num2error_ONTO : thm val num2error_error2num : thm @@ -218,6 +247,12 @@ sig val result_distinct : thm val result_induction : thm val result_nchotomy : thm + val update_ind : thm + val update_len : thm + val update_spec : thm + val vec_insert_back_spec : thm + val vec_len_spec : thm + val vec_to_list_int_bounds : thm val primitives_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -225,61 +260,84 @@ sig [string] Parent theory of "primitives" - [int_to_u128_id] Axiom + [mk_vec_spec] Axiom - [oracles: ] [axioms: int_to_u128_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n + [oracles: ] [axioms: mk_vec_spec] [] + ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l - [int_to_u64_id] Axiom + [VEC_TO_LIST_BOUNDS] Axiom - [oracles: ] [axioms: int_to_u64_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n + [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] [] + ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max) - [int_to_u32_id] Axiom + [isize_bounds] Axiom - [oracles: ] [axioms: int_to_u32_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n + [oracles: ] [axioms: isize_bounds] [] + ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max - [int_to_u16_id] Axiom + [usize_bounds] Axiom - [oracles: ] [axioms: int_to_u16_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n + [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max - [int_to_u8_id] Axiom + [isize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u8_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n + [oracles: ] [axioms: isize_to_int_bounds] [] + ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max - [int_to_i128_id] Axiom + [i8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i128_id] [] - ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n + [oracles: ] [axioms: i8_to_int_bounds] [] + ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max - [int_to_i64_id] Axiom + [i16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i64_id] [] - ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n + [oracles: ] [axioms: i16_to_int_bounds] [] + ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max - [int_to_i32_id] Axiom + [i32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i32_id] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [oracles: ] [axioms: i32_to_int_bounds] [] + ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max - [int_to_i16_id] Axiom + [i64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i16_id] [] - ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [oracles: ] [axioms: i64_to_int_bounds] [] + ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max - [int_to_i8_id] Axiom + [i128_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i8_id] [] - ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n + [oracles: ] [axioms: i128_to_int_bounds] [] + ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max - [int_to_usize_id] Axiom + [usize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_usize_id] [] - ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒ - usize_to_int (int_to_usize n) = n + [oracles: ] [axioms: usize_to_int_bounds] [] + ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max + + [u8_to_int_bounds] Axiom + + [oracles: ] [axioms: u8_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max + + [u16_to_int_bounds] Axiom + + [oracles: ] [axioms: u16_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max + + [u32_to_int_bounds] Axiom + + [oracles: ] [axioms: u32_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max + + [u64_to_int_bounds] Axiom + + [oracles: ] [axioms: u64_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max + + [u128_to_int_bounds] Axiom + + [oracles: ] [axioms: u128_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max [int_to_isize_id] Axiom @@ -287,79 +345,127 @@ sig ⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒ isize_to_int (int_to_isize n) = n - [u128_to_int_bounds] Axiom + [int_to_usize_id] Axiom - [oracles: ] [axioms: u128_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max + [oracles: ] [axioms: int_to_usize_id] [] + ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒ + usize_to_int (int_to_usize n) = n - [u64_to_int_bounds] Axiom + [int_to_i8_id] Axiom - [oracles: ] [axioms: u64_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max + [oracles: ] [axioms: int_to_i8_id] [] + ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n - [u32_to_int_bounds] Axiom + [int_to_i16_id] Axiom - [oracles: ] [axioms: u32_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max + [oracles: ] [axioms: int_to_i16_id] [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n - [u16_to_int_bounds] Axiom + [int_to_i32_id] Axiom - [oracles: ] [axioms: u16_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max + [oracles: ] [axioms: int_to_i32_id] [] + ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n - [u8_to_int_bounds] Axiom + [int_to_i64_id] Axiom - [oracles: ] [axioms: u8_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max + [oracles: ] [axioms: int_to_i64_id] [] + ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n - [usize_to_int_bounds] Axiom + [int_to_i128_id] Axiom - [oracles: ] [axioms: usize_to_int_bounds] [] - ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max + [oracles: ] [axioms: int_to_i128_id] [] + ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n - [i128_to_int_bounds] Axiom + [int_to_u8_id] Axiom - [oracles: ] [axioms: i128_to_int_bounds] [] - ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max + [oracles: ] [axioms: int_to_u8_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n - [i64_to_int_bounds] Axiom + [int_to_u16_id] Axiom - [oracles: ] [axioms: i64_to_int_bounds] [] - ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max + [oracles: ] [axioms: int_to_u16_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n - [i32_to_int_bounds] Axiom + [int_to_u32_id] Axiom - [oracles: ] [axioms: i32_to_int_bounds] [] - ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max + [oracles: ] [axioms: int_to_u32_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - [i16_to_int_bounds] Axiom + [int_to_u64_id] Axiom - [oracles: ] [axioms: i16_to_int_bounds] [] - ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max + [oracles: ] [axioms: int_to_u64_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n - [i8_to_int_bounds] Axiom + [int_to_u128_id] Axiom - [oracles: ] [axioms: i8_to_int_bounds] [] - ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max + [oracles: ] [axioms: int_to_u128_id] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n - [isize_to_int_bounds] Axiom + [int_to_i8_i8_to_int] Axiom - [oracles: ] [axioms: isize_to_int_bounds] [] - ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max + [oracles: ] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀i. int_to_i8 (i8_to_int i) = i - [usize_bounds] Axiom + [int_to_i16_i16_to_int] Axiom - [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max + [oracles: ] [axioms: int_to_i16_i16_to_int] [] + ⊢ ∀i. int_to_i16 (i16_to_int i) = i - [isize_bounds] Axiom + [int_to_i32_i32_to_int] Axiom - [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max + [oracles: ] [axioms: int_to_i32_i32_to_int] [] + ⊢ ∀i. int_to_i32 (i32_to_int i) = i - [VEC_TO_LIST_BOUNDS] Axiom + [int_to_i64_i64_to_int] Axiom - [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] [] - ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295) + [oracles: ] [axioms: int_to_i64_i64_to_int] [] + ⊢ ∀i. int_to_i64 (i64_to_int i) = i + + [int_to_i128_i128_to_int] Axiom + + [oracles: ] [axioms: int_to_i128_i128_to_int] [] + ⊢ ∀i. int_to_i128 (i128_to_int i) = i + + [int_to_isize_isize_to_int] Axiom + + [oracles: ] [axioms: int_to_isize_isize_to_int] [] + ⊢ ∀i. int_to_isize (isize_to_int i) = i + + [int_to_u8_u8_to_int] Axiom + + [oracles: ] [axioms: int_to_u8_u8_to_int] [] + ⊢ ∀i. int_to_u8 (u8_to_int i) = i + + [int_to_u16_u16_to_int] Axiom + + [oracles: ] [axioms: int_to_u16_u16_to_int] [] + ⊢ ∀i. int_to_u16 (u16_to_int i) = i + + [int_to_u32_u32_to_int] Axiom + + [oracles: ] [axioms: int_to_u32_u32_to_int] [] + ⊢ ∀i. int_to_u32 (u32_to_int i) = i + + [int_to_u64_u64_to_int] Axiom + + [oracles: ] [axioms: int_to_u64_u64_to_int] [] + ⊢ ∀i. int_to_u64 (u64_to_int i) = i + + [int_to_u128_u128_to_int] Axiom + + [oracles: ] [axioms: int_to_u128_u128_to_int] [] + ⊢ ∀i. int_to_u128 (u128_to_int i) = i + + [int_to_usize_usize_to_int] Axiom + + [oracles: ] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i. int_to_usize (usize_to_int i) = i + + [MK_VEC_SPEC] Axiom + + [oracles: ] [axioms: MK_VEC_SPEC] [] + ⊢ ∀l. &LENGTH l ≤ usize_max ⇒ + ∃v. mk_vec l = Return v ∧ vec_to_list v = l [bind_def] Definition @@ -554,6 +660,12 @@ sig ⊢ ∀x y. i8_sub x y = mk_i8 (i8_to_int x − i8_to_int y) + [index_def] Definition + + ⊢ ∀i x ls. + index i (x::ls) = + if i = 0 then x else if 0 < i then index (i − 1) ls else ARB + [int_rem_def] Definition ⊢ ∀x y. @@ -586,6 +698,10 @@ sig ⊢ ∀x y. isize_sub x y = mk_isize (isize_to_int x − isize_to_int y) + [len_def] Definition + + ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls + [massert_def] Definition ⊢ ∀b. massert b = if b then Return () else Fail Failure @@ -857,6 +973,15 @@ sig ⊢ ∀x y. u8_sub x y = mk_u8 (u8_to_int x − u8_to_int y) + [update_def] Definition + + ⊢ (∀i y. update [] i y = []) ∧ + ∀x ls i y. + update (x::ls) i y = + if i = 0 then y::ls + else if 0 < i then x::update ls (i − 1) y + else x::ls + [usize_add_def] Definition ⊢ ∀x y. usize_add x y = mk_usize (usize_to_int x + usize_to_int y) @@ -883,9 +1008,32 @@ sig ⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y) + [vec_index_def] Definition + + ⊢ ∀i v. + vec_index i v = + if usize_to_int i ≤ usize_to_int (vec_len v) then + Return (index (usize_to_int i) (vec_to_list v)) + else Fail Failure + + [vec_insert_back_def] Definition + + ⊢ ∀v i x. + vec_insert_back v i x = + mk_vec (update (vec_to_list v) (usize_to_int i) x) + [vec_len_def] Definition - ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v)) + ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) + + [vec_new_def] Definition + + ⊢ vec_new = + case mk_vec [] of Return v => v | Fail v2 => ARB | Loop => ARB + + [vec_push_back_def] Definition + + ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x]) [I128_ADD_EQ] Theorem @@ -1140,6 +1288,14 @@ sig ∃z. i8_sub x y = Return z ∧ i8_to_int z = i8_to_int x − i8_to_int y + [INT_OF_NUM] Theorem + + ⊢ ∀i. 0 ≤ i ⇒ &Num i = i + + [INT_OF_NUM_NEQ_INJ] Theorem + + ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m + [ISIZE_ADD_EQ] Theorem [oracles: DISK_THM] @@ -1495,10 +1651,26 @@ sig ∃z. usize_sub x y = Return z ∧ usize_to_int z = usize_to_int x − usize_to_int y + [USIZE_TO_INT_INJ] Theorem + + [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j + + [USIZE_TO_INT_NEQ_INJ] Theorem + + [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j + + [VEC_NEW_SPEC] Theorem + + [oracles: DISK_THM] [axioms: usize_bounds, MK_VEC_SPEC] [] + ⊢ vec_to_list vec_new = [] + [VEC_TO_LIST_INT_BOUNDS] Theorem - [oracles: DISK_THM] [axioms: VEC_TO_LIST_BOUNDS] [] - ⊢ ∀v. (let l = &LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ u32_max) + [oracles: DISK_THM] [axioms: usize_bounds, VEC_TO_LIST_BOUNDS] [] + ⊢ ∀v. 0 ≤ &LENGTH (vec_to_list v) ∧ + &LENGTH (vec_to_list v) ≤ usize_max [datatype_error] Theorem @@ -1554,6 +1726,23 @@ sig ⊢ ∀a. a = Failure + [index_update_diff] Theorem + + ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y + + [index_update_same] Theorem + + ⊢ ∀ls i j y. + 0 ≤ i ⇒ + i < len ls ⇒ + j < len ls ⇒ + j ≠ i ⇒ + index j (update ls i y) = index j ls + + [int_induction] Theorem + + ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i + [num2error_11] Theorem ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r') @@ -1607,6 +1796,48 @@ sig ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop + [update_ind] Theorem + + ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧ + (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒ + ∀v v1 v2. P v v1 v2 + + [update_len] Theorem + + ⊢ ∀ls i y. len (update ls i y) = len ls + + [update_spec] Theorem + + ⊢ ∀ls i y. + 0 ≤ i ⇒ + i < len ls ⇒ + len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧ + ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls + + [vec_insert_back_spec] Theorem + + [oracles: DISK_THM, cheat] + [axioms: usize_to_int_bounds, int_to_usize_id, mk_vec_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 ∧ + ∀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 + + [vec_len_spec] Theorem + + [oracles: DISK_THM, cheat] [axioms: ] [] + ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧ + 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max + + [vec_to_list_int_bounds] Theorem + + [oracles: cheat] [axioms: ] [] + ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max + *) end diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml index fe1c1e11..a2d15117 100644 --- a/backends/hol4/testScript.sml +++ b/backends/hol4/testScript.sml @@ -722,7 +722,7 @@ fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_ If the lemma is not an implication, we directly call the theorem tactic. *) -fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = +fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = let val c = concl thm; (* First case: there is a premise to prove *) @@ -734,9 +734,9 @@ fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then end -(* Same as {!intro_premise_then} but fails if the premise_tac fails to prove the premise *) +(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *) fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = - intro_premise_then + sg_premise_then (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise") then_tac thm @@ -1294,7 +1294,7 @@ fun pure_progress_with (premise_tac : tactic) val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th; in (* Apply the theorem *) - intro_premise_then premise_tac (then_tac fgoal) th (asms, g) + sg_premise_then premise_tac (then_tac fgoal) th (asms, g) end (* |