# HG changeset patch # User traytel # Date 1460044582 -7200 # Node ID 52c5a25e0c96ecb0fba9fb5dc188ab66a497b60f # Parent 94535e6dd16841ceb68f9136d0b2ab8ce110bcfc derive (co)rec uniformly from (un)fold diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Apr 07 17:56:22 2016 +0200 @@ -242,6 +242,49 @@ lemma top_conj: "top x \ P \ P" "P \ top x \ P" by blast+ +lemma fst_convol': "fst (\f, g\ x) = f x" + using fst_convol unfolding convol_def by simp + +lemma snd_convol': "snd (\f, g\ x) = g x" + using snd_convol unfolding convol_def by simp + +lemma convol_expand_snd: "fst o f = g \ \g, snd o f\ = f" + unfolding convol_def by auto + +lemma convol_expand_snd': + assumes "(fst o f = g)" + shows "h = snd o f \ \g, h\ = f" +proof - + from assms have *: "\g, snd o f\ = f" by (rule convol_expand_snd) + then have "h = snd o f \ h = snd o \g, snd o f\" by simp + moreover have "\ \ h = snd o f" by (simp add: snd_convol) + moreover have "\ \ \g, h\ = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) + ultimately show ?thesis by simp +qed + +lemma case_sum_expand_Inr_pointfree: "f o Inl = g \ case_sum g (f o Inr) = f" + by (auto split: sum.splits) + +lemma case_sum_expand_Inr': "f o Inl = g \ h = f o Inr \ case_sum g h = f" + by (rule iffI) (auto simp add: fun_eq_iff split: sum.splits) + +lemma case_sum_expand_Inr: "f o Inl = g \ f x = case_sum g (f o Inr) x" + by (auto split: sum.splits) + +lemma id_transfer: "rel_fun A A id id" + unfolding rel_fun_def by simp + +lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst" + unfolding rel_fun_def by simp + +lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd" + unfolding rel_fun_def by simp + +lemma convol_transfer: + "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol" + unfolding rel_fun_def convol_def by auto + +ML_file "Tools/BNF/bnf_fp_util_tactics.ML" ML_file "Tools/BNF/bnf_fp_util.ML" ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/BNF/bnf_fp_def_sugar.ML" diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/BNF_Greatest_Fixpoint.thy --- a/src/HOL/BNF_Greatest_Fixpoint.thy Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy Thu Apr 07 17:56:22 2016 +0200 @@ -31,14 +31,6 @@ lemma neq_eq_eq_contradict: "\t \ u; s = t; s = u\ \ P" by fast -lemma case_sum_expand_Inr: "f o Inl = g \ f x = case_sum g (f o Inr) x" - by (auto split: sum.splits) - -lemma case_sum_expand_Inr': "f o Inl = g \ h = f o Inr \ case_sum g h = f" - apply rule - apply (rule ext, force split: sum.split) - by (rule ext, metis case_sum_o_inj(2)) - lemma converse_Times: "(A \ B) ^-1 = B \ A" by fast diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Apr 07 17:56:22 2016 +0200 @@ -40,26 +40,6 @@ lemma FieldI2: "(i, j) \ R \ j \ Field R" unfolding Field_def by auto -lemma fst_convol': "fst (\f, g\ x) = f x" - using fst_convol unfolding convol_def by simp - -lemma snd_convol': "snd (\f, g\ x) = g x" - using snd_convol unfolding convol_def by simp - -lemma convol_expand_snd: "fst o f = g \ \g, snd o f\ = f" - unfolding convol_def by auto - -lemma convol_expand_snd': - assumes "(fst o f = g)" - shows "h = snd o f \ \g, h\ = f" -proof - - from assms have *: "\g, snd o f\ = f" by (rule convol_expand_snd) - then have "h = snd o f \ h = snd o \g, snd o f\" by simp - moreover have "\ \ h = snd o f" by (simp add: snd_convol) - moreover have "\ \ \g, h\ = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff) - ultimately show ?thesis by simp -qed - lemma bij_betwE: "bij_betw f A B \ \a\A. f a \ B" unfolding bij_betw_def by auto @@ -172,19 +152,6 @@ lemma predicate2D_vimage2p: "\R \ vimage2p f g S; R x y\ \ S (f x) (g y)" unfolding vimage2p_def by auto -lemma id_transfer: "rel_fun A A id id" - unfolding rel_fun_def by simp - -lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst" - unfolding rel_fun_def by simp - -lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd" - unfolding rel_fun_def by simp - -lemma convol_transfer: - "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol" - unfolding rel_fun_def convol_def by auto - lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Apr 07 17:56:22 2016 +0200 @@ -24,12 +24,6 @@ open BNF_Tactics open BNF_FP_N2M_Tactics -fun force_typ ctxt T = - Term.map_types Type_Infer.paramify_vars - #> Type.constraint T - #> Syntax.check_term ctxt - #> singleton (Variable.polymorphic ctxt); - fun mk_prod_map f g = let val ((fAT, fBT), fT) = `dest_funT (fastype_of f); diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Apr 07 17:56:22 2016 +0200 @@ -188,6 +188,8 @@ val mk_sum_Cinfinite: thm list -> thm val mk_sum_card_order: thm list -> thm + val force_typ: Proof.context -> typ -> term -> term + val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm @@ -196,6 +198,10 @@ ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list + val derive_xtor_co_recs: BNF_Util.fp_kind -> binding list -> (typ list -> typ list) -> + (typ list list * typ list) -> BNF_Def.bnf list -> term list -> term list -> + thm -> thm list -> thm list -> thm list -> thm list -> local_theory -> + (term list * (thm list * thm * thm list * thm list)) * local_theory val fixpoint_bnf: (binding -> binding) -> (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> @@ -213,6 +219,7 @@ open BNF_Comp open BNF_Def open BNF_Util +open BNF_FP_Util_Tactics type fp_result = {Ts: typ list, @@ -611,6 +618,232 @@ split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems) end; +fun force_typ ctxt T = + Term.map_types Type_Infer.paramify_vars + #> Type.constraint T + #> Syntax.check_term ctxt + #> singleton (Variable.polymorphic ctxt); + +fun mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique_thm map_id0s = + (xtor_un_fold_unique_thm OF + map (fn thm => case_fp fp + (mk_trans @{thm id_o} + (mk_sym (thm RS @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) + (mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) + @{thm trans[OF id_o o_id[symmetric]]})) + map_id0s) + |> split_conj_thm |> map mk_sym; + +fun derive_xtor_co_recs fp bs mk_Ts (Dss, resDs) pre_bnfs xtors0 un_folds0 + xtor_un_fold_unique xtor_un_folds xtor_un_fold_transfers xtor_maps xtor_rels lthy = + let + fun co_swap pair = case_fp fp I swap pair; + val mk_co_comp = curry (HOLogic.mk_comp o co_swap); + fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); + val co_alg_funT = case_fp fp domain_type range_type; + val mk_co_product = curry (case_fp fp mk_convol mk_case_sum); + val co_proj1_const = case_fp fp fst_const (uncurry Inl_const o dest_sumT) o co_alg_funT; + val co_proj2_const = case_fp fp snd_const (uncurry Inr_const o dest_sumT) o co_alg_funT; + val mk_co_productT = curry (case_fp fp HOLogic.mk_prodT mk_sumT); + + val n = length pre_bnfs; + val live = live_of_bnf (hd pre_bnfs); + val m = live - n; + val ks = 1 upto n; + + val map_id0s = map map_id0_of_bnf pre_bnfs; + val map_comps = map map_comp_of_bnf pre_bnfs; + val map_cong0s = map map_cong0_of_bnf pre_bnfs; + val map_transfers = map map_transfer_of_bnf pre_bnfs; + val sym_map_comp0s = map (mk_sym o map_comp0_of_bnf) pre_bnfs; + + val deads = fold (union (op =)) Dss resDs; + val ((((As, Bs), Xs), Ys), names_lthy) = lthy + |> fold Variable.declare_typ deads + |> mk_TFrees m + ||>> mk_TFrees m + ||>> mk_TFrees n + ||>> mk_TFrees n; + + val XFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Xs)) Dss pre_bnfs; + val co_algXFTs = @{map 2} mk_co_algT XFTs Xs; + val Ts = mk_Ts As; + val un_foldTs = @{map 2} (fn T => fn X => co_algXFTs ---> mk_co_algT T X) Ts Xs; + val un_folds = @{map 2} (force_typ names_lthy) un_foldTs un_folds0; + val ABs = As ~~ Bs; + val XYs = Xs ~~ Ys; + + val Us = map (typ_subst_atomic ABs) Ts; + + val TFTs = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ Ts)) Dss pre_bnfs; + + val xtors = @{map 3} (force_typ names_lthy oo mk_co_algT) TFTs Ts xtors0; + + val ids = map HOLogic.id_const As; + val co_rec_Xs = @{map 2} mk_co_productT Ts Xs; + val co_rec_Ys = @{map 2} mk_co_productT Us Ys; + val co_rec_algXs = @{map 2} mk_co_algT co_rec_Xs Xs; + val co_proj1s = map co_proj1_const co_rec_algXs; + val co_rec_maps = @{map 2} (fn Ds => + mk_map_of_bnf Ds (As @ case_fp fp co_rec_Xs Ts) (As @ case_fp fp Ts co_rec_Xs)) Dss pre_bnfs; + val co_rec_Ts = @{map 2} (fn Ds => mk_T_of_bnf Ds (As @ co_rec_Xs)) Dss pre_bnfs + val co_rec_argTs = @{map 2} mk_co_algT co_rec_Ts Xs; + val co_rec_resTs = @{map 2} mk_co_algT Ts Xs; + + val (((co_rec_ss, fs), xs), names_lthy) = names_lthy + |> mk_Frees "s" co_rec_argTs + ||>> mk_Frees "f" co_rec_resTs + ||>> mk_Frees "x" (case_fp fp TFTs Xs); + + val co_rec_strs = + @{map 3} (fn xtor => fn s => fn mapx => + mk_co_product (mk_co_comp xtor (list_comb (mapx, ids @ co_proj1s))) s) + xtors co_rec_ss co_rec_maps; + + val theta = Xs ~~ co_rec_Xs; + val co_rec_un_folds = map (subst_atomic_types theta) un_folds; + + val co_rec_spec0s = map (fn un_fold => list_comb (un_fold, co_rec_strs)) co_rec_un_folds; + + val co_rec_ids = @{map 2} (mk_co_comp o co_proj1_const) co_rec_algXs co_rec_spec0s; + val co_rec_specs = @{map 2} (mk_co_comp o co_proj2_const) co_rec_algXs co_rec_spec0s; + + val co_recN = case_fp fp ctor_recN dtor_corecN; + fun co_rec_bind i = nth bs (i - 1) |> Binding.prefix_name (co_recN ^ "_"); + val co_rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o co_rec_bind; + + fun co_rec_spec i = + fold_rev (Term.absfree o Term.dest_Free) co_rec_ss (nth co_rec_specs (i - 1)); + + val ((co_rec_frees, (_, co_rec_def_frees)), (lthy, lthy_old)) = + lthy + |> Local_Theory.open_target |> snd + |> fold_map (fn i => + Local_Theory.define ((co_rec_bind i, NoSyn), (co_rec_def_bind i, co_rec_spec i))) ks + |>> apsnd split_list o split_list + ||> `Local_Theory.close_target; + + val phi = Proof_Context.export_morphism lthy_old lthy; + val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees; + val co_recs = @{map 2} (fn name => fn resT => + Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs; + val co_rec_defs = map (fn def => + mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees; + + val xtor_un_fold_xtor_thms = mk_xtor_un_fold_xtor_thms fp xtor_un_fold_unique map_id0s; + + val co_rec_id_thms = + let + val goal = @{map 2} (fn T => fn t => HOLogic.mk_eq (t, HOLogic.id_const T)) Ts co_rec_ids + |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtor_thms + xtor_un_fold_unique xtor_un_folds map_comps) + |> Thm.close_derivation + |> split_conj_thm + end; + + val co_rec_app_ss = map (fn co_rec => list_comb (co_rec, co_rec_ss)) co_recs; + val co_products = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts co_rec_app_ss; + val co_rec_maps_rev = @{map 2} (fn Ds => + mk_map_of_bnf Ds (As @ case_fp fp Ts co_rec_Xs) (As @ case_fp fp co_rec_Xs Ts)) Dss pre_bnfs; + fun mk_co_app f g x = case_fp fp (f $ (g $ x)) (g $ (f $ x)); + val co_rec_expand_thms = map (fn thm => thm RS + case_fp fp @{thm convol_expand_snd} @{thm case_sum_expand_Inr_pointfree}) co_rec_id_thms; + val xtor_co_rec_thms = + let + fun mk_goal co_rec s mapx xtor x = + let + val lhs = mk_co_app co_rec xtor x; + val rhs = mk_co_app s (list_comb (mapx, ids @ co_products)) x; + in + mk_Trueprop_eq (lhs, rhs) + end; + val goals = @{map 5} mk_goal co_rec_app_ss co_rec_ss co_rec_maps_rev xtors xs; + in + map2 (fn goal => fn un_fold => + Variable.add_free_names lthy goal [] + |> (fn vars => Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => + mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms)) + |> Thm.close_derivation) + goals xtor_un_folds + end; + + val co_product_fs = @{map 2} (fn T => mk_co_product (HOLogic.id_const T)) Ts fs; + val co_rec_expand'_thms = map (fn thm => + thm RS case_fp fp @{thm convol_expand_snd'} @{thm case_sum_expand_Inr'}) co_rec_id_thms; + val xtor_co_rec_unique_thm = + let + fun mk_prem f s mapx xtor = + let + val lhs = mk_co_comp f xtor; + val rhs = mk_co_comp s (list_comb (mapx, ids @ co_product_fs)); + in + mk_Trueprop_eq (co_swap (lhs, rhs)) + end; + val prems = @{map 4} mk_prem fs co_rec_ss co_rec_maps_rev xtors; + val concl = @{map 2} (curry HOLogic.mk_eq) fs co_rec_app_ss + |> Library.foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop; + val goal = Logic.list_implies (prems, concl); + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal + (fn {context = ctxt, prems = _} => mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs + co_rec_expand'_thms xtor_un_fold_unique map_id0s sym_map_comp0s) + |> Thm.close_derivation + end; + + val xtor_co_rec_o_map_thms = mk_xtor_co_iter_o_map_thms fp true m xtor_co_rec_unique_thm + (map (mk_pointfree lthy) xtor_maps) (map (mk_pointfree lthy) xtor_co_rec_thms) + sym_map_comp0s map_cong0s; + + val ABphiTs = @{map 2} mk_pred2T As Bs; + val XYphiTs = @{map 2} mk_pred2T Xs Ys; + + val ((ABphis, XYphis), names_lthy) = names_lthy + |> mk_Frees "R" ABphiTs + ||>> mk_Frees "S" XYphiTs; + + val pre_rels = + @{map 2} (fn Ds => mk_rel_of_bnf Ds (As @ co_rec_Xs) (Bs @ co_rec_Ys)) Dss pre_bnfs; + val rels = @{map 3} (fn T => fn T' => Thm.prop_of #> HOLogic.dest_Trueprop + #> fst o dest_comb #> fst o dest_comb #> funpow n (snd o dest_comb) + #> case_fp fp (fst o dest_comb #> snd o dest_comb) (snd o dest_comb) #> head_of + #> force_typ names_lthy (ABphiTs ---> mk_pred2T T T')) + Ts Us xtor_un_fold_transfers; + + fun tac {context = ctxt, prems = _} = mk_xtor_co_rec_transfer_tac ctxt fp n m co_rec_defs + xtor_un_fold_transfers map_transfers xtor_rels; + + val mk_rel_co_product = case_fp fp mk_rel_prod mk_rel_sum; + val rec_phis = + map2 (fn rel => mk_rel_co_product (Term.list_comb (rel, ABphis))) rels XYphis; + + val xtor_co_rec_transfer_thms = + mk_xtor_co_iter_transfer_thms fp pre_rels rec_phis XYphis rels ABphis + co_recs (map (subst_atomic_types (ABs @ XYs)) co_recs) tac lthy; + + val notes = + [(case_fp fp ctor_recN dtor_corecN, xtor_co_rec_thms), + (case_fp fp ctor_rec_uniqueN dtor_corec_uniqueN, split_conj_thm xtor_co_rec_unique_thm), + (case_fp fp ctor_rec_o_mapN dtor_corec_o_mapN, xtor_co_rec_o_map_thms), + (case_fp fp ctor_rec_transferN dtor_corec_transferN, xtor_co_rec_transfer_thms)] + |> map (apsnd (map single)) + |> maps (fn (thmN, thmss) => + map2 (fn b => fn thms => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) + bs thmss); + + val lthy = lthy |> Config.get lthy bnf_internals ? snd o Local_Theory.notes notes; + in + ((co_recs, + (xtor_co_rec_thms, xtor_co_rec_unique_thm, xtor_co_rec_o_map_thms, xtor_co_rec_transfer_thms)), + lthy) + end; + fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy = let val time = time lthy; diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/Tools/BNF/bnf_fp_util_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/BNF/bnf_fp_util_tactics.ML Thu Apr 07 17:56:22 2016 +0200 @@ -0,0 +1,79 @@ +(* Title: HOL/Tools/BNF/bnf_fp_util_tactics.ML + Author: Dmitriy Traytel, ETH Zürich + Copyright 2016 + +Common tactics for datatype and codatatype constructions. +*) + +signature BNF_FP_UTIL_TACTICS = +sig + +val mk_xtor_co_rec_id_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> tactic +val mk_xtor_co_rec_tac: Proof.context -> thm -> thm list -> thm list -> tactic +val mk_xtor_co_rec_unique_tac: Proof.context -> BNF_Util.fp_kind -> thm list -> thm list -> thm -> + thm list -> thm list -> tactic +val mk_xtor_co_rec_transfer_tac: Proof.context -> BNF_Util.fp_kind -> int -> int -> thm list -> + thm list -> thm list -> thm list -> tactic + +end + +structure BNF_FP_Util_Tactics = +struct + +open BNF_Tactics +open BNF_Util + +fun mk_xtor_co_rec_id_tac ctxt xtor_un_fold_xtors xtor_un_fold_unique xtor_un_folds map_comps = + unfold_thms_tac ctxt (map mk_sym xtor_un_fold_xtors) THEN + HEADGOAL (rtac ctxt xtor_un_fold_unique THEN_ALL_NEW EVERY' [rtac ctxt ext, + SELECT_GOAL (unfold_thms_tac ctxt + (o_apply :: @{thms fst_convol' id_o sum.case} @ map_comps @ xtor_un_folds)), + rtac ctxt refl]); + +fun mk_xtor_co_rec_tac ctxt un_fold co_rec_defs co_rec_expand_thms = + unfold_thms_tac ctxt (un_fold :: + @{thms o_apply sum.case snd_convol' case_sum_o_inj(2)} @ co_rec_defs @ co_rec_expand_thms) THEN + HEADGOAL (rtac ctxt refl); + +fun mk_xtor_co_rec_unique_tac ctxt fp co_rec_defs co_rec_expand's un_fold_unique map_ids map_comps = + unfold_thms_tac ctxt (co_rec_defs @ co_rec_expand's) THEN + HEADGOAL (EVERY' [rtac ctxt un_fold_unique]) THEN + unfold_thms_tac ctxt (map_ids @ map_comps @ case_fp fp + @{thms id_o o_id convol_o fst_convol o_assoc[symmetric]} + @{thms id_o o_id o_case_sum case_sum_o_inj(1) o_assoc}) THEN + ALLGOALS (etac ctxt (case_fp fp + @{thm arg_cong2[of _ _ _ _ BNF_Def.convol, OF refl]} + @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]})); + +fun mk_xtor_co_rec_transfer_tac ctxt fp n m defs un_fold_transfers pre_T_map_transfers xtor_rels = + case_fp fp + (CONJ_WRAP (fn (def, un_fold_transfer) => + REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN + unfold_thms_tac ctxt [def, o_apply] THEN + HEADGOAL (rtac ctxt @{thm rel_funD[OF snd_transfer]} THEN' + etac ctxt (mk_rel_funDN_rotated (n + 1) un_fold_transfer) THEN' + EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel => + etac ctxt (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN' + rtac ctxt (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN' + rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' + REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' + REPEAT_DETERM o rtac ctxt @{thm fst_transfer} THEN' + rtac ctxt rel_funI THEN' + etac ctxt (xtor_rel RS iffD2)) pre_T_map_transfers xtor_rels))) + (defs ~~ un_fold_transfers)) + (CONJ_WRAP (fn (def, un_fold_transfer) => + REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN + unfold_thms_tac ctxt [def, o_apply] THEN + HEADGOAL (rtac ctxt (mk_rel_funDN (n + 1) un_fold_transfer) THEN' + EVERY' (map2 (fn pre_T_map_transfer => fn xtor_rel => + etac ctxt (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN' + rtac ctxt (mk_rel_funDN 2 @{thm comp_transfer}) THEN' + rtac ctxt (mk_rel_funDN (m + n) pre_T_map_transfer) THEN' + REPEAT_DETERM_N m o rtac ctxt @{thm id_transfer} THEN' + REPEAT_DETERM_N n o rtac ctxt @{thm Inl_transfer} THEN' + rtac ctxt rel_funI THEN' + etac ctxt (xtor_rel RS iffD1)) pre_T_map_transfers xtor_rels) THEN' + etac ctxt (mk_rel_funDN 1 @{thm Inr_transfer}))) + (defs ~~ un_fold_transfers)); + +end \ No newline at end of file diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Apr 07 17:56:22 2016 +0200 @@ -1602,52 +1602,6 @@ val timer = time (timer "ctor definitions & thms"); - val corec_Inl_sum_thms = - let - val mor = mor_comp_thm OF [mor_case_sum_thm, mor_unfold_thm]; - in - map2 (fn unique => fn unfold_dtor => - trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms - end; - - fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_"); - val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind; - - fun mk_corec_strs corec_ss = - @{map 3} (fn dtor => fn sum_s => fn mapx => - mk_case_sum - (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s)) - dtors corec_ss corec_maps; - - fun corec_spec i T AT = - fold_rev (Term.absfree o Term.dest_Free) corec_ss - (HOLogic.mk_comp (mk_unfold Ts (mk_corec_strs corec_ss) i, Inr_const T AT)); - - val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) = - lthy - |> Local_Theory.open_target |> snd - |> @{fold_map 3} (fn i => fn T => fn AT => - Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT))) - ks Ts activeAs - |>> apsnd split_list o split_list - ||> `Local_Theory.close_target; - - val phi = Proof_Context.export_morphism lthy_old lthy; - val corecs = map (Morphism.term phi) corec_frees; - val corec_names = map (fst o dest_Const) corecs; - fun mk_corecs Ts passives actives = - let val Tactives = map2 (curry mk_sumT) Ts actives; - in - @{map 3} (fn name => fn T => fn active => - Const (name, Library.foldr (op -->) - (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T))) - corec_names Ts actives - end; - fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->) - (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss); - val corec_defs = map (fn def => - mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) corec_def_frees; - val ((((((((zs, Jzs), Jzs_copy), Jzs1), Jzs2), unfold_fs), corec_ss), phis), _) = lthy |> mk_Frees "b" activeAs @@ -1659,57 +1613,6 @@ ||>> mk_Frees "s" corec_sTs ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts); - val case_sums = - map2 (fn T => fn i => mk_case_sum (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks; - val dtor_corec_thms = - let - fun mk_goal i corec_s corec_map dtor z = - let - val lhs = dtor $ (mk_corec corec_ss i $ z); - val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z); - in - mk_Trueprop_eq (lhs, rhs) - end; - val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs; - in - @{map 3} (fn goal => fn unfold => fn map_cong0 => - Variable.add_free_names lthy goal [] - |> (fn vars => Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0 - corec_Inl_sum_thms)) - |> Thm.close_derivation) - goals dtor_unfold_thms map_cong0s - end; - - val corec_unique_mor_thm = - let - val id_fs = map2 (fn T => fn f => mk_case_sum (HOLogic.id_const T, f)) Ts unfold_fs; - val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs (mk_corec_strs corec_ss) UNIVs dtors id_fs); - fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i); - val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map2 mk_fun_eq unfold_fs ks)); - val vars = fold (Variable.add_free_names lthy) [prem, unique] []; - in - Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique)) - (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs - corec_Inl_sum_thms unfold_unique_mor_thm) - |> Thm.close_derivation - end; - - val map_id0s_o_id = - map (fn thm => - mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_comp}) - map_id0s; - - val (dtor_corec_unique_thms, dtor_corec_unique_thm) = - `split_conj_thm (split_conj_prems n - (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) - |> unfold_thms lthy (@{thms o_case_sum comp_id id_comp comp_assoc[symmetric] - case_sum_o_inj(1)} @ map_id0s_o_id @ sym_map_comps) - OF replicate n @{thm arg_cong2[of _ _ _ _ case_sum, OF refl]}); - - val timer = time (timer "corec definitions & thms"); - val (coinduct_params, dtor_coinduct_thm) = let val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs; @@ -2661,9 +2564,6 @@ val dtor_unfold_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP false m dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) sym_map_comps map_cong0s; - val dtor_corec_o_Jmap_thms = mk_xtor_co_iter_o_map_thms Greatest_FP true m - dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms) - sym_map_comps map_cong0s; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val Jrels = if m = 0 then map HOLogic.eq_const Ts @@ -2676,20 +2576,19 @@ (map map_transfer_of_bnf bnfs) dtor_unfold_thms) lthy; - val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs; - val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs; - val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs; - val corec_activephis = - map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis; - val dtor_corec_transfer_thms = - mk_xtor_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis - (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs) - (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs - dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms) - lthy; - val timer = time (timer "relator coinduction"); + fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts; + val export = map (Morphism.term (Local_Theory.target_morphism lthy)) + val ((corecs, (dtor_corec_thms, dtor_corec_unique_thm, dtor_corec_o_Jmap_thms, + dtor_corec_transfer_thms)), lthy) = lthy + |> derive_xtor_co_recs Greatest_FP external_bs mk_Ts (Dss, resDs) bnfs + (export dtors) (export unfolds) + dtor_unfold_unique_thm dtor_unfold_thms dtor_unfold_transfer_thms + dtor_Jmap_thms dtor_Jrel_thms; + + val timer = time (timer "recursor"); + val common_notes = [(dtor_coinductN, [dtor_coinduct_thm]), (dtor_rel_coinductN, [Jrel_coinduct_thm])] @@ -2700,10 +2599,6 @@ [(ctor_dtorN, ctor_dtor_thms), (ctor_exhaustN, ctor_exhaust_thms), (ctor_injectN, ctor_inject_thms), - (dtor_corecN, dtor_corec_thms), - (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms), - (dtor_corec_transferN, dtor_corec_transfer_thms), - (dtor_corec_uniqueN, dtor_corec_unique_thms), (dtor_ctorN, dtor_ctor_thms), (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms), @@ -2721,7 +2616,7 @@ val fp_res = {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = corecs, + ctors = ctors, dtors = dtors, xtor_un_folds_legacy = unfolds, xtor_co_recs = export corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss', diff -r 94535e6dd168 -r 52c5a25e0c96 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:26:22 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Apr 07 17:56:22 2016 +0200 @@ -1202,50 +1202,6 @@ val timer = time (timer "dtor definitions & thms"); - val fst_rec_pair_thms = - let - val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm]; - in - map2 (fn unique => fn fold_ctor => - trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms - end; - - fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_"); - val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind; - - fun mk_rec_strs rec_ss = - @{map 3} (fn ctor => fn prod_s => fn mapx => - mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s)) - ctors rec_ss rec_maps; - - fun rec_spec i T AT = - fold_rev (Term.absfree o Term.dest_Free) rec_ss - (HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts (mk_rec_strs rec_ss) i)); - - val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) = - lthy - |> Local_Theory.open_target |> snd - |> @{fold_map 3} (fn i => fn T => fn AT => - Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs - |>> apsnd split_list o split_list - ||> `Local_Theory.close_target; - - val phi = Proof_Context.export_morphism lthy_old lthy; - val recs = map (Morphism.term phi) rec_frees; - val rec_names = map (fst o dest_Const) recs; - fun mk_recs Ts passives actives = - let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives; - in - @{map 3} (fn name => fn T => fn active => - Const (name, Library.foldr (op -->) - (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active))) - rec_names Ts actives - end; - fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->) - (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); - val rec_defs = map (fn def => - mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) rec_def_frees; - val (((((((((Izs, (Izs1, Izs1'))), (Izs2, Izs2')), xFs), yFs), fs), rec_ss), init_phis), _) = lthy |> mk_Frees "z" Ts @@ -1260,48 +1216,6 @@ val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; - val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks; - val ctor_rec_thms = - let - fun mk_goal i rec_s rec_map ctor x = - let - val lhs = mk_rec rec_ss i $ (ctor $ x); - val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x); - in - mk_Trueprop_eq (lhs, rhs) - end; - val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs; - in - map2 (fn goal => fn foldx => - Variable.add_free_names lthy goal [] - |> (fn vars => Goal.prove_sorry lthy vars [] goal - (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)) - |> Thm.close_derivation) - goals ctor_fold_thms - end; - - val rec_unique_mor_thm = - let - val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs; - val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs (mk_rec_strs rec_ss) id_fs); - fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i); - val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks)); - val vars = fold (Variable.add_free_names lthy) [prem, unique] []; - in - Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique)) - (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms - fold_unique_mor_thm) - |> Thm.close_derivation - end; - - val (ctor_rec_unique_thms, ctor_rec_unique_thm) = - `split_conj_thm (split_conj_prems n - (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) - |> unfold_thms lthy (@{thms convol_o comp_id id_comp comp_assoc fst_convol} @ - map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); - - val timer = time (timer "rec definitions & thms"); - val (ctor_induct_thm, induct_params) = let fun mk_prem phi ctor sets x = @@ -1909,8 +1823,6 @@ val ctor_fold_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP false m ctor_fold_unique_thm ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; - val ctor_rec_o_Imap_thms = mk_xtor_co_iter_o_map_thms Least_FP true m ctor_rec_unique_thm - ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; @@ -1927,19 +1839,17 @@ (map map_transfer_of_bnf bnfs) ctor_fold_thms) lthy; - val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs; - val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs; - val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs; - val rec_activephis = - map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis; - val ctor_rec_transfer_thms = - mk_xtor_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis - (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs) - (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs - ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms) - lthy; + val timer = time (timer "relator induction"); - val timer = time (timer "relator induction"); + fun mk_Ts As = map (typ_subst_atomic (passiveAs ~~ As)) Ts; + val export = map (Morphism.term (Local_Theory.target_morphism lthy)) + val ((recs, (ctor_rec_thms, ctor_rec_unique_thm, ctor_rec_o_Imap_thms, ctor_rec_transfer_thms)), + lthy) = lthy + |> derive_xtor_co_recs Least_FP external_bs mk_Ts (Dss, resDs) bnfs + (export ctors) (export folds) + ctor_fold_unique_thm ctor_fold_thms ctor_fold_transfer_thms ctor_Imap_thms ctor_Irel_thms; + + val timer = time (timer "recursor"); val common_notes = [(ctor_inductN, [ctor_induct_thm]), @@ -1955,11 +1865,7 @@ (ctor_fold_o_mapN, ctor_fold_o_Imap_thms), (ctor_fold_transferN, ctor_fold_transfer_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), - (ctor_rec_o_mapN, ctor_rec_o_Imap_thms), - (ctor_rec_transferN, ctor_rec_transfer_thms), - (ctor_rec_uniqueN, ctor_rec_unique_thms), (ctor_injectN, ctor_inject_thms), - (ctor_recN, ctor_rec_thms), (dtor_ctorN, dtor_ctor_thms), (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms)] @@ -1973,7 +1879,7 @@ val fp_res = {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos, - ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = recs, + ctors = ctors, dtors = dtors, xtor_un_folds_legacy = folds, xtor_co_recs = export recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,