# HG changeset patch
# User wenzelm
# Date 1411657664 -7200
# Node ID 75b92e25f59f6f27326724b37d08a1f97c801c06
# Parent  e2d3c296b9fefa383f1463ecd88c38d55d409470# Parent  22424e43038d41315443418ab4f9fa6f4511dc24
merged

diff -r 22424e43038d -r 75b92e25f59f Admin/isatest/isatest-settings
--- a/Admin/isatest/isatest-settings	Thu Sep 25 15:01:42 2014 +0200
+++ b/Admin/isatest/isatest-settings	Thu Sep 25 17:07:44 2014 +0200
@@ -24,7 +24,8 @@
 krauss@in.tum.de \
 noschinl@in.tum.de \
 kuncar@in.tum.de \
-ns441@cam.ac.uk"
+ns441@cam.ac.uk \
+traytel@in.tum.de"
 
 LOGPREFIX=$HOME/log
 MASTERLOG=$LOGPREFIX/isatest.log
diff -r 22424e43038d -r 75b92e25f59f src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -1014,6 +1014,9 @@
 (The @{text "[code]"} attribute is set by the @{text code} plugin,
 Section~\ref{ssec:code-generator}.)
 
+\item[@{text "t."}\hthm{rec_transfer}\rm:] ~ \\
+@{thm list.rec_transfer[no_vars]}
+
 \end{description}
 \end{indentblock}
 
@@ -1842,6 +1845,9 @@
 @{thm llist.corec_sel(1)[no_vars]} \\
 @{thm llist.corec_sel(2)[no_vars]}
 
+\item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
+@{thm llist.corec_transfer[no_vars]}
+
 \end{description}
 \end{indentblock}
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Def.thy	Thu Sep 25 17:07:44 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))"
diff -r 22424e43038d -r 75b92e25f59f src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 17:07:44 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,49 @@
 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
+
+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 22424e43038d -r 75b92e25f59f src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -169,15 +169,26 @@
   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
 
 lemma id_transfer: "rel_fun A A id id"
   unfolding rel_fun_def by simp
 
+lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
+  unfolding rel_fun_def rel_prod_def by simp
+
+lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
+  unfolding rel_fun_def rel_prod_def by simp
+
+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)
+
+lemma convol_transfer:
+  "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 ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   by (rule ssubst)
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Basic_BNFs.thy	Thu Sep 25 17:07:44 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"
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Datatype_Examples/Compat.thy
--- a/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -40,10 +40,10 @@
 export_code old_len checking SML OCaml? Haskell? Scala
 
 lemma "Old_Nl = Old_Cns x xs"
-  nitpick [expect = genuine]
+  nitpick (* [expect = genuine] *)
   quickcheck [exhaustive, expect = counterexample]
   quickcheck [random, expect = counterexample]
-  quickcheck [narrowing, expect = counterexample]
+  quickcheck [narrowing (* , expect = counterexample *)]
   oops
 
 lemma "old_len xs = size xs"
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -997,6 +997,10 @@
   finally show ?thesis by auto
 qed
 
+lemma (in ordered_comm_monoid_add) setsum_pos: 
+  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
+  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
+
 
 subsubsection {* Cardinality of products *}
 
@@ -1192,8 +1196,4 @@
   "finite S ==> (setprod f S > 0) = (ALL x : S. f x > (0::nat))"
 using setprod_zero_iff by(simp del:neq0_conv add:neq0_conv[symmetric])
 
-lemma (in ordered_comm_monoid_add) setsum_pos: 
-  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
-  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
-
 end
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -285,6 +285,12 @@
       setsum_product)
 qed
 
+lemma Sum_any_eq_zero_iff [simp]: 
+  fixes f :: "'a \<Rightarrow> nat"
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "Sum_any f = 0 \<longleftrightarrow> f = (\<lambda>_. 0)"
+  using assms by (simp add: Sum_any.expand_set fun_eq_iff)
+
 
 subsection \<open>Concrete product\<close>
 
@@ -337,4 +343,15 @@
   shows "f a \<noteq> 0"
   using assms Prod_any_zero [of f] by blast
 
+lemma power_Sum_any:
+  assumes "finite {a. f a \<noteq> 0}"
+  shows "c ^ (\<Sum>a. f a) = (\<Prod>a. c ^ f a)"
+proof -
+  have "{a. c ^ f a \<noteq> 1} \<subseteq> {a. f a \<noteq> 0}"
+    by (auto intro: ccontr)
+  with assms show ?thesis
+    by (simp add: Sum_any.expand_set Prod_any.expand_superset power_setsum)
+qed
+
 end
+
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/More_List.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -182,47 +182,86 @@
 
 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a"
 where
-  "nth_default x xs n = (if n < length xs then xs ! n else x)"
-
-lemma nth_default_Nil [simp]:
-  "nth_default y [] n = y"
-  by (simp add: nth_default_def)
-
-lemma nth_default_Cons_0 [simp]:
-  "nth_default y (x # xs) 0 = x"
-  by (simp add: nth_default_def)
-
-lemma nth_default_Cons_Suc [simp]:
-  "nth_default y (x # xs) (Suc n) = nth_default y xs n"
-  by (simp add: nth_default_def)
-
-lemma nth_default_map_eq:
-  "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)"
-  by (simp add: nth_default_def)
-
-lemma nth_default_strip_while_eq [simp]:
-  "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n"
-proof -
-  from split_strip_while_append obtain ys zs
-    where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast
-  then show ?thesis by (simp add: nth_default_def not_less nth_append)
-qed
-
-lemma nth_default_Cons:
-  "nth_default y (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default y xs n')"
-  by (simp split: nat.split)
+  "nth_default dflt xs n = (if n < length xs then xs ! n else dflt)"
 
 lemma nth_default_nth:
-  "n < length xs \<Longrightarrow> nth_default y xs n = xs ! n"
+  "n < length xs \<Longrightarrow> nth_default dflt xs n = xs ! n"
   by (simp add: nth_default_def)
 
 lemma nth_default_beyond:
-  "length xs \<le> n \<Longrightarrow> nth_default y xs n = y"
+  "length xs \<le> n \<Longrightarrow> nth_default dflt xs n = dflt"
+  by (simp add: nth_default_def)
+
+lemma nth_default_Nil [simp]:
+  "nth_default dflt [] n = dflt"
+  by (simp add: nth_default_def)
+
+lemma nth_default_Cons:
+  "nth_default dflt (x # xs) n = (case n of 0 \<Rightarrow> x | Suc n' \<Rightarrow> nth_default dflt xs n')"
+  by (simp add: nth_default_def split: nat.split)
+
+lemma nth_default_Cons_0 [simp]:
+  "nth_default dflt (x # xs) 0 = x"
+  by (simp add: nth_default_Cons)
+
+lemma nth_default_Cons_Suc [simp]:
+  "nth_default dflt (x # xs) (Suc n) = nth_default dflt xs n"
+  by (simp add: nth_default_Cons)
+
+lemma nth_default_replicate_dflt [simp]:
+  "nth_default dflt (replicate n dflt) m = dflt"
   by (simp add: nth_default_def)
 
+lemma nth_default_append:
+  "nth_default dflt (xs @ ys) n =
+    (if n < length xs then nth xs n else nth_default dflt ys (n - length xs))"
+  by (auto simp add: nth_default_def nth_append)
+
+lemma nth_default_append_trailing [simp]:
+  "nth_default dflt (xs @ replicate n dflt) = nth_default dflt xs"
+  by (simp add: fun_eq_iff nth_default_append) (simp add: nth_default_def)
+
+lemma nth_default_snoc_default [simp]:
+  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
+  by (auto simp add: nth_default_def fun_eq_iff nth_append)
+
+lemma nth_default_eq_dflt_iff:
+  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
+  by (simp add: nth_default_def)
+
+lemma in_enumerate_iff_nth_default_eq:
+  "x \<noteq> dflt \<Longrightarrow> (n, x) \<in> set (enumerate 0 xs) \<longleftrightarrow> nth_default dflt xs n = x"
+  by (auto simp add: nth_default_def in_set_conv_nth enumerate_eq_zip)
+
+lemma last_conv_nth_default:
+  assumes "xs \<noteq> []"
+  shows "last xs = nth_default dflt xs (length xs - 1)"
+  using assms by (simp add: nth_default_def last_conv_nth)
+  
+lemma nth_default_map_eq:
+  "f dflt' = dflt \<Longrightarrow> nth_default dflt (map f xs) n = f (nth_default dflt' xs n)"
+  by (simp add: nth_default_def)
+
+lemma finite_nth_default_neq_default [simp]:
+  "finite {k. nth_default dflt xs k \<noteq> dflt}"
+  by (simp add: nth_default_def)
+
+lemma sorted_list_of_set_nth_default:
+  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (enumerate 0 xs))"
+  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth
+    sorted_filter distinct_map_filter enumerate_eq_zip intro: rev_image_eqI)
+
+lemma map_nth_default:
+  "map (nth_default x xs) [0..<length xs] = xs"
+proof -
+  have *: "map (nth_default x xs) [0..<length xs] = map (List.nth xs) [0..<length xs]"
+    by (rule map_cong) (simp_all add: nth_default_nth)
+  show ?thesis by (simp add: * map_nth)
+qed
+
 lemma range_nth_default [simp]:
   "range (nth_default dflt xs) = insert dflt (set xs)"
-  by (auto simp add: nth_default_def[abs_def] in_set_conv_nth)
+  by (auto simp add: nth_default_def [abs_def] in_set_conv_nth)
 
 lemma nth_strip_while:
   assumes "n < length (strip_while P xs)"
@@ -241,25 +280,59 @@
   by (subst (2) length_rev[symmetric])
     (simp add: strip_while_def length_dropWhile_le del: length_rev)
 
-lemma finite_nth_default_neq_default [simp]:
-  "finite {k. nth_default dflt xs k \<noteq> dflt}"
-  by (simp add: nth_default_def)
-
-lemma sorted_list_of_set_nth_default:
-  "sorted_list_of_set {k. nth_default dflt xs k \<noteq> dflt} = map fst (filter (\<lambda>(_, x). x \<noteq> dflt) (zip [0..<length xs] xs))"
-  by (rule sorted_distinct_set_unique) (auto simp add: nth_default_def in_set_conv_nth sorted_filter distinct_map_filter intro: rev_image_eqI)
-
-lemma nth_default_snoc_default [simp]:
-  "nth_default dflt (xs @ [dflt]) = nth_default dflt xs"
-  by (auto simp add: nth_default_def fun_eq_iff nth_append)
-
 lemma nth_default_strip_while_dflt [simp]:
- "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
+  "nth_default dflt (strip_while (op = dflt) xs) = nth_default dflt xs"
   by (induct xs rule: rev_induct) auto
 
-lemma nth_default_eq_dflt_iff:
-  "nth_default dflt xs k = dflt \<longleftrightarrow> (k < length xs \<longrightarrow> xs ! k = dflt)"
-  by (simp add: nth_default_def)
+lemma nth_default_eq_iff:
+  "nth_default dflt xs = nth_default dflt ys
+     \<longleftrightarrow> strip_while (HOL.eq dflt) xs = strip_while (HOL.eq dflt) ys" (is "?P \<longleftrightarrow> ?Q")
+proof
+  let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+  assume ?P
+  then have eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+    by simp
+  have len: "length ?xs = length ?ys"
+  proof (rule ccontr)
+    assume len: "length ?xs \<noteq> length ?ys"
+    { fix xs ys :: "'a list"
+      let ?xs = "strip_while (HOL.eq dflt) xs" and ?ys = "strip_while (HOL.eq dflt) ys"
+      assume eq: "nth_default dflt ?xs = nth_default dflt ?ys"
+      assume len: "length ?xs < length ?ys"
+      then have "length ?ys > 0" by arith
+      then have "?ys \<noteq> []" by simp
+      with last_conv_nth_default [of ?ys dflt]
+      have "last ?ys = nth_default dflt ?ys (length ?ys - 1)"
+        by auto
+      moreover from `?ys \<noteq> []` no_trailing_strip_while [of "HOL.eq dflt" ys]
+        have "last ?ys \<noteq> dflt" by (simp add: no_trailing_unfold)
+      ultimately have "nth_default dflt ?xs (length ?ys - 1) \<noteq> dflt"
+        using eq by simp
+      moreover from len have "length ?ys - 1 \<ge> length ?xs" by simp
+      ultimately have False by (simp only: nth_default_beyond) simp
+    } 
+    from this [of xs ys] this [of ys xs] len eq show False
+      by (auto simp only: linorder_class.neq_iff)
+  qed
+  then show ?Q
+  proof (rule nth_equalityI [rule_format])
+    fix n
+    assume "n < length ?xs"
+    moreover with len have "n < length ?ys"
+      by simp
+    ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
+      and ys: "nth_default dflt ?ys n = ?ys ! n"
+      by (simp_all only: nth_default_nth)
+    with eq show "?xs ! n = ?ys ! n"
+      by simp
+  qed
+next
+  assume ?Q
+  then have "nth_default dflt (strip_while (HOL.eq dflt) xs) = nth_default dflt (strip_while (HOL.eq dflt) ys)"
+    by simp
+  then show ?P
+    by simp
+qed
 
 end
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Library/Tree.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -14,6 +14,16 @@
   | "right Leaf = Leaf"
 datatype_compat tree
 
+text{* Can be seen as counting the number of leaves rather than nodes: *}
+
+definition size1 :: "'a tree \<Rightarrow> nat" where
+"size1 t = size t + 1"
+
+lemma size1_simps[simp]:
+  "size1 \<langle>\<rangle> = 1"
+  "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
+by (simp_all add: size1_def)
+
 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
 by (cases t) auto
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Lifting_Product.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -19,18 +19,10 @@
 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
-
-lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
-  unfolding rel_fun_def rel_prod_def by simp
-
-lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
-  unfolding rel_fun_def rel_prod_def by simp
-
-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 Pair_transfer [transfer_rule]
+declare fst_transfer [transfer_rule]
+declare snd_transfer [transfer_rule]
+declare case_prod_transfer [transfer_rule]
 
 lemma curry_transfer [transfer_rule]:
   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
diff -r 22424e43038d -r 75b92e25f59f src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/List.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -2796,6 +2796,10 @@
   "fold g (map f xs) = fold (g o f) xs"
   by (induct xs) simp_all
 
+lemma fold_filter:
+  "fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
+  by (induct xs) simp_all
+
 lemma fold_rev:
   assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y"
   shows "fold f (rev xs) = fold f xs"
@@ -2942,6 +2946,10 @@
   "foldr g (map f xs) a = foldr (g o f) xs a"
   by (simp add: foldr_conv_fold fold_map rev_map)
 
+lemma foldr_filter:
+  "foldr f (filter P xs) = foldr (\<lambda>x. if P x then f x else id) xs"
+  by (simp add: foldr_conv_fold rev_filter fold_filter)
+  
 lemma foldl_map [code_unfold]:
   "foldl g a (map f xs) = foldl (\<lambda>a x. g a (f x)) a xs"
   by (simp add: foldl_conv_fold fold_map comp_def)
@@ -3030,6 +3038,7 @@
   "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
   by (induct n) simp_all
 
+ 
 lemma nth_take_lemma:
   "k <= length xs ==> k <= length ys ==>
      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
@@ -3479,6 +3488,18 @@
   by (induct xs rule: remdups_adj.induct, 
       auto simp add: injD[OF assms])
 
+lemma remdups_upt [simp]:
+  "remdups [m..<n] = [m..<n]"
+proof (cases "m \<le> n")
+  case False then show ?thesis by simp
+next
+  case True then obtain q where "n = m + q"
+    by (auto simp add: le_iff_add)
+  moreover have "remdups [m..<m + q] = [m..<m + q]"
+    by (induct q) simp_all
+  ultimately show ?thesis by simp
+qed
+
 
 subsubsection {* @{const insert} *}
 
@@ -3699,6 +3720,15 @@
 lemma length_replicate [simp]: "length (replicate n x) = n"
 by (induct n) auto
 
+lemma replicate_eqI:
+  assumes "length xs = n" and "\<And>y. y \<in> set xs \<Longrightarrow> y = x"
+  shows "xs = replicate n x"
+using assms proof (induct xs arbitrary: n)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) then show ?case by (cases n) simp_all
+qed
+
 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
 by (rule exI[of _ "replicate n undefined"]) simp
 
@@ -3951,6 +3981,18 @@
   "distinct (enumerate n xs)"
   by (simp add: enumerate_eq_zip distinct_zipI1)
 
+lemma enumerate_append_eq:
+  "enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
+  unfolding enumerate_eq_zip apply auto
+  apply (subst zip_append [symmetric]) apply simp
+  apply (subst upt_add_eq_append [symmetric])
+  apply (simp_all add: ac_simps)
+  done
+
+lemma enumerate_map_upt:
+  "enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
+  by (cases "n \<le> m") (simp_all add: zip_map2 zip_same_conv_map enumerate_eq_zip)
+  
 
 subsubsection {* @{const rotate1} and @{const rotate} *}
 
@@ -4755,6 +4797,10 @@
 lemma sorted_upt[simp]: "sorted[i..<j]"
 by (induct j) (simp_all add:sorted_append)
 
+lemma sort_upt [simp]:
+  "sort [m..<n] = [m..<n]"
+  by (rule sorted_sort_id) simp
+
 lemma sorted_upto[simp]: "sorted[i..j]"
 apply(induct i j rule:upto.induct)
 apply(subst upto.simps)
@@ -4777,6 +4823,10 @@
   qed
 qed
 
+lemma sorted_enumerate [simp]:
+  "sorted (map fst (enumerate n xs))"
+  by (simp add: enumerate_eq_zip)
+
 
 subsubsection {* @{const transpose} on sorted lists *}
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Power.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -795,6 +795,10 @@
     by simp
 qed
 
+lemma power_setsum:
+  "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
+  by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
+
 lemma setprod_gen_delta:
   assumes fS: "finite S"
   shows "setprod (\<lambda>k. if k=a then b k else c) S = (if a \<in> S then (b a ::'a::comm_monoid_mult) * c^ (card S - 1) else c^ card S)"
diff -r 22424e43038d -r 75b92e25f59f src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/SMT.thy	Thu Sep 25 17:07:44 2014 +0200
@@ -183,7 +183,7 @@
 *}
 
 declare [[cvc3_options = ""]]
-declare [[cvc4_options = ""]]
+declare [[cvc4_options = "--full-saturate-quant --quant-cf"]]
 declare [[veriT_options = ""]]
 declare [[z3_options = ""]]
 
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 17:07:44 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'
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 17:07:44 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,8 +142,10 @@
 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";
 val set_casesN = "set_cases";
 val set_introsN = "set_intros";
 val set_inductN = "set_induct";
@@ -418,9 +424,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 +434,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 +467,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']
@@ -1001,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 =
@@ -1063,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)));
@@ -1092,10 +1098,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 +1327,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
@@ -1481,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 =
@@ -1711,11 +1720,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 +1803,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,
+             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
@@ -1857,13 +1868,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 +2010,31 @@
         rel_distincts setss =
       injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
 
+    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));
+
+        val ((Rs, Ss), names_lthy) = lthy
+          |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+          ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
+
+        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 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
+      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 +2044,10 @@
             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);
+
         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 +2080,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;
@@ -2056,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) =
@@ -2088,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
@@ -2134,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 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 17:07:44 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
@@ -33,6 +36,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 +62,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 +106,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 +128,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 +165,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 =
@@ -174,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 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 17:07:44 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 = [],
+        xtor_co_rec_transfer_thms = []}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 17:07:44 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,
+     xtor_co_rec_transfer_thms: thm list}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
 
@@ -62,6 +63,7 @@
   val ctor_map_uniqueN: string
   val ctor_recN: string
   val ctor_rec_o_mapN: string
+  val ctor_rec_transferN: string
   val ctor_rec_uniqueN: string
   val ctor_relN: string
   val ctor_rel_inductN: string
@@ -71,6 +73,7 @@
   val dtor_coinductN: string
   val dtor_corecN: string
   val dtor_corec_o_mapN: string
+  val dtor_corec_transferN: string
   val dtor_corec_uniqueN: string
   val dtor_ctorN: string
   val dtor_exhaustN: string
@@ -138,6 +141,8 @@
   val mk_proj: typ -> int -> int -> term
 
   val mk_convol: term * term -> term
+  val mk_rel_prod: term -> term -> term
+  val mk_rel_sum: term -> term -> term
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
@@ -174,9 +179,9 @@
   val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
-  val mk_un_fold_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
-    term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
-    Proof.context -> thm list
+  val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
+    term list -> term list -> term list -> term list ->
+    ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
@@ -214,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,
+   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} =
+    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+    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,
@@ -235,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,
+   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)) ^
@@ -292,9 +300,11 @@
 val corecN = coN ^ recN
 val ctor_recN = ctorN ^ "_" ^ recN
 val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
+val ctor_rec_transferN = ctor_recN ^ transferN
 val ctor_rec_uniqueN = ctor_recN ^ uniqueN
 val dtor_corecN = dtorN ^ "_" ^ corecN
 val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
+val dtor_corec_transferN = dtor_corecN ^ transferN
 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
 
 val ctor_dtorN = ctorN ^ "_" ^ dtorN
@@ -376,6 +386,20 @@
     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
   in Const (@{const_name convol}, convolT) $ f $ g end;
 
+fun mk_rel_prod R S =
+  let
+    val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+    val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+    val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2));
+  in Const (@{const_name rel_prod}, rel_prodT) $ R $ S end;
+
+fun mk_rel_sum R S =
+  let
+    val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+    val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+    val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2));
+  in Const (@{const_name rel_sum}, rel_sumT) $ R $ S end;
+
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
 
@@ -498,18 +522,18 @@
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
-fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
+fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
   let
-    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
+    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
     fun flip f x y = if fp = Greatest_FP then f y x else f x y;
 
-    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
+    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
     fun mk_transfer relphi pre_phi un_fold un_fold' =
       fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
-    val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
+    val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds';
 
-    val goal = fold_rev Logic.all (phis @ pre_phis)
+    val goal = fold_rev Logic.all (phis @ pre_ophis)
       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   in
     Goal.prove_sorry lthy [] [] goal tac
@@ -607,7 +631,7 @@
     val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
 
-    val Dss = map3 (append oo map o nth) livess kill_poss deadss;
+    val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
       #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 17:07:44 2014 +0200
@@ -1541,6 +1541,14 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val corecs = map (Morphism.term phi) corec_frees;
     val corec_names = map (fst o dest_Const) corecs;
+    fun mk_corecs Ts passives actives =
+      let val Tactives = map2 (curry mk_sumT) Ts actives;
+      in
+        map3 (fn name => fn T => fn active =>
+          Const (name, Library.foldr (op -->)
+            (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
+        corec_names Ts actives
+      end;
     fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
     val corec_defs = map (fn def =>
@@ -2474,16 +2482,28 @@
       sym_map_comps map_cong0s;
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+    val Jrels = if m = 0 then map HOLogic.eq_const Ts
+      else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
 
     val dtor_unfold_transfer_thms =
-      mk_un_fold_transfer_thms Greatest_FP rels activephis
-        (if m = 0 then map HOLogic.eq_const Ts
-          else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
+      mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
         (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
           (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
         lthy;
 
+    val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
+    val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
+    val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
+    val corec_activephis =
+      map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
+    val dtor_corec_transfer_thms =
+      mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
+        (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
+        (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs
+           dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms)
+        lthy;
+
     val timer = time (timer "relator coinduction");
 
     val common_notes =
@@ -2498,6 +2518,7 @@
       (ctor_exhaustN, ctor_exhaust_thms),
       (ctor_injectN, ctor_inject_thms),
       (dtor_corecN, dtor_corec_thms),
+      (dtor_corec_transferN, dtor_corec_transfer_thms),
       (dtor_ctorN, dtor_ctor_thms),
       (dtor_exhaustN, dtor_exhaust_thms),
       (dtor_injectN, dtor_inject_thms),
@@ -2521,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};
+       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 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 17:07:44 2014 +0200
@@ -28,6 +28,8 @@
   val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic
   val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic
   val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
+  val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
+    thm list -> tactic
   val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -609,7 +611,7 @@
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
-            rtac equalityI, rtac subsetI, etac thin_rl, 
+            rtac equalityI, rtac subsetI, etac thin_rl,
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
@@ -926,7 +928,24 @@
   unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
   ALLGOALS (TRY o
-    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
+    FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]);
+
+fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers
+    dtor_rels =
+  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 =
@@ -991,7 +1010,7 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
+fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss
   dtor_unfolds dtor_maps in_rels =
   let
     val n = length ks;
@@ -1088,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}])
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 17:07:44 2014 +0200
@@ -1154,6 +1154,14 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val recs = map (Morphism.term phi) rec_frees;
     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
+        map3 (fn name => fn T => fn active =>
+          Const (name, Library.foldr (op -->)
+            (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
+        rec_names Ts actives
+      end;
     fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
     val rec_defs = map (fn def =>
@@ -1764,18 +1772,31 @@
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val ctor_fold_transfer_thms =
-      mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
+      mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
         (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
           (map map_transfer_of_bnf bnfs) ctor_fold_thms)
         lthy;
 
+    val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs;
+    val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs;
+    val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs;
+    val rec_activephis =
+      map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
+    val ctor_rec_transfer_thms =
+      mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
+        (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
+        (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
+           ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)
+        lthy;
+
     val timer = time (timer "relator induction");
 
     val common_notes =
       [(ctor_inductN, [ctor_induct_thm]),
       (ctor_induct2N, [ctor_induct2_thm]),
       (ctor_fold_transferN, ctor_fold_transfer_thms),
+      (ctor_rec_transferN, ctor_rec_transfer_thms),
       (ctor_rel_inductN, [Irel_induct_thm])]
       |> map (fn (thmN, thms) =>
         ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
@@ -1808,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 = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 17:07:44 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 = [],
+   xtor_co_rec_transfer_thms = []};
 
 fun fp_sugar_of_sum ctxt =
   let
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 17:07:44 2014 +0200
@@ -22,6 +22,8 @@
   val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
     thm list -> tactic
   val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
+  val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
+    thm list -> tactic
   val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -701,6 +703,23 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
+fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
+    ctor_rels =
+  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;
   in
@@ -729,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])
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 17:07:44 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}
diff -r 22424e43038d -r 75b92e25f59f src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/HOL/Transfer.thy	Thu Sep 25 17:07:44 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
@@ -458,9 +457,7 @@
 lemma id_transfer [transfer_rule]: "(A ===> A) id id"
   unfolding rel_fun_def by simp
 
-lemma comp_transfer [transfer_rule]:
-  "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
-  unfolding rel_fun_def by simp
+declare comp_transfer [transfer_rule]
 
 lemma fun_upd_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
diff -r 22424e43038d -r 75b92e25f59f src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Sep 25 15:01:42 2014 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Sep 25 17:07:44 2014 +0200
@@ -478,7 +478,7 @@
 
 val dummyt = Const ("dummy", dummyT);
 
-fun extract thms thy =
+fun extract thm_vss thy =
   let
     val thy' = add_syntax thy;
     val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
@@ -769,7 +769,7 @@
 
       | extr d vs ts Ts hs _ defs = error "extr: bad proof";
 
-    fun prep_thm (thm, vs) =
+    fun prep_thm vs thm =
       let
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
@@ -778,11 +778,11 @@
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")
-      in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
+      in Reconstruct.reconstruct_proof thy prop prf end;
 
     val defs =
-      fold (fn (prf, vs) => snd o extr 0 vs [] [] [] prf)
-        (map prep_thm thms) [];
+      fold (fn (thm, vs) => snd o (extr 0 vs [] [] [] o prep_thm vs) thm)
+        thm_vss [];
 
     fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
       (case Sign.const_type thy (extr_name s vs) of