471 |
471 |
472 fun mk_closed_tac (k, (morE, set_maps)) = |
472 fun mk_closed_tac (k, (morE, set_maps)) = |
473 EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, |
473 EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI, |
474 rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac, |
474 rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac, |
475 REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, |
475 REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec}, |
476 EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; |
476 EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac]; |
477 |
477 |
478 fun mk_induct_tac (Rep, Rep_inv) = |
478 fun mk_induct_tac (Rep, Rep_inv) = |
479 EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))]; |
479 EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))]; |
480 in |
480 in |
481 (rtac mp THEN' rtac impI THEN' |
481 (rtac mp THEN' rtac impI THEN' |
545 rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
545 rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
546 rtac sym, rtac (nth set_nats (i - 1)), |
546 rtac sym, rtac (nth set_nats (i - 1)), |
547 REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
547 REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), |
548 EVERY' (map useIH (drop m set_nats))]; |
548 EVERY' (map useIH (drop m set_nats))]; |
549 in |
549 in |
550 (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 |
550 (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1 |
551 end; |
551 end; |
552 |
552 |
553 fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = |
553 fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i = |
554 let |
554 let |
555 val n = length ctor_sets; |
555 val n = length ctor_sets; |
579 rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong), |
579 rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong), |
580 EVERY' (map use_asm (map hd set_setss)), |
580 EVERY' (map use_asm (map hd set_setss)), |
581 EVERY' (map useIH (transpose (map tl set_setss))), |
581 EVERY' (map useIH (transpose (map tl set_setss))), |
582 rtac sym, rtac ctor_map]; |
582 rtac sym, rtac ctor_map]; |
583 in |
583 in |
584 (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 |
584 (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 |
585 end; |
585 end; |
586 |
586 |
587 fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = |
587 fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = |
588 EVERY' (rtac induct :: |
588 EVERY' (rtac induct :: |
589 map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => |
589 @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => |
590 EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), |
590 EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), |
591 REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2), |
591 REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2), |
592 rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}), |
592 rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}), |
593 rtac @{thm relcomppI}, atac, atac, |
593 rtac @{thm relcomppI}, atac, atac, |
594 REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac], |
594 REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac], |
723 fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = |
723 fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = |
724 let val n = length ks; |
724 let val n = length ks; |
725 in |
725 in |
726 unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN |
726 unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN |
727 EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, |
727 EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, |
728 EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 => |
728 EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 => |
729 EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), |
729 EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), |
730 etac rel_mono_strong0, |
730 etac rel_mono_strong0, |
731 REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, |
731 REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, |
732 EVERY' (map (fn j => |
732 EVERY' (map (fn j => |
733 EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]}, |
733 EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]}, |