--- a/src/HOL/BNF/BNF.thy Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF.thy Thu Jul 25 16:46:53 2013 +0200
@@ -13,7 +13,7 @@
imports More_BNFs
begin
-hide_const (open) vimagep Gr Grp collect fsts snds setl setr
+hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr
convol thePull pick_middlep fstOp sndOp csquare inver
image2 relImage relInvImage prefCl PrefCl Succ Shift shift
--- a/src/HOL/BNF/BNF_Def.thy Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy Thu Jul 25 16:46:53 2013 +0200
@@ -193,20 +193,20 @@
((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
unfolding Func_def by (auto elim: the_inv_into_f_f)
-definition vimagep where
- "vimagep f g R = (\<lambda>x y. R (f x) (g y))"
+definition vimage2p where
+ "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
-lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
- unfolding vimagep_def by -
+lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
+ unfolding vimage2p_def by -
-lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
- unfolding vimagep_def by -
+lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
+ unfolding vimage2p_def by -
-lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
- unfolding fun_rel_def vimagep_def by auto
+lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
+ unfolding fun_rel_def vimage2p_def by auto
-lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
- unfolding vimagep_def convol_def by auto
+lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+ unfolding vimage2p_def convol_def by auto
ML_file "Tools/bnf_def_tactics.ML"
ML_file "Tools/bnf_def.ML"
--- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Thu Jul 25 16:46:53 2013 +0200
@@ -113,6 +113,10 @@
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
+lemma fun_rel_def_butlast:
+ "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
+ unfolding fun_rel_def ..
+
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/BNF_GFP.thy Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Thu Jul 25 16:46:53 2013 +0200
@@ -307,6 +307,27 @@
lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
by auto
+definition image2p where
+ "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
+
+lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
+ unfolding image2p_def by blast
+
+lemma image2p_eqI: "\<lbrakk>fx = f x; gy = g y; R x y\<rbrakk> \<Longrightarrow> (image2p f g R) fx gy"
+ unfolding image2p_def by blast
+
+lemma image2pE: "\<lbrakk>(image2p f g R) fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+ unfolding image2p_def by blast
+
+lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
+ unfolding fun_rel_def image2p_def by auto
+
+lemma convol_image_image2p: "<f o fst, g o snd> ` Collect (split R) \<subseteq> Collect (split (image2p f g R))"
+ unfolding convol_def image2p_def by fastforce
+
+lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
+ unfolding fun_rel_def image2p_def by auto
+
ML_file "Tools/bnf_gfp_util.ML"
ML_file "Tools/bnf_gfp_tactics.ML"
ML_file "Tools/bnf_gfp.ML"
--- a/src/HOL/BNF/BNF_LFP.thy Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Thu Jul 25 16:46:53 2013 +0200
@@ -226,6 +226,12 @@
shows "PROP P x y"
by (rule `(\<And>x y. PROP P x y)`)
+lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
+ unfolding fun_rel_def vimage2p_def by auto
+
+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
+
ML_file "Tools/bnf_lfp_util.ML"
ML_file "Tools/bnf_lfp_tactics.ML"
ML_file "Tools/bnf_lfp.ML"
--- a/src/HOL/BNF/Tools/bnf_def.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Jul 25 16:46:53 2013 +0200
@@ -374,7 +374,7 @@
val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
-val map_transfer_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
+val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 16:46:53 2013 +0200
@@ -217,13 +217,13 @@
val n = length set_map's;
in
REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
- unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
+ unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
- rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
- etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]}))
+ etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
set_map's,
rtac conjI,
EVERY' (map (fn convol =>
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jul 25 16:46:53 2013 +0200
@@ -54,6 +54,7 @@
val ctor_injectN: string
val ctor_foldN: string
val ctor_fold_uniqueN: string
+ val ctor_fold_transferN: string
val ctor_mapN: string
val ctor_map_uniqueN: string
val ctor_recN: string
@@ -82,6 +83,7 @@
val dtor_strong_coinductN: string
val dtor_unfoldN: string
val dtor_unfold_uniqueN: string
+ val dtor_unfold_transferN: string
val exhaustN: string
val foldN: string
val hsetN: string
@@ -169,6 +171,9 @@
val mk_rel_co_induct_thm: 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
+ val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list ->
+ term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
+ Proof.context -> thm list
val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> local_theory -> 'a) ->
@@ -240,6 +245,7 @@
val foldN = "fold"
val unfoldN = unN ^ foldN
val uniqueN = "_unique"
+val transferN = "_transfer"
val simpsN = "simps"
val ctorN = "ctor"
val dtorN = "dtor"
@@ -247,6 +253,8 @@
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val ctor_fold_transferN = ctor_foldN ^ transferN
+val dtor_unfold_transferN = dtor_unfoldN ^ transferN
val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
val ctor_mapN = ctorN ^ "_" ^ mapN
val dtor_mapN = dtorN ^ "_" ^ mapN
@@ -485,6 +493,25 @@
|> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
end;
+fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
+ let
+ val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
+ val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
+ fun flip f x y = if fp = Greatest_FP then f y x else f x y;
+
+ val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
+ fun mk_transfer relphi pre_phi un_fold un_fold' =
+ fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
+ val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
+
+ val goal = fold_rev Logic.all (phis @ pre_phis)
+ (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
+ in
+ Goal.prove_sorry lthy [] [] goal tac
+ |> Thm.close_derivation
+ |> split_conj_thm
+ end;
+
fun fp_bnf construct_fp bs resBs eqs lthy =
let
val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 25 16:46:53 2013 +0200
@@ -72,12 +72,12 @@
val names_lthy = fold Variable.declare_typ deads lthy;
(* tvars *)
- val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
+ val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
(passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy
|> mk_TFrees live
|> apfst (`(chop m))
||> mk_TFrees live
- ||>> apfst (chop m)
+ ||>> apfst (`(chop m))
||> mk_TFrees live
||>> apfst (chop m)
||>> mk_TFrees m
@@ -1762,6 +1762,11 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val unfolds = map (Morphism.term phi) unfold_frees;
val unfold_names = map (fst o dest_Const) unfolds;
+ fun mk_unfolds passives actives =
+ map3 (fn name => fn T => fn active =>
+ Const (name, Library.foldr (op -->)
+ (map2 (curry (op -->)) actives (mk_FTs (passives @ actives)), active --> T)))
+ unfold_names (mk_Ts passives) actives;
fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
@@ -2116,9 +2121,11 @@
val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
val fstsTsTs' = map fst_const prodTsTs';
val sndsTsTs' = map snd_const prodTsTs';
+ val activephiTs = map2 mk_pred2T activeAs activeBs;
val activeJphiTs = map2 mk_pred2T Ts Ts';
- val ((Jphis, activeJphis), names_lthy) = names_lthy
+ val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy
|> mk_Frees "R" JphiTs
+ ||>> mk_Frees "S" activephiTs
||>> mk_Frees "JR" activeJphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val in_rels = map in_rel_of_bnf bnfs;
@@ -2867,6 +2874,14 @@
mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
Jrel_coinduct_tac lthy;
+ val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+ val dtor_unfold_transfer_thms =
+ mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis
+ (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
+ (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
+ dtor_unfold_thms)
+ lthy;
+
val timer = time (timer "relator coinduction");
val common_notes =
@@ -2874,7 +2889,8 @@
(dtor_map_coinductN, [dtor_map_coinduct_thm]),
(dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
(dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
- (rel_coinductN, [Jrel_coinduct_thm])]
+ (rel_coinductN, [Jrel_coinduct_thm]),
+ (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 25 16:46:53 2013 +0200
@@ -115,6 +115,8 @@
val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
thm list -> thm list -> thm list list -> thm list list -> tactic
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
+ val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
val mk_unique_mor_tac: thm list -> thm -> tactic
val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
@@ -1458,4 +1460,23 @@
(in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
end;
+fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
+ let
+ val n = length map_transfers;
+ in
+ unfold_thms_tac ctxt
+ @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+ unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
+ HEADGOAL (EVERY'
+ [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct,
+ EVERY' (map (fn map_transfer => EVERY'
+ [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
+ SELECT_GOAL (unfold_thms_tac ctxt unfolds),
+ rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+ REPEAT_DETERM_N m o rtac @{thm id_transfer},
+ REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
+ etac @{thm predicate2D}, etac @{thm image2pI}])
+ map_transfers)])
+ end;
+
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jul 25 16:46:53 2013 +0200
@@ -42,12 +42,12 @@
val names_lthy = fold Variable.declare_typ deads lthy;
(* tvars *)
- val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
+ val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
activeCs), passiveXs), passiveYs) = names_lthy
|> mk_TFrees live
|> apfst (`(chop m))
||> mk_TFrees live
- ||>> apfst (chop m)
+ ||>> apfst (`(chop m))
||>> mk_TFrees n
||>> mk_TFrees m
||> fst o mk_TFrees m;
@@ -1091,6 +1091,11 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
val folds = map (Morphism.term phi) fold_frees;
val fold_names = map (fst o dest_Const) folds;
+ fun mk_folds passives actives =
+ map3 (fn name => fn T => fn active =>
+ Const (name, Library.foldr (op -->)
+ (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active)))
+ fold_names (mk_Ts passives) actives;
fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
val fold_defs = map (Morphism.thm phi) fold_def_frees;
@@ -1382,9 +1387,11 @@
trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
val IphiTs = map2 mk_pred2T passiveAs passiveBs;
+ val activephiTs = map2 mk_pred2T activeAs activeBs;
val activeIphiTs = map2 mk_pred2T Ts Ts';
- val ((Iphis, activeIphis), names_lthy) = names_lthy
+ val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy
|> mk_Frees "R" IphiTs
+ ||>> mk_Frees "S" activephiTs
||>> mk_Frees "IR" activeIphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
@@ -1801,12 +1808,20 @@
(mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs))
lthy;
+ val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+ val ctor_fold_transfer_thms =
+ mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
+ (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
+ (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
+ lthy;
+
val timer = time (timer "relator induction");
val common_notes =
[(ctor_inductN, [ctor_induct_thm]),
(ctor_induct2N, [ctor_induct2_thm]),
- (rel_inductN, [Irel_induct_thm])]
+ (rel_inductN, [Irel_induct_thm]),
+ (ctor_fold_transferN, ctor_fold_transfer_thms)]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Jul 25 16:46:53 2013 +0200
@@ -34,6 +34,8 @@
thm list -> tactic
val mk_iso_alt_tac: thm list -> thm -> tactic
val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
+ val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
thm list list -> thm list list list -> thm list -> tactic
@@ -838,4 +840,24 @@
IHs ctor_rels rel_mono_strongs)] 1
end;
+fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
+ let
+ val n = length map_transfers;
+ in
+ unfold_thms_tac ctxt
+ @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+ unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+ HEADGOAL (EVERY'
+ [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct,
+ EVERY' (map (fn map_transfer => EVERY'
+ [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
+ SELECT_GOAL (unfold_thms_tac ctxt folds),
+ etac @{thm predicate2D_vimage2p},
+ rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
+ REPEAT_DETERM_N m o rtac @{thm id_transfer},
+ REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
+ atac])
+ map_transfers)])
+ end;
+
end;