1600 val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; |
1600 val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms; |
1601 val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; |
1601 val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms; |
1602 |
1602 |
1603 val timer = time (timer "ctor definitions & thms"); |
1603 val timer = time (timer "ctor definitions & thms"); |
1604 |
1604 |
1605 val corec_Inl_sum_thms = |
|
1606 let |
|
1607 val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm]; |
|
1608 in |
|
1609 map2 (fn unique => fn unfold_dtor => |
|
1610 trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms |
|
1611 end; |
|
1612 |
|
1613 fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_"); |
|
1614 val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind; |
|
1615 |
|
1616 fun mk_corec_strs corec_ss = |
|
1617 @{map 3} (fn dtor => fn sum_s => fn mapx => |
|
1618 mk_case_sum |
|
1619 (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) |
|
1620 dtors corec_ss corec_maps; |
|
1621 |
|
1622 fun corec_spec i T AT = |
|
1623 fold_rev (Term.absfree o Term.dest_Free) corec_ss |
|
1624 (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT)); |
|
1625 |
|
1626 val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = |
|
1627 lthy |
|
1628 |> Local_Theory.open_target |> snd |
|
1629 |> @{fold_map 3} (fn i => fn T => fn AT => |
|
1630 Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT))) |
|
1631 ks Ts activeAs |
|
1632 |>> apsnd split_list o split_list |
|
1633 ||> `Local_Theory.close_target; |
|
1634 |
|
1635 val phi = Proof_Context.export_morphism lthy_old lthy; |
|
1636 val corecs = map (Morphism.term phi) corec_frees; |
|
1637 val corec_names = map (fst o dest_Const) corecs; |
|
1638 fun mk_corecs Ts passives actives = |
|
1639 let val Tactives = map2 (curry mk_sumT) Ts actives; |
|
1640 in |
|
1641 @{map 3} (fn name => fn T => fn active => |
|
1642 Const (name, Library.foldr (op -->) |
|
1643 (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T))) |
|
1644 corec_names Ts actives |
|
1645 end; |
|
1646 fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->) |
|
1647 (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss); |
|
1648 val corec_defs = map (fn def => |
|
1649 mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees; |
|
1650 |
|
1651 val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) = |
1605 val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) = |
1652 lthy |
1606 lthy |
1653 |> mk_Frees "b" activeAs |
1607 |> mk_Frees "b" activeAs |
1654 ||>> mk_Frees "z" Ts |
1608 ||>> mk_Frees "z" Ts |
1655 ||>> mk_Frees "z'" Ts |
1609 ||>> mk_Frees "z'" Ts |
1656 ||>> mk_Frees "z1" Ts |
1610 ||>> mk_Frees "z1" Ts |
1657 ||>> mk_Frees "z2" Ts |
1611 ||>> mk_Frees "z2" Ts |
1658 ||>> mk_Frees "f" unfold_fTs |
1612 ||>> mk_Frees "f" unfold_fTs |
1659 ||>> mk_Frees "s" corec_sTs |
1613 ||>> mk_Frees "s" corec_sTs |
1660 ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); |
1614 ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); |
1661 |
|
1662 val case_sums = |
|
1663 map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks; |
|
1664 val dtor_corec_thms = |
|
1665 let |
|
1666 fun mk_goal i corec_s corec_map dtor z = |
|
1667 let |
|
1668 val lhs = dtor $ (mk_corec corec_ss i $ z); |
|
1669 val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z); |
|
1670 in |
|
1671 mk_Trueprop_eq (lhs, rhs) |
|
1672 end; |
|
1673 val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs; |
|
1674 in |
|
1675 @{map 3} (fn goal => fn unfold => fn map_cong0 => |
|
1676 Variable.add_free_names lthy goal [] |
|
1677 |> (fn vars => Goal.prove_sorry lthy vars [] goal |
|
1678 (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0 |
|
1679 corec_Inl_sum_thms)) |
|
1680 |> Thm.close_derivation) |
|
1681 goals dtor_unfold_thms map_cong0s |
|
1682 end; |
|
1683 |
|
1684 val corec_unique_mor_thm = |
|
1685 let |
|
1686 val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs; |
|
1687 val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs); |
|
1688 fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i); |
|
1689 val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
|
1690 (map2 mk_fun_eq unfold_fs ks)); |
|
1691 val vars = fold (Variable.add_free_names lthy) [prem, unique] []; |
|
1692 in |
|
1693 Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique)) |
|
1694 (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs |
|
1695 corec_Inl_sum_thms unfold_unique_mor_thm) |
|
1696 |> Thm.close_derivation |
|
1697 end; |
|
1698 |
|
1699 val map_id0s_o_id = |
|
1700 map (fn thm => |
|
1701 mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp}) |
|
1702 map_id0s; |
|
1703 |
|
1704 val (dtor_corec_unique_thms, dtor_corec_unique_thm) = |
|
1705 `split_conj_thm (split_conj_prems n |
|
1706 (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |
|
1707 |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric] |
|
1708 case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps) |
|
1709 OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]}); |
|
1710 |
|
1711 val timer = time (timer "corec definitions & thms"); |
|
1712 |
1615 |
1713 val (coinduct_params, dtor_coinduct_thm) = |
1616 val (coinduct_params, dtor_coinduct_thm) = |
1714 let |
1617 let |
1715 val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs; |
1618 val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs; |
1716 |
1619 |
2674 (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) |
2574 (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) |
2675 (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm |
2575 (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm |
2676 (map map_transfer_of_bnf bnfs) dtor_unfold_thms) |
2576 (map map_transfer_of_bnf bnfs) dtor_unfold_thms) |
2677 lthy; |
2577 lthy; |
2678 |
2578 |
2679 val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs; |
|
2680 val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs; |
|
2681 val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs; |
|
2682 val corec_activephis = |
|
2683 map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis; |
|
2684 val dtor_corec_transfer_thms = |
|
2685 mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis |
|
2686 (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs) |
|
2687 (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs |
|
2688 dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms) |
|
2689 lthy; |
|
2690 |
|
2691 val timer = time (timer "relator coinduction"); |
2579 val timer = time (timer "relator coinduction"); |
|
2580 |
|
2581 fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts; |
|
2582 val export = map (Morphism.term (Local_Theory.target_morphism lthy)) |
|
2583 val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms, |
|
2584 dtor_corec_transfer_thms)), lthy) = lthy |
|
2585 |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs |
|
2586 (export dtors) (export unfolds) |
|
2587 dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms |
|
2588 dtor_Jmap_thms dtor_Jrel_thms; |
|
2589 |
|
2590 val timer = time (timer "recursor"); |
2692 |
2591 |
2693 val common_notes = |
2592 val common_notes = |
2694 [(dtor_coinductN, [dtor_coinduct_thm]), |
2593 [(dtor_coinductN, [dtor_coinduct_thm]), |
2695 (dtor_rel_coinductN, [Jrel_coinduct_thm])] |
2594 (dtor_rel_coinductN, [Jrel_coinduct_thm])] |
2696 |> map (fn (thmN, thms) => |
2595 |> map (fn (thmN, thms) => |
2698 |
2597 |
2699 val notes = |
2598 val notes = |
2700 [(ctor_dtorN, ctor_dtor_thms), |
2599 [(ctor_dtorN, ctor_dtor_thms), |
2701 (ctor_exhaustN, ctor_exhaust_thms), |
2600 (ctor_exhaustN, ctor_exhaust_thms), |
2702 (ctor_injectN, ctor_inject_thms), |
2601 (ctor_injectN, ctor_inject_thms), |
2703 (dtor_corecN, dtor_corec_thms), |
|
2704 (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms), |
|
2705 (dtor_corec_transferN, dtor_corec_transfer_thms), |
|
2706 (dtor_corec_uniqueN, dtor_corec_unique_thms), |
|
2707 (dtor_ctorN, dtor_ctor_thms), |
2602 (dtor_ctorN, dtor_ctor_thms), |
2708 (dtor_exhaustN, dtor_exhaust_thms), |
2603 (dtor_exhaustN, dtor_exhaust_thms), |
2709 (dtor_injectN, dtor_inject_thms), |
2604 (dtor_injectN, dtor_inject_thms), |
2710 (dtor_unfoldN, dtor_unfold_thms), |
2605 (dtor_unfoldN, dtor_unfold_thms), |
2711 (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), |
2606 (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms), |
2719 |
2614 |
2720 val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); |
2615 val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); |
2721 |
2616 |
2722 val fp_res = |
2617 val fp_res = |
2723 {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, |
2618 {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, |
2724 ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs, |
2619 ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs, |
2725 xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, |
2620 xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, |
2726 ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, |
2621 ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, |
2727 xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss', |
2622 xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss', |
2728 xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms, |
2623 xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms, |
2729 xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique_legacy = dtor_unfold_unique_thm, |
2624 xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique_legacy = dtor_unfold_unique_thm, |