--- 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 \<and> P \<longleftrightarrow> P" "P \<and> top x \<longleftrightarrow> P"
by blast+
+lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
+ using fst_convol unfolding convol_def by simp
+
+lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
+ using snd_convol unfolding convol_def by simp
+
+lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
+ unfolding convol_def by auto
+
+lemma convol_expand_snd':
+ assumes "(fst o f = g)"
+ shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
+proof -
+ from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
+ then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
+ moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
+ moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = 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 \<Longrightarrow> case_sum g (f o Inr) = f"
+ by (auto split: sum.splits)
+
+lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> 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 \<Longrightarrow> 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"
--- 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: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
by fast
-lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
- by (auto split: sum.splits)
-
-lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> 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 \<times> B) ^-1 = B \<times> A"
by fast
--- 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) \<in> R \<Longrightarrow> j \<in> Field R"
unfolding Field_def by auto
-lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
- using fst_convol unfolding convol_def by simp
-
-lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
- using snd_convol unfolding convol_def by simp
-
-lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
- unfolding convol_def by auto
-
-lemma convol_expand_snd':
- assumes "(fst o f = g)"
- shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
-proof -
- from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
- then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
- moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
- moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = 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 \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
unfolding bij_betw_def by auto
@@ -172,19 +152,6 @@
lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
--- 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);
--- 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;
--- /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
--- 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',
--- 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,