equal
deleted
inserted
replaced
5 Tactics for wrapping existing freely generated type's constructors. |
5 Tactics for wrapping existing freely generated type's constructors. |
6 *) |
6 *) |
7 |
7 |
8 signature CTR_SUGAR_GENERAL_TACTICS = |
8 signature CTR_SUGAR_GENERAL_TACTICS = |
9 sig |
9 sig |
|
10 val clean_blast_tac: Proof.context -> int -> tactic |
10 val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
11 val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic |
11 val unfold_thms_tac: Proof.context -> thm list -> tactic |
12 val unfold_thms_tac: Proof.context -> thm list -> tactic |
12 end; |
13 end; |
13 |
14 |
14 signature CTR_SUGAR_TACTICS = |
15 signature CTR_SUGAR_TACTICS = |
38 struct |
39 struct |
39 |
40 |
40 open Ctr_Sugar_Util |
41 open Ctr_Sugar_Util |
41 |
42 |
42 val meta_mp = @{thm meta_mp}; |
43 val meta_mp = @{thm meta_mp}; |
|
44 |
|
45 fun clean_blast_tac ctxt = blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt); |
43 |
46 |
44 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, |
47 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl, |
45 tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); |
48 tac, REPEAT_DETERM_N (n - k) o etac thin_rl]); |
46 |
49 |
47 fun unfold_thms_tac _ [] = all_tac |
50 fun unfold_thms_tac _ [] = all_tac |
155 fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss = |
158 fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss = |
156 HEADGOAL (rtac uexhaust) THEN |
159 HEADGOAL (rtac uexhaust) THEN |
157 ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' |
160 ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' |
158 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ |
161 simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ |
159 flat (nth distinctsss (k - 1))) ctxt)) k) THEN |
162 flat (nth distinctsss (k - 1))) ctxt)) k) THEN |
160 ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt)); |
163 ALLGOALS (clean_blast_tac ctxt); |
161 |
164 |
162 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
165 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
163 |
166 |
164 fun mk_split_asm_tac ctxt split = |
167 fun mk_split_asm_tac ctxt split = |
165 HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN |
168 HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN |