1646 fun mk_induct_raw_prem names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts = |
1646 fun mk_induct_raw_prem names_lthy Xss setss_fp_nesting p ctr ctr_Ts ctrXs_Ts = |
1647 let |
1647 let |
1648 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; |
1648 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts; |
1649 val pprems = |
1649 val pprems = |
1650 flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts); |
1650 flat (map2 (mk_induct_raw_prem_prems names_lthy' Xss setss_fp_nesting) xs ctrXs_Ts); |
1651 in (xs, pprems, HOLogic.mk_Trueprop (p $ Term.list_comb (ctr, xs))) end; |
1651 val y = Term.list_comb (ctr, xs); |
|
1652 val p' = enforce_type names_lthy domain_type (fastype_of y) p; |
|
1653 in (xs, pprems, HOLogic.mk_Trueprop (p' $ y)) end; |
1652 |
1654 |
1653 fun close_induct_prem_prem nn ps xs t = |
1655 fun close_induct_prem_prem nn ps xs t = |
1654 fold_rev Logic.all (map Free (drop (nn + length xs) |
1656 fold_rev Logic.all (map Free (drop (nn + length xs) |
1655 (rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t; |
1657 (rev (Term.add_frees t (map dest_Free xs @ map_filter (try dest_Free) ps))))) t; |
1656 |
1658 |
1657 fun finish_induct_prem_prem lthy nn ps xs (xysets, (j, x)) = |
1659 fun finish_induct_prem_prem lthy nn ps xs (xysets, (j, x)) = |
1658 close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) => |
1660 let val p' = enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) in |
1659 mk_Trueprop_mem (y, set $ x')) xysets, |
1661 close_induct_prem_prem nn ps xs (Logic.list_implies (map (fn (x', (y, set)) => |
1660 HOLogic.mk_Trueprop (enforce_type lthy domain_type (fastype_of x) (nth ps (j - 1)) $ x))); |
1662 mk_Trueprop_mem (y, set $ x')) xysets, |
|
1663 HOLogic.mk_Trueprop (p' $ x))) |
|
1664 end; |
1661 |
1665 |
1662 fun finish_induct_prem lthy nn ps (xs, raw_pprems, concl) = |
1666 fun finish_induct_prem lthy nn ps (xs, raw_pprems, concl) = |
1663 fold_rev Logic.all xs (Logic.list_implies |
1667 fold_rev Logic.all xs (Logic.list_implies |
1664 (map (finish_induct_prem_prem lthy nn ps xs) raw_pprems, concl)); |
1668 (map (finish_induct_prem_prem lthy nn ps xs) raw_pprems, concl)); |
1665 |
1669 |
1715 (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, |
1719 (postproc_co_induct lthy nn @{thm predicate2D} @{thm predicate2D_conj} rel_induct0_thm, |
1716 mk_induct_attrs ctrAss) |
1720 mk_induct_attrs ctrAss) |
1717 end; |
1721 end; |
1718 |
1722 |
1719 fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms |
1723 fun derive_induct_recs_thms_for_types plugins pre_bnfs rec_args_typess ctor_induct ctor_rec_thms |
1720 live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions |
1724 live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses pre_type_definitions |
1721 abs_inverses ctrss ctr_defss recs rec_defs lthy = |
1725 abs_inverses ctrss ctr_defss recs rec_defs lthy = |
1722 let |
1726 let |
1723 val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; |
1727 val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss; |
1724 |
1728 |
1725 val nn = length pre_bnfs; |
1729 val nn = length pre_bnfs; |
1755 (raw_premss, concl); |
1759 (raw_premss, concl); |
1756 val vars = Variable.add_free_names lthy goal []; |
1760 val vars = Variable.add_free_names lthy goal []; |
1757 |
1761 |
1758 val kksss = map (map (map (fst o snd) o #2)) raw_premss; |
1762 val kksss = map (map (map (fst o snd) o #2)) raw_premss; |
1759 |
1763 |
1760 val ctor_induct' = ctor_induct OF (map2 mk_absumprodE fp_type_definitions mss); |
1764 val ctor_induct' = ctor_induct OF (map2 mk_absumprodE pre_type_definitions mss); |
1761 |
1765 |
1762 val thm = |
1766 val thm = |
1763 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => |
1767 Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => |
1764 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses |
1768 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct' fp_abs_inverses |
1765 abs_inverses fp_nesting_set_maps pre_set_defss) |
1769 abs_inverses fp_nesting_set_maps pre_set_defss) |