|
1 (* Title: HOL/Codatatype/Tools/bnf_gfp_tactics.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012 |
|
6 |
|
7 Tactics for the codatatype construction. |
|
8 *) |
|
9 |
|
10 signature BNF_GFP_TACTICS = |
|
11 sig |
|
12 val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic |
|
13 val mk_bd_card_order_tac: thm -> tactic |
|
14 val mk_bd_cinfinite_tac: thm -> tactic |
|
15 val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list -> |
|
16 {prems: 'a, context: Proof.context} -> tactic |
|
17 val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic |
|
18 val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
|
19 val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic |
|
20 val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic |
|
21 val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm -> |
|
22 {prems: 'a, context: Proof.context} -> tactic |
|
23 val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic |
|
24 val mk_coalgT_tac: int -> thm list -> thm list -> thm list list -> |
|
25 {prems: 'a, context: Proof.context} -> tactic |
|
26 val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list -> |
|
27 tactic |
|
28 val mk_coalg_set_tac: thm -> tactic |
|
29 val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list -> |
|
30 {prems: 'a, context: Proof.context} -> tactic |
|
31 val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic |
|
32 val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm -> |
|
33 thm list list -> tactic |
|
34 val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list -> |
|
35 {prems: 'a, context: Proof.context} -> tactic |
|
36 val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic |
|
37 val mk_corec_tac: int -> thm list -> thm -> thm -> thm list -> |
|
38 {prems: 'a, context: Proof.context} -> tactic |
|
39 val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic |
|
40 val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic |
|
41 val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list -> |
|
42 {prems: 'a, context: Proof.context} -> tactic |
|
43 val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm -> |
|
44 thm -> thm -> thm -> tactic |
|
45 val mk_incl_lsbis_tac: int -> int -> thm -> tactic |
|
46 val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
|
47 val mk_length_Lev'_tac: thm -> tactic |
|
48 val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic |
|
49 val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic |
|
50 val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> |
|
51 thm list list -> thm list list list -> tactic |
|
52 val mk_map_id_tac: thm list -> thm -> thm -> tactic |
|
53 val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic |
|
54 val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
|
55 val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic |
|
56 val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list -> |
|
57 thm list -> {prems: 'a, context: Proof.context} -> tactic |
|
58 val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic |
|
59 val mk_mor_UNIV_tac: thm list -> thm -> tactic |
|
60 val mk_mor_beh_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list -> |
|
61 thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list -> |
|
62 thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> |
|
63 thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> |
|
64 {prems: 'a, context: Proof.context} -> tactic |
|
65 val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> |
|
66 thm list -> tactic |
|
67 val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic |
|
68 val mk_mor_elim_tac: thm -> tactic |
|
69 val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list -> |
|
70 thm list -> thm list list -> thm list list -> tactic |
|
71 val mk_mor_hset_tac: thm -> thm -> tactic |
|
72 val mk_mor_incl_tac: thm -> thm list -> tactic |
|
73 val mk_mor_str_tac: 'a list -> thm -> tactic |
|
74 val mk_mor_sum_case_tac: 'a list -> thm -> tactic |
|
75 val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list -> |
|
76 {prems: thm list, context: Proof.context} -> tactic |
|
77 val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list -> |
|
78 {prems: thm list, context: Proof.context} -> tactic |
|
79 val mk_mor_thePull_pick_tac: thm -> thm list -> thm list -> |
|
80 {prems: 'a, context: Proof.context} -> tactic |
|
81 val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic |
|
82 val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic) |
|
83 val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list -> |
|
84 thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} -> |
|
85 tactic |
|
86 val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
|
87 thm list -> thm list -> thm -> thm list -> tactic |
|
88 val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic |
|
89 val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list -> |
|
90 thm list -> tactic |
|
91 val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> |
|
92 thm list -> thm list -> thm list list -> tactic |
|
93 val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic |
|
94 val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic |
|
95 val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list -> |
|
96 thm list list -> tactic |
|
97 val mk_set_bd_tac: thm -> thm -> thm -> tactic |
|
98 val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic |
|
99 val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list -> |
|
100 thm list list -> thm list list -> tactic |
|
101 val mk_set_incl_hin_tac: thm list -> tactic |
|
102 val mk_set_incl_hset_tac: thm -> thm -> tactic |
|
103 val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic |
|
104 val mk_set_natural_tac: thm -> thm -> tactic |
|
105 val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> |
|
106 thm list list -> thm list list -> tactic |
|
107 val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic |
|
108 val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list -> |
|
109 cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> |
|
110 thm list list -> thm list list -> thm -> thm list list -> tactic |
|
111 val mk_unf_coinduct_tac: int -> int list -> thm -> thm -> tactic |
|
112 val mk_unf_coinduct_upto_tac: int list -> ctyp option list -> cterm option list -> thm -> thm -> |
|
113 thm -> tactic |
|
114 val mk_unf_o_fld_tac: thm -> thm -> thm -> thm -> thm list -> |
|
115 {prems: 'a, context: Proof.context} -> tactic |
|
116 val mk_unique_mor_tac: thm list -> thm -> tactic |
|
117 val mk_wit_tac: int -> thm list -> thm list -> thm list -> |
|
118 {prems: 'a, context: Proof.context} -> tactic |
|
119 val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic |
|
120 end; |
|
121 |
|
122 structure BNF_GFP_Tactics : BNF_GFP_TACTICS = |
|
123 struct |
|
124 |
|
125 open BNF_Tactics |
|
126 open BNF_Util |
|
127 open BNF_GFP_Util |
|
128 |
|
129 fun mk_coalg_set_tac coalg_def = |
|
130 dtac (coalg_def RS @{thm subst[of _ _ "\<lambda>x. x"]}) 1 THEN |
|
131 REPEAT_DETERM (etac conjE 1) THEN |
|
132 EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN |
|
133 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1; |
|
134 |
|
135 fun mk_mor_elim_tac mor_def = |
|
136 (dtac (subst OF [mor_def]) THEN' |
|
137 REPEAT o etac conjE THEN' |
|
138 TRY o rtac @{thm image_subsetI} THEN' |
|
139 etac bspec THEN' |
|
140 atac) 1; |
|
141 |
|
142 fun mk_mor_incl_tac mor_def map_id's = |
|
143 (stac mor_def THEN' |
|
144 rtac conjI THEN' |
|
145 CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm set_mp}, stac @{thm id_apply}, atac])) |
|
146 map_id's THEN' |
|
147 CONJ_WRAP' (fn thm => |
|
148 (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)])) |
|
149 map_id's) 1; |
|
150 |
|
151 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids = |
|
152 let |
|
153 fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac]; |
|
154 fun mor_tac ((mor_image, morE), map_comp_id) = |
|
155 EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans, |
|
156 etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac]; |
|
157 in |
|
158 (stac mor_def THEN' rtac conjI THEN' |
|
159 CONJ_WRAP' fbetw_tac mor_images THEN' |
|
160 CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1 |
|
161 end; |
|
162 |
|
163 fun mk_mor_UNIV_tac morEs mor_def = |
|
164 let |
|
165 val n = length morEs; |
|
166 fun mor_tac morE = EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, etac morE, |
|
167 rtac UNIV_I, rtac sym, rtac o_apply]; |
|
168 in |
|
169 EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, |
|
170 stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, |
|
171 CONJ_WRAP' (fn i => |
|
172 EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1 |
|
173 end; |
|
174 |
|
175 fun mk_mor_str_tac ks mor_UNIV = |
|
176 (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1; |
|
177 |
|
178 fun mk_mor_sum_case_tac ks mor_UNIV = |
|
179 (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm sum_case_comp_Inl[symmetric]})) ks) 1; |
|
180 |
|
181 fun mk_set_incl_hset_tac def rec_Suc = |
|
182 EVERY' (stac def :: |
|
183 map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, |
|
184 sym, rec_Suc]) 1; |
|
185 |
|
186 fun mk_set_hset_incl_hset_tac n defs rec_Suc i = |
|
187 EVERY' (map (TRY oo stac) defs @ |
|
188 map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, @{thm set_mp}, equalityD2, rec_Suc, |
|
189 UnI2, mk_UnN n i] @ |
|
190 [etac @{thm UN_I}, atac]) 1; |
|
191 |
|
192 fun mk_set_incl_hin_tac incls = |
|
193 if null incls then rtac @{thm subset_UNIV} 1 |
|
194 else EVERY' [rtac subsetI, rtac CollectI, |
|
195 CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1; |
|
196 |
|
197 fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} = |
|
198 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
199 REPEAT_DETERM o rtac allI, |
|
200 CONJ_WRAP' (fn thm => EVERY' |
|
201 [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s, |
|
202 REPEAT_DETERM o rtac allI, |
|
203 CONJ_WRAP' (fn rec_Suc => EVERY' |
|
204 [rtac @{thm ord_eq_le_trans}, rtac rec_Suc, |
|
205 if m = 0 then K all_tac |
|
206 else (rtac @{thm Un_least} THEN' Goal.assume_rule_tac ctxt), |
|
207 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) |
|
208 (K (EVERY' [rtac @{thm UN_least}, REPEAT_DETERM o eresolve_tac [allE, conjE], |
|
209 rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s]) |
|
210 rec_Sucs] 1; |
|
211 |
|
212 fun mk_hset_minimal_tac n hset_defs hset_rec_minimal {context = ctxt, prems = _} = |
|
213 (CONJ_WRAP' (fn def => (EVERY' [rtac @{thm ord_eq_le_trans}, rtac def, |
|
214 rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal, |
|
215 EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI, |
|
216 REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1 |
|
217 |
|
218 fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss = |
|
219 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
220 REPEAT_DETERM o rtac allI, |
|
221 CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s, |
|
222 REPEAT_DETERM o rtac allI, |
|
223 CONJ_WRAP' |
|
224 (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) => |
|
225 EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym), |
|
226 if m = 0 then K all_tac |
|
227 else EVERY' [rtac @{thm Un_cong}, rtac box_equals, |
|
228 rtac (nth passive_set_naturals (j - 1) RS sym), |
|
229 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac (morE RS arg_cong), atac], |
|
230 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) |
|
231 (fn (i, (set_natural, coalg_set)) => |
|
232 EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})), |
|
233 etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural, |
|
234 rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}), |
|
235 ftac coalg_set, atac, dtac @{thm set_mp}, atac, rtac mp, rtac (mk_conjunctN n i), |
|
236 REPEAT_DETERM o etac allE, atac, atac]) |
|
237 (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))]) |
|
238 (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1; |
|
239 |
|
240 fun mk_mor_hset_tac hset_def mor_hset_rec = |
|
241 EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec, |
|
242 atac, atac, rtac (hset_def RS sym)] 1 |
|
243 |
|
244 fun mk_bis_rel_tac m bis_def rel_defs map_comps map_congs set_naturalss = |
|
245 let |
|
246 val n = length rel_defs; |
|
247 val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ rel_defs); |
|
248 |
|
249 fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) = |
|
250 EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i), |
|
251 etac allE, etac allE, etac impE, atac, etac bexE, etac conjE, |
|
252 rtac (rel_def RS equalityD2 RS @{thm set_mp}), |
|
253 rtac @{thm relcompI}, rtac @{thm converseI}, |
|
254 EVERY' (map (fn thm => |
|
255 EVERY' [rtac @{thm GrI}, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
256 rtac CollectI, |
|
257 CONJ_WRAP' (fn (i, thm) => |
|
258 if i <= m |
|
259 then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac subset_trans, |
|
260 etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm diagI}] |
|
261 else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm, |
|
262 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac]) |
|
263 (1 upto (m + n) ~~ set_naturals), |
|
264 rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm, |
|
265 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac]) |
|
266 @{thms fst_diag_id snd_diag_id})]; |
|
267 |
|
268 fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), rel_def) = |
|
269 EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, |
|
270 etac allE, etac allE, etac impE, atac, |
|
271 dtac (rel_def RS equalityD1 RS @{thm set_mp}), |
|
272 REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
|
273 REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE], |
|
274 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
275 REPEAT_DETERM o etac conjE, |
|
276 hyp_subst_tac, |
|
277 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
278 rtac bexI, rtac conjI, rtac trans, rtac map_comp, |
|
279 REPEAT_DETERM_N m o stac @{thm id_o}, |
|
280 REPEAT_DETERM_N n o stac @{thm o_id}, |
|
281 etac sym, rtac trans, rtac map_comp, |
|
282 REPEAT_DETERM_N m o stac @{thm id_o}, |
|
283 REPEAT_DETERM_N n o stac @{thm o_id}, |
|
284 rtac trans, rtac map_cong, |
|
285 REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac @{thm set_mp}, atac], |
|
286 REPEAT_DETERM_N n o rtac refl, |
|
287 etac sym, rtac CollectI, |
|
288 CONJ_WRAP' (fn (i, thm) => |
|
289 if i <= m |
|
290 then EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI}, |
|
291 rtac @{thm diag_fst}, etac @{thm set_mp}, atac] |
|
292 else EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac thm, |
|
293 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac]) |
|
294 (1 upto (m + n) ~~ set_naturals)]; |
|
295 in |
|
296 EVERY' [rtac (bis_def RS trans), |
|
297 rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, |
|
298 etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1 |
|
299 end; |
|
300 |
|
301 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses = |
|
302 EVERY' [stac bis_rel, dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}), |
|
303 REPEAT_DETERM o etac conjE, rtac conjI, |
|
304 CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans, |
|
305 rtac equalityD2, rtac @{thm converse_Times}])) rel_congs, |
|
306 CONJ_WRAP' (fn (rel_cong, rel_converse) => |
|
307 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
|
308 rtac (rel_cong RS trans), |
|
309 REPEAT_DETERM_N m o rtac @{thm diag_converse}, |
|
310 REPEAT_DETERM_N (length rel_congs) o rtac refl, |
|
311 rtac rel_converse, |
|
312 REPEAT_DETERM o etac allE, |
|
313 rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1; |
|
314 |
|
315 fun mk_bis_O_tac m bis_rel rel_congs rel_Os = |
|
316 EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS @{thm subst[of _ _ "%x. x"]}), |
|
317 REPEAT_DETERM o etac conjE, rtac conjI, |
|
318 CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs, |
|
319 CONJ_WRAP' (fn (rel_cong, rel_O) => |
|
320 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
|
321 rtac (rel_cong RS trans), |
|
322 REPEAT_DETERM_N m o rtac @{thm diag_Comp}, |
|
323 REPEAT_DETERM_N (length rel_congs) o rtac refl, |
|
324 rtac rel_O, |
|
325 etac @{thm relcompE}, |
|
326 REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
327 etac conjE, hyp_subst_tac, |
|
328 REPEAT_DETERM o etac allE, rtac @{thm relcompI}, |
|
329 etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1; |
|
330 |
|
331 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins |
|
332 {context = ctxt, prems = _} = |
|
333 Local_Defs.unfold_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN |
|
334 EVERY' [rtac conjI, |
|
335 CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images, |
|
336 CONJ_WRAP' (fn (coalg_in, morE) => |
|
337 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrI}, etac coalg_in, |
|
338 etac @{thm GrD1}, etac (morE RS trans), etac @{thm GrD1}, |
|
339 etac (@{thm GrD2} RS arg_cong)]) (coalg_ins ~~ morEs)] 1; |
|
340 |
|
341 fun mk_bis_Union_tac bis_def in_monos {context = ctxt, prems = _} = |
|
342 let |
|
343 val n = length in_monos; |
|
344 val ks = 1 upto n; |
|
345 in |
|
346 Local_Defs.unfold_tac ctxt [bis_def] THEN |
|
347 EVERY' [rtac conjI, |
|
348 CONJ_WRAP' (fn i => |
|
349 EVERY' [rtac @{thm UN_least}, dtac bspec, atac, |
|
350 dtac conjunct1, etac (mk_conjunctN n i)]) ks, |
|
351 CONJ_WRAP' (fn (i, in_mono) => |
|
352 EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac, |
|
353 dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp, |
|
354 atac, etac bexE, rtac bexI, atac, rtac in_mono, |
|
355 REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]}, |
|
356 atac]) (ks ~~ in_monos)] 1 |
|
357 end; |
|
358 |
|
359 fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong = |
|
360 let |
|
361 val n = length lsbis_defs; |
|
362 in |
|
363 EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs), |
|
364 rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE], |
|
365 hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1 |
|
366 end; |
|
367 |
|
368 fun mk_incl_lsbis_tac n i lsbis_def = |
|
369 EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, |
|
370 REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, |
|
371 rtac (mk_nth_conv n i)] 1; |
|
372 |
|
373 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O = |
|
374 EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF equiv_def]}, |
|
375 |
|
376 rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF refl_on_def]}, |
|
377 rtac conjI, rtac lsbis_incl, rtac ballI, rtac @{thm set_mp}, |
|
378 rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI}, |
|
379 |
|
380 rtac conjI, rtac @{thm ssubst[of _ _ "%x. x", OF sym_def]}, |
|
381 rtac allI, rtac allI, rtac impI, rtac @{thm set_mp}, |
|
382 rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI}, |
|
383 |
|
384 rtac @{thm ssubst[of _ _ "%x. x", OF trans_def]}, |
|
385 rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac @{thm set_mp}, |
|
386 rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis, |
|
387 etac @{thm relcompI}, atac] 1; |
|
388 |
|
389 fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} = |
|
390 let |
|
391 val n = length strT_defs; |
|
392 val ks = 1 upto n; |
|
393 fun coalg_tac (i, ((passive_sets, active_sets), def)) = |
|
394 EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
|
395 hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans), |
|
396 rtac (mk_sum_casesN n i), rtac CollectI, |
|
397 EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS @{thm ord_eq_le_trans}), |
|
398 etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS |
|
399 @{thm ord_eq_le_trans})]) passive_sets), |
|
400 CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}), |
|
401 rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl, |
|
402 rtac conjI, |
|
403 rtac conjI, etac @{thm empty_Shift}, dtac @{thm set_rev_mp}, |
|
404 etac equalityD1, etac CollectD, |
|
405 rtac conjI, etac @{thm Shift_clists}, |
|
406 rtac conjI, etac @{thm Shift_prefCl}, |
|
407 rtac conjI, rtac ballI, |
|
408 rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1, |
|
409 SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Succ_Shift shift_def}), |
|
410 etac bspec, etac @{thm ShiftD}, |
|
411 CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD}, |
|
412 dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i), |
|
413 dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]}, |
|
414 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, |
|
415 rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans), |
|
416 rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac, |
|
417 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
|
418 CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong}, |
|
419 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift}, |
|
420 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks, |
|
421 rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE], |
|
422 etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac, |
|
423 dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec, |
|
424 etac @{thm set_mp[OF equalityD1]}, atac, |
|
425 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, |
|
426 rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans), |
|
427 etac (@{thm append_Nil} RS sym RS arg_cong RS trans), |
|
428 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
|
429 CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong}, |
|
430 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift}, |
|
431 rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)]; |
|
432 in |
|
433 Local_Defs.unfold_tac ctxt defs THEN |
|
434 CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1 |
|
435 end; |
|
436 |
|
437 fun mk_card_of_carT_tac m isNode_defs sbd_sbd |
|
438 sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds = |
|
439 let |
|
440 val n = length isNode_defs; |
|
441 in |
|
442 EVERY' [rtac (Thm.permute_prems 0 1 ctrans), |
|
443 rtac @{thm card_of_Sigma_ordLeq_Cinfinite}, rtac @{thm Cinfinite_cexp}, |
|
444 if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2}, |
|
445 rtac @{thm Card_order_ctwo}, rtac @{thm Cinfinite_cexp}, |
|
446 rtac @{thm ctwo_ordLeq_Cinfinite}, rtac sbd_Cinfinite, rtac sbd_Cinfinite, |
|
447 rtac ctrans, rtac @{thm card_of_diff}, |
|
448 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso}, |
|
449 rtac @{thm Card_order_cpow}, rtac @{thm ordIso_ordLeq_trans}, |
|
450 rtac @{thm cpow_cexp_ctwo}, rtac ctrans, rtac @{thm cexp_mono1_Cnotzero}, |
|
451 if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2}, |
|
452 rtac @{thm Card_order_ctwo}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_clists}, |
|
453 rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm ordIso_ordLeq_trans}, |
|
454 rtac @{thm clists_Cinfinite}, |
|
455 if n = 1 then rtac sbd_Cinfinite else rtac (sbd_Cinfinite RS @{thm Cinfinite_csum1}), |
|
456 rtac @{thm ordIso_ordLeq_trans}, rtac sbd_sbd, rtac @{thm infinite_ordLeq_cexp}, |
|
457 rtac sbd_Cinfinite, |
|
458 if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, |
|
459 rtac @{thm Cnotzero_clists}, |
|
460 rtac ballI, rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Func_Ffunc}, |
|
461 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm Func_cexp}, |
|
462 rtac ctrans, rtac @{thm cexp_mono}, |
|
463 rtac @{thm ordLeq_ordIso_trans}, |
|
464 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 |
|
465 (sbd_Cinfinite RS @{thm Cinfinite_cexp[OF ordLeq_csum2[OF Card_order_ctwo]]} |
|
466 RSN (3, @{thm Un_Cinfinite_bound})))) |
|
467 (fn thm => EVERY' [rtac ctrans, rtac @{thm card_of_image}, rtac thm]) (rev in_sbds), |
|
468 rtac @{thm cexp_cong1_Cnotzero}, rtac @{thm csum_cong1}, |
|
469 REPEAT_DETERM_N m o rtac @{thm csum_cong2}, |
|
470 CONJ_WRAP_GEN' (rtac @{thm csum_cong}) |
|
471 (K (rtac (sbd_Card_order RS @{thm card_of_Field_ordIso}))) in_sbds, |
|
472 rtac sbd_Card_order, |
|
473 rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, |
|
474 rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, |
|
475 rtac @{thm ordLeq_ordIso_trans}, etac @{thm clists_bound}, |
|
476 rtac @{thm clists_Cinfinite}, TRY o rtac @{thm Cinfinite_csum1}, rtac sbd_Cinfinite, |
|
477 rtac disjI2, rtac @{thm cone_ordLeq_cexp}, rtac @{thm cone_ordLeq_cexp}, |
|
478 rtac ctrans, rtac @{thm cone_ordLeq_ctwo}, rtac @{thm ordLeq_csum2}, |
|
479 rtac @{thm Card_order_ctwo}, rtac FalseE, etac @{thm cpow_clists_czero}, atac, |
|
480 rtac @{thm card_of_Card_order}, |
|
481 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod}, |
|
482 rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, |
|
483 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong2_Cnotzero}, |
|
484 rtac @{thm ordIso_transitive}, rtac @{thm cprod_cong2}, rtac sbd_sbd, |
|
485 rtac @{thm cprod_infinite}, rtac sbd_Cinfinite, |
|
486 rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac @{thm Card_order_cprod}, |
|
487 rtac ctrans, rtac @{thm cexp_mono1_Cnotzero}, |
|
488 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm ordIso_transitive}, rtac @{thm csum_cong1}, |
|
489 rtac @{thm ordIso_transitive}, |
|
490 REPEAT_DETERM_N m o rtac @{thm csum_cong2}, |
|
491 rtac sbd_sbd, |
|
492 BNF_Tactics.mk_rotate_eq_tac (rtac @{thm ordIso_refl} THEN' |
|
493 FIRST' [rtac @{thm card_of_Card_order}, |
|
494 rtac @{thm Card_order_csum}, rtac sbd_Card_order]) |
|
495 @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
|
496 (1 upto m + 1) (m + 1 :: (1 upto m)), |
|
497 if m = 0 then K all_tac else EVERY' [rtac @{thm ordIso_transitive}, rtac @{thm csum_assoc}], |
|
498 rtac @{thm csum_com}, rtac @{thm csum_cexp'}, rtac sbd_Cinfinite, |
|
499 if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum}, |
|
500 if m = 0 then rtac @{thm ordLeq_refl} else rtac @{thm ordLeq_csum2}, |
|
501 rtac @{thm Card_order_ctwo}, |
|
502 rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac sbd_Card_order, |
|
503 rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cprod_ordLeq}, |
|
504 if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, |
|
505 rtac sbd_Cinfinite, rtac sbd_Cnotzero, rtac @{thm ordLeq_refl}, rtac sbd_Card_order, |
|
506 rtac @{thm cexp_mono2_Cnotzero}, rtac @{thm infinite_ordLeq_cexp}, |
|
507 rtac sbd_Cinfinite, |
|
508 if m = 0 then rtac @{thm ctwo_Cnotzero} else rtac @{thm csum_Cnotzero2[OF ctwo_Cnotzero]}, |
|
509 rtac sbd_Cnotzero, |
|
510 rtac @{thm card_of_mono1}, rtac subsetI, |
|
511 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac, |
|
512 rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac @{thm set_mp}, rtac equalityD2, |
|
513 rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans), |
|
514 rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE}, |
|
515 hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS @{thm set_mp}), |
|
516 rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1, |
|
517 CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' |
|
518 [rtac (mk_UnN n i), dtac (def RS @{thm subst[of _ _ "%x. x"]}), |
|
519 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, |
|
520 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
|
521 CONJ_WRAP' (K (EVERY' [etac @{thm ord_eq_le_trans}, rtac subset_trans, |
|
522 rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order}, |
|
523 rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs), |
|
524 atac] 1 |
|
525 end; |
|
526 |
|
527 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= |
|
528 EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}), |
|
529 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
|
530 dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, |
|
531 etac conjE, hyp_subst_tac, |
|
532 dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}), |
|
533 REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
534 rtac (equalityD2 RS @{thm set_mp}), |
|
535 rtac (strT_def RS arg_cong RS trans), |
|
536 etac (arg_cong RS trans), |
|
537 fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt, |
|
538 rtac set_natural, rtac imageI, etac (equalityD2 RS @{thm set_mp}), rtac CollectI, |
|
539 etac @{thm prefCl_Succ}, atac] 1; |
|
540 |
|
541 fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs |
|
542 set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss = |
|
543 let |
|
544 val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss; |
|
545 val ks = 1 upto n; |
|
546 fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) = |
|
547 CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN' |
|
548 (if i = i' |
|
549 then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset, |
|
550 rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans), |
|
551 rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)), |
|
552 rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]), |
|
553 rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] |
|
554 else EVERY' [dtac (carT_def RS equalityD1 RS @{thm set_mp}), |
|
555 REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE, |
|
556 dtac conjunct2, dtac @{thm Pair_eq[THEN subst, of "%x. x"]}, etac conjE, |
|
557 hyp_subst_tac, dtac (isNode_def RS @{thm subst[of _ _ "%x. x"]}), |
|
558 REPEAT_DETERM o eresolve_tac [exE, conjE], |
|
559 rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac])) |
|
560 (ks ~~ (carT_defs ~~ isNode_defs)); |
|
561 fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) = |
|
562 dtac (mk_conjunctN n i) THEN' |
|
563 CONJ_WRAP' (fn (coalg_set, (carT_set, set_hset_incl_hset)) => |
|
564 EVERY' [rtac impI, etac conjE, etac impE, rtac conjI, |
|
565 rtac (coalgT RS coalg_set RS @{thm set_mp}), atac, etac carT_set, atac, atac, |
|
566 etac (@{thm shift_def} RS fun_cong RS trans), etac subset_trans, |
|
567 rtac set_hset_incl_hset, etac carT_set, atac, atac]) |
|
568 (coalg_sets ~~ (carT_sets ~~ set_hset_incl_hsets)); |
|
569 in |
|
570 EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}), |
|
571 REPEAT_DETERM o rtac allI, rtac impI, |
|
572 CONJ_WRAP' base_tac |
|
573 (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))), |
|
574 REPEAT_DETERM o rtac allI, rtac impI, |
|
575 REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI}, |
|
576 CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN' |
|
577 CONJ_WRAP_GEN' (K all_tac) step_tac |
|
578 (ks ~~ (drop m coalg_setss ~~ (carT_setss ~~ set_hset_incl_hsetss)))) ks] 1 |
|
579 end; |
|
580 |
|
581 fun mk_isNode_hset_tac n isNode_def strT_hsets {context = ctxt, prems = _} = |
|
582 let |
|
583 val m = length strT_hsets; |
|
584 in |
|
585 if m = 0 then atac 1 |
|
586 else (Local_Defs.unfold_tac ctxt [isNode_def] THEN |
|
587 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
|
588 rtac exI, rtac conjI, atac, |
|
589 CONJ_WRAP' (fn (thm, i) => if i > m then atac |
|
590 else EVERY' [rtac (thm RS subset_trans), atac, rtac conjI, atac, atac, atac]) |
|
591 (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1) |
|
592 end; |
|
593 |
|
594 fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss = |
|
595 let |
|
596 val n = length Lev_0s; |
|
597 val ks = 1 upto n; |
|
598 in |
|
599 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
600 REPEAT_DETERM o rtac allI, |
|
601 CONJ_WRAP' (fn Lev_0 => |
|
602 EVERY' (map rtac [@{thm ord_eq_le_trans}, Lev_0, @{thm Nil_clists}])) Lev_0s, |
|
603 REPEAT_DETERM o rtac allI, |
|
604 CONJ_WRAP' (fn (Lev_Suc, to_sbds) => |
|
605 EVERY' [rtac @{thm ord_eq_le_trans}, rtac Lev_Suc, |
|
606 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) |
|
607 (fn (i, to_sbd) => EVERY' [rtac subsetI, |
|
608 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
609 rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd, |
|
610 etac @{thm set_rev_mp}, REPEAT_DETERM o etac allE, |
|
611 etac (mk_conjunctN n i)]) |
|
612 (rev (ks ~~ to_sbds))]) |
|
613 (Lev_Sucs ~~ to_sbdss)] 1 |
|
614 end; |
|
615 |
|
616 fun mk_length_Lev_tac cts Lev_0s Lev_Sucs = |
|
617 let |
|
618 val n = length Lev_0s; |
|
619 val ks = n downto 1; |
|
620 in |
|
621 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
622 REPEAT_DETERM o rtac allI, |
|
623 CONJ_WRAP' (fn Lev_0 => |
|
624 EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), |
|
625 etac @{thm singletonE}, etac ssubst, rtac @{thm list.size(3)}]) Lev_0s, |
|
626 REPEAT_DETERM o rtac allI, |
|
627 CONJ_WRAP' (fn Lev_Suc => |
|
628 EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
629 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
630 (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
631 rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]}, |
|
632 REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks]) |
|
633 Lev_Sucs] 1 |
|
634 end; |
|
635 |
|
636 fun mk_length_Lev'_tac length_Lev = |
|
637 EVERY' [ftac length_Lev, etac ssubst, atac] 1; |
|
638 |
|
639 fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs = |
|
640 let |
|
641 val n = length Lev_0s; |
|
642 val ks = n downto 1; |
|
643 in |
|
644 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
645 REPEAT_DETERM o rtac allI, |
|
646 CONJ_WRAP' (fn Lev_0 => |
|
647 EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), |
|
648 etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]}, |
|
649 hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]}, |
|
650 rtac Lev_0, rtac @{thm singletonI}]) Lev_0s, |
|
651 REPEAT_DETERM o rtac allI, |
|
652 CONJ_WRAP' (fn (Lev_0, Lev_Suc) => |
|
653 EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
654 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
655 (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
656 dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac, |
|
657 rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]}, |
|
658 rtac Lev_0, rtac @{thm singletonI}, |
|
659 REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, |
|
660 rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]}, |
|
661 rtac Lev_Suc, rtac (mk_UnN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, |
|
662 rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), |
|
663 etac mp, etac conjI, atac]) ks]) |
|
664 (Lev_0s ~~ Lev_Sucs)] 1 |
|
665 end; |
|
666 |
|
667 fun mk_rv_last_tac cTs cts rv_Nils rv_Conss = |
|
668 let |
|
669 val n = length rv_Nils; |
|
670 val ks = 1 upto n; |
|
671 in |
|
672 EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}), |
|
673 REPEAT_DETERM o rtac allI, |
|
674 CONJ_WRAP' (fn rv_Cons => |
|
675 CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI, |
|
676 rtac (@{thm append_Nil} RS arg_cong RS trans), |
|
677 rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), rtac rv_Nil])) |
|
678 (ks ~~ rv_Nils)) |
|
679 rv_Conss, |
|
680 REPEAT_DETERM o rtac allI, rtac (mk_sumEN n), |
|
681 EVERY' (map (fn i => |
|
682 CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), |
|
683 CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI, |
|
684 rtac (@{thm append_Cons} RS arg_cong RS trans), |
|
685 rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans), |
|
686 rtac (mk_sum_casesN n i RS arg_cong RS trans), atac]) |
|
687 ks]) |
|
688 rv_Conss) |
|
689 ks)] 1 |
|
690 end; |
|
691 |
|
692 fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss = |
|
693 let |
|
694 val n = length Lev_0s; |
|
695 val ks = 1 upto n; |
|
696 in |
|
697 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
698 REPEAT_DETERM o rtac allI, |
|
699 CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) => |
|
700 EVERY' [rtac impI, REPEAT_DETERM o etac conjE, |
|
701 dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), etac @{thm singletonE}, etac ssubst, |
|
702 rtac (rv_Nil RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}), |
|
703 rtac (mk_sum_casesN n i RS @{thm ssubst[of _ _ "%x. x"]}), |
|
704 CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)]) |
|
705 (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)), |
|
706 REPEAT_DETERM o rtac allI, |
|
707 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) => |
|
708 EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
709 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
710 (fn (i, (from_to_sbd, coalg_set)) => |
|
711 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
712 rtac (rv_Cons RS arg_cong RS @{thm ssubst[of _ _ "%x. x"]}), |
|
713 rtac (mk_sum_casesN n i RS arg_cong RS trans RS @{thm ssubst[of _ _ "%x. x"]}), |
|
714 etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE, |
|
715 dtac (mk_conjunctN n i), etac mp, etac conjI, etac @{thm set_rev_mp}, |
|
716 etac coalg_set, atac]) |
|
717 (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))]) |
|
718 ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1 |
|
719 end; |
|
720 |
|
721 fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss = |
|
722 let |
|
723 val n = length Lev_0s; |
|
724 val ks = 1 upto n; |
|
725 in |
|
726 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
727 REPEAT_DETERM o rtac allI, |
|
728 CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => |
|
729 EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), |
|
730 etac @{thm singletonE}, hyp_subst_tac, |
|
731 CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN' |
|
732 (if i = i' |
|
733 then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac, |
|
734 CONJ_WRAP' (fn (i'', Lev_0'') => |
|
735 EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]}, |
|
736 rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i''), |
|
737 rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, |
|
738 etac conjI, rtac (Lev_0'' RS equalityD2 RS @{thm set_mp}), |
|
739 rtac @{thm singletonI}]) |
|
740 (ks ~~ Lev_0s)] |
|
741 else etac (mk_InN_not_InM i' i RS notE))) |
|
742 ks]) |
|
743 ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), |
|
744 REPEAT_DETERM o rtac allI, |
|
745 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), from_to_sbds) => |
|
746 EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
747 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
748 (fn (i, from_to_sbd) => |
|
749 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
750 CONJ_WRAP' (fn i' => rtac impI THEN' |
|
751 CONJ_WRAP' (fn i'' => |
|
752 EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), |
|
753 rtac @{thm ssubst_mem[OF append_Cons]}, rtac (mk_UnN n i), |
|
754 rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, |
|
755 rtac conjI, atac, dtac (sym RS trans RS sym), |
|
756 rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS trans), |
|
757 etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE, |
|
758 dtac (mk_conjunctN n i), dtac mp, atac, |
|
759 dtac (mk_conjunctN n i'), dtac mp, atac, |
|
760 dtac (mk_conjunctN n i''), etac mp, atac]) |
|
761 ks) |
|
762 ks]) |
|
763 (rev (ks ~~ from_to_sbds))]) |
|
764 ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1 |
|
765 end; |
|
766 |
|
767 fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss = |
|
768 let |
|
769 val n = length Lev_0s; |
|
770 val ks = 1 upto n; |
|
771 in |
|
772 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
773 REPEAT_DETERM o rtac allI, |
|
774 CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) => |
|
775 EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS @{thm set_mp}), |
|
776 etac @{thm singletonE}, hyp_subst_tac, |
|
777 CONJ_WRAP' (fn i' => rtac impI THEN' |
|
778 CONJ_WRAP' (fn i'' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN' |
|
779 (if i = i'' |
|
780 then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]}, |
|
781 dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), dtac (mk_InN_inject n i), |
|
782 hyp_subst_tac, |
|
783 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
784 (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
|
785 dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN' |
|
786 (if k = i' |
|
787 then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI] |
|
788 else etac (mk_InN_not_InM i' k RS notE))) |
|
789 (rev ks)] |
|
790 else etac (mk_InN_not_InM i'' i RS notE))) |
|
791 ks) |
|
792 ks]) |
|
793 ((ks ~~ (Lev_0s ~~ Lev_Sucs)) ~~ rv_Nils), |
|
794 REPEAT_DETERM o rtac allI, |
|
795 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, to_sbd_injs)) => |
|
796 EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
797 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
|
798 (fn (i, (from_to_sbd, to_sbd_inj)) => |
|
799 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN' |
|
800 CONJ_WRAP' (fn i' => rtac impI THEN' |
|
801 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN' |
|
802 dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}) THEN' |
|
803 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k => |
|
804 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
|
805 dtac @{thm list.inject[THEN subst, of "%x. x"]} THEN' etac conjE THEN' |
|
806 (if k = i |
|
807 then EVERY' [dtac (mk_InN_inject n i), |
|
808 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})), |
|
809 atac, atac, hyp_subst_tac] THEN' |
|
810 CONJ_WRAP' (fn i'' => |
|
811 EVERY' [rtac impI, dtac (sym RS trans), |
|
812 rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), |
|
813 etac (from_to_sbd RS arg_cong), |
|
814 REPEAT_DETERM o etac allE, |
|
815 dtac (mk_conjunctN n i), dtac mp, atac, |
|
816 dtac (mk_conjunctN n i'), dtac mp, atac, |
|
817 dtac (mk_conjunctN n i''), etac mp, etac sym]) |
|
818 ks |
|
819 else etac (mk_InN_not_InM i k RS notE))) |
|
820 (rev ks)) |
|
821 ks) |
|
822 (rev (ks ~~ (from_to_sbds ~~ to_sbd_injs)))]) |
|
823 ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1 |
|
824 end; |
|
825 |
|
826 fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs |
|
827 to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's |
|
828 prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss |
|
829 map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} = |
|
830 let |
|
831 val n = length beh_defs; |
|
832 val ks = 1 upto n; |
|
833 |
|
834 fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd, |
|
835 ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals, |
|
836 (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) = |
|
837 EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS @{thm set_mp}), |
|
838 rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI, |
|
839 rtac conjI, |
|
840 rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), |
|
841 rtac @{thm singletonI}, |
|
842 rtac conjI, |
|
843 rtac @{thm UN_least}, rtac Lev_sbd, |
|
844 rtac conjI, |
|
845 rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI, |
|
846 rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans}, |
|
847 etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac, |
|
848 rtac conjI, |
|
849 rtac ballI, etac @{thm UN_E}, rtac conjI, |
|
850 if n = 1 then K all_tac else rtac (mk_sumEN n), |
|
851 EVERY' (map6 (fn i => fn isNode_def => fn set_naturals => |
|
852 fn set_rv_Levs => fn set_Levs => fn set_image_Levs => |
|
853 EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst), |
|
854 rtac exI, rtac conjI, |
|
855 (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' |
|
856 else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN' |
|
857 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)), |
|
858 EVERY' (map2 (fn set_natural => fn set_rv_Lev => |
|
859 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans), |
|
860 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, |
|
861 etac set_rv_Lev, TRY o atac, etac conjI, atac]) |
|
862 (take m set_naturals) set_rv_Levs), |
|
863 CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => |
|
864 EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, |
|
865 rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, |
|
866 if n = 1 then rtac refl else atac, atac, rtac subsetI, |
|
867 REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], |
|
868 rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev', |
|
869 etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, |
|
870 if n = 1 then rtac refl else atac]) |
|
871 (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))]) |
|
872 ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss), |
|
873 CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals, |
|
874 (set_rv_Levs, (set_Levs, set_image_Levs)))))) => |
|
875 EVERY' [rtac ballI, |
|
876 REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], |
|
877 rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst), |
|
878 rtac exI, rtac conjI, |
|
879 (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' |
|
880 else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN' |
|
881 etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)), |
|
882 EVERY' (map2 (fn set_natural => fn set_rv_Lev => |
|
883 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans), |
|
884 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, |
|
885 etac set_rv_Lev, TRY o atac, etac conjI, atac]) |
|
886 (take m set_naturals) set_rv_Levs), |
|
887 CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => |
|
888 EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, |
|
889 rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, |
|
890 if n = 1 then rtac refl else atac, atac, rtac subsetI, |
|
891 REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], |
|
892 REPEAT_DETERM_N 4 o etac thin_rl, |
|
893 rtac set_image_Lev, |
|
894 atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev', |
|
895 etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, |
|
896 if n = 1 then rtac refl else atac]) |
|
897 (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))]) |
|
898 (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~ |
|
899 (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))), |
|
900 (**) |
|
901 rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI, |
|
902 etac notE, etac @{thm UN_I[OF UNIV_I]}, |
|
903 (*root isNode*) |
|
904 rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans), |
|
905 rtac length_Lev', rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI}, |
|
906 CONVERSION (Conv.top_conv |
|
907 (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), |
|
908 if n = 1 then rtac refl else rtac (mk_sum_casesN n i), |
|
909 EVERY' (map2 (fn set_natural => fn coalg_set => |
|
910 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac (set_natural RS trans), |
|
911 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, etac coalg_set, atac]) |
|
912 (take m set_naturals) (take m coalg_sets)), |
|
913 CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) => |
|
914 EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI}, |
|
915 rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev, |
|
916 rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), rtac @{thm singletonI}, rtac rv_Nil, |
|
917 atac, rtac subsetI, |
|
918 REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], |
|
919 rtac set_image_Lev, rtac (Lev_0 RS equalityD2 RS @{thm set_mp}), |
|
920 rtac @{thm singletonI}, dtac length_Lev', |
|
921 etac @{thm set_mp[OF equalityD1[OF arg_cong[OF |
|
922 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]}, |
|
923 rtac rv_Nil]) |
|
924 (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; |
|
925 |
|
926 fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)), |
|
927 ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = |
|
928 EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def, |
|
929 rtac (@{thm if_P} RS |
|
930 (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans), |
|
931 rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS @{thm set_mp}), |
|
932 rtac Lev_0, rtac @{thm singletonI}, |
|
933 CONVERSION (Conv.top_conv |
|
934 (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), |
|
935 if n = 1 then K all_tac |
|
936 else (rtac (@{thm sum_case_cong} RS trans) THEN' |
|
937 rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)), |
|
938 rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl), |
|
939 EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => |
|
940 DETERM o EVERY' [rtac trans, rtac o_apply, rtac ssubst, rtac @{thm Pair_eq}, rtac conjI, |
|
941 rtac trans, rtac @{thm Shift_def}, |
|
942 rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl, |
|
943 REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl, |
|
944 etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]}, |
|
945 rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc, |
|
946 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
|
947 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
|
948 dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE, |
|
949 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
|
950 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})), |
|
951 atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}] |
|
952 else etac (mk_InN_not_InM i' i'' RS notE)]) |
|
953 (rev ks), |
|
954 rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]}, |
|
955 rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI, |
|
956 REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, |
|
957 rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI, |
|
958 rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI, |
|
959 dtac asm_rl, dtac asm_rl, dtac asm_rl, |
|
960 dtac (Lev_Suc RS equalityD1 RS @{thm set_mp}), |
|
961 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
|
962 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
|
963 dtac @{thm list.inject[THEN subst, of "%x. x"]}, etac conjE, |
|
964 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
|
965 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS @{thm subst[of _ _ "%x. x"]})), |
|
966 atac, atac, hyp_subst_tac, atac] |
|
967 else etac (mk_InN_not_InM i' i'' RS notE)]) |
|
968 (rev ks), |
|
969 rtac (Lev_Suc RS equalityD2 RS @{thm set_mp}), rtac (mk_UnN n i'), rtac CollectI, |
|
970 REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, |
|
971 CONVERSION (Conv.top_conv |
|
972 (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), |
|
973 if n = 1 then K all_tac |
|
974 else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans), |
|
975 SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl, |
|
976 rtac refl]) |
|
977 ks to_sbd_injs from_to_sbds)]; |
|
978 in |
|
979 (rtac mor_cong THEN' |
|
980 EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN' |
|
981 stac mor_def THEN' rtac conjI THEN' |
|
982 CONJ_WRAP' fbetw_tac |
|
983 (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~ |
|
984 ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~ |
|
985 (set_naturalss ~~ (coalg_setss ~~ |
|
986 (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN' |
|
987 CONJ_WRAP' mor_tac |
|
988 (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~ |
|
989 ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~ |
|
990 (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1 |
|
991 end; |
|
992 |
|
993 fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs = |
|
994 EVERY' [rtac @{thm congruentI}, dtac lsbisE, |
|
995 REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans), |
|
996 etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans), |
|
997 rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl, |
|
998 EVERY' (map (fn equiv_LSBIS => |
|
999 EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac @{thm set_mp}, atac]) |
|
1000 equiv_LSBISs), rtac sym, rtac (o_apply RS trans), |
|
1001 etac (sym RS arg_cong RS trans), rtac map_comp_id] 1; |
|
1002 |
|
1003 fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss = |
|
1004 EVERY' [stac coalg_def, |
|
1005 CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) => |
|
1006 EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final, |
|
1007 rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI, |
|
1008 EVERY' (map2 (fn set_natural => fn coalgT_set => |
|
1009 EVERY' [rtac conjI, rtac (set_natural RS @{thm ord_eq_le_trans}), |
|
1010 rtac @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]}, |
|
1011 etac coalgT_set]) |
|
1012 (take m set_naturals) (take m coalgT_sets)), |
|
1013 CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) => |
|
1014 EVERY' [rtac (set_natural RS @{thm ord_eq_le_trans}), |
|
1015 rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff}, |
|
1016 rtac equiv_LSBIS, etac @{thm set_rev_mp}, etac coalgT_set]) |
|
1017 (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))]) |
|
1018 ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1; |
|
1019 |
|
1020 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs = |
|
1021 EVERY' [stac mor_def, rtac conjI, |
|
1022 CONJ_WRAP' (fn equiv_LSBIS => |
|
1023 EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac]) |
|
1024 equiv_LSBISs, |
|
1025 CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) => |
|
1026 EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS, |
|
1027 rtac congruent_str_final, atac, rtac o_apply]) |
|
1028 (equiv_LSBISs ~~ congruent_str_finals)] 1; |
|
1029 |
|
1030 fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs |
|
1031 {context = ctxt, prems = _} = |
|
1032 Local_Defs.unfold_tac ctxt defs THEN |
|
1033 EVERY' [rtac conjI, |
|
1034 CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps, |
|
1035 CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) => |
|
1036 EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL, |
|
1037 EVERY' (map2 (fn Abs_inverse => fn coalg_final_set => |
|
1038 EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse, |
|
1039 etac @{thm set_rev_mp}, rtac coalg_final_set, rtac Rep]) |
|
1040 Abs_inverses (drop m coalg_final_sets))]) |
|
1041 (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1; |
|
1042 |
|
1043 fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} = |
|
1044 Local_Defs.unfold_tac ctxt defs THEN |
|
1045 EVERY' [rtac conjI, |
|
1046 CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses, |
|
1047 CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1; |
|
1048 |
|
1049 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs = |
|
1050 EVERY' [rtac @{thm ssubst[of _ _ "%x. x"]}, rtac mor_UNIV, |
|
1051 CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) => |
|
1052 EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans), |
|
1053 rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans), |
|
1054 rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans), |
|
1055 rtac (o_apply RS trans RS sym), rtac map_cong, |
|
1056 REPEAT_DETERM_N m o rtac refl, |
|
1057 EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)]) |
|
1058 ((Abs_inverses ~~ morEs) ~~ ((unf_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1; |
|
1059 |
|
1060 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final |
|
1061 sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = |
|
1062 let |
|
1063 val n = length Rep_injects; |
|
1064 in |
|
1065 EVERY' [rtac rev_mp, ftac (bis_def RS @{thm subst[of _ _ "%x. x"]}), |
|
1066 REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse, |
|
1067 rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg, |
|
1068 rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr}, |
|
1069 rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT, |
|
1070 rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT, |
|
1071 rtac mor_T_final, EVERY' (map (fn thm => rtac (thm RS @{thm relInvImage_Gr})) lsbis_incls), |
|
1072 rtac impI, |
|
1073 CONJ_WRAP' (fn (Rep_inject, (equiv_LSBIS , (incl_lsbis, lsbis_incl))) => |
|
1074 EVERY' [rtac subset_trans, rtac @{thm relInvImage_UNIV_relImage}, rtac subset_trans, |
|
1075 rtac @{thm relInvImage_mono}, rtac subset_trans, etac incl_lsbis, |
|
1076 rtac @{thm ord_eq_le_trans}, rtac @{thm sym[OF relImage_relInvImage]}, |
|
1077 rtac @{thm xt1(3)}, rtac @{thm Sigma_cong}, |
|
1078 rtac @{thm proj_image}, rtac @{thm proj_image}, rtac lsbis_incl, |
|
1079 rtac subset_trans, rtac @{thm relImage_mono}, rtac incl_lsbis, atac, |
|
1080 rtac @{thm relImage_proj}, rtac equiv_LSBIS, rtac @{thm relInvImage_diag}, |
|
1081 rtac Rep_inject]) |
|
1082 (Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1 |
|
1083 end; |
|
1084 |
|
1085 fun mk_unique_mor_tac raw_coinds bis = |
|
1086 CONJ_WRAP' (fn raw_coind => |
|
1087 EVERY' [rtac impI, rtac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), atac, |
|
1088 etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac]) |
|
1089 raw_coinds 1; |
|
1090 |
|
1091 fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs = |
|
1092 CONJ_WRAP' (fn (raw_coind, coiter_def) => |
|
1093 EVERY' [rtac ext, etac (bis RS raw_coind RS @{thm set_mp} RS @{thm IdD}), rtac mor, |
|
1094 rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans), |
|
1095 rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1; |
|
1096 |
|
1097 fun mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unfs |
|
1098 {context = ctxt, prems = _} = |
|
1099 Local_Defs.unfold_tac ctxt [fld_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply, |
|
1100 rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL, |
|
1101 EVERY' (map (fn thm => |
|
1102 rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_unfs), |
|
1103 rtac sym, rtac @{thm id_apply}] 1; |
|
1104 |
|
1105 fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} = |
|
1106 Local_Defs.unfold_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong), |
|
1107 rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong, |
|
1108 REPEAT_DETERM_N m o rtac refl, |
|
1109 EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1; |
|
1110 |
|
1111 fun mk_rel_coinduct_tac ks raw_coind bis_rel = |
|
1112 EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI, |
|
1113 CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, |
|
1114 CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI, |
|
1115 REPEAT_DETERM o etac allE, etac mp, etac CollectE, etac @{thm splitD}])) ks, |
|
1116 rtac impI, REPEAT_DETERM o etac conjE, |
|
1117 CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac @{thm set_mp}, |
|
1118 rtac CollectI, etac @{thm prod_caseI}])) ks] 1; |
|
1119 |
|
1120 fun mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids = |
|
1121 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts rel_coinduct), |
|
1122 EVERY' (map2 (fn rel_mono => fn rel_Id => |
|
1123 EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE, |
|
1124 etac disjE, etac mp, atac, hyp_subst_tac, rtac (rel_mono RS @{thm set_mp}), |
|
1125 REPEAT_DETERM_N m o rtac @{thm subset_refl}, |
|
1126 REPEAT_DETERM_N (length rel_monos) o rtac @{thm Id_subset}, |
|
1127 rtac (rel_Id RS equalityD2 RS @{thm set_mp}), rtac @{thm IdI}]) |
|
1128 rel_monos rel_Ids), |
|
1129 rtac impI, REPEAT_DETERM o etac conjE, |
|
1130 CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) rel_Ids] 1; |
|
1131 |
|
1132 fun mk_unf_coinduct_tac m ks raw_coind bis_def = |
|
1133 let |
|
1134 val n = length ks; |
|
1135 in |
|
1136 EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_def, rtac conjI, |
|
1137 CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks, |
|
1138 CONJ_WRAP' (fn i => EVERY' [select_prem_tac n (dtac asm_rl) i, REPEAT_DETERM o rtac allI, |
|
1139 rtac impI, REPEAT_DETERM o dtac @{thm meta_spec}, etac CollectE, etac @{thm meta_impE}, |
|
1140 atac, etac exE, etac conjE, etac conjE, rtac bexI, rtac conjI, |
|
1141 etac @{thm fst_conv[THEN subst]}, etac @{thm snd_conv[THEN subst]}, |
|
1142 rtac CollectI, REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}), |
|
1143 CONJ_WRAP' (fn i' => EVERY' [rtac subsetI, rtac CollectI, dtac (mk_conjunctN n i'), |
|
1144 REPEAT_DETERM o etac allE, etac mp, rtac @{thm ssubst_mem[OF pair_collapse]}, atac]) |
|
1145 ks]) |
|
1146 ks, |
|
1147 rtac impI, |
|
1148 CONJ_WRAP' (fn i => EVERY' [rtac impI, dtac (mk_conjunctN n i), |
|
1149 rtac @{thm subst[OF pair_in_Id_conv]}, etac @{thm set_mp}, |
|
1150 rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 |
|
1151 end; |
|
1152 |
|
1153 fun mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def bis_diag = |
|
1154 EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts unf_coinduct), |
|
1155 EVERY' (map (fn i => |
|
1156 EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp}, |
|
1157 atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag, |
|
1158 rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE, |
|
1159 etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE], |
|
1160 rtac exI, rtac conjI, etac conjI, atac, |
|
1161 CONJ_WRAP' (K (EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], |
|
1162 rtac disjI2, rtac @{thm diagE}, etac @{thm set_mp}, atac])) ks]) |
|
1163 ks), |
|
1164 rtac impI, REPEAT_DETERM o etac conjE, |
|
1165 CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1; |
|
1166 |
|
1167 fun mk_map_tac m n cT coiter map_comp' map_cong = |
|
1168 EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym), |
|
1169 rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong, |
|
1170 REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong), |
|
1171 REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), |
|
1172 rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1; |
|
1173 |
|
1174 fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss = |
|
1175 EVERY' [rtac hset_minimal, |
|
1176 REPEAT_DETERM_N n o rtac @{thm Un_upper1}, |
|
1177 REPEAT_DETERM_N n o |
|
1178 EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets => |
|
1179 EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnN n i), etac @{thm UN_I}, |
|
1180 etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE, |
|
1181 EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)]) |
|
1182 (1 upto n) set_hsets set_hset_hsetss)] 1; |
|
1183 |
|
1184 fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets = |
|
1185 EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset, |
|
1186 REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, |
|
1187 EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; |
|
1188 |
|
1189 fun mk_map_id_tac maps coiter_unique coiter_unf = |
|
1190 EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps), |
|
1191 rtac coiter_unf] 1; |
|
1192 |
|
1193 fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique = |
|
1194 EVERY' [rtac coiter_unique, |
|
1195 EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong => |
|
1196 EVERY' (map rtac |
|
1197 ([@{thm o_assoc} RS trans, |
|
1198 @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans, |
|
1199 @{thm o_assoc} RS trans RS sym, |
|
1200 @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans, |
|
1201 @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans, |
|
1202 @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans, |
|
1203 ext, o_apply RS trans, o_apply RS trans RS sym, map_cong] @ |
|
1204 replicate m (@{thm id_o} RS fun_cong) @ |
|
1205 replicate n (@{thm o_id} RS fun_cong)))) |
|
1206 maps map_comps map_congs)] 1; |
|
1207 |
|
1208 val o_apply_trans_sym = o_apply RS trans RS sym; |
|
1209 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym; |
|
1210 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; |
|
1211 |
|
1212 fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss |
|
1213 set_hset_hsetsss = |
|
1214 let |
|
1215 val n = length map_comp's; |
|
1216 val ks = 1 upto n; |
|
1217 in |
|
1218 EVERY' ([rtac rev_mp, |
|
1219 coinduct_tac] @ |
|
1220 maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets), |
|
1221 set_hset_hsetss) => |
|
1222 [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI, |
|
1223 rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong, |
|
1224 REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}), |
|
1225 REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym, |
|
1226 rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong, |
|
1227 EVERY' (maps (fn set_hset => |
|
1228 [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE, |
|
1229 REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), |
|
1230 REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym, |
|
1231 CONJ_WRAP' (fn (set_natural, set_hset_hsets) => |
|
1232 EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD}, |
|
1233 etac @{thm set_rev_mp}, rtac @{thm ord_eq_le_trans}, rtac set_natural, |
|
1234 rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE, |
|
1235 REPEAT_DETERM o etac conjE, |
|
1236 CONJ_WRAP' (fn set_hset_hset => |
|
1237 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets]) |
|
1238 (drop m set_naturals ~~ set_hset_hsetss)]) |
|
1239 (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~ |
|
1240 map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @ |
|
1241 [rtac impI, |
|
1242 CONJ_WRAP' (fn k => |
|
1243 EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI, |
|
1244 rtac conjI, rtac refl, rtac refl]) ks]) 1 |
|
1245 end |
|
1246 |
|
1247 fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} = |
|
1248 rtac coiter_unique 1 THEN |
|
1249 Local_Defs.unfold_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN |
|
1250 ALLGOALS (etac sym); |
|
1251 |
|
1252 fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss |
|
1253 {context = ctxt, prems = _} = |
|
1254 let |
|
1255 val n = length map_simps; |
|
1256 in |
|
1257 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
1258 REPEAT_DETERM o rtac allI, SELECT_GOAL (Local_Defs.unfold_tac ctxt rec_0s), |
|
1259 CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s, |
|
1260 REPEAT_DETERM o rtac allI, |
|
1261 CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY' |
|
1262 [SELECT_GOAL (Local_Defs.unfold_tac ctxt |
|
1263 (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), |
|
1264 rtac @{thm Un_cong}, rtac refl, |
|
1265 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) |
|
1266 (fn i => EVERY' [rtac @{thm UN_cong[OF refl]}, |
|
1267 REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)]) |
|
1268 (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1 |
|
1269 end; |
|
1270 |
|
1271 fun mk_set_natural_tac hset_def col_natural = |
|
1272 EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym, |
|
1273 (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans), |
|
1274 (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1; |
|
1275 |
|
1276 fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss = |
|
1277 let |
|
1278 val n = length rec_0s; |
|
1279 in |
|
1280 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
1281 REPEAT_DETERM o rtac allI, |
|
1282 CONJ_WRAP' (fn rec_0 => EVERY' (map rtac [@{thm ordIso_ordLeq_trans}, |
|
1283 @{thm card_of_ordIso_subst}, rec_0, @{thm Card_order_empty}, sbd_Card_order])) rec_0s, |
|
1284 REPEAT_DETERM o rtac allI, |
|
1285 CONJ_WRAP' (fn (rec_Suc, set_sbds) => EVERY' |
|
1286 [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac rec_Suc, |
|
1287 rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_sbds (j - 1)), |
|
1288 REPEAT_DETERM_N (n - 1) o rtac (sbd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), |
|
1289 EVERY' (map2 (fn i => fn set_sbd => EVERY' [rtac @{thm UNION_Cinfinite_bound}, |
|
1290 rtac set_sbd, rtac ballI, REPEAT_DETERM o etac allE, |
|
1291 etac (mk_conjunctN n i), rtac sbd_Cinfinite]) (1 upto n) (drop m set_sbds))]) |
|
1292 (rec_Sucs ~~ set_sbdss)] 1 |
|
1293 end; |
|
1294 |
|
1295 fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd = |
|
1296 EVERY' (map rtac [@{thm ordIso_ordLeq_trans}, @{thm card_of_ordIso_subst}, hset_def, |
|
1297 ctrans, @{thm UNION_Cinfinite_bound}, @{thm ordIso_ordLeq_trans}, @{thm card_of_nat}, |
|
1298 @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite, |
|
1299 ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1; |
|
1300 |
|
1301 fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets |
|
1302 sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg = |
|
1303 let |
|
1304 val n = length isNode_hsets; |
|
1305 val in_hin_tac = rtac CollectI THEN' |
|
1306 CONJ_WRAP' (fn mor_hset => EVERY' (map etac |
|
1307 [mor_hset OF [coalgT, mor_T_final] RS sym RS @{thm ord_eq_le_trans}, |
|
1308 arg_cong RS sym RS @{thm ord_eq_le_trans}, |
|
1309 mor_hset OF [tcoalg, mor_Rep, UNIV_I] RS @{thm ord_eq_le_trans}])) mor_hsets; |
|
1310 in |
|
1311 EVERY' [rtac (Thm.permute_prems 0 1 @{thm ordLeq_transitive}), rtac ctrans, |
|
1312 rtac @{thm card_of_image}, rtac @{thm ordIso_ordLeq_trans}, |
|
1313 rtac @{thm card_of_ordIso_subst}, rtac @{thm sym[OF proj_image]}, rtac ctrans, |
|
1314 rtac @{thm card_of_image}, rtac ctrans, rtac card_of_carT, rtac @{thm cexp_mono2_Cnotzero}, |
|
1315 rtac @{thm cexp_ordLeq_ccexp}, rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, |
|
1316 rtac @{thm Cnotzero_cexp}, rtac sbd_Cnotzero, rtac sbd_Card_order, |
|
1317 rtac @{thm card_of_mono1}, rtac subsetI, rtac @{thm image_eqI}, rtac sym, |
|
1318 rtac Rep_inverse, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
1319 rtac @{thm set_mp}, rtac equalityD2, rtac @{thm sym[OF proj_image]}, rtac imageE, |
|
1320 rtac @{thm set_rev_mp}, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2, |
|
1321 rtac @{thm proj_image}, rtac @{thm image_eqI}, atac, |
|
1322 ftac (carT_def RS equalityD1 RS @{thm set_mp}), |
|
1323 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
|
1324 rtac (carT_def RS equalityD2 RS @{thm set_mp}), rtac CollectI, REPEAT_DETERM o rtac exI, |
|
1325 rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI, |
|
1326 rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI, |
|
1327 CONJ_WRAP_GEN' (etac disjE) (fn (i, isNode_hset) => |
|
1328 EVERY' [rtac (mk_disjIN n i), rtac isNode_hset, atac, atac, atac, in_hin_tac]) |
|
1329 (1 upto n ~~ isNode_hsets), |
|
1330 CONJ_WRAP' (fn isNode_hset => |
|
1331 EVERY' [rtac ballI, rtac isNode_hset, atac, ftac CollectD, etac @{thm SuccD}, |
|
1332 etac bspec, atac, in_hin_tac]) |
|
1333 isNode_hsets, |
|
1334 atac, rtac isNode_hset, atac, atac, atac, in_hin_tac] 1 |
|
1335 end; |
|
1336 |
|
1337 fun mk_bd_card_order_tac sbd_card_order = |
|
1338 EVERY' (map rtac [@{thm card_order_ccexp}, sbd_card_order, sbd_card_order]) 1; |
|
1339 |
|
1340 fun mk_bd_cinfinite_tac sbd_Cinfinite = |
|
1341 EVERY' (map rtac [@{thm cinfinite_ccexp}, @{thm ctwo_ordLeq_Cinfinite}, |
|
1342 sbd_Cinfinite, sbd_Cinfinite]) 1; |
|
1343 |
|
1344 fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq = |
|
1345 let |
|
1346 val m = length set_incl_hsets; |
|
1347 in |
|
1348 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
|
1349 EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets), |
|
1350 CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins, |
|
1351 REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, |
|
1352 EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets), |
|
1353 CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins, |
|
1354 REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq] |
|
1355 end; |
|
1356 |
|
1357 fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs |
|
1358 {context = ctxt, prems = _} = |
|
1359 Local_Defs.unfold_tac ctxt [coalg_def] THEN |
|
1360 CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) => |
|
1361 EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, |
|
1362 REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], |
|
1363 hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), |
|
1364 EVERY' (map (etac o mk_conjunctN m) (1 upto m)), |
|
1365 pickWP_assms_tac, |
|
1366 SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), rtac impI, |
|
1367 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
1368 rtac CollectI, |
|
1369 REPEAT_DETERM_N m o (rtac conjI THEN' rtac @{thm subset_UNIV}), |
|
1370 CONJ_WRAP' (fn set_natural => |
|
1371 EVERY' [rtac @{thm ord_eq_le_trans}, rtac trans, rtac set_natural, |
|
1372 rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, atac]) |
|
1373 (drop m set_naturals)]) |
|
1374 (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1; |
|
1375 |
|
1376 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs |
|
1377 {context = ctxt, prems = _} = |
|
1378 let |
|
1379 val n = length map_comps; |
|
1380 in |
|
1381 Local_Defs.unfold_tac ctxt [mor_def] THEN |
|
1382 EVERY' [rtac conjI, |
|
1383 CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n), |
|
1384 CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) => |
|
1385 EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, |
|
1386 REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], |
|
1387 hyp_subst_tac, |
|
1388 SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms o_apply prod.cases}), |
|
1389 rtac (map_comp RS trans), |
|
1390 SELECT_GOAL (Local_Defs.unfold_tac ctxt (conv :: @{thms o_id id_o})), |
|
1391 rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac, |
|
1392 pickWP_assms_tac]) |
|
1393 (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1 |
|
1394 end; |
|
1395 |
|
1396 val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)}; |
|
1397 val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)}; |
|
1398 |
|
1399 fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} = |
|
1400 Local_Defs.unfold_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN |
|
1401 CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN |
|
1402 CONJ_WRAP' (fn (coiter, map_comp) => |
|
1403 EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE], |
|
1404 hyp_subst_tac, |
|
1405 SELECT_GOAL (Local_Defs.unfold_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})), |
|
1406 rtac refl]) |
|
1407 (coiters ~~ map_comps) 1; |
|
1408 |
|
1409 fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs |
|
1410 {context = ctxt, prems = _} = |
|
1411 let |
|
1412 val n = length rec_0s; |
|
1413 val ks = n downto 1; |
|
1414 in |
|
1415 EVERY' [rtac (Drule.instantiate' [] cts @{thm nat_induct}), |
|
1416 REPEAT_DETERM o rtac allI, |
|
1417 CONJ_WRAP' (fn thm => EVERY' |
|
1418 [rtac impI, rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm empty_subsetI}]) rec_0s, |
|
1419 REPEAT_DETERM o rtac allI, |
|
1420 CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) => |
|
1421 EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]}, |
|
1422 REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}], |
|
1423 hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}), |
|
1424 EVERY' (map (etac o mk_conjunctN m) (1 upto m)), |
|
1425 pickWP_assms_tac, |
|
1426 rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
|
1427 rtac @{thm ord_eq_le_trans}, rtac rec_Suc, |
|
1428 rtac @{thm Un_least}, |
|
1429 SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, nth set_naturals (j - 1), |
|
1430 @{thm prod.cases}]), |
|
1431 etac @{thm ord_eq_le_trans[OF trans [OF fun_cong[OF image_id] id_apply]]}, |
|
1432 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) => |
|
1433 EVERY' [rtac @{thm UN_least}, |
|
1434 SELECT_GOAL (Local_Defs.unfold_tac ctxt [coiter, set_natural, @{thm prod.cases}]), |
|
1435 etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE, |
|
1436 dtac (mk_conjunctN n i), etac mp, etac @{thm set_mp}, atac]) |
|
1437 (ks ~~ rev (drop m set_naturals))]) |
|
1438 (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 |
|
1439 end; |
|
1440 |
|
1441 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick |
|
1442 mor_unique pick_cols hset_defs = |
|
1443 EVERY' [rtac @{thm ssubst[of _ _ "%x. x", OF wpull_def]}, REPEAT_DETERM o rtac allI, rtac impI, |
|
1444 REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI, |
|
1445 rtac box_equals, rtac mor_unique, |
|
1446 rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1447 rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1448 rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1449 rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, |
|
1450 rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv}, |
|
1451 rtac box_equals, rtac mor_unique, |
|
1452 rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1453 rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1454 rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1455 rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, |
|
1456 rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv}, |
|
1457 rtac CollectI, |
|
1458 CONJ_WRAP' (fn (pick, def) => |
|
1459 EVERY' [rtac (def RS @{thm ord_eq_le_trans}), rtac @{thm UN_least}, |
|
1460 rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
|
1461 rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI, |
|
1462 rtac @{thm prod_caseI}, etac conjI, etac conjI, atac]) |
|
1463 (pick_cols ~~ hset_defs)] 1; |
|
1464 |
|
1465 fun mk_wit_tac n unf_flds set_simp wit {context = ctxt, prems = _} = |
|
1466 REPEAT_DETERM (atac 1 ORELSE |
|
1467 EVERY' [dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp, |
|
1468 K (Local_Defs.unfold_tac ctxt unf_flds), |
|
1469 REPEAT_DETERM_N n o etac UnE, |
|
1470 REPEAT_DETERM o |
|
1471 (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN' |
|
1472 (eresolve_tac wit ORELSE' |
|
1473 (dresolve_tac wit THEN' |
|
1474 (etac FalseE ORELSE' |
|
1475 EVERY' [hyp_subst_tac, dtac @{thm set_rev_mp}, rtac equalityD1, resolve_tac set_simp, |
|
1476 K (Local_Defs.unfold_tac ctxt unf_flds), REPEAT_DETERM_N n o etac UnE]))))] 1); |
|
1477 |
|
1478 fun mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld |
|
1479 set_naturals set_incls set_set_inclss = |
|
1480 let |
|
1481 val m = length set_incls; |
|
1482 val n = length set_set_inclss; |
|
1483 val (passive_set_naturals, active_set_naturals) = chop m set_naturals; |
|
1484 val in_Jrel = nth in_Jrels (i - 1); |
|
1485 val if_tac = |
|
1486 EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], |
|
1487 rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
|
1488 EVERY' (map2 (fn set_natural => fn set_incl => |
|
1489 EVERY' [rtac conjI, rtac @{thm ord_eq_le_trans}, rtac set_natural, |
|
1490 rtac @{thm ord_eq_le_trans}, rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, |
|
1491 etac (set_incl RS @{thm subset_trans})]) |
|
1492 passive_set_naturals set_incls), |
|
1493 CONJ_WRAP' (fn (in_Jrel, (set_natural, set_set_incls)) => |
|
1494 EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_natural, rtac @{thm image_subsetI}, |
|
1495 rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
|
1496 CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls, |
|
1497 rtac conjI, rtac refl, rtac refl]) |
|
1498 (in_Jrels ~~ (active_set_naturals ~~ set_set_inclss)), |
|
1499 CONJ_WRAP' (fn conv => |
|
1500 EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, |
|
1501 REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
|
1502 REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), |
|
1503 rtac trans, rtac sym, rtac map_simp, rtac (unf_inject RS iffD2), atac]) |
|
1504 @{thms fst_conv snd_conv}]; |
|
1505 val only_if_tac = |
|
1506 EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], |
|
1507 rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
|
1508 CONJ_WRAP' (fn (set_simp, passive_set_natural) => |
|
1509 EVERY' [rtac @{thm ord_eq_le_trans}, rtac set_simp, rtac @{thm Un_least}, |
|
1510 rtac @{thm ord_eq_le_trans}, rtac box_equals, rtac passive_set_natural, |
|
1511 rtac (unf_fld RS sym RS arg_cong), rtac @{thm trans[OF fun_cong[OF image_id] id_apply]}, |
|
1512 atac, |
|
1513 CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) |
|
1514 (fn (active_set_natural, in_Jrel) => EVERY' [rtac @{thm ord_eq_le_trans}, |
|
1515 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]}, |
|
1516 rtac active_set_natural, rtac (unf_fld RS sym RS arg_cong), rtac @{thm UN_least}, |
|
1517 dtac @{thm set_rev_mp}, etac @{thm image_mono}, etac imageE, |
|
1518 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), |
|
1519 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, |
|
1520 dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, |
|
1521 hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac]) |
|
1522 (rev (active_set_naturals ~~ in_Jrels))]) |
|
1523 (set_simps ~~ passive_set_naturals), |
|
1524 rtac conjI, |
|
1525 REPEAT_DETERM_N 2 o EVERY'[rtac (unf_inject RS iffD1), rtac trans, rtac map_simp, |
|
1526 rtac box_equals, rtac map_comp, rtac (unf_fld RS sym RS arg_cong), rtac trans, |
|
1527 rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
|
1528 EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac @{thm set_rev_mp}, atac, |
|
1529 dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jrel RS iffD1), dtac @{thm someI_ex}, |
|
1530 REPEAT_DETERM o etac conjE, atac]) in_Jrels), |
|
1531 atac]] |
|
1532 in |
|
1533 EVERY' [rtac iffI, if_tac, only_if_tac] 1 |
|
1534 end; |
|
1535 |
|
1536 end; |