127 open BNF_Tactics |
127 open BNF_Tactics |
128 open BNF_Util |
128 open BNF_Util |
129 open BNF_FP |
129 open BNF_FP |
130 open BNF_GFP_Util |
130 open BNF_GFP_Util |
131 |
131 |
132 val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]}; |
|
133 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym; |
132 val fst_convol_fun_cong_sym = @{thm fst_convol} RS fun_cong RS sym; |
134 val list_inject_subst_id = @{thm list.inject[THEN subst, of "%x. x"]}; |
133 val list_inject_iffD1 = @{thm list.inject[THEN iffD1]}; |
135 val nat_induct = @{thm nat_induct}; |
134 val nat_induct = @{thm nat_induct}; |
136 val o_apply_trans_sym = o_apply RS trans RS sym; |
135 val o_apply_trans_sym = o_apply RS trans RS sym; |
137 val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
136 val ord_eq_le_trans = @{thm ord_eq_le_trans}; |
138 val ord_eq_le_trans_trans_fun_cong_image_id_id_apply = |
137 val ord_eq_le_trans_trans_fun_cong_image_id_id_apply = |
139 @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]}; |
138 @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]}; |
140 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans}; |
139 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans}; |
141 val set_mp = @{thm set_mp}; |
|
142 val set_rev_mp = @{thm set_rev_mp}; |
|
143 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; |
140 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; |
144 val ssubst_id = @{thm ssubst[of _ _ "%x. x"]}; |
|
145 val subst_id = @{thm subst[of _ _ "%x. x"]}; |
|
146 val sum_case_weak_cong = @{thm sum_case_weak_cong}; |
141 val sum_case_weak_cong = @{thm sum_case_weak_cong}; |
147 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; |
142 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; |
148 |
143 |
149 fun mk_coalg_set_tac coalg_def = |
144 fun mk_coalg_set_tac coalg_def = |
150 dtac (coalg_def RS subst_id) 1 THEN |
145 dtac (coalg_def RS iffD1) 1 THEN |
151 REPEAT_DETERM (etac conjE 1) THEN |
146 REPEAT_DETERM (etac conjE 1) THEN |
152 EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN |
147 EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN |
153 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1; |
148 REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1; |
154 |
149 |
155 fun mk_mor_elim_tac mor_def = |
150 fun mk_mor_elim_tac mor_def = |
289 EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, |
284 EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, |
290 etac allE, etac allE, etac impE, atac, |
285 etac allE, etac allE, etac impE, atac, |
291 dtac (rel_O_Gr RS equalityD1 RS set_mp), |
286 dtac (rel_O_Gr RS equalityD1 RS set_mp), |
292 REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
287 REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}], |
293 REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE], |
288 REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE], |
294 REPEAT_DETERM o dtac Pair_eq_subst_id, |
289 REPEAT_DETERM o dtac Pair_eqD, |
295 REPEAT_DETERM o etac conjE, |
290 REPEAT_DETERM o etac conjE, |
296 hyp_subst_tac, |
291 hyp_subst_tac, |
297 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
292 REPEAT_DETERM o eresolve_tac [CollectE, conjE], |
298 rtac bexI, rtac conjI, rtac trans, rtac map_comp, |
293 rtac bexI, rtac conjI, rtac trans, rtac map_comp, |
299 REPEAT_DETERM_N m o stac @{thm id_o}, |
294 REPEAT_DETERM_N m o stac @{thm id_o}, |
317 rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, |
312 rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms, |
318 etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1 |
313 etac conjE, etac conjI, CONJ_WRAP' mk_only_if_tac thms] 1 |
319 end; |
314 end; |
320 |
315 |
321 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses = |
316 fun mk_bis_converse_tac m bis_rel rel_congs rel_converses = |
322 EVERY' [stac bis_rel, dtac (bis_rel RS subst_id), |
317 EVERY' [stac bis_rel, dtac (bis_rel RS iffD1), |
323 REPEAT_DETERM o etac conjE, rtac conjI, |
318 REPEAT_DETERM o etac conjE, rtac conjI, |
324 CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans, |
319 CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans, |
325 rtac equalityD2, rtac @{thm converse_Times}])) rel_congs, |
320 rtac equalityD2, rtac @{thm converse_Times}])) rel_congs, |
326 CONJ_WRAP' (fn (rel_cong, rel_converse) => |
321 CONJ_WRAP' (fn (rel_cong, rel_converse) => |
327 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
322 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
331 rtac rel_converse, |
326 rtac rel_converse, |
332 REPEAT_DETERM o etac allE, |
327 REPEAT_DETERM o etac allE, |
333 rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1; |
328 rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converses)] 1; |
334 |
329 |
335 fun mk_bis_O_tac m bis_rel rel_congs rel_Os = |
330 fun mk_bis_O_tac m bis_rel rel_congs rel_Os = |
336 EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS subst_id), |
331 EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1), |
337 REPEAT_DETERM o etac conjE, rtac conjI, |
332 REPEAT_DETERM o etac conjE, rtac conjI, |
338 CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs, |
333 CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs, |
339 CONJ_WRAP' (fn (rel_cong, rel_O) => |
334 CONJ_WRAP' (fn (rel_cong, rel_O) => |
340 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
335 EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm set_mp[OF equalityD2]}, |
341 rtac (rel_cong RS trans), |
336 rtac (rel_cong RS trans), |
342 REPEAT_DETERM_N m o rtac @{thm diag_Comp}, |
337 REPEAT_DETERM_N m o rtac @{thm diag_Comp}, |
343 REPEAT_DETERM_N (length rel_congs) o rtac refl, |
338 REPEAT_DETERM_N (length rel_congs) o rtac refl, |
344 rtac rel_O, |
339 rtac rel_O, |
345 etac @{thm relcompE}, |
340 etac @{thm relcompE}, |
346 REPEAT_DETERM o dtac Pair_eq_subst_id, |
341 REPEAT_DETERM o dtac Pair_eqD, |
347 etac conjE, hyp_subst_tac, |
342 etac conjE, hyp_subst_tac, |
348 REPEAT_DETERM o etac allE, rtac @{thm relcompI}, |
343 REPEAT_DETERM o etac allE, rtac @{thm relcompI}, |
349 etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1; |
344 etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_Os)] 1; |
350 |
345 |
351 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins |
346 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins |
389 EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, |
384 EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, |
390 REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, |
385 REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, |
391 rtac (mk_nth_conv n i)] 1; |
386 rtac (mk_nth_conv n i)] 1; |
392 |
387 |
393 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O = |
388 fun mk_equiv_lsbis_tac sbis_lsbis lsbis_incl incl_lsbis bis_diag bis_converse bis_O = |
394 EVERY' [rtac (@{thm equiv_def} RS ssubst_id), |
389 EVERY' [rtac (@{thm equiv_def} RS iffD2), |
395 |
390 |
396 rtac conjI, rtac (@{thm refl_on_def} RS ssubst_id), |
391 rtac conjI, rtac (@{thm refl_on_def} RS iffD2), |
397 rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp, |
392 rtac conjI, rtac lsbis_incl, rtac ballI, rtac set_mp, |
398 rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI}, |
393 rtac incl_lsbis, rtac bis_diag, atac, etac @{thm diagI}, |
399 |
394 |
400 rtac conjI, rtac (@{thm sym_def} RS ssubst_id), |
395 rtac conjI, rtac (@{thm sym_def} RS iffD2), |
401 rtac allI, rtac allI, rtac impI, rtac set_mp, |
396 rtac allI, rtac allI, rtac impI, rtac set_mp, |
402 rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI}, |
397 rtac incl_lsbis, rtac bis_converse, rtac sbis_lsbis, etac @{thm converseI}, |
403 |
398 |
404 rtac (@{thm trans_def} RS ssubst_id), |
399 rtac (@{thm trans_def} RS iffD2), |
405 rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp, |
400 rtac allI, rtac allI, rtac allI, rtac impI, rtac impI, rtac set_mp, |
406 rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis, |
401 rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis, |
407 etac @{thm relcompI}, atac] 1; |
402 etac @{thm relcompI}, atac] 1; |
408 |
403 |
409 fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} = |
404 fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} = |
533 rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans), |
528 rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans), |
534 rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE}, |
529 rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE}, |
535 hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp), |
530 hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp), |
536 rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1, |
531 rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1, |
537 CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' |
532 CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY' |
538 [rtac (mk_UnIN n i), dtac (def RS subst_id), |
533 [rtac (mk_UnIN n i), dtac (def RS iffD1), |
539 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, |
534 REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm image_eqI}, atac, rtac CollectI, |
540 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
535 REPEAT_DETERM_N m o (rtac conjI THEN' atac), |
541 CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans, |
536 CONJ_WRAP' (K (EVERY' [etac ord_eq_le_trans, rtac subset_trans, |
542 rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order}, |
537 rtac @{thm subset_UNIV}, rtac equalityD2, rtac @{thm Field_card_order}, |
543 rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs), |
538 rtac sbd_card_order])) isNode_defs]) (1 upto n ~~ isNode_defs), |
545 end; |
540 end; |
546 |
541 |
547 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= |
542 fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}= |
548 EVERY' [dtac (carT_def RS equalityD1 RS set_mp), |
543 EVERY' [dtac (carT_def RS equalityD1 RS set_mp), |
549 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
544 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
550 dtac Pair_eq_subst_id, |
545 dtac Pair_eqD, |
551 etac conjE, hyp_subst_tac, |
546 etac conjE, hyp_subst_tac, |
552 dtac (isNode_def RS subst_id), |
547 dtac (isNode_def RS iffD1), |
553 REPEAT_DETERM o eresolve_tac [exE, conjE], |
548 REPEAT_DETERM o eresolve_tac [exE, conjE], |
554 rtac (equalityD2 RS set_mp), |
549 rtac (equalityD2 RS set_mp), |
555 rtac (strT_def RS arg_cong RS trans), |
550 rtac (strT_def RS arg_cong RS trans), |
556 etac (arg_cong RS trans), |
551 etac (arg_cong RS trans), |
557 fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt, |
552 fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt, |
571 rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)), |
566 rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)), |
572 rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]), |
567 rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]), |
573 rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] |
568 rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] |
574 else EVERY' [dtac (carT_def RS equalityD1 RS set_mp), |
569 else EVERY' [dtac (carT_def RS equalityD1 RS set_mp), |
575 REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE, |
570 REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE, |
576 dtac conjunct2, dtac Pair_eq_subst_id, etac conjE, |
571 dtac conjunct2, dtac Pair_eqD, etac conjE, |
577 hyp_subst_tac, dtac (isNode_def RS subst_id), |
572 hyp_subst_tac, dtac (isNode_def RS iffD1), |
578 REPEAT_DETERM o eresolve_tac [exE, conjE], |
573 REPEAT_DETERM o eresolve_tac [exE, conjE], |
579 rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac])) |
574 rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac])) |
580 (ks ~~ (carT_defs ~~ isNode_defs)); |
575 (ks ~~ (carT_defs ~~ isNode_defs)); |
581 fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) = |
576 fun step_tac (i, (coalg_sets, (carT_sets, set_hset_incl_hsets))) = |
582 dtac (mk_conjunctN n i) THEN' |
577 dtac (mk_conjunctN n i) THEN' |
717 EVERY' [rtac (Drule.instantiate' [] cts nat_induct), |
712 EVERY' [rtac (Drule.instantiate' [] cts nat_induct), |
718 REPEAT_DETERM o rtac allI, |
713 REPEAT_DETERM o rtac allI, |
719 CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) => |
714 CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) => |
720 EVERY' [rtac impI, REPEAT_DETERM o etac conjE, |
715 EVERY' [rtac impI, REPEAT_DETERM o etac conjE, |
721 dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst, |
716 dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst, |
722 rtac (rv_Nil RS arg_cong RS ssubst_id), |
717 rtac (rv_Nil RS arg_cong RS iffD2), |
723 rtac (mk_sum_casesN n i RS ssubst_id), |
718 rtac (mk_sum_casesN n i RS iffD2), |
724 CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)]) |
719 CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)]) |
725 (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)), |
720 (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)), |
726 REPEAT_DETERM o rtac allI, |
721 REPEAT_DETERM o rtac allI, |
727 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) => |
722 CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) => |
728 EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp), |
723 EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp), |
729 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
724 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
730 (fn (i, (from_to_sbd, coalg_set)) => |
725 (fn (i, (from_to_sbd, coalg_set)) => |
731 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
726 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac, |
732 rtac (rv_Cons RS arg_cong RS ssubst_id), |
727 rtac (rv_Cons RS arg_cong RS iffD2), |
733 rtac (mk_sum_casesN n i RS arg_cong RS trans RS ssubst_id), |
728 rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2), |
734 etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE, |
729 etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE, |
735 dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp, |
730 dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp, |
736 etac coalg_set, atac]) |
731 etac coalg_set, atac]) |
737 (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))]) |
732 (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))]) |
738 ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1 |
733 ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1 |
800 then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]}, |
795 then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]}, |
801 dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i), |
796 dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i), |
802 hyp_subst_tac, |
797 hyp_subst_tac, |
803 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
798 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) |
804 (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
799 (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
805 dtac list_inject_subst_id THEN' etac conjE THEN' |
800 dtac list_inject_iffD1 THEN' etac conjE THEN' |
806 (if k = i' |
801 (if k = i' |
807 then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI] |
802 then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI] |
808 else etac (mk_InN_not_InM i' k RS notE))) |
803 else etac (mk_InN_not_InM i' k RS notE))) |
809 (rev ks)] |
804 (rev ks)] |
810 else etac (mk_InN_not_InM i'' i RS notE))) |
805 else etac (mk_InN_not_InM i'' i RS notE))) |
820 CONJ_WRAP' (fn i' => rtac impI THEN' |
815 CONJ_WRAP' (fn i' => rtac impI THEN' |
821 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN' |
816 dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN' |
822 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN' |
817 dtac (Lev_Suc RS equalityD1 RS set_mp) THEN' |
823 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k => |
818 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn k => |
824 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
819 REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' |
825 dtac list_inject_subst_id THEN' etac conjE THEN' |
820 dtac list_inject_iffD1 THEN' etac conjE THEN' |
826 (if k = i |
821 (if k = i |
827 then EVERY' [dtac (mk_InN_inject n i), |
822 then EVERY' [dtac (mk_InN_inject n i), |
828 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)), |
823 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), |
829 atac, atac, hyp_subst_tac] THEN' |
824 atac, atac, hyp_subst_tac] THEN' |
830 CONJ_WRAP' (fn i'' => |
825 CONJ_WRAP' (fn i'' => |
831 EVERY' [rtac impI, dtac (sym RS trans), |
826 EVERY' [rtac impI, dtac (sym RS trans), |
832 rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), |
827 rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans), |
833 etac (from_to_sbd RS arg_cong), |
828 etac (from_to_sbd RS arg_cong), |
955 if n = 1 then K all_tac |
950 if n = 1 then K all_tac |
956 else (rtac (sum_case_weak_cong RS trans) THEN' |
951 else (rtac (sum_case_weak_cong RS trans) THEN' |
957 rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)), |
952 rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)), |
958 rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl), |
953 rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl), |
959 EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => |
954 EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => |
960 DETERM o EVERY' [rtac trans, rtac o_apply, rtac ssubst, rtac @{thm Pair_eq}, rtac conjI, |
955 DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI, |
961 rtac trans, rtac @{thm Shift_def}, |
956 rtac trans, rtac @{thm Shift_def}, |
962 rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl, |
957 rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl, |
963 REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl, |
958 REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl, |
964 etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]}, |
959 etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]}, |
965 rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc, |
960 rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc, |
966 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
961 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
967 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
962 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
968 dtac list_inject_subst_id, etac conjE, |
963 dtac list_inject_iffD1, etac conjE, |
969 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
964 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
970 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)), |
965 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), |
971 atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}] |
966 atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}] |
972 else etac (mk_InN_not_InM i' i'' RS notE)]) |
967 else etac (mk_InN_not_InM i' i'' RS notE)]) |
973 (rev ks), |
968 (rev ks), |
974 rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]}, |
969 rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]}, |
975 rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, |
970 rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, |
978 rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI, |
973 rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI, |
979 dtac asm_rl, dtac asm_rl, dtac asm_rl, |
974 dtac asm_rl, dtac asm_rl, dtac asm_rl, |
980 dtac (Lev_Suc RS equalityD1 RS set_mp), |
975 dtac (Lev_Suc RS equalityD1 RS set_mp), |
981 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
976 CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => |
982 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
977 EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], |
983 dtac list_inject_subst_id, etac conjE, |
978 dtac list_inject_iffD1, etac conjE, |
984 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
979 if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), |
985 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS subst_id)), |
980 dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), |
986 atac, atac, hyp_subst_tac, atac] |
981 atac, atac, hyp_subst_tac, atac] |
987 else etac (mk_InN_not_InM i' i'' RS notE)]) |
982 else etac (mk_InN_not_InM i' i'' RS notE)]) |
988 (rev ks), |
983 (rev ks), |
989 rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, |
984 rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, |
990 REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, |
985 REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, |
1065 EVERY' [rtac conjI, |
1060 EVERY' [rtac conjI, |
1066 CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses, |
1061 CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses, |
1067 CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1; |
1062 CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1; |
1068 |
1063 |
1069 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs = |
1064 fun mk_mor_coiter_tac m mor_UNIV unf_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs = |
1070 EVERY' [rtac ssubst_id, rtac mor_UNIV, |
1065 EVERY' [rtac iffD2, rtac mor_UNIV, |
1071 CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) => |
1066 CONJ_WRAP' (fn ((Abs_inverse, morE), ((unf_def, coiter_def), (map_comp_id, map_cong))) => |
1072 EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans), |
1067 EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (unf_def RS trans), |
1073 rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans), |
1068 rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans), |
1074 rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans), |
1069 rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans), |
1075 rtac (o_apply RS trans RS sym), rtac map_cong, |
1070 rtac (o_apply RS trans RS sym), rtac map_cong, |
1080 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final |
1075 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final |
1081 sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = |
1076 sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects = |
1082 let |
1077 let |
1083 val n = length Rep_injects; |
1078 val n = length Rep_injects; |
1084 in |
1079 in |
1085 EVERY' [rtac rev_mp, ftac (bis_def RS subst_id), |
1080 EVERY' [rtac rev_mp, ftac (bis_def RS iffD1), |
1086 REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse, |
1081 REPEAT_DETERM o etac conjE, rtac bis_cong, rtac bis_O, rtac bis_converse, |
1087 rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg, |
1082 rtac bis_Gr, rtac tcoalg, rtac mor_Rep, rtac bis_O, atac, rtac bis_Gr, rtac tcoalg, |
1088 rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr}, |
1083 rtac mor_Rep, REPEAT_DETERM_N n o etac @{thm relImage_Gr}, |
1089 rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT, |
1084 rtac impI, rtac rev_mp, rtac bis_cong, rtac bis_O, rtac bis_Gr, rtac coalgT, |
1090 rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT, |
1085 rtac mor_T_final, rtac bis_O, rtac sbis_lsbis, rtac bis_converse, rtac bis_Gr, rtac coalgT, |
1454 (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 |
1449 (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1 |
1455 end; |
1450 end; |
1456 |
1451 |
1457 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick |
1452 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick |
1458 mor_unique pick_cols hset_defs = |
1453 mor_unique pick_cols hset_defs = |
1459 EVERY' [rtac (@{thm wpull_def} RS ssubst_id), REPEAT_DETERM o rtac allI, rtac impI, |
1454 EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI, |
1460 REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI, |
1455 REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI, |
1461 rtac box_equals, rtac mor_unique, |
1456 rtac box_equals, rtac mor_unique, |
1462 rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
1457 rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
1463 rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
1458 rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
1464 rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |
1459 rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac, |