changeset 49305 | 8241f21d104b |
parent 49304 | 6964373dd6ac |
child 49463 | 83ac281bcdc2 |
49304:6964373dd6ac | 49305:8241f21d104b |
---|---|
42 struct |
42 struct |
43 |
43 |
44 open BNF_Util |
44 open BNF_Util |
45 open BNF_Tactics |
45 open BNF_Tactics |
46 |
46 |
47 val Card_order_csum = @{thm Card_order_csum}; |
|
48 val Card_order_ctwo = @{thm Card_order_ctwo}; |
|
49 val Cnotzero_UNIV = @{thm Cnotzero_UNIV}; |
|
47 val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
50 val arg_cong_Union = @{thm arg_cong[of _ _ Union]}; |
51 val card_of_Card_order = @{thm card_of_Card_order}; |
|
52 val csum_Cnotzero1 = @{thm csum_Cnotzero1}; |
|
53 val csum_Cnotzero2 = @{thm csum_Cnotzero2}; |
|
54 val ctwo_Cnotzero = @{thm ctwo_Cnotzero}; |
|
48 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
55 val o_eq_dest_lhs = @{thm o_eq_dest_lhs}; |
56 val ordIso_transitive = @{thm ordIso_transitive}; |
|
57 val ordLeq_csum2 = @{thm ordLeq_csum2}; |
|
49 val set_mp = @{thm set_mp}; |
58 val set_mp = @{thm set_mp}; |
59 val subset_UNIV = @{thm subset_UNIV}; |
|
50 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
60 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]}; |
51 val trans_o_apply = @{thm trans[OF o_apply]}; |
61 val trans_o_apply = @{thm trans[OF o_apply]}; |
52 |
62 |
53 |
63 |
54 |
64 |
78 rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
88 rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, |
79 rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
89 rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, |
80 rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
90 rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ |
81 [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]}, |
91 [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]}, |
82 rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
92 rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply, |
83 rtac @{thm trans[OF image_cong[OF o_apply refl]]}, rtac @{thm trans[OF image_image]}, |
93 rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]}, |
84 rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
94 rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}], |
85 rtac @{thm image_empty}]) 1; |
95 rtac @{thm image_empty}]) 1; |
86 |
96 |
87 fun mk_comp_map_cong_tac comp_set_alts map_cong map_congs = |
97 fun mk_comp_map_cong_tac comp_set_alts map_cong map_congs = |
88 let |
98 let |
150 REPEAT_DETERM ( |
160 REPEAT_DETERM ( |
151 rtac @{thm subsetI} 1 THEN |
161 rtac @{thm subsetI} 1 THEN |
152 Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN |
162 Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN |
153 (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
163 (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
154 REPEAT_DETERM (CHANGED (( |
164 REPEAT_DETERM (CHANGED (( |
155 (rtac conjI THEN' (atac ORELSE' rtac @{thm subset_UNIV})) ORELSE' |
165 (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE' |
156 atac ORELSE' |
166 atac ORELSE' |
157 (rtac @{thm subset_UNIV})) 1)) ORELSE rtac @{thm subset_UNIV} 1)); |
167 (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1)); |
158 |
168 |
159 fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order = |
169 fun mk_comp_in_bd_tac comp_in_alt Fin_bds Gin_bd Fbd_Cinfs Gbd_Card_order = |
160 let |
170 let |
161 val (bds, last_bd) = split_last Fin_bds; |
171 val (bds, last_bd) = split_last Fin_bds; |
162 val (Cinfs, _) = split_last Fbd_Cinfs; |
172 val (Cinfs, _) = split_last Fbd_Cinfs; |
164 fun gen_after (_, (bd_Cinf, next_bd_Cinf)) = |
174 fun gen_after (_, (bd_Cinf, next_bd_Cinf)) = |
165 TRY o (rtac @{thm csum_cexp} THEN' |
175 TRY o (rtac @{thm csum_cexp} THEN' |
166 rtac bd_Cinf THEN' |
176 rtac bd_Cinf THEN' |
167 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE' |
177 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac next_bd_Cinf ORELSE' |
168 rtac next_bd_Cinf) THEN' |
178 rtac next_bd_Cinf) THEN' |
169 ((rtac @{thm Card_order_csum} THEN' rtac @{thm ordLeq_csum2}) ORELSE' |
179 ((rtac Card_order_csum THEN' rtac ordLeq_csum2) ORELSE' |
170 (rtac @{thm Card_order_ctwo} THEN' rtac @{thm ordLeq_refl})) THEN' |
180 (rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl})) THEN' |
171 rtac @{thm Card_order_ctwo}); |
181 rtac Card_order_ctwo); |
172 in |
182 in |
173 (rtac @{thm ordIso_ordLeq_trans} THEN' |
183 (rtac @{thm ordIso_ordLeq_trans} THEN' |
174 rtac @{thm card_of_ordIso_subst} THEN' |
184 rtac @{thm card_of_ordIso_subst} THEN' |
175 rtac comp_in_alt THEN' |
185 rtac comp_in_alt THEN' |
176 rtac ctrans THEN' |
186 rtac ctrans THEN' |
180 rtac @{thm ordLeq_ordIso_trans} THEN' |
190 rtac @{thm ordLeq_ordIso_trans} THEN' |
181 rtac @{thm csum_mono1} THEN' |
191 rtac @{thm csum_mono1} THEN' |
182 WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN' |
192 WRAP' gen_before gen_after (bds ~~ (Cinfs ~~ tl Fbd_Cinfs)) (rtac last_bd) THEN' |
183 rtac @{thm csum_absorb1} THEN' |
193 rtac @{thm csum_absorb1} THEN' |
184 rtac @{thm Cinfinite_cexp} THEN' |
194 rtac @{thm Cinfinite_cexp} THEN' |
185 (rtac @{thm ordLeq_csum2} ORELSE' rtac @{thm ordLeq_refl}) THEN' |
195 (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN' |
186 rtac @{thm Card_order_ctwo} THEN' |
196 rtac Card_order_ctwo THEN' |
187 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
197 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
188 rtac (hd Fbd_Cinfs)) THEN' |
198 rtac (hd Fbd_Cinfs)) THEN' |
189 rtac @{thm ctwo_ordLeq_Cinfinite} THEN' |
199 rtac @{thm ctwo_ordLeq_Cinfinite} THEN' |
190 rtac @{thm Cinfinite_cexp} THEN' |
200 rtac @{thm Cinfinite_cexp} THEN' |
191 (rtac @{thm ordLeq_csum2} ORELSE' rtac @{thm ordLeq_refl}) THEN' |
201 (rtac ordLeq_csum2 ORELSE' rtac @{thm ordLeq_refl}) THEN' |
192 rtac @{thm Card_order_ctwo} THEN' |
202 rtac Card_order_ctwo THEN' |
193 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
203 (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE' |
194 rtac (hd Fbd_Cinfs)) THEN' |
204 rtac (hd Fbd_Cinfs)) THEN' |
195 rtac disjI1 THEN' |
205 rtac disjI1 THEN' |
196 TRY o rtac @{thm csum_Cnotzero2} THEN' |
206 TRY o rtac csum_Cnotzero2 THEN' |
197 rtac @{thm ctwo_Cnotzero} THEN' |
207 rtac ctwo_Cnotzero THEN' |
198 rtac Gbd_Card_order THEN' |
208 rtac Gbd_Card_order THEN' |
199 rtac @{thm cexp_cprod} THEN' |
209 rtac @{thm cexp_cprod} THEN' |
200 TRY o rtac @{thm csum_Cnotzero2} THEN' |
210 TRY o rtac csum_Cnotzero2 THEN' |
201 rtac @{thm ctwo_Cnotzero}) 1 |
211 rtac ctwo_Cnotzero) 1 |
202 end; |
212 end; |
203 |
213 |
204 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def |
214 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def |
205 Union_image_insert Union_image_empty}; |
215 Union_image_insert Union_image_empty}; |
206 |
216 |
232 rtac @{thm card_of_card_order_on} THEN' |
242 rtac @{thm card_of_card_order_on} THEN' |
233 rtac bd_card_order) 1; |
243 rtac bd_card_order) 1; |
234 |
244 |
235 fun mk_kill_bd_cinfinite_tac bd_Cinfinite = |
245 fun mk_kill_bd_cinfinite_tac bd_Cinfinite = |
236 (rtac @{thm cinfinite_cprod2} THEN' |
246 (rtac @{thm cinfinite_cprod2} THEN' |
237 TRY o rtac @{thm csum_Cnotzero1} THEN' |
247 TRY o rtac csum_Cnotzero1 THEN' |
238 rtac @{thm Cnotzero_UNIV} THEN' |
248 rtac Cnotzero_UNIV THEN' |
239 rtac bd_Cinfinite) 1; |
249 rtac bd_Cinfinite) 1; |
240 |
250 |
241 fun mk_kill_set_bd_tac bd_Card_order set_bd = |
251 fun mk_kill_set_bd_tac bd_Card_order set_bd = |
242 (rtac ctrans THEN' |
252 (rtac ctrans THEN' |
243 rtac set_bd THEN' |
253 rtac set_bd THEN' |
244 rtac @{thm ordLeq_cprod2} THEN' |
254 rtac @{thm ordLeq_cprod2} THEN' |
245 TRY o rtac @{thm csum_Cnotzero1} THEN' |
255 TRY o rtac csum_Cnotzero1 THEN' |
246 rtac @{thm Cnotzero_UNIV} THEN' |
256 rtac Cnotzero_UNIV THEN' |
247 rtac bd_Card_order) 1 |
257 rtac bd_Card_order) 1 |
248 |
258 |
249 val kill_in_alt_tac = |
259 val kill_in_alt_tac = |
250 ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN |
260 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
251 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
261 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
252 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
262 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
253 rtac conjI THEN' rtac @{thm subset_UNIV}) 1)) THEN |
263 rtac conjI THEN' rtac subset_UNIV) 1)) THEN |
254 (rtac @{thm subset_UNIV} ORELSE' atac) 1 THEN |
264 (rtac subset_UNIV ORELSE' atac) 1 THEN |
255 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
265 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
256 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE |
266 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE |
257 ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
267 ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN |
258 REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm subset_UNIV} 1)); |
268 REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1)); |
259 |
269 |
260 fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero = |
270 fun mk_kill_in_bd_tac n nontrivial_kill_in in_alt in_bd bd_Card_order bd_Cinfinite bd_Cnotzero = |
261 (rtac @{thm ordIso_ordLeq_trans} THEN' |
271 (rtac @{thm ordIso_ordLeq_trans} THEN' |
262 rtac @{thm card_of_ordIso_subst} THEN' |
272 rtac @{thm card_of_ordIso_subst} THEN' |
263 rtac in_alt THEN' |
273 rtac in_alt THEN' |
264 rtac ctrans THEN' |
274 rtac ctrans THEN' |
265 rtac in_bd THEN' |
275 rtac in_bd THEN' |
266 rtac @{thm ordIso_ordLeq_trans} THEN' |
276 rtac @{thm ordIso_ordLeq_trans} THEN' |
267 rtac @{thm cexp_cong1}) 1 THEN |
277 rtac @{thm cexp_cong1}) 1 THEN |
268 (if nontrivial_kill_in then |
278 (if nontrivial_kill_in then |
269 rtac @{thm ordIso_transitive} 1 THEN |
279 rtac ordIso_transitive 1 THEN |
270 REPEAT_DETERM_N (n - 1) |
280 REPEAT_DETERM_N (n - 1) |
271 ((rtac @{thm csum_cong1} THEN' |
281 ((rtac @{thm csum_cong1} THEN' |
272 rtac @{thm ordIso_symmetric} THEN' |
282 rtac @{thm ordIso_symmetric} THEN' |
273 rtac @{thm csum_assoc} THEN' |
283 rtac @{thm csum_assoc} THEN' |
274 rtac @{thm ordIso_transitive}) 1) THEN |
284 rtac ordIso_transitive) 1) THEN |
275 (rtac @{thm ordIso_refl} THEN' |
285 (rtac @{thm ordIso_refl} THEN' |
276 rtac @{thm Card_order_csum} THEN' |
286 rtac Card_order_csum THEN' |
277 rtac @{thm ordIso_transitive} THEN' |
287 rtac ordIso_transitive THEN' |
278 rtac @{thm csum_assoc} THEN' |
288 rtac @{thm csum_assoc} THEN' |
279 rtac @{thm ordIso_transitive} THEN' |
289 rtac ordIso_transitive THEN' |
280 rtac @{thm csum_cong1} THEN' |
290 rtac @{thm csum_cong1} THEN' |
281 K (mk_flatten_assoc_tac |
291 K (mk_flatten_assoc_tac |
282 (rtac @{thm ordIso_refl} THEN' |
292 (rtac @{thm ordIso_refl} THEN' |
283 FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}]) |
293 FIRST' [rtac card_of_Card_order, rtac Card_order_csum]) |
284 @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_cong}) THEN' |
294 ordIso_transitive @{thm csum_assoc} @{thm csum_cong}) THEN' |
285 rtac @{thm ordIso_refl} THEN' |
295 rtac @{thm ordIso_refl} THEN' |
286 (rtac @{thm card_of_Card_order} ORELSE' rtac @{thm Card_order_csum})) 1 |
296 (rtac card_of_Card_order ORELSE' rtac Card_order_csum)) 1 |
287 else all_tac) THEN |
297 else all_tac) THEN |
288 (rtac @{thm csum_com} THEN' |
298 (rtac @{thm csum_com} THEN' |
289 rtac bd_Card_order THEN' |
299 rtac bd_Card_order THEN' |
290 rtac disjI1 THEN' |
300 rtac disjI1 THEN' |
291 rtac @{thm csum_Cnotzero2} THEN' |
301 rtac csum_Cnotzero2 THEN' |
292 rtac @{thm ctwo_Cnotzero} THEN' |
302 rtac ctwo_Cnotzero THEN' |
293 rtac disjI1 THEN' |
303 rtac disjI1 THEN' |
294 rtac @{thm csum_Cnotzero2} THEN' |
304 rtac csum_Cnotzero2 THEN' |
295 TRY o rtac @{thm csum_Cnotzero1} THEN' |
305 TRY o rtac csum_Cnotzero1 THEN' |
296 rtac @{thm Cnotzero_UNIV} THEN' |
306 rtac Cnotzero_UNIV THEN' |
297 rtac @{thm ordLeq_ordIso_trans} THEN' |
307 rtac @{thm ordLeq_ordIso_trans} THEN' |
298 rtac @{thm cexp_mono1} THEN' |
308 rtac @{thm cexp_mono1} THEN' |
299 rtac ctrans THEN' |
309 rtac ctrans THEN' |
300 rtac @{thm csum_mono2} THEN' |
310 rtac @{thm csum_mono2} THEN' |
301 rtac @{thm ordLeq_cprod1} THEN' |
311 rtac @{thm ordLeq_cprod1} THEN' |
302 (rtac @{thm card_of_Card_order} ORELSE' rtac @{thm Card_order_csum}) THEN' |
312 (rtac card_of_Card_order ORELSE' rtac Card_order_csum) THEN' |
303 rtac bd_Cnotzero THEN' |
313 rtac bd_Cnotzero THEN' |
304 rtac @{thm csum_cexp'} THEN' |
314 rtac @{thm csum_cexp'} THEN' |
305 rtac @{thm Cinfinite_cprod2} THEN' |
315 rtac @{thm Cinfinite_cprod2} THEN' |
306 TRY o rtac @{thm csum_Cnotzero1} THEN' |
316 TRY o rtac csum_Cnotzero1 THEN' |
307 rtac @{thm Cnotzero_UNIV} THEN' |
317 rtac Cnotzero_UNIV THEN' |
308 rtac bd_Cinfinite THEN' |
318 rtac bd_Cinfinite THEN' |
309 ((rtac @{thm Card_order_ctwo} THEN' rtac @{thm ordLeq_refl}) ORELSE' |
319 ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE' |
310 (rtac @{thm Card_order_csum} THEN' rtac @{thm ordLeq_csum2})) THEN' |
320 (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN' |
311 rtac @{thm Card_order_ctwo} THEN' |
321 rtac Card_order_ctwo THEN' |
312 rtac disjI1 THEN' |
322 rtac disjI1 THEN' |
313 rtac @{thm csum_Cnotzero2} THEN' |
323 rtac csum_Cnotzero2 THEN' |
314 TRY o rtac @{thm csum_Cnotzero1} THEN' |
324 TRY o rtac csum_Cnotzero1 THEN' |
315 rtac @{thm Cnotzero_UNIV} THEN' |
325 rtac Cnotzero_UNIV THEN' |
316 rtac bd_Card_order THEN' |
326 rtac bd_Card_order THEN' |
317 rtac @{thm cexp_cprod_ordLeq} THEN' |
327 rtac @{thm cexp_cprod_ordLeq} THEN' |
318 TRY o rtac @{thm csum_Cnotzero2} THEN' |
328 TRY o rtac csum_Cnotzero2 THEN' |
319 rtac @{thm ctwo_Cnotzero} THEN' |
329 rtac ctwo_Cnotzero THEN' |
320 rtac @{thm Cinfinite_cprod2} THEN' |
330 rtac @{thm Cinfinite_cprod2} THEN' |
321 TRY o rtac @{thm csum_Cnotzero1} THEN' |
331 TRY o rtac csum_Cnotzero1 THEN' |
322 rtac @{thm Cnotzero_UNIV} THEN' |
332 rtac Cnotzero_UNIV THEN' |
323 rtac bd_Cinfinite THEN' |
333 rtac bd_Cinfinite THEN' |
324 rtac bd_Cnotzero THEN' |
334 rtac bd_Cnotzero THEN' |
325 rtac @{thm ordLeq_cprod2} THEN' |
335 rtac @{thm ordLeq_cprod2} THEN' |
326 TRY o rtac @{thm csum_Cnotzero1} THEN' |
336 TRY o rtac csum_Cnotzero1 THEN' |
327 rtac @{thm Cnotzero_UNIV} THEN' |
337 rtac Cnotzero_UNIV THEN' |
328 rtac bd_Card_order) 1; |
338 rtac bd_Card_order) 1; |
329 |
339 |
330 |
340 |
331 |
341 |
332 (* Lift operation *) |
342 (* Lift operation *) |
334 val empty_natural_tac = rtac @{thm empty_natural} 1; |
344 val empty_natural_tac = rtac @{thm empty_natural} 1; |
335 |
345 |
336 fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1; |
346 fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1; |
337 |
347 |
338 val lift_in_alt_tac = |
348 val lift_in_alt_tac = |
339 ((rtac @{thm Collect_cong} THEN' rtac @{thm iffI}) 1 THEN |
349 ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN |
340 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
350 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
341 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN |
351 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN |
342 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
352 REPEAT_DETERM (CHANGED (etac conjE 1)) THEN |
343 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
353 REPEAT_DETERM (CHANGED ((etac conjI ORELSE' |
344 rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN |
354 rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN |
354 rtac in_bd THEN' |
364 rtac in_bd THEN' |
355 rtac @{thm cexp_mono1}) 1 THEN |
365 rtac @{thm cexp_mono1}) 1 THEN |
356 ((rtac @{thm csum_mono1} 1 THEN |
366 ((rtac @{thm csum_mono1} 1 THEN |
357 REPEAT_DETERM_N (n - 1) |
367 REPEAT_DETERM_N (n - 1) |
358 ((rtac ctrans THEN' |
368 ((rtac ctrans THEN' |
359 rtac @{thm ordLeq_csum2} THEN' |
369 rtac ordLeq_csum2 THEN' |
360 (rtac @{thm Card_order_csum} ORELSE' rtac @{thm card_of_Card_order})) 1) THEN |
370 (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) THEN |
361 (rtac @{thm ordLeq_csum2} THEN' |
371 (rtac ordLeq_csum2 THEN' |
362 (rtac @{thm Card_order_csum} ORELSE' rtac @{thm card_of_Card_order})) 1) ORELSE |
372 (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE |
363 (rtac @{thm ordLeq_csum2} THEN' rtac @{thm Card_order_ctwo}) 1) THEN |
373 (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN |
364 (rtac disjI1 THEN' TRY o rtac @{thm csum_Cnotzero2} THEN' rtac @{thm ctwo_Cnotzero} |
374 (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero |
365 THEN' rtac bd_Card_order) 1; |
375 THEN' rtac bd_Card_order) 1; |
366 |
376 |
367 |
377 |
368 |
378 |
369 (* Permute operation *) |
379 (* Permute operation *) |
381 rtac in_bd THEN' |
391 rtac in_bd THEN' |
382 rtac @{thm cexp_cong1} THEN' |
392 rtac @{thm cexp_cong1} THEN' |
383 rtac @{thm csum_cong1} THEN' |
393 rtac @{thm csum_cong1} THEN' |
384 mk_rotate_eq_tac |
394 mk_rotate_eq_tac |
385 (rtac @{thm ordIso_refl} THEN' |
395 (rtac @{thm ordIso_refl} THEN' |
386 FIRST' [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}]) |
396 FIRST' [rtac card_of_Card_order, rtac Card_order_csum]) |
387 @{thm ordIso_transitive} @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
397 ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong} |
388 src dest THEN' |
398 src dest THEN' |
389 rtac bd_Card_order THEN' |
399 rtac bd_Card_order THEN' |
390 rtac disjI1 THEN' |
400 rtac disjI1 THEN' |
391 TRY o rtac @{thm csum_Cnotzero2} THEN' |
401 TRY o rtac csum_Cnotzero2 THEN' |
392 rtac @{thm ctwo_Cnotzero} THEN' |
402 rtac ctwo_Cnotzero THEN' |
393 rtac disjI1 THEN' |
403 rtac disjI1 THEN' |
394 TRY o rtac @{thm csum_Cnotzero2} THEN' |
404 TRY o rtac csum_Cnotzero2 THEN' |
395 rtac @{thm ctwo_Cnotzero}) 1; |
405 rtac ctwo_Cnotzero) 1; |
396 |
406 |
397 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = |
407 fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull = |
398 (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN |
408 (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN |
399 WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN |
409 WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN |
400 TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); |
410 TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1)); |