# HG changeset patch # User desharna # Date 1411655756 -7200 # Node ID a1d4e7473c980a8873bccf437fc3d123672033e8 # Parent ea23ce403a3eab554344dee1267055797f7168d1 generate 'corec_transfer' for codatatypes diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/BNF_Fixpoint_Base.thy --- 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 \) (op \)" 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" diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/BNF_Least_Fixpoint.thy --- 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: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Lifting_Product.thy --- 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] diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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; diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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' diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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) diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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)) ^ diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_gfp.ML --- 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; diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_lfp.ML --- 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; diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- 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 diff -r ea23ce403a3e -r a1d4e7473c98 src/HOL/Transfer.thy --- 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