generate 'rec_transfer' for datatypes
authordesharna
Thu Sep 25 16:35:53 2014 +0200 (2014-09-25)
changeset 58446e89f57d1e46c
parent 58445 86b5b02ef33a
child 58447 ea23ce403a3e
generate 'rec_transfer' for datatypes
src/HOL/BNF_Def.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Basic_BNFs.thy
src/HOL/Lifting_Product.thy
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
     1.1 --- a/src/HOL/BNF_Def.thy	Thu Sep 25 16:35:51 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Thu Sep 25 16:35:53 2014 +0200
     1.3 @@ -19,6 +19,14 @@
     1.4    by auto
     1.5  
     1.6  definition
     1.7 +   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     1.8 +where
     1.9 +   "rel_sum R1 R2 x y =
    1.10 +     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.11 +     | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.12 +     | _ \<Rightarrow> False)"
    1.13 +
    1.14 +definition
    1.15    rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
    1.16  where
    1.17    "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
     2.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:51 2014 +0200
     2.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:53 2014 +0200
     2.3 @@ -177,6 +177,9 @@
     2.4  lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
     2.5    unfolding fun_eq_iff vimage2p_def o_apply by simp
     2.6  
     2.7 +lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
     2.8 +  unfolding rel_fun_def vimage2p_def by auto
     2.9 +
    2.10  lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
    2.11    by (erule arg_cong)
    2.12  
    2.13 @@ -189,15 +192,27 @@
    2.14  lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
    2.15    by (case_tac x) simp+
    2.16  
    2.17 +lemma case_sum_transfer:
    2.18 +  "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
    2.19 +  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
    2.20 +
    2.21  lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
    2.22    by (case_tac x) simp+
    2.23  
    2.24 +lemma case_prod_transfer:
    2.25 +  "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
    2.26 +  unfolding rel_fun_def rel_prod_def by simp
    2.27 +
    2.28  lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
    2.29    by (simp add: inj_on_def)
    2.30  
    2.31  lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
    2.32    by simp
    2.33  
    2.34 +lemma comp_transfer:
    2.35 +  "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
    2.36 +  unfolding rel_fun_def by simp
    2.37 +
    2.38  ML_file "Tools/BNF/bnf_fp_util.ML"
    2.39  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    2.40  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
     3.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:51 2014 +0200
     3.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:53 2014 +0200
     3.3 @@ -169,9 +169,6 @@
     3.4    ultimately show P by (blast intro: assms(3))
     3.5  qed
     3.6  
     3.7 -lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
     3.8 -  unfolding rel_fun_def vimage2p_def by auto
     3.9 -
    3.10  lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    3.11    unfolding vimage2p_def by auto
    3.12  
    3.13 @@ -184,10 +181,6 @@
    3.14  lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
    3.15    unfolding rel_fun_def rel_prod_def by simp
    3.16  
    3.17 -lemma case_sum_transfer:
    3.18 -  "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
    3.19 -  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
    3.20 -
    3.21  lemma map_sum_transfer:
    3.22    "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"
    3.23    unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
    3.24 @@ -196,10 +189,6 @@
    3.25    "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"
    3.26    unfolding rel_prod_def rel_fun_def convol_def by auto
    3.27  
    3.28 -lemma comp_transfer:
    3.29 -  "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
    3.30 -  unfolding rel_fun_def by simp
    3.31 -
    3.32  lemma Inl_transfer:
    3.33    "rel_fun S (rel_sum S T) Inl Inl"
    3.34    by auto
     4.1 --- a/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:51 2014 +0200
     4.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:53 2014 +0200
     4.3 @@ -21,14 +21,6 @@
     4.4  
     4.5  lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
     4.6  
     4.7 -definition
     4.8 -   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
     4.9 -where
    4.10 -   "rel_sum R1 R2 x y =
    4.11 -     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    4.12 -     | (Inr x, Inr y) \<Rightarrow> R2 x y
    4.13 -     | _ \<Rightarrow> False)"
    4.14 -
    4.15  lemma rel_sum_simps[simp]:
    4.16    "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    4.17    "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
     5.1 --- a/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:51 2014 +0200
     5.2 +++ b/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:53 2014 +0200
     5.3 @@ -24,10 +24,7 @@
     5.4  
     5.5  declare fst_transfer [transfer_rule]
     5.6  declare snd_transfer [transfer_rule]
     5.7 -
     5.8 -lemma case_prod_transfer [transfer_rule]:
     5.9 -  "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
    5.10 -  unfolding rel_fun_def rel_prod_def by simp
    5.11 +declare case_prod_transfer [transfer_rule]
    5.12  
    5.13  lemma curry_transfer [transfer_rule]:
    5.14    "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
     6.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
     6.3 @@ -243,7 +243,7 @@
     6.4        REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN'
     6.5          REPEAT_DETERM o atac));
     6.6    in
     6.7 -    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
     6.8 +    REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
     6.9      (HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE
    6.10       REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
    6.11         @{thms exE conjE CollectE}))) THEN
    6.12 @@ -260,7 +260,7 @@
    6.13            @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
    6.14        set_maps;
    6.15    in
    6.16 -    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
    6.17 +    REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN
    6.18      unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
    6.19      HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
    6.20        rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
    6.21 @@ -340,7 +340,7 @@
    6.22  
    6.23  fun mk_set_transfer_tac ctxt in_rel set_maps =
    6.24    Goal.conjunction_tac 1 THEN
    6.25 -  EVERY (map (fn set_map => HEADGOAL (rtac @{thm rel_funI}) THEN
    6.26 +  EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN
    6.27    REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
    6.28      @{thms exE conjE CollectE}))) THEN
    6.29    HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:51 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:53 2014 +0200
     7.3 @@ -140,6 +140,7 @@
     7.4  val corec_codeN = "corec_code";
     7.5  val map_disc_iffN = "map_disc_iff";
     7.6  val map_selN = "map_sel";
     7.7 +val rec_transferN = "rec_transfer";
     7.8  val set_casesN = "set_cases";
     7.9  val set_introsN = "set_intros";
    7.10  val set_inductN = "set_induct";
    7.11 @@ -418,9 +419,9 @@
    7.12        val ks = 1 upto n;
    7.13        val ms = map length ctr_Tss;
    7.14  
    7.15 -      val B_ify = Term.typ_subst_atomic (As ~~ Bs);
    7.16 +      val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
    7.17  
    7.18 -      val fpBT = B_ify fpT;
    7.19 +      val fpBT = B_ify_T fpT;
    7.20        val live_AsBs = filter (op <>) (As ~~ Bs);
    7.21        val fTs = map (op -->) live_AsBs;
    7.22  
    7.23 @@ -428,7 +429,7 @@
    7.24          |> fold (fold Variable.declare_typ) [As, Bs]
    7.25          |> mk_TFrees 2
    7.26          ||>> mk_Freess "x" ctr_Tss
    7.27 -        ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
    7.28 +        ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
    7.29          ||>> mk_Frees "f" fTs
    7.30          ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
    7.31          ||>> yield_singleton (mk_Frees "a") fpT
    7.32 @@ -461,7 +462,7 @@
    7.33          end;
    7.34  
    7.35        val cxIns = map2 (mk_cIn ctor) ks xss;
    7.36 -      val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
    7.37 +      val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
    7.38  
    7.39        fun mk_map_thm ctr_def' cxIn =
    7.40          fold_thms lthy [ctr_def']
    7.41 @@ -1092,10 +1093,12 @@
    7.42  fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
    7.43      ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
    7.44    let
    7.45 -    val B_ify = typ_subst_nonatomic (As ~~ Bs);
    7.46 -    val fpB_Ts = map B_ify fpA_Ts;
    7.47 -    val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
    7.48 -    val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
    7.49 +    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
    7.50 +    val B_ify = Term.subst_atomic_types (As ~~ Bs);
    7.51 +
    7.52 +    val fpB_Ts = map B_ify_T fpA_Ts;
    7.53 +    val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss;
    7.54 +    val ctrBss = map (map B_ify) ctrAss;
    7.55  
    7.56      val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
    7.57        |> mk_Frees "R" (map2 mk_pred2T As Bs)
    7.58 @@ -1319,7 +1322,8 @@
    7.59      abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
    7.60      live_nesting_rel_eqs =
    7.61    let
    7.62 -    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
    7.63 +    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
    7.64 +    val fpB_Ts = map B_ify_T fpA_Ts;
    7.65  
    7.66      val (Rs, IRs, fpAs, fpBs, names_lthy) =
    7.67        let
    7.68 @@ -1711,11 +1715,12 @@
    7.69      val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
    7.70      val set_bss = map (map (the_default Binding.empty)) set_boss;
    7.71  
    7.72 -    val (((Bs0, Cs), Xs), names_no_defs_lthy) =
    7.73 +    val ((((Bs0, Cs), Es), Xs), names_no_defs_lthy) =
    7.74        no_defs_lthy
    7.75        |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
    7.76        |> mk_TFrees num_As
    7.77        ||>> mk_TFrees nn
    7.78 +      ||>> mk_TFrees nn
    7.79        ||>> variant_tfrees fp_b_names;
    7.80  
    7.81      fun add_fake_type spec =
    7.82 @@ -1793,7 +1798,8 @@
    7.83      val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
    7.84               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
    7.85               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
    7.86 -             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
    7.87 +             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
    7.88 +             ctor_rec_transfer_thms, ...},
    7.89             lthy)) =
    7.90        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
    7.91          (map dest_TFree killed_As) fp_eqs no_defs_lthy
    7.92 @@ -1857,13 +1863,13 @@
    7.93            if alive then resort_tfree_or_tvar S B else A)
    7.94          (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
    7.95  
    7.96 -    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
    7.97 +    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
    7.98  
    7.99      val ctors = map (mk_ctor As) ctors0;
   7.100      val dtors = map (mk_dtor As) dtors0;
   7.101  
   7.102      val fpTs = map (domain_type o fastype_of) dtors;
   7.103 -    val fpBTs = map B_ify fpTs;
   7.104 +    val fpBTs = map B_ify_T fpTs;
   7.105  
   7.106      val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
   7.107  
   7.108 @@ -1999,6 +2005,28 @@
   7.109          rel_distincts setss =
   7.110        injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
   7.111  
   7.112 +    fun derive_rec_transfer_thms lthy recs rec_defs ns =
   7.113 +      let
   7.114 +        val liveAsBs = filter (op <>) (As ~~ Bs);
   7.115 +        val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
   7.116 +
   7.117 +        val ((Rs, Ss), names_lthy) = lthy
   7.118 +          |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
   7.119 +          ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
   7.120 +
   7.121 +        val recBs = map B_ify recs;
   7.122 +        val goals = map2 (mk_parametricity_goal lthy (Rs @ Ss)) recs recBs;
   7.123 +      in
   7.124 +        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   7.125 +          (fn {context = ctxt, prems = _} =>
   7.126 +             mk_rec_transfer_tac names_lthy nn ns (map (certify ctxt) Ss)
   7.127 +               (map (certify ctxt) Rs) rec_defs ctor_rec_transfer_thms pre_rel_defs
   7.128 +               live_nesting_rel_eqs)
   7.129 +        |> Conjunction.elim_balanced nn
   7.130 +        |> Proof_Context.export names_lthy lthy
   7.131 +        |> map Thm.close_derivation
   7.132 +      end;
   7.133 +
   7.134      fun derive_note_induct_recs_thms_for_types
   7.135          ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
   7.136            (recs, rec_defs)), lthy) =
   7.137 @@ -2008,6 +2036,11 @@
   7.138              xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
   7.139              type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
   7.140  
   7.141 +        val rec_transfer_thmss =
   7.142 +          if live = 0 then replicate nn []
   7.143 +          else
   7.144 +            map single (derive_rec_transfer_thms lthy recs rec_defs ns);
   7.145 +
   7.146          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   7.147          val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
   7.148  
   7.149 @@ -2040,6 +2073,7 @@
   7.150          val notes =
   7.151            [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
   7.152             (recN, rec_thmss, K rec_attrs),
   7.153 +           (rec_transferN, rec_transfer_thmss, K []),
   7.154             (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
   7.155             (simpsN, simp_thmss, K [])]
   7.156            |> massage_multi_notes fp_b_names fpTs;
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
     8.3 @@ -33,6 +33,8 @@
     8.4      thm list -> tactic
     8.5    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     8.6      tactic
     8.7 +  val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
     8.8 +    thm list -> thm list -> thm list -> thm list -> tactic
     8.9    val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
    8.10      thm list -> thm list -> thm list -> tactic
    8.11    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
    8.12 @@ -57,6 +59,11 @@
    8.13  open BNF_Util
    8.14  open BNF_FP_Util
    8.15  
    8.16 +val case_sum_transfer = @{thm case_sum_transfer};
    8.17 +val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", unfolded sum.rel_eq]};
    8.18 +val case_prod_transfer = @{thm case_prod_transfer};
    8.19 +val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", unfolded prod.rel_eq]};
    8.20 +
    8.21  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    8.22  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    8.23  val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
    8.24 @@ -96,19 +103,19 @@
    8.25    let
    8.26      val n = length (tl (prems_of rel_cases));
    8.27    in
    8.28 -    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
    8.29 +    REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
    8.30      HEADGOAL (etac rel_cases) THEN
    8.31      ALLGOALS (hyp_subst_tac ctxt) THEN
    8.32      unfold_thms_tac ctxt cases THEN
    8.33      ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN
    8.34 -    ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
    8.35 +    ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac rel_funD))
    8.36    end;
    8.37  
    8.38  fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
    8.39    HEADGOAL Goal.conjunction_tac THEN
    8.40 -  ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
    8.41 -    TRY o (REPEAT_DETERM1 o atac ORELSE'
    8.42 -      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl)));
    8.43 +  ALLGOALS (REPEAT o (resolve_tac (rel_funI :: rel_intros) THEN'
    8.44 +    TRY o (REPEAT_DETERM1 o (atac ORELSE'
    8.45 +      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl))));
    8.46  
    8.47  fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc=
    8.48    let
    8.49 @@ -118,7 +125,7 @@
    8.50          rotate_tac ~1 THEN' etac (rotate_prems 1 notE) THEN' eresolve_tac distinct_disc));
    8.51    in
    8.52      HEADGOAL Goal.conjunction_tac THEN
    8.53 -    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI} THEN' dtac (rel_sel RS iffD1) THEN'
    8.54 +    REPEAT_DETERM (HEADGOAL (rtac rel_funI THEN' dtac (rel_sel RS iffD1) THEN'
    8.55        REPEAT_DETERM o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN
    8.56      TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
    8.57    end;
    8.58 @@ -155,6 +162,39 @@
    8.59    unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
    8.60      pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
    8.61  
    8.62 +fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs
    8.63 +    rel_eqs =
    8.64 +  let
    8.65 +    val ctor_rec_transfers' =
    8.66 +      map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
    8.67 +    val ns' = Integer.sum ns;
    8.68 +  in
    8.69 +    HEADGOAL Goal.conjunction_tac THEN
    8.70 +    EVERY (map (fn ctor_rec_transfer =>
    8.71 +        REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
    8.72 +        unfold_thms_tac ctxt rec_defs THEN
    8.73 +        HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN
    8.74 +        unfold_thms_tac ctxt rel_pre_T_defs THEN
    8.75 +        EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc)
    8.76 +            (HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN
    8.77 +             HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN
    8.78 +             unfold_thms_tac ctxt rel_eqs THEN
    8.79 +             EVERY (map (fn n =>
    8.80 +                 REPEAT_DETERM (HEADGOAL
    8.81 +                   (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
    8.82 +                    rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
    8.83 +                 HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
    8.84 +                 HEADGOAL (SELECT_GOAL (HEADGOAL
    8.85 +                   ((REPEAT_DETERM o (atac ORELSE'
    8.86 +                       rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
    8.87 +                       rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE'
    8.88 +                       rtac rel_funI)) THEN_ALL_NEW
    8.89 +                    (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac)))))
    8.90 +               (1 upto k))))
    8.91 +          ns 0)))
    8.92 +      ctor_rec_transfers')
    8.93 +  end;
    8.94 +
    8.95  val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
    8.96  
    8.97  fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:51 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:53 2014 +0200
     9.3 @@ -477,7 +477,8 @@
     9.4          xtor_co_rec_thms = xtor_co_rec_thms,
     9.5          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
     9.6          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
     9.7 -        dtor_set_induct_thms = []}
     9.8 +        dtor_set_induct_thms = [],
     9.9 +        ctor_rec_transfer_thms = []}
    9.10         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    9.11    in
    9.12      (fp_res, lthy)
    10.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:51 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:53 2014 +0200
    10.3 @@ -27,7 +27,8 @@
    10.4       xtor_co_rec_thms: thm list,
    10.5       xtor_co_rec_o_map_thms: thm list,
    10.6       rel_xtor_co_induct_thm: thm,
    10.7 -     dtor_set_induct_thms: thm list}
    10.8 +     dtor_set_induct_thms: thm list,
    10.9 +     ctor_rec_transfer_thms: thm list}
   10.10  
   10.11    val morph_fp_result: morphism -> fp_result -> fp_result
   10.12  
   10.13 @@ -218,11 +219,13 @@
   10.14     xtor_co_rec_thms: thm list,
   10.15     xtor_co_rec_o_map_thms: thm list,
   10.16     rel_xtor_co_induct_thm: thm,
   10.17 -   dtor_set_induct_thms: thm list};
   10.18 +   dtor_set_induct_thms: thm list,
   10.19 +   ctor_rec_transfer_thms: thm list};
   10.20  
   10.21  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
   10.22      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
   10.23 -    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
   10.24 +    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
   10.25 +    dtor_set_induct_thms, ctor_rec_transfer_thms} =
   10.26    {Ts = map (Morphism.typ phi) Ts,
   10.27     bnfs = map (morph_bnf phi) bnfs,
   10.28     ctors = map (Morphism.term phi) ctors,
   10.29 @@ -239,7 +242,8 @@
   10.30     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
   10.31     xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
   10.32     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
   10.33 -   dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
   10.34 +   dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
   10.35 +   ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
   10.36  
   10.37  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   10.38    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
    11.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:51 2014 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:53 2014 +0200
    11.3 @@ -2542,7 +2542,7 @@
    11.4         xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
    11.5         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
    11.6         xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
    11.7 -       dtor_set_induct_thms = dtor_Jset_induct_thms};
    11.8 +       dtor_set_induct_thms = dtor_Jset_induct_thms, ctor_rec_transfer_thms = []};
    11.9    in
   11.10      timer; (fp_res, lthy')
   11.11    end;
    12.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
    12.3 @@ -932,26 +932,20 @@
    12.4  
    12.5  fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
    12.6      dtor_rels =
    12.7 -  let
    12.8 -    val rel_funD = @{thm rel_funD};
    12.9 -    fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
   12.10 -    val rel_funD_n_rotated = rotate_prems 1 oo rel_funD_n;
   12.11 -  in
   12.12 -    CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
   12.13 -        REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
   12.14 -        unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
   12.15 -        HEADGOAL (rtac (rel_funD_n (n + 1) dtor_unfold_transfer) THEN'
   12.16 -          EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
   12.17 -            etac (rel_funD_n_rotated 2 @{thm case_sum_transfer}) THEN'
   12.18 -            rtac (rel_funD_n 2 @{thm comp_transfer}) THEN'
   12.19 -            rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
   12.20 -            REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
   12.21 -            REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN'
   12.22 -            rtac @{thm rel_funI} THEN'
   12.23 -            etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
   12.24 -          etac (rel_funD_n 1 @{thm Inr_transfer})))
   12.25 -      (dtor_corec_defs ~~ dtor_unfold_transfer)
   12.26 -  end;
   12.27 +  CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
   12.28 +      REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
   12.29 +      unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
   12.30 +      HEADGOAL (rtac (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
   12.31 +        EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
   12.32 +          etac (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
   12.33 +          rtac (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
   12.34 +          rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
   12.35 +          REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
   12.36 +          REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN'
   12.37 +          rtac rel_funI THEN'
   12.38 +          etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
   12.39 +        etac (mk_rel_funDN 1 @{thm Inr_transfer})))
   12.40 +    (dtor_corec_defs ~~ dtor_unfold_transfer);
   12.41  
   12.42  fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
   12.43      dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
   12.44 @@ -1113,7 +1107,7 @@
   12.45        EVERY' (map (fn map_transfer => EVERY'
   12.46          [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
   12.47          SELECT_GOAL (unfold_thms_tac ctxt unfolds),
   12.48 -        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
   12.49 +        rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
   12.50          REPEAT_DETERM_N m o rtac @{thm id_transfer},
   12.51          REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
   12.52          etac @{thm predicate2D}, etac @{thm image2pI}])
    13.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:51 2014 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:53 2014 +0200
    13.3 @@ -1829,7 +1829,7 @@
    13.4         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
    13.5         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
    13.6         xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
    13.7 -       dtor_set_induct_thms = []};
    13.8 +       dtor_set_induct_thms = [], ctor_rec_transfer_thms = ctor_rec_transfer_thms};
    13.9    in
   13.10      timer; (fp_res, lthy')
   13.11    end;
    14.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:51 2014 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:53 2014 +0200
    14.3 @@ -47,7 +47,8 @@
    14.4     xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
    14.5     xtor_co_rec_o_map_thms = [ctor_rec_o_map],
    14.6     rel_xtor_co_induct_thm = xtor_rel_induct,
    14.7 -   dtor_set_induct_thms = []};
    14.8 +   dtor_set_induct_thms = [],
    14.9 +   ctor_rec_transfer_thms = []};
   14.10  
   14.11  fun fp_sugar_of_sum ctxt =
   14.12    let
    15.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
    15.3 @@ -705,26 +705,20 @@
    15.4  
    15.5  fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
    15.6      ctor_rels =
    15.7 -  let
    15.8 -    val rel_funD = @{thm rel_funD};
    15.9 -    fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
   15.10 -    val rel_funD_n_rotated = rotate_prems ~1 oo rel_funD_n;
   15.11 -  in
   15.12 -    CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
   15.13 -        REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
   15.14 -        unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
   15.15 -        HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
   15.16 -          etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN'
   15.17 -          EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
   15.18 -            etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN'
   15.19 -            rtac (rel_funD_n_rotated 2 @{thm comp_transfer}) THEN'
   15.20 -            rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
   15.21 -            REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
   15.22 -            REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
   15.23 -            rtac @{thm rel_funI} THEN'
   15.24 -            etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
   15.25 -      (ctor_rec_defs ~~ ctor_fold_transfers)
   15.26 -  end;
   15.27 +  CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
   15.28 +      REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
   15.29 +      unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
   15.30 +      HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
   15.31 +        etac (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
   15.32 +        EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
   15.33 +          etac (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
   15.34 +          rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
   15.35 +          rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
   15.36 +          REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
   15.37 +          REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
   15.38 +          rtac rel_funI THEN'
   15.39 +          etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
   15.40 +    (ctor_rec_defs ~~ ctor_fold_transfers);
   15.41  
   15.42  fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
   15.43    let val n = length ks;
   15.44 @@ -754,7 +748,7 @@
   15.45          [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
   15.46          SELECT_GOAL (unfold_thms_tac ctxt folds),
   15.47          etac @{thm predicate2D_vimage2p},
   15.48 -        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
   15.49 +        rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
   15.50          REPEAT_DETERM_N m o rtac @{thm id_transfer},
   15.51          REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
   15.52          atac])
    16.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 16:35:51 2014 +0200
    16.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 16:35:53 2014 +0200
    16.3 @@ -35,11 +35,11 @@
    16.4        'o) ->
    16.5      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    16.6      'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
    16.7 - val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
    16.8 +  val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
    16.9        'o -> 'p) ->
   16.10      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   16.11      'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
   16.12 - val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
   16.13 +  val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
   16.14        'o -> 'p -> 'q) ->
   16.15      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   16.16      'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
   16.17 @@ -116,13 +116,6 @@
   16.18    val mk_nthN: int -> term -> int -> term
   16.19  
   16.20    (*parameterized thms*)
   16.21 -  val mk_Un_upper: int -> int -> thm
   16.22 -  val mk_conjIN: int -> thm
   16.23 -  val mk_nthI: int -> int -> thm
   16.24 -  val mk_nth_conv: int -> int -> thm
   16.25 -  val mk_ordLeq_csum: int -> int -> thm -> thm
   16.26 -  val mk_UnIN: int -> int -> thm
   16.27 -
   16.28    val eqTrueI: thm
   16.29    val eqFalseI: thm
   16.30    val prod_injectD: thm
   16.31 @@ -132,11 +125,22 @@
   16.32    val meta_mp: thm
   16.33    val meta_spec: thm
   16.34    val o_apply: thm
   16.35 +  val rel_funD: thm
   16.36 +  val rel_funI: thm
   16.37    val set_mp: thm
   16.38    val set_rev_mp: thm
   16.39    val subset_UNIV: thm
   16.40 +
   16.41 +  val mk_conjIN: int -> thm
   16.42 +  val mk_nthI: int -> int -> thm
   16.43 +  val mk_nth_conv: int -> int -> thm
   16.44 +  val mk_ordLeq_csum: int -> int -> thm -> thm
   16.45 +  val mk_rel_funDN: int -> thm -> thm
   16.46 +  val mk_rel_funDN_rotated: int -> thm -> thm
   16.47    val mk_sym: thm -> thm
   16.48    val mk_trans: thm -> thm -> thm
   16.49 +  val mk_UnIN: int -> int -> thm
   16.50 +  val mk_Un_upper: int -> int -> thm
   16.51  
   16.52    val is_refl_bool: term -> bool
   16.53    val is_refl: thm -> bool
   16.54 @@ -528,6 +532,8 @@
   16.55  val meta_mp = @{thm meta_mp};
   16.56  val meta_spec = @{thm meta_spec};
   16.57  val o_apply = @{thm o_apply};
   16.58 +val rel_funD = @{thm rel_funD};
   16.59 +val rel_funI = @{thm rel_funI};
   16.60  val set_mp = @{thm set_mp};
   16.61  val set_rev_mp = @{thm set_rev_mp};
   16.62  val subset_UNIV = @{thm subset_UNIV};
   16.63 @@ -560,6 +566,10 @@
   16.64    | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
   16.65      [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
   16.66  
   16.67 +fun mk_rel_funDN n = funpow n (fn thm => thm RS @{thm rel_funD});
   16.68 +
   16.69 +val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;
   16.70 +
   16.71  local
   16.72    fun mk_Un_upper' 0 = subset_refl
   16.73      | mk_Un_upper' 1 = @{thm Un_upper1}