374 let |
374 let |
375 val concl = mk_trp (defined (con_app con args)); |
375 val concl = mk_trp (defined (con_app con args)); |
376 val goal = lift_defined %: (nonlazy args, concl); |
376 val goal = lift_defined %: (nonlazy args, concl); |
377 fun tacs ctxt = [ |
377 fun tacs ctxt = [ |
378 rtac @{thm rev_contrapos} 1, |
378 rtac @{thm rev_contrapos} 1, |
379 RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1, |
379 eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1, |
380 asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; |
380 asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; |
381 in pg [] goal tacs end; |
381 in pg [] goal tacs end; |
382 in |
382 in |
383 val con_stricts = maps con_strict cons; |
383 val con_stricts = maps con_strict cons; |
384 val con_defins = map con_defin cons; |
384 val con_defins = map con_defin cons; |
475 let |
475 let |
476 val goal = lift_defined %: (nonlazy args1, |
476 val goal = lift_defined %: (nonlazy args1, |
477 mk_trp (con_app con1 args1 ~<< con_app con2 args2)); |
477 mk_trp (con_app con1 args1 ~<< con_app con2 args2)); |
478 fun tacs ctxt = [ |
478 fun tacs ctxt = [ |
479 rtac @{thm rev_contrapos} 1, |
479 rtac @{thm rev_contrapos} 1, |
480 RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] |
480 eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] |
481 @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) |
481 @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) |
482 @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; |
482 @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; |
483 in pg [] goal tacs end; |
483 in pg [] goal tacs end; |
484 |
484 |
485 fun distinct (con1, args1) (con2, args2) = |
485 fun distinct (con1, args1) (con2, args2) = |
707 fun ind_term concf = Library.foldr one_eq |
707 fun ind_term concf = Library.foldr one_eq |
708 (mapn (fn n => fn x => (P_name n, x)) 1 conss, |
708 (mapn (fn n => fn x => (P_name n, x)) 1 conss, |
709 mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); |
709 mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); |
710 val take_ss = HOL_ss addsimps take_rews; |
710 val take_ss = HOL_ss addsimps take_rews; |
711 fun quant_tac ctxt i = EVERY |
711 fun quant_tac ctxt i = EVERY |
712 (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); |
712 (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); |
713 |
713 |
714 fun ind_prems_tac prems = EVERY |
714 fun ind_prems_tac prems = EVERY |
715 (maps (fn cons => |
715 (maps (fn cons => |
716 (resolve_tac prems 1 :: |
716 (resolve_tac prems 1 :: |
717 maps (fn (_,args) => |
717 maps (fn (_,args) => |
764 map arg_tac (List.filter is_nonlazy_rec args) @ |
764 map arg_tac (List.filter is_nonlazy_rec args) @ |
765 [resolve_tac prems 1] @ |
765 [resolve_tac prems 1] @ |
766 map (K (atac 1)) (nonlazy args) @ |
766 map (K (atac 1)) (nonlazy args) @ |
767 map (K (etac spec 1)) (List.filter is_rec args); |
767 map (K (etac spec 1)) (List.filter is_rec args); |
768 fun cases_tacs (cons, cases) = |
768 fun cases_tacs (cons, cases) = |
769 RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 :: |
769 res_inst_tac context [(("x", 0), "x")] cases 1 :: |
770 asm_simp_tac (take_ss addsimps prems) 1 :: |
770 asm_simp_tac (take_ss addsimps prems) 1 :: |
771 maps con_tacs cons; |
771 maps con_tacs cons; |
772 in |
772 in |
773 tacs1 @ maps cases_tacs (conss ~~ cases) |
773 tacs1 @ maps cases_tacs (conss ~~ cases) |
774 end; |
774 end; |
781 val lhs = dc_take dn $ Bound 0 `%(x_name n); |
781 val lhs = dc_take dn $ Bound 0 `%(x_name n); |
782 val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); |
782 val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); |
783 val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); |
783 val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); |
784 val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; |
784 val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; |
785 fun tacf {prems, context} = [ |
785 fun tacf {prems, context} = [ |
786 RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, |
786 res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, |
787 RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, |
787 res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, |
788 stac fix_def2 1, |
788 stac fix_def2 1, |
789 REPEAT (CHANGED |
789 REPEAT (CHANGED |
790 (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), |
790 (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), |
791 stac contlub_cfun_fun 1, |
791 stac contlub_cfun_fun 1, |
792 stac contlub_cfun_fun 2, |
792 stac contlub_cfun_fun 2, |
831 (x_name n, Type (dn,args), mk_disj (disj1, disj2)) |
831 (x_name n, Type (dn,args), mk_disj (disj1, disj2)) |
832 end; |
832 end; |
833 val goal = |
833 val goal = |
834 mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); |
834 mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); |
835 fun arg_tacs ctxt vn = [ |
835 fun arg_tacs ctxt vn = [ |
836 RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, |
836 eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, |
837 etac disjE 1, |
837 etac disjE 1, |
838 asm_simp_tac (HOL_ss addsimps con_rews) 1, |
838 asm_simp_tac (HOL_ss addsimps con_rews) 1, |
839 asm_simp_tac take_ss 1]; |
839 asm_simp_tac take_ss 1]; |
840 fun con_tacs ctxt (con, args) = |
840 fun con_tacs ctxt (con, args) = |
841 asm_simp_tac take_ss 1 :: |
841 asm_simp_tac take_ss 1 :: |
842 maps (arg_tacs ctxt) (nonlazy_rec args); |
842 maps (arg_tacs ctxt) (nonlazy_rec args); |
843 fun foo_tacs ctxt n (cons, cases) = |
843 fun foo_tacs ctxt n (cons, cases) = |
844 simp_tac take_ss 1 :: |
844 simp_tac take_ss 1 :: |
845 rtac allI 1 :: |
845 rtac allI 1 :: |
846 RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: |
846 res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: |
847 asm_simp_tac take_ss 1 :: |
847 asm_simp_tac take_ss 1 :: |
848 maps (con_tacs ctxt) cons; |
848 maps (con_tacs ctxt) cons; |
849 fun tacs ctxt = |
849 fun tacs ctxt = |
850 rtac allI 1 :: |
850 rtac allI 1 :: |
851 InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: |
851 InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: |
885 in (finites, ind) end (* let *) |
885 in (finites, ind) end (* let *) |
886 |
886 |
887 else (* infinite case *) |
887 else (* infinite case *) |
888 let |
888 let |
889 fun one_finite n dn = |
889 fun one_finite n dn = |
890 RuleInsts.read_instantiate global_ctxt |
890 read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; |
891 [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; |
|
892 val finites = mapn one_finite 1 dnames; |
891 val finites = mapn one_finite 1 dnames; |
893 |
892 |
894 val goal = |
893 val goal = |
895 let |
894 let |
896 fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); |
895 fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); |
934 Library.foldr mk_imp (mapn mk_prj 0 dnames, |
933 Library.foldr mk_imp (mapn mk_prj 0 dnames, |
935 foldr1 mk_conj (mapn mk_eqn 0 dnames))))); |
934 foldr1 mk_conj (mapn mk_eqn 0 dnames))))); |
936 fun x_tacs ctxt n x = [ |
935 fun x_tacs ctxt n x = [ |
937 rotate_tac (n+1) 1, |
936 rotate_tac (n+1) 1, |
938 etac all2E 1, |
937 etac all2E 1, |
939 RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
938 eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, |
940 TRY (safe_tac HOL_cs), |
939 TRY (safe_tac HOL_cs), |
941 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
940 REPEAT (CHANGED (asm_simp_tac take_ss 1))]; |
942 fun tacs ctxt = [ |
941 fun tacs ctxt = [ |
943 rtac impI 1, |
942 rtac impI 1, |
944 InductTacs.induct_tac ctxt [[SOME "n"]] 1, |
943 InductTacs.induct_tac ctxt [[SOME "n"]] 1, |