author | wenzelm |
Sun, 18 Oct 2015 21:30:01 +0200 | |
changeset 61476 | 1884c40f1539 |
parent 60784 | 4f590c08fd5d |
child 61760 | 1647bb489522 |
permissions | -rw-r--r-- |
54701 | 1 |
(* Title: HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
54397 | 3 |
Copyright 2012, 2013 |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
4 |
|
51797 | 5 |
Tactics for wrapping existing freely generated type's constructors. |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
6 |
*) |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
7 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
8 |
signature CTR_SUGAR_GENERAL_TACTICS = |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
9 |
sig |
60728 | 10 |
val select_prem_tac: Proof.context -> int -> (int -> tactic) -> int -> int -> tactic |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
11 |
val unfold_thms_tac: Proof.context -> thm list -> tactic |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
12 |
end; |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
13 |
|
54006 | 14 |
signature CTR_SUGAR_TACTICS = |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
15 |
sig |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
16 |
include CTR_SUGAR_GENERAL_TACTICS |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
17 |
|
49148
93f281430e77
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
blanchet
parents:
49137
diff
changeset
|
18 |
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic |
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
19 |
val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
20 |
val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic |
59266 | 21 |
val mk_case_distrib_tac: Proof.context -> cterm -> thm -> thm list -> tactic |
54491 | 22 |
val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> |
23 |
thm list list -> tactic |
|
49118 | 24 |
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic |
59271 | 25 |
val mk_disc_eq_case_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> |
26 |
tactic |
|
60728 | 27 |
val mk_exhaust_disc_tac: Proof.context -> int -> thm -> thm list -> tactic |
28 |
val mk_exhaust_sel_tac: Proof.context -> int -> thm -> thm list -> tactic |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
29 |
val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51686
diff
changeset
|
30 |
thm list list list -> thm list list list -> tactic |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
31 |
val mk_half_distinct_disc_tac: Proof.context -> int -> thm -> thm -> tactic |
60728 | 32 |
val mk_nchotomy_tac: Proof.context -> int -> thm -> tactic |
33 |
val mk_other_half_distinct_disc_tac: Proof.context -> thm -> tactic |
|
60251
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
34 |
val mk_split_tac: Proof.context -> int list -> thm -> thm list -> thm list list -> |
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
35 |
thm list list -> thm list list list -> tactic |
49044 | 36 |
val mk_split_asm_tac: Proof.context -> thm -> tactic |
60728 | 37 |
val mk_unique_disc_def_tac: Proof.context -> int -> thm -> tactic |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
38 |
end; |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
39 |
|
54006 | 40 |
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS = |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
41 |
struct |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
42 |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
43 |
open Ctr_Sugar_Util |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
44 |
|
49486 | 45 |
val meta_mp = @{thm meta_mp}; |
46 |
||
60728 | 47 |
fun select_prem_tac ctxt n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac ctxt thin_rl, |
48 |
tac, REPEAT_DETERM_N (n - k) o etac ctxt thin_rl]); |
|
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
49 |
|
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
50 |
fun unfold_thms_tac _ [] = all_tac |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
51 |
| unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms); |
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
52 |
|
49212 | 53 |
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P}); |
49031 | 54 |
|
60728 | 55 |
fun mk_nchotomy_tac ctxt n exhaust = |
56 |
HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN' |
|
60752 | 57 |
EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt]) |
58 |
(1 upto n))); |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
59 |
|
60728 | 60 |
fun mk_unique_disc_def_tac ctxt m uexhaust = |
60752 | 61 |
HEADGOAL (EVERY' |
62 |
[rtac ctxt iffI, rtac ctxt uexhaust, REPEAT_DETERM_N m o rtac ctxt exI, |
|
63 |
assume_tac ctxt, rtac ctxt refl]); |
|
49137 | 64 |
|
49486 | 65 |
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust = |
60728 | 66 |
HEADGOAL (EVERY' ([rtac ctxt (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans), |
67 |
rtac ctxt @{thm iffI_np}, REPEAT_DETERM o etac ctxt exE, |
|
68 |
hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac ctxt allI, |
|
69 |
rtac ctxt distinct, rtac ctxt uexhaust] @ |
|
60752 | 70 |
(([etac ctxt notE, REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt], |
71 |
[REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt]) |
|
52325 | 72 |
|> k = 1 ? swap |> op @))); |
49116
3d520eec2746
allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
blanchet
parents:
49075
diff
changeset
|
73 |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
74 |
fun mk_half_distinct_disc_tac ctxt m discD disc' = |
60728 | 75 |
HEADGOAL (dtac ctxt discD THEN' REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN' |
76 |
rtac ctxt disc'); |
|
49028 | 77 |
|
60728 | 78 |
fun mk_other_half_distinct_disc_tac ctxt half = |
79 |
HEADGOAL (etac ctxt @{thm contrapos_pn} THEN' etac ctxt half); |
|
80 |
||
81 |
fun mk_exhaust_disc_or_sel_tac ctxt n exhaust destIs = |
|
82 |
HEADGOAL (rtac ctxt exhaust THEN' |
|
83 |
EVERY' (map2 (fn k => fn destI => dtac ctxt destI THEN' |
|
60752 | 84 |
select_prem_tac ctxt n (etac ctxt meta_mp) k THEN' assume_tac ctxt) (1 upto n) destIs)); |
53916 | 85 |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
86 |
val mk_exhaust_disc_tac = mk_exhaust_disc_or_sel_tac; |
53916 | 87 |
|
60728 | 88 |
fun mk_exhaust_sel_tac ctxt n exhaust_disc collapses = |
89 |
mk_exhaust_disc_or_sel_tac ctxt n exhaust_disc collapses ORELSE |
|
60757 | 90 |
HEADGOAL (etac ctxt meta_mp THEN' resolve_tac ctxt collapses); |
49029 | 91 |
|
49484 | 92 |
fun mk_collapse_tac ctxt m discD sels = |
60728 | 93 |
HEADGOAL (dtac ctxt discD THEN' |
52325 | 94 |
(if m = 0 then |
60752 | 95 |
assume_tac ctxt |
52325 | 96 |
else |
60728 | 97 |
REPEAT_DETERM_N m o etac ctxt exE THEN' hyp_subst_tac ctxt THEN' |
98 |
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac ctxt refl)); |
|
49030 | 99 |
|
59271 | 100 |
fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases = |
101 |
HEADGOAL Goal.conjunction_tac THEN |
|
60784 | 102 |
ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW |
59271 | 103 |
(hyp_subst_tac ctxt THEN' |
104 |
SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @ |
|
105 |
((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59271
diff
changeset
|
106 |
resolve_tac ctxt @{thms TrueI True_not_False False_not_True})); |
59271 | 107 |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
108 |
fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
109 |
distinct_discsss' = |
49486 | 110 |
if ms = [0] then |
60728 | 111 |
HEADGOAL (rtac ctxt (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN' |
60752 | 112 |
TRY o |
113 |
EVERY' [rtac ctxt uexhaust_disc, assume_tac ctxt, rtac ctxt vexhaust_disc, assume_tac ctxt]) |
|
49486 | 114 |
else |
51742
b5ff7393642d
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)
blanchet
parents:
51717
diff
changeset
|
115 |
let val ks = 1 upto n in |
60728 | 116 |
HEADGOAL (rtac ctxt uexhaust_disc THEN' |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
57983
diff
changeset
|
117 |
EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse => |
60752 | 118 |
EVERY' [rtac ctxt (uuncollapse RS trans) THEN' |
119 |
TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc, |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
57983
diff
changeset
|
120 |
EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse => |
52325 | 121 |
EVERY' |
122 |
(if k' = k then |
|
60752 | 123 |
[rtac ctxt (vuncollapse RS trans), TRY o assume_tac ctxt] @ |
52325 | 124 |
(if m = 0 then |
60728 | 125 |
[rtac ctxt refl] |
52325 | 126 |
else |
60752 | 127 |
[if n = 1 then K all_tac |
128 |
else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt], |
|
60728 | 129 |
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE, |
52325 | 130 |
asm_simp_tac (ss_only [] ctxt)]) |
131 |
else |
|
60728 | 132 |
[dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')), |
133 |
etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}), |
|
60752 | 134 |
assume_tac ctxt, assume_tac ctxt])) |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
135 |
ks distinct_discss distinct_discss' uncollapses)]) |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57525
diff
changeset
|
136 |
ks ms distinct_discsss distinct_discsss' uncollapses)) |
49486 | 137 |
end; |
138 |
||
52967 | 139 |
fun mk_case_same_ctr_tac ctxt injects = |
60728 | 140 |
REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN' |
52967 | 141 |
(case injects of |
60752 | 142 |
[] => assume_tac ctxt |
60728 | 143 |
| [inject] => dtac ctxt (inject RS iffD1) THEN' REPEAT_DETERM o etac ctxt conjE THEN' |
144 |
hyp_subst_tac ctxt THEN' rtac ctxt refl); |
|
52967 | 145 |
|
146 |
fun mk_case_distinct_ctrs_tac ctxt distincts = |
|
60728 | 147 |
REPEAT_DETERM o etac ctxt exE THEN' etac ctxt conjE THEN' full_simp_tac (ss_only distincts ctxt); |
52967 | 148 |
|
52968
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
149 |
fun mk_case_tac ctxt n k case_def injects distinctss = |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
150 |
let |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
151 |
val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq); |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
152 |
val ks = 1 upto n; |
2b430bbb5a1a
define case constant from other 'free constructor' axioms
blanchet
parents:
52967
diff
changeset
|
153 |
in |
60728 | 154 |
HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN' |
155 |
rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN' rtac ctxt refl THEN' |
|
156 |
rtac ctxt refl THEN' |
|
52967 | 157 |
EVERY' (map2 (fn k' => fn distincts => |
60728 | 158 |
(if k' < n then etac ctxt disjE else K all_tac) THEN' |
52967 | 159 |
(if k' = k then mk_case_same_ctr_tac ctxt injects |
160 |
else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) |
|
161 |
end; |
|
162 |
||
59266 | 163 |
fun mk_case_distrib_tac ctxt ct exhaust cases = |
60784 | 164 |
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)) THEN |
60728 | 165 |
ALLGOALS (hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt cases) THEN' rtac ctxt refl); |
59266 | 166 |
|
54491 | 167 |
fun mk_case_cong_tac ctxt uexhaust cases = |
60728 | 168 |
HEADGOAL (rtac ctxt uexhaust THEN' |
169 |
EVERY' (maps (fn casex => [dtac ctxt sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); |
|
54491 | 170 |
|
171 |
fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss = |
|
60728 | 172 |
HEADGOAL (rtac ctxt uexhaust THEN' |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
57983
diff
changeset
|
173 |
EVERY' (@{map 3} (fn casex => fn if_discs => fn sels => |
52325 | 174 |
EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), |
60728 | 175 |
rtac ctxt casex]) |
52325 | 176 |
cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)); |
49031 | 177 |
|
60251
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
178 |
fun mk_split_tac ctxt ms uexhaust cases selss injectss distinctsss = |
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
179 |
let val depth = fold Integer.max ms 0 in |
60728 | 180 |
HEADGOAL (rtac ctxt uexhaust) THEN |
60251
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
181 |
ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' |
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
182 |
simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @ |
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
183 |
flat (nth distinctsss (k - 1))) ctxt)) k) THEN |
60728 | 184 |
ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN' |
185 |
REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN' |
|
60752 | 186 |
hyp_subst_tac ctxt THEN' assume_tac ctxt THEN' |
187 |
REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN' |
|
188 |
REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN' |
|
189 |
rtac ctxt refl THEN' assume_tac ctxt) |
|
60251
98754695b421
made split-rule tactic go beyond constructors with 20 arguments
blanchet
parents:
59498
diff
changeset
|
190 |
end; |
49032 | 191 |
|
49044 | 192 |
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex}; |
193 |
||
194 |
fun mk_split_asm_tac ctxt split = |
|
60728 | 195 |
HEADGOAL (rtac ctxt (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN |
196 |
HEADGOAL (rtac ctxt refl); |
|
49044 | 197 |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
diff
changeset
|
198 |
end; |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
199 |
|
54491 | 200 |
structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics; |