equal
deleted
inserted
replaced
780 end; |
780 end; |
781 |
781 |
782 fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} = |
782 fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = IHs} = |
783 let val n = length ks; |
783 let val n = length ks; |
784 in |
784 in |
785 unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN |
785 unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN |
786 EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, |
786 EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, |
787 EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong => |
787 EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong => |
788 EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), |
788 EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), |
789 etac rel_mono_strong, |
789 etac rel_mono_strong, |
790 REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, |
790 REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, |