--- a/src/HOL/BNF_Def.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Def.thy Thu Sep 25 16:35:53 2014 +0200
@@ -19,6 +19,14 @@
by auto
definition
+ rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+where
+ "rel_sum R1 R2 x y =
+ (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+ | (Inr x, Inr y) \<Rightarrow> R2 x y
+ | _ \<Rightarrow> False)"
+
+definition
rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
where
"rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
--- a/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 16:35:53 2014 +0200
@@ -177,6 +177,9 @@
lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
unfolding fun_eq_iff vimage2p_def o_apply by simp
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+ unfolding rel_fun_def vimage2p_def by auto
+
lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
by (erule arg_cong)
@@ -189,15 +192,27 @@
lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
by (case_tac x) simp+
+lemma case_sum_transfer:
+ "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
+ unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
by (case_tac x) simp+
+lemma case_prod_transfer:
+ "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
+ unfolding rel_fun_def rel_prod_def by simp
+
lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
by (simp add: inj_on_def)
lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
by simp
+lemma comp_transfer:
+ "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
+ unfolding rel_fun_def by simp
+
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_Least_Fixpoint.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:53 2014 +0200
@@ -169,9 +169,6 @@
ultimately show P by (blast intro: assms(3))
qed
-lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
- unfolding rel_fun_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
@@ -184,10 +181,6 @@
lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
unfolding rel_fun_def rel_prod_def by simp
-lemma case_sum_transfer:
- "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
- unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
-
lemma map_sum_transfer:
"rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
@@ -196,10 +189,6 @@
"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_prod_def rel_fun_def convol_def by auto
-lemma comp_transfer:
- "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
- unfolding rel_fun_def by simp
-
lemma Inl_transfer:
"rel_fun S (rel_sum S T) Inl Inl"
by auto
--- a/src/HOL/Basic_BNFs.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Basic_BNFs.thy Thu Sep 25 16:35:53 2014 +0200
@@ -21,14 +21,6 @@
lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
-definition
- rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
-where
- "rel_sum R1 R2 x y =
- (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
- | (Inr x, Inr y) \<Rightarrow> R2 x y
- | _ \<Rightarrow> False)"
-
lemma rel_sum_simps[simp]:
"rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
"rel_sum R1 R2 (Inl a1) (Inr b2) = False"
--- a/src/HOL/Lifting_Product.thy Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Sep 25 16:35:53 2014 +0200
@@ -24,10 +24,7 @@
declare fst_transfer [transfer_rule]
declare snd_transfer [transfer_rule]
-
-lemma case_prod_transfer [transfer_rule]:
- "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
- unfolding rel_fun_def rel_prod_def by simp
+declare case_prod_transfer [transfer_rule]
lemma curry_transfer [transfer_rule]:
"((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 25 16:35:53 2014 +0200
@@ -243,7 +243,7 @@
REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN'
REPEAT_DETERM o atac));
in
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
@{thms exE conjE CollectE}))) THEN
@@ -260,7 +260,7 @@
@{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
set_maps;
in
- REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN
unfold_thms_tac ctxt @{thms rel_fun_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),
@@ -340,7 +340,7 @@
fun mk_set_transfer_tac ctxt in_rel set_maps =
Goal.conjunction_tac 1 THEN
- EVERY (map (fn set_map => HEADGOAL (rtac @{thm rel_funI}) THEN
+ EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN
REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
@{thms exE conjE CollectE}))) THEN
HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 16:35:53 2014 +0200
@@ -140,6 +140,7 @@
val corec_codeN = "corec_code";
val map_disc_iffN = "map_disc_iff";
val map_selN = "map_sel";
+val rec_transferN = "rec_transfer";
val set_casesN = "set_cases";
val set_introsN = "set_intros";
val set_inductN = "set_induct";
@@ -418,9 +419,9 @@
val ks = 1 upto n;
val ms = map length ctr_Tss;
- val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
- val fpBT = B_ify fpT;
+ val fpBT = B_ify_T fpT;
val live_AsBs = filter (op <>) (As ~~ Bs);
val fTs = map (op -->) live_AsBs;
@@ -428,7 +429,7 @@
|> fold (fold Variable.declare_typ) [As, Bs]
|> mk_TFrees 2
||>> mk_Freess "x" ctr_Tss
- ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
+ ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
||>> mk_Frees "f" fTs
||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
||>> yield_singleton (mk_Frees "a") fpT
@@ -461,7 +462,7 @@
end;
val cxIns = map2 (mk_cIn ctor) ks xss;
- val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
+ val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
fun mk_map_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
@@ -1092,10 +1093,12 @@
fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
let
- val B_ify = typ_subst_nonatomic (As ~~ Bs);
- val fpB_Ts = map B_ify fpA_Ts;
- val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
- val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify = Term.subst_atomic_types (As ~~ Bs);
+
+ val fpB_Ts = map B_ify_T fpA_Ts;
+ val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss;
+ val ctrBss = map (map B_ify) ctrAss;
val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
|> mk_Frees "R" (map2 mk_pred2T As Bs)
@@ -1319,7 +1322,8 @@
abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
live_nesting_rel_eqs =
let
- val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+ val fpB_Ts = map B_ify_T fpA_Ts;
val (Rs, IRs, fpAs, fpBs, names_lthy) =
let
@@ -1711,11 +1715,12 @@
val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
val set_bss = map (map (the_default Binding.empty)) set_boss;
- val (((Bs0, Cs), Xs), names_no_defs_lthy) =
+ val ((((Bs0, Cs), Es), Xs), names_no_defs_lthy) =
no_defs_lthy
|> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
|> mk_TFrees num_As
||>> mk_TFrees nn
+ ||>> mk_TFrees nn
||>> variant_tfrees fp_b_names;
fun add_fake_type spec =
@@ -1793,7 +1798,8 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
+ xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
+ ctor_rec_transfer_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -1857,13 +1863,13 @@
if alive then resort_tfree_or_tvar S B else A)
(liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
- val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
val ctors = map (mk_ctor As) ctors0;
val dtors = map (mk_dtor As) dtors0;
val fpTs = map (domain_type o fastype_of) dtors;
- val fpBTs = map B_ify fpTs;
+ val fpBTs = map B_ify_T fpTs;
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
@@ -1999,6 +2005,28 @@
rel_distincts setss =
injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
+ fun derive_rec_transfer_thms lthy recs rec_defs ns =
+ let
+ val liveAsBs = filter (op <>) (As ~~ Bs);
+ val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+
+ val ((Rs, Ss), names_lthy) = lthy
+ |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+ ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
+
+ val recBs = map B_ify recs;
+ val goals = map2 (mk_parametricity_goal lthy (Rs @ Ss)) recs recBs;
+ in
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} =>
+ mk_rec_transfer_tac names_lthy nn ns (map (certify ctxt) Ss)
+ (map (certify ctxt) Rs) rec_defs ctor_rec_transfer_thms pre_rel_defs
+ live_nesting_rel_eqs)
+ |> Conjunction.elim_balanced nn
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
+ end;
+
fun derive_note_induct_recs_thms_for_types
((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
@@ -2008,6 +2036,11 @@
xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
+ val rec_transfer_thmss =
+ if live = 0 then replicate nn []
+ else
+ map single (derive_rec_transfer_thms lthy recs rec_defs ns);
+
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2040,6 +2073,7 @@
val notes =
[(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
(recN, rec_thmss, K rec_attrs),
+ (rec_transferN, rec_transfer_thmss, K []),
(rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
(simpsN, simp_thmss, K [])]
|> massage_multi_notes fp_b_names fpTs;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 25 16:35:53 2014 +0200
@@ -33,6 +33,8 @@
thm list -> tactic
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
+ val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
+ thm list -> thm list -> thm list -> thm list -> tactic
val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -57,6 +59,11 @@
open BNF_Util
open BNF_FP_Util
+val case_sum_transfer = @{thm case_sum_transfer};
+val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", unfolded sum.rel_eq]};
+val case_prod_transfer = @{thm case_prod_transfer};
+val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", unfolded prod.rel_eq]};
+
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
@@ -96,19 +103,19 @@
let
val n = length (tl (prems_of rel_cases));
in
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
HEADGOAL (etac rel_cases) THEN
ALLGOALS (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt cases THEN
ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN
- ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
+ ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac rel_funD))
end;
fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
HEADGOAL Goal.conjunction_tac THEN
- ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
- TRY o (REPEAT_DETERM1 o atac ORELSE'
- K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl)));
+ ALLGOALS (REPEAT o (resolve_tac (rel_funI :: rel_intros) THEN'
+ TRY o (REPEAT_DETERM1 o (atac ORELSE'
+ K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl))));
fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc=
let
@@ -118,7 +125,7 @@
rotate_tac ~1 THEN' etac (rotate_prems 1 notE) THEN' eresolve_tac distinct_disc));
in
HEADGOAL Goal.conjunction_tac THEN
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI} THEN' dtac (rel_sel RS iffD1) THEN'
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI THEN' dtac (rel_sel RS iffD1) THEN'
REPEAT_DETERM o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN
TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
end;
@@ -155,6 +162,39 @@
unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
+fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs
+ rel_eqs =
+ let
+ val ctor_rec_transfers' =
+ map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
+ val ns' = Integer.sum ns;
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ EVERY (map (fn ctor_rec_transfer =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt rec_defs THEN
+ HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN
+ unfold_thms_tac ctxt rel_pre_T_defs THEN
+ EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc)
+ (HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN
+ HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN
+ unfold_thms_tac ctxt rel_eqs THEN
+ EVERY (map (fn n =>
+ REPEAT_DETERM (HEADGOAL
+ (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
+ rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
+ HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
+ HEADGOAL (SELECT_GOAL (HEADGOAL
+ ((REPEAT_DETERM o (atac ORELSE'
+ rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
+ rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE'
+ rtac rel_funI)) THEN_ALL_NEW
+ (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac)))))
+ (1 upto k))))
+ ns 0)))
+ ctor_rec_transfers')
+ end;
+
val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 16:35:53 2014 +0200
@@ -477,7 +477,8 @@
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
- dtor_set_induct_thms = []}
+ dtor_set_induct_thms = [],
+ ctor_rec_transfer_thms = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:53 2014 +0200
@@ -27,7 +27,8 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list}
+ dtor_set_induct_thms: thm list,
+ ctor_rec_transfer_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -218,11 +219,13 @@
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
- dtor_set_induct_thms: thm list};
+ dtor_set_induct_thms: thm list,
+ ctor_rec_transfer_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+ dtor_set_induct_thms, ctor_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -239,7 +242,8 @@
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
- dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
+ dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
+ ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 16:35:53 2014 +0200
@@ -2542,7 +2542,7 @@
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
- dtor_set_induct_thms = dtor_Jset_induct_thms};
+ dtor_set_induct_thms = dtor_Jset_induct_thms, ctor_rec_transfer_thms = []};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 16:35:53 2014 +0200
@@ -932,26 +932,20 @@
fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
dtor_rels =
- let
- val rel_funD = @{thm rel_funD};
- fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
- val rel_funD_n_rotated = rotate_prems 1 oo rel_funD_n;
- in
- CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
- unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
- HEADGOAL (rtac (rel_funD_n (n + 1) dtor_unfold_transfer) THEN'
- EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
- etac (rel_funD_n_rotated 2 @{thm case_sum_transfer}) THEN'
- rtac (rel_funD_n 2 @{thm comp_transfer}) THEN'
- rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
- REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
- REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN'
- rtac @{thm rel_funI} THEN'
- etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
- etac (rel_funD_n 1 @{thm Inr_transfer})))
- (dtor_corec_defs ~~ dtor_unfold_transfer)
- end;
+ CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
+ HEADGOAL (rtac (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
+ etac (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
+ rtac (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
+ rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN'
+ rtac rel_funI THEN'
+ etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
+ etac (mk_rel_funDN 1 @{thm Inr_transfer})))
+ (dtor_corec_defs ~~ dtor_unfold_transfer);
fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
@@ -1113,7 +1107,7 @@
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 rel_funD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
etac @{thm predicate2D}, etac @{thm image2pI}])
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:53 2014 +0200
@@ -1829,7 +1829,7 @@
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
- dtor_set_induct_thms = []};
+ dtor_set_induct_thms = [], ctor_rec_transfer_thms = ctor_rec_transfer_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 25 16:35:53 2014 +0200
@@ -47,7 +47,8 @@
xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
xtor_co_rec_o_map_thms = [ctor_rec_o_map],
rel_xtor_co_induct_thm = xtor_rel_induct,
- dtor_set_induct_thms = []};
+ dtor_set_induct_thms = [],
+ ctor_rec_transfer_thms = []};
fun fp_sugar_of_sum ctxt =
let
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:53 2014 +0200
@@ -705,26 +705,20 @@
fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
ctor_rels =
- let
- val rel_funD = @{thm rel_funD};
- fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
- val rel_funD_n_rotated = rotate_prems ~1 oo rel_funD_n;
- in
- CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
- REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
- unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
- HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
- etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN'
- EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
- etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN'
- rtac (rel_funD_n_rotated 2 @{thm comp_transfer}) THEN'
- rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
- REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
- REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
- rtac @{thm rel_funI} THEN'
- etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
- (ctor_rec_defs ~~ ctor_fold_transfers)
- end;
+ CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
+ HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
+ etac (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
+ etac (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
+ rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
+ rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
+ rtac rel_funI THEN'
+ etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
+ (ctor_rec_defs ~~ ctor_fold_transfers);
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
let val n = length ks;
@@ -754,7 +748,7 @@
[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 rel_funD}) map_transfer),
+ rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
REPEAT_DETERM_N m o rtac @{thm id_transfer},
REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
atac])
--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 25 16:35:53 2014 +0200
@@ -35,11 +35,11 @@
'o) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
- val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
'o -> 'p) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
- val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
'o -> 'p -> 'q) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
@@ -116,13 +116,6 @@
val mk_nthN: int -> term -> int -> term
(*parameterized thms*)
- val mk_Un_upper: int -> int -> thm
- val mk_conjIN: int -> thm
- val mk_nthI: int -> int -> thm
- val mk_nth_conv: int -> int -> thm
- val mk_ordLeq_csum: int -> int -> thm -> thm
- val mk_UnIN: int -> int -> thm
-
val eqTrueI: thm
val eqFalseI: thm
val prod_injectD: thm
@@ -132,11 +125,22 @@
val meta_mp: thm
val meta_spec: thm
val o_apply: thm
+ val rel_funD: thm
+ val rel_funI: thm
val set_mp: thm
val set_rev_mp: thm
val subset_UNIV: thm
+
+ val mk_conjIN: int -> thm
+ val mk_nthI: int -> int -> thm
+ val mk_nth_conv: int -> int -> thm
+ val mk_ordLeq_csum: int -> int -> thm -> thm
+ val mk_rel_funDN: int -> thm -> thm
+ val mk_rel_funDN_rotated: int -> thm -> thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
+ val mk_UnIN: int -> int -> thm
+ val mk_Un_upper: int -> int -> thm
val is_refl_bool: term -> bool
val is_refl: thm -> bool
@@ -528,6 +532,8 @@
val meta_mp = @{thm meta_mp};
val meta_spec = @{thm meta_spec};
val o_apply = @{thm o_apply};
+val rel_funD = @{thm rel_funD};
+val rel_funI = @{thm rel_funI};
val set_mp = @{thm set_mp};
val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
@@ -560,6 +566,10 @@
| mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
[mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
+fun mk_rel_funDN n = funpow n (fn thm => thm RS @{thm rel_funD});
+
+val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;
+
local
fun mk_Un_upper' 0 = subset_refl
| mk_Un_upper' 1 = @{thm Un_upper1}