--- a/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 25 16:35:56 2014 +0200
@@ -213,6 +213,28 @@
"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 If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If"
+ unfolding rel_fun_def by simp
+
+lemma Abs_transfer:
+ assumes type_copy1: "type_definition Rep1 Abs1 UNIV"
+ assumes type_copy2: "type_definition Rep2 Abs2 UNIV"
+ shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2"
+ unfolding vimage2p_def rel_fun_def
+ type_definition.Abs_inverse[OF type_copy1 UNIV_I]
+ type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp
+
+lemma Inl_transfer:
+ "rel_fun S (rel_sum S T) Inl Inl"
+ by auto
+
+lemma Inr_transfer:
+ "rel_fun T (rel_sum S T) Inr Inr"
+ by auto
+
+lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
+ unfolding rel_fun_def rel_prod_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:54 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:56 2014 +0200
@@ -189,14 +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 Inl_transfer:
- "rel_fun S (rel_sum S T) Inl Inl"
- by auto
-
-lemma Inr_transfer:
- "rel_fun T (rel_sum S T) Inr Inr"
- 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/Lifting_Product.thy Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Sep 25 16:35:56 2014 +0200
@@ -19,9 +19,7 @@
begin
interpretation lifting_syntax .
-lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
- unfolding rel_fun_def rel_prod_def by simp
-
+declare Pair_transfer [transfer_rule]
declare fst_transfer [transfer_rule]
declare snd_transfer [transfer_rule]
declare case_prod_transfer [transfer_rule]
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 25 16:35:56 2014 +0200
@@ -73,7 +73,8 @@
(term list
* (typ list list * typ list list list list * term list list * term list list list list) option
* (string * term list * term list list
- * ((term list list * term list list list) * typ list)) option)
+ * (((term list list * term list list * term list list list list * term list list list list)
+ * term list list list) * typ list)) option)
* Proof.context
val repair_nullary_single_ctr: typ list list -> typ list list
val mk_corec_p_pred_types: typ list -> int list -> typ list list
@@ -88,8 +89,9 @@
(string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
(term * thm) * Proof.context
val define_corec: 'a * term list * term list list
- * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
- typ list -> term list -> term -> local_theory -> (term * thm) * local_theory
+ * (((term list list * term list list * term list list list list * term list list list list)
+ * term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list ->
+ term list -> term -> local_theory -> (term * thm) * local_theory
val mk_induct_attrs: term list list -> Token.src list
val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
Token.src list * Token.src list
@@ -99,7 +101,9 @@
typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
term list -> thm list -> Proof.context -> lfp_sugar_thms
val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
- string * term list * term list list * ((term list list * term list list list) * typ list) ->
+ string * term list * term list list
+ * (((term list list * term list list * term list list list list * term list list list list)
+ * term list list list) * typ list) ->
thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
@@ -138,6 +142,7 @@
val ctr_transferN = "ctr_transfer";
val disc_transferN = "disc_transfer";
val corec_codeN = "corec_code";
+val corec_transferN = "corec_transfer";
val map_disc_iffN = "map_disc_iff";
val map_selN = "map_sel";
val rec_transferN = "rec_transfer";
@@ -1002,7 +1007,7 @@
val cgssss = map2 (map o map o map o rapp) cs gssss;
val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
in
- ((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy)
+ ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
end;
fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
@@ -1064,7 +1069,7 @@
ctor_rec_absTs reps fss xssss)))
end;
-fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
+fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
let
val nn = length fpTs;
val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
@@ -1485,7 +1490,7 @@
end) (transpose setss)
end;
-fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
+fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
corecs corec_defs export_args lthy =
@@ -1799,7 +1804,7 @@
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,
- ctor_rec_transfer_thms, ...},
+ xtor_co_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
@@ -2005,7 +2010,7 @@
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 =
+ fun mk_co_rec_transfer_goals lthy co_recs =
let
val liveAsBs = filter (op <>) (As ~~ Bs);
val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
@@ -2014,14 +2019,17 @@
|> 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;
+ val co_recBs = map B_ify co_recs;
in
+ (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy)
+ end;
+
+ fun derive_rec_transfer_thms lthy recs rec_defs =
+ let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs 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)
+ mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
+ xtor_co_rec_transfer_thms pre_rel_defs live_nesting_rel_eqs)
|> Conjunction.elim_balanced nn
|> Proof_Context.export names_lthy lthy
|> map Thm.close_derivation
@@ -2038,8 +2046,7 @@
val rec_transfer_thmss =
if live = 0 then replicate nn []
- else
- map single (derive_rec_transfer_thms lthy recs rec_defs ns);
+ else map single (derive_rec_transfer_thms lthy recs rec_defs);
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
@@ -2090,6 +2097,21 @@
rel_injectss rel_distinctss
end;
+ fun derive_corec_transfer_thms lthy corecs corec_defs =
+ let
+ val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;
+ val (_, _, _, (((pgss, pss, qssss, gssss), _), _)) = the corecs_args_types;
+ in
+ Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} =>
+ mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
+ type_definitions corec_defs xtor_co_rec_transfer_thms pre_rel_defs
+ live_nesting_rel_eqs (flat pgss) pss qssss gssss)
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ |> map Thm.close_derivation
+ end;
+
fun derive_note_coinduct_corecs_thms_for_types
((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
@@ -2122,6 +2144,10 @@
val flat_corec_thms = append oo append;
+ val corec_transfer_thmss =
+ if live = 0 then replicate nn []
+ else map single (derive_corec_transfer_thms lthy corecs corec_defs);
+
val ((rel_coinduct_thmss, common_rel_coinduct_thms),
(rel_coinduct_attrs, common_rel_coinduct_attrs)) =
if live = 0 then
@@ -2168,6 +2194,7 @@
(corec_discN, corec_disc_thmss, K []),
(corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
(corec_selN, corec_sel_thmss, K corec_sel_attrs),
+ (corec_transferN, corec_transfer_thmss, K []),
(rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_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:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 25 16:35:56 2014 +0200
@@ -19,6 +19,9 @@
thm list list list -> tactic
val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list ->
+ thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list ->
+ ''a list list list list -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
val mk_ctr_transfer_tac: Proof.context -> thm list -> thm list -> tactic
@@ -214,6 +217,71 @@
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
(map rtac case_splits' @ [K all_tac]) corecs discs);
+fun mk_corec_transfer_tac ctxt actives passives type_definitions corec_defs dtor_corec_transfers
+ rel_pre_T_defs rel_eqs pgs pss qssss gssss =
+ let
+ val num_pgs = length pgs;
+ fun prem_no_of x = 1 + find_index (curry (op =) x) pgs;
+
+ val Inl_Inr_Pair_tac = REPEAT_DETERM o
+ (rtac (mk_rel_funDN 1 @{thm Inl_transfer}) ORELSE'
+ rtac (mk_rel_funDN 1 @{thm Inr_transfer}) ORELSE'
+ rtac (mk_rel_funDN 2 @{thm Pair_transfer}));
+
+ fun mk_unfold_If_tac total pos =
+ HEADGOAL (Inl_Inr_Pair_tac THEN'
+ rtac (mk_rel_funDN 3 @{thm If_transfer}) THEN'
+ select_prem_tac total (dtac asm_rl) pos THEN'
+ dtac rel_funD THEN' atac THEN' atac);
+
+ fun mk_unfold_Inl_Inr_Pair_tac total pos =
+ HEADGOAL (Inl_Inr_Pair_tac THEN'
+ select_prem_tac total (dtac asm_rl) pos THEN'
+ dtac rel_funD THEN' atac THEN' atac);
+
+ fun mk_unfold_arg_tac qs gs =
+ EVERY (map (mk_unfold_If_tac num_pgs o prem_no_of) qs) THEN
+ EVERY (map (mk_unfold_Inl_Inr_Pair_tac num_pgs o prem_no_of) gs);
+
+ fun mk_unfold_ctr_tac type_definition qss gss =
+ HEADGOAL (rtac (mk_rel_funDN 1 (@{thm Abs_transfer} OF
+ [type_definition, type_definition])) THEN' Inl_Inr_Pair_tac) THEN
+ (case (qss, gss) of
+ ([], []) => HEADGOAL (rtac refl)
+ | _ => EVERY (map2 mk_unfold_arg_tac qss gss));
+
+ fun mk_unfold_type_tac type_definition ps qsss gsss =
+ let
+ val p_tacs = map (mk_unfold_If_tac num_pgs o prem_no_of) ps;
+ val qg_tacs = map2 (mk_unfold_ctr_tac type_definition) qsss gsss;
+ fun mk_unfold_ty [] [qg_tac] = qg_tac
+ | mk_unfold_ty (p_tac :: p_tacs) (qg_tac :: qg_tacs) =
+ p_tac THEN qg_tac THEN mk_unfold_ty p_tacs qg_tacs
+ in
+ HEADGOAL (rtac rel_funI) THEN mk_unfold_ty p_tacs qg_tacs
+ end;
+
+ fun mk_unfold_corec_type_tac dtor_corec_transfer corec_def =
+ let
+ val active :: actives' = actives;
+ val dtor_corec_transfer' = cterm_instantiate_pos
+ (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ unfold_thms_tac ctxt [corec_def] THEN
+ HEADGOAL (etac (mk_rel_funDN_rotated (1 + length actives) dtor_corec_transfer')) THEN
+ unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
+ end;
+
+ fun mk_unfold_prop_tac dtor_corec_transfer corec_def =
+ mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN
+ EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss);
+ in
+ HEADGOAL Goal.conjunction_tac THEN
+ EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs)
+ end;
+
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Sep 25 16:35:56 2014 +0200
@@ -478,7 +478,7 @@
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 = [],
- ctor_rec_transfer_thms = []}
+ xtor_co_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:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:56 2014 +0200
@@ -28,7 +28,7 @@
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
dtor_set_induct_thms: thm list,
- ctor_rec_transfer_thms: thm list}
+ xtor_co_rec_transfer_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -220,12 +220,12 @@
xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm,
dtor_set_induct_thms: thm list,
- ctor_rec_transfer_thms: thm list};
+ xtor_co_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, ctor_rec_transfer_thms} =
+ dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -243,7 +243,7 @@
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,
- ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
+ xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_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:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 16:35:56 2014 +0200
@@ -2542,7 +2542,8 @@
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, ctor_rec_transfer_thms = []};
+ dtor_set_induct_thms = dtor_Jset_induct_thms,
+ xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:56 2014 +0200
@@ -1156,7 +1156,7 @@
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
+ in
map3 (fn name => fn T => fn active =>
Const (name, Library.foldr (op -->)
(map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
@@ -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 = [], ctor_rec_transfer_thms = ctor_rec_transfer_thms};
+ dtor_set_induct_thms = [], xtor_co_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:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Thu Sep 25 16:35:56 2014 +0200
@@ -48,7 +48,7 @@
xtor_co_rec_o_map_thms = [ctor_rec_o_map],
rel_xtor_co_induct_thm = xtor_rel_induct,
dtor_set_induct_thms = [],
- ctor_rec_transfer_thms = []};
+ xtor_co_rec_transfer_thms = []};
fun fp_sugar_of_sum ctxt =
let
--- a/src/HOL/Transfer.thy Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 25 16:35:56 2014 +0200
@@ -449,8 +449,7 @@
shows "((A ===> op =) ===> op =) Ex Ex"
using assms unfolding bi_total_def rel_fun_def by fast
-lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
- unfolding rel_fun_def by simp
+declare If_transfer [transfer_rule]
lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
unfolding rel_fun_def by simp