1 (* Title: HOL/BNF/Tools/bnf_comp_tactics.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Jasmin Blanchette, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Tactics for composition of bounded natural functors. |
|
7 *) |
|
8 |
|
9 signature BNF_COMP_TACTICS = |
|
10 sig |
|
11 val mk_comp_bd_card_order_tac: thm list -> thm -> tactic |
|
12 val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic |
|
13 val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic |
|
14 val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic |
|
15 val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic |
|
16 val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic |
|
17 val mk_comp_set_alt_tac: Proof.context -> thm -> tactic |
|
18 val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic |
|
19 val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic |
|
20 val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic |
|
21 |
|
22 val mk_kill_bd_card_order_tac: int -> thm -> tactic |
|
23 val mk_kill_bd_cinfinite_tac: thm -> tactic |
|
24 val kill_in_alt_tac: tactic |
|
25 val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic |
|
26 val mk_kill_set_bd_tac: thm -> thm -> tactic |
|
27 |
|
28 val empty_natural_tac: tactic |
|
29 val lift_in_alt_tac: tactic |
|
30 val mk_lift_set_bd_tac: thm -> tactic |
|
31 |
|
32 val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic |
|
33 |
|
34 val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic |
|
35 val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic |
|
36 val mk_simple_wit_tac: thm list -> tactic |
|
37 end; |
|
38 |
|
39 structure BNF_Comp_Tactics : BNF_COMP_TACTICS = |
|
40 struct |
|
41 |
|
42 open BNF_Util |
|
43 open BNF_Tactics |
|
44 |
|
45 val Cnotzero_UNIV = @{thm Cnotzero_UNIV}; |
|
46 val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
|
47 val csum_Cnotzero1 = @{thm csum_Cnotzero1}; |
|
48 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
|
49 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
|
50 val trans_o_apply = @{thm trans[OF o_apply]}; |
|
51 |
|
52 |
|
53 |
|
54 (* Composition *) |
|
55 |
|
56 fun mk_comp_set_alt_tac ctxt collect_set_map = |
|
57 unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN |
|
58 unfold_thms_tac ctxt [collect_set_map RS sym] THEN |
|
59 rtac refl 1; |
|
60 |
|
61 fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s = |
|
62 EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @ |
|
63 map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1; |
|
64 |
|
65 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s = |
|
66 EVERY' ([rtac ext, rtac sym, rtac trans_o_apply, |
|
67 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @ |
|
68 map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1; |
|
69 |
|
70 fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s = |
|
71 EVERY' ([rtac ext] @ |
|
72 replicate 3 (rtac trans_o_apply) @ |
|
73 [rtac (arg_cong_Union RS trans), |
|
74 rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans), |
|
75 rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), |
|
76 rtac Gmap_cong0] @ |
|
77 map (fn thm => rtac (thm RS fun_cong)) set_map0s @ |
|
78 [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, |
|
79 rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, |
|
80 rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), |
|
81 rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
|
82 rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
|
83 rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
|
84 [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]}, |
|
85 rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
|
86 rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, |
|
87 rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
|
88 rtac @{thm image_empty}]) 1; |
|
89 |
|
90 fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s = |
|
91 let |
|
92 val n = length comp_set_alts; |
|
93 in |
|
94 (if n = 0 then rtac refl 1 |
|
95 else rtac map_cong0 1 THEN |
|
96 EVERY' (map_index (fn (i, map_cong0) => |
|
97 rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) => |
|
98 EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp, |
|
99 rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans), |
|
100 rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union), |
|
101 rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2}, |
|
102 rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp), |
|
103 etac @{thm imageI}, atac]) |
|
104 comp_set_alts)) |
|
105 map_cong0s) 1) |
|
106 end; |
|
107 |
|
108 fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order = |
|
109 let |
|
110 val (card_orders, last_card_order) = split_last Fbd_card_orders; |
|
111 fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm; |
|
112 in |
|
113 (rtac @{thm card_order_cprod} THEN' |
|
114 WRAP' gen_before (K (K all_tac)) card_orders (rtac last_card_order) THEN' |
|
115 rtac Gbd_card_order) 1 |
|
116 end; |
|
117 |
|
118 fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite = |
|
119 (rtac @{thm cinfinite_cprod} THEN' |
|
120 ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN' |
|
121 ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE' |
|
122 rtac Fbd_cinfinite)) ORELSE' |
|
123 rtac Fbd_cinfinite) THEN' |
|
124 rtac Gbd_cinfinite) 1; |
|
125 |
|
126 fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds = |
|
127 let |
|
128 val (bds, last_bd) = split_last Gset_Fset_bds; |
|
129 fun gen_before bd = |
|
130 rtac ctrans THEN' rtac @{thm Un_csum} THEN' |
|
131 rtac ctrans THEN' rtac @{thm csum_mono} THEN' |
|
132 rtac bd; |
|
133 fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1}; |
|
134 in |
|
135 unfold_thms_tac ctxt [comp_set_alt] THEN |
|
136 rtac @{thm comp_set_bd_Union_o_collect} 1 THEN |
|
137 unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN |
|
138 (rtac ctrans THEN' |
|
139 WRAP' gen_before gen_after bds (rtac last_bd) THEN' |
|
140 rtac @{thm ordIso_imp_ordLeq} THEN' |
|
141 rtac @{thm cprod_com}) 1 |
|
142 end; |
|
143 |
|
144 val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert |
|
145 Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset |
|
146 conj_assoc}; |
|
147 |
|
148 fun mk_comp_in_alt_tac ctxt comp_set_alts = |
|
149 unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN |
|
150 unfold_thms_tac ctxt @{thms set_eq_subset} THEN |
|
151 rtac conjI 1 THEN |
|
152 REPEAT_DETERM ( |
|
153 rtac @{thm subsetI} 1 THEN |
|
154 unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN |
|
155 (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
|
156 REPEAT_DETERM (CHANGED (( |
|
157 (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE' |
|
158 atac ORELSE' |
|
159 (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1)); |
|
160 |
|
161 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def |
|
162 Union_image_insert Union_image_empty}; |
|
163 |
|
164 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms = |
|
165 ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN |
|
166 unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN |
|
167 REPEAT_DETERM ((atac ORELSE' |
|
168 REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN' |
|
169 etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN' |
|
170 (etac FalseE ORELSE' |
|
171 hyp_subst_tac ctxt THEN' |
|
172 dresolve_tac Fwit_thms THEN' |
|
173 (etac FalseE ORELSE' atac))) 1); |
|
174 |
|
175 |
|
176 |
|
177 (* Kill operation *) |
|
178 |
|
179 fun mk_kill_map_cong0_tac ctxt n m map_cong0 = |
|
180 (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN' |
|
181 EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1; |
|
182 |
|
183 fun mk_kill_bd_card_order_tac n bd_card_order = |
|
184 (rtac @{thm card_order_cprod} THEN' |
|
185 K (REPEAT_DETERM_N (n - 1) |
|
186 ((rtac @{thm card_order_csum} THEN' |
|
187 rtac @{thm card_of_card_order_on}) 1)) THEN' |
|
188 rtac @{thm card_of_card_order_on} THEN' |
|
189 rtac bd_card_order) 1; |
|
190 |
|
191 fun mk_kill_bd_cinfinite_tac bd_Cinfinite = |
|
192 (rtac @{thm cinfinite_cprod2} THEN' |
|
193 TRY o rtac csum_Cnotzero1 THEN' |
|
194 rtac Cnotzero_UNIV THEN' |
|
195 rtac bd_Cinfinite) 1; |
|
196 |
|
197 fun mk_kill_set_bd_tac bd_Card_order set_bd = |
|
198 (rtac ctrans THEN' |
|
199 rtac set_bd THEN' |
|
200 rtac @{thm ordLeq_cprod2} THEN' |
|
201 TRY o rtac csum_Cnotzero1 THEN' |
|
202 rtac Cnotzero_UNIV THEN' |
|
203 rtac bd_Card_order) 1 |
|
204 |
|
205 val kill_in_alt_tac = |
|
206 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
|
207 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
|
208 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
|
209 rtac conjI THEN' rtac subset_UNIV) 1)) THEN |
|
210 (rtac subset_UNIV ORELSE' atac) 1 THEN |
|
211 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
|
212 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE |
|
213 ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
|
214 REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1)); |
|
215 |
|
216 |
|
217 |
|
218 (* Lift operation *) |
|
219 |
|
220 val empty_natural_tac = rtac @{thm empty_natural} 1; |
|
221 |
|
222 fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1; |
|
223 |
|
224 val lift_in_alt_tac = |
|
225 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
|
226 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
|
227 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN |
|
228 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
|
229 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
|
230 rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN |
|
231 (rtac @{thm empty_subsetI} ORELSE' atac) 1) ORELSE |
|
232 ((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
|
233 REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1)); |
|
234 |
|
235 |
|
236 |
|
237 (* Permute operation *) |
|
238 |
|
239 fun mk_permute_in_alt_tac src dest = |
|
240 (rtac @{thm Collect_cong} THEN' |
|
241 mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong} |
|
242 dest src) 1; |
|
243 |
|
244 fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs = |
|
245 EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1; |
|
246 |
|
247 fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm = |
|
248 rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1; |
|
249 |
|
250 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms)); |
|
251 |
|
252 end; |
|