blanchet@55144
|
1 |
(* Title: HOL/BNF/Tools/ctr_sugar_tactics.ML
|
blanchet@50035
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@50035
|
3 |
Copyright 2012
|
blanchet@50035
|
4 |
|
blanchet@52934
|
5 |
Tactics for wrapping existing freely generated type's constructors.
|
blanchet@50035
|
6 |
*)
|
blanchet@50035
|
7 |
|
blanchet@55145
|
8 |
signature CTR_SUGAR_GENERAL_TACTICS =
|
blanchet@55145
|
9 |
sig
|
blanchet@55145
|
10 |
val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
|
blanchet@55145
|
11 |
val unfold_thms_tac: Proof.context -> thm list -> tactic
|
blanchet@55145
|
12 |
end;
|
blanchet@55145
|
13 |
|
blanchet@55143
|
14 |
signature CTR_SUGAR_TACTICS =
|
blanchet@50035
|
15 |
sig
|
blanchet@55145
|
16 |
include CTR_SUGAR_GENERAL_TACTICS
|
blanchet@55145
|
17 |
|
blanchet@50163
|
18 |
val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
|
blanchet@54105
|
19 |
val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
|
wenzelm@52854
|
20 |
val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
|
blanchet@54994
|
21 |
val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
|
blanchet@54994
|
22 |
thm list list -> tactic
|
blanchet@50133
|
23 |
val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
|
blanchet@50044
|
24 |
val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
|
wenzelm@52854
|
25 |
val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
|
wenzelm@52854
|
26 |
thm list list list -> thm list list list -> tactic
|
wenzelm@52935
|
27 |
val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
|
blanchet@50035
|
28 |
val mk_nchotomy_tac: int -> thm -> tactic
|
blanchet@50137
|
29 |
val mk_other_half_disc_exclude_tac: thm -> tactic
|
blanchet@55053
|
30 |
val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
|
blanchet@55054
|
31 |
val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
|
blanchet@55054
|
32 |
list list -> tactic
|
blanchet@50059
|
33 |
val mk_split_asm_tac: Proof.context -> thm -> tactic
|
blanchet@50152
|
34 |
val mk_unique_disc_def_tac: int -> thm -> tactic
|
blanchet@50035
|
35 |
end;
|
blanchet@50035
|
36 |
|
blanchet@55143
|
37 |
structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
|
blanchet@50035
|
38 |
struct
|
blanchet@50035
|
39 |
|
blanchet@55145
|
40 |
open Ctr_Sugar_Util
|
blanchet@50035
|
41 |
|
blanchet@50501
|
42 |
val meta_mp = @{thm meta_mp};
|
blanchet@50501
|
43 |
|
blanchet@55145
|
44 |
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
|
blanchet@55145
|
45 |
tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
|
blanchet@55145
|
46 |
|
blanchet@55145
|
47 |
fun unfold_thms_tac _ [] = all_tac
|
blanchet@55145
|
48 |
| unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
|
blanchet@55145
|
49 |
|
blanchet@50227
|
50 |
fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
|
blanchet@50046
|
51 |
|
blanchet@50035
|
52 |
fun mk_nchotomy_tac n exhaust =
|
blanchet@53462
|
53 |
HEADGOAL (rtac allI THEN' rtac exhaust THEN'
|
blanchet@54103
|
54 |
EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
|
blanchet@50035
|
55 |
|
blanchet@50501
|
56 |
fun mk_unique_disc_def_tac m uexhaust =
|
blanchet@53462
|
57 |
HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
|
blanchet@50152
|
58 |
|
blanchet@50501
|
59 |
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
|
blanchet@53462
|
60 |
HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
|
traytel@50645
|
61 |
rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
|
wenzelm@52935
|
62 |
hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
|
blanchet@50501
|
63 |
rtac distinct, rtac uexhaust] @
|
blanchet@50189
|
64 |
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|
blanchet@53462
|
65 |
|> k = 1 ? swap |> op @)));
|
blanchet@50131
|
66 |
|
wenzelm@52935
|
67 |
fun mk_half_disc_exclude_tac ctxt m discD disc' =
|
blanchet@53462
|
68 |
HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
|
blanchet@53462
|
69 |
rtac disc');
|
blanchet@50043
|
70 |
|
blanchet@53462
|
71 |
fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
|
blanchet@50043
|
72 |
|
blanchet@55053
|
73 |
fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
|
blanchet@53462
|
74 |
HEADGOAL (rtac exhaust THEN'
|
blanchet@55053
|
75 |
EVERY' (map2 (fn k => fn destI => dtac destI THEN'
|
blanchet@55053
|
76 |
select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
|
blanchet@55053
|
77 |
|
blanchet@55053
|
78 |
val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
|
blanchet@55053
|
79 |
|
blanchet@55053
|
80 |
fun mk_sel_exhaust_tac n disc_exhaust collapses =
|
blanchet@55057
|
81 |
mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
|
blanchet@55057
|
82 |
HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
|
blanchet@50044
|
83 |
|
blanchet@50499
|
84 |
fun mk_collapse_tac ctxt m discD sels =
|
blanchet@53462
|
85 |
HEADGOAL (dtac discD THEN'
|
blanchet@53462
|
86 |
(if m = 0 then
|
blanchet@53462
|
87 |
atac
|
blanchet@53462
|
88 |
else
|
blanchet@53462
|
89 |
REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
|
blanchet@53462
|
90 |
SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
|
blanchet@50045
|
91 |
|
blanchet@52879
|
92 |
fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
|
blanchet@52879
|
93 |
disc_excludesss' =
|
blanchet@50501
|
94 |
if ms = [0] then
|
blanchet@53462
|
95 |
HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
|
blanchet@53462
|
96 |
TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
|
blanchet@50501
|
97 |
else
|
blanchet@52879
|
98 |
let val ks = 1 upto n in
|
blanchet@53462
|
99 |
HEADGOAL (rtac udisc_exhaust THEN'
|
blanchet@53462
|
100 |
EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
|
blanchet@53462
|
101 |
fn uuncollapse =>
|
blanchet@53462
|
102 |
EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
|
blanchet@53462
|
103 |
rtac sym, rtac vdisc_exhaust,
|
blanchet@53462
|
104 |
EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
|
blanchet@53462
|
105 |
EVERY'
|
blanchet@53462
|
106 |
(if k' = k then
|
blanchet@53462
|
107 |
[rtac (vuncollapse RS trans), TRY o atac] @
|
blanchet@53462
|
108 |
(if m = 0 then
|
blanchet@53462
|
109 |
[rtac refl]
|
blanchet@53462
|
110 |
else
|
blanchet@53462
|
111 |
[if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
|
blanchet@53462
|
112 |
REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
|
blanchet@53462
|
113 |
asm_simp_tac (ss_only [] ctxt)])
|
blanchet@53462
|
114 |
else
|
blanchet@53462
|
115 |
[dtac (the_single (if k = n then disc_excludes else disc_excludes')),
|
blanchet@53462
|
116 |
etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
|
blanchet@53462
|
117 |
atac, atac]))
|
blanchet@53462
|
118 |
ks disc_excludess disc_excludess' uncollapses)])
|
blanchet@53462
|
119 |
ks ms disc_excludesss disc_excludesss' uncollapses))
|
blanchet@50501
|
120 |
end;
|
blanchet@50501
|
121 |
|
blanchet@54104
|
122 |
fun mk_case_same_ctr_tac ctxt injects =
|
blanchet@54104
|
123 |
REPEAT_DETERM o etac exE THEN' etac conjE THEN'
|
blanchet@54104
|
124 |
(case injects of
|
blanchet@54104
|
125 |
[] => atac
|
blanchet@54104
|
126 |
| [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
|
blanchet@54104
|
127 |
hyp_subst_tac ctxt THEN' rtac refl);
|
blanchet@54104
|
128 |
|
blanchet@54104
|
129 |
fun mk_case_distinct_ctrs_tac ctxt distincts =
|
blanchet@54104
|
130 |
REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
|
blanchet@54104
|
131 |
|
blanchet@54105
|
132 |
fun mk_case_tac ctxt n k case_def injects distinctss =
|
blanchet@54105
|
133 |
let
|
blanchet@54105
|
134 |
val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
|
blanchet@54105
|
135 |
val ks = 1 upto n;
|
blanchet@54105
|
136 |
in
|
blanchet@54105
|
137 |
HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
|
blanchet@54105
|
138 |
rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
|
blanchet@54105
|
139 |
rtac refl THEN'
|
blanchet@54104
|
140 |
EVERY' (map2 (fn k' => fn distincts =>
|
blanchet@54104
|
141 |
(if k' < n then etac disjE else K all_tac) THEN'
|
blanchet@54104
|
142 |
(if k' = k then mk_case_same_ctr_tac ctxt injects
|
blanchet@54104
|
143 |
else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
|
blanchet@54104
|
144 |
end;
|
blanchet@54104
|
145 |
|
blanchet@54994
|
146 |
fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
|
blanchet@53462
|
147 |
HEADGOAL (rtac uexhaust THEN'
|
blanchet@53462
|
148 |
EVERY' (map3 (fn casex => fn if_discs => fn sels =>
|
blanchet@53462
|
149 |
EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
|
blanchet@53462
|
150 |
rtac casex])
|
blanchet@53462
|
151 |
cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
|
blanchet@50046
|
152 |
|
wenzelm@52854
|
153 |
fun mk_case_cong_tac ctxt uexhaust cases =
|
blanchet@53462
|
154 |
HEADGOAL (rtac uexhaust THEN'
|
blanchet@53462
|
155 |
EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
|
blanchet@50058
|
156 |
|
blanchet@55054
|
157 |
fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
|
blanchet@53462
|
158 |
HEADGOAL (rtac uexhaust) THEN
|
wenzelm@52935
|
159 |
ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
|
blanchet@55054
|
160 |
simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
|
wenzelm@52854
|
161 |
flat (nth distinctsss (k - 1))) ctxt)) k) THEN
|
wenzelm@53074
|
162 |
ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
|
blanchet@50047
|
163 |
|
blanchet@50059
|
164 |
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
|
blanchet@50059
|
165 |
|
blanchet@50059
|
166 |
fun mk_split_asm_tac ctxt split =
|
blanchet@53462
|
167 |
HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
|
blanchet@53462
|
168 |
HEADGOAL (rtac refl);
|
blanchet@50059
|
169 |
|
blanchet@50035
|
170 |
end;
|
blanchet@55145
|
171 |
|
blanchet@55145
|
172 |
structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;
|