merged

--- a/src/HOL/Probability/Complete_Measure.thy	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Probability/Complete_Measure.thy	Mon Oct 06 17:27:27 2014 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Complete_Measure
-imports Bochner_Integration
+  imports Bochner_Integration Probability_Measure
 begin
 
 definition
@@ -314,4 +314,19 @@
   qed auto
 qed
 
+lemma (in prob_space) prob_space_completion: "prob_space (completion M)"
+  by (rule prob_spaceI) (simp add: emeasure_space_1)
+
+lemma null_sets_completionI: "N \<in> null_sets M \<Longrightarrow> N \<in> null_sets (completion M)"
+  by (auto simp: null_sets_def)
+
+lemma AE_completion: "(AE x in M. P x) \<Longrightarrow> (AE x in completion M. P x)"
+  unfolding eventually_ae_filter by (auto intro: null_sets_completionI)
+
+lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M"
+  by (auto simp: null_sets_def)
+
+lemma AE_completion_iff: "{x\<in>space M. P x} \<in> sets M \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in completion M. P x)"
+  by (simp add: AE_iff_null null_sets_completion_iff)
+
 end

--- a/src/HOL/Probability/Probability.thy	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Probability/Probability.thy	Mon Oct 06 17:27:27 2014 +0200
@@ -2,11 +2,11 @@
 imports
   Discrete_Topology
   Complete_Measure
-  Probability_Measure
-  Infinite_Product_Measure
   Projective_Limit
   Independent_Family
   Distributions
+  Probability_Mass_Function
+  Stream_Space
 begin
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 06 17:27:27 2014 +0200
@@ -0,0 +1,358 @@
+theory Probability_Mass_Function
+  imports Probability_Measure
+begin
+
+lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
+  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
+
+lemma finite_subset_card:
+  assumes X: "infinite X" shows "\<exists>A\<subseteq>X. finite A \<and> card A = n"
+proof (induct n)
+  case (Suc n) then guess A .. note A = this
+  with X obtain x where "x \<in> X" "x \<notin> A"
+    by (metis subset_antisym subset_eq)
+  with A show ?case  
+    by (intro exI[of _ "insert x A"]) auto
+qed (simp cong: conj_cong)
+
+lemma (in prob_space) countable_support:
+  "countable {x. measure M {x} \<noteq> 0}"
+proof -
+  let ?m = "\<lambda>x. measure M {x}"
+  have *: "{x. ?m x \<noteq> 0} = (\<Union>n. {x. inverse (real (Suc n)) < ?m x})"
+    by (auto intro!: measure_nonneg reals_Archimedean order_le_neq_trans)
+  have **: "\<And>n. finite {x. inverse (Suc n) < ?m x}"
+  proof (rule ccontr)
+    fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X")
+    then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
+      by (metis finite_subset_card)
+    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> 1 / Suc n \<le> ?m x" 
+      by (auto simp: inverse_eq_divide)
+    { fix x assume "x \<in> X"
+      from *[OF this] have "?m x \<noteq> 0" by auto
+      then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
+    note singleton_sets = this
+    have "1 < (\<Sum>x\<in>X. 1 / Suc n)"
+      by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc)
+    also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
+      by (rule setsum_mono) fact
+    also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
+      using singleton_sets `finite X`
+      by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
+    finally show False
+      using prob_le_1[of "\<Union>x\<in>X. {x}"] by arith
+  qed
+  show ?thesis
+    unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
+qed
+
+lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
+  unfolding measure_def
+  by (cases "finite X") (simp_all add: emeasure_notin_sets)
+
+typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
+  morphisms measure_pmf Abs_pmf
+  apply (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
+  apply (auto intro!: prob_space_uniform_measure simp: measure_count_space)
+  apply (subst uniform_measure_def)
+  apply (simp add: AE_density AE_count_space split: split_indicator)
+  done
+
+declare [[coercion measure_pmf]]
+
+lemma prob_space_measure_pmf: "prob_space (measure_pmf p)"
+  using pmf.measure_pmf[of p] by auto
+
+interpretation measure_pmf!: prob_space "measure_pmf M" for M
+  by (rule prob_space_measure_pmf)
+
+locale pmf_as_measure
+begin
+
+setup_lifting type_definition_pmf
+
+end
+
+context
+begin
+
+interpretation pmf_as_measure .
+
+lift_definition pmf :: "'a pmf \<Rightarrow> 'a \<Rightarrow> real" is "\<lambda>M x. measure M {x}" .
+
+lift_definition set_pmf :: "'a pmf \<Rightarrow> 'a set" is "\<lambda>M. {x. measure M {x} \<noteq> 0}" .
+
+lift_definition map_pmf :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf" is
+  "\<lambda>f M. distr M (count_space UNIV) f"
+proof safe
+  fix M and f :: "'a \<Rightarrow> 'b"
+  let ?D = "distr M (count_space UNIV) f"
+  assume "prob_space M" and [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0"
+  interpret prob_space M by fact
+  from ae have "AE x in M. measure M (f -` {f x}) \<noteq> 0"
+  proof eventually_elim
+    fix x
+    have "measure M {x} \<le> measure M (f -` {f x})"
+      by (intro finite_measure_mono) auto
+    then show "measure M {x} \<noteq> 0 \<Longrightarrow> measure M (f -` {f x}) \<noteq> 0"
+      using measure_nonneg[of M "{x}"] by auto
+  qed
+  then show "AE x in ?D. measure ?D {x} \<noteq> 0"
+    by (simp add: AE_distr_iff measure_distr measurable_def)
+qed (auto simp: measurable_def prob_space.prob_space_distr)
+
+declare [[coercion set_pmf]]
+
+lemma countable_set_pmf: "countable (set_pmf p)"
+  by transfer (metis prob_space.countable_support)
+
+lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
+  by transfer metis
+
+lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
+  using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
+
+lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N"
+  by (auto simp: measurable_def)
+
+lemma measurable_pmf_measure2[simp]: "measurable N (M :: 'a pmf) = measurable N (count_space UNIV)"
+  by (intro measurable_cong_sets) simp_all
+
+lemma pmf_positive: "x \<in> set_pmf p \<Longrightarrow> 0 < pmf p x"
+  by transfer (simp add: less_le measure_nonneg)
+
+lemma pmf_nonneg: "0 \<le> pmf p x"
+  by transfer (simp add: measure_nonneg)
+
+lemma emeasure_pmf_single:
+  fixes M :: "'a pmf"
+  shows "emeasure M {x} = pmf M x"
+  by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
+
+lemma AE_measure_pmf: "AE x in (M::'a pmf). x \<in> M"
+  by transfer simp
+
+lemma emeasure_pmf_single_eq_zero_iff:
+  fixes M :: "'a pmf"
+  shows "emeasure M {y} = 0 \<longleftrightarrow> y \<notin> M"
+  by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
+
+lemma AE_measure_pmf_iff: "(AE x in measure_pmf M. P x) \<longleftrightarrow> (\<forall>y\<in>M. P y)"
+proof -
+  { fix y assume y: "y \<in> M" and P: "AE x in M. P x" "\<not> P y"
+    with P have "AE x in M. x \<noteq> y"
+      by auto
+    with y have False
+      by (simp add: emeasure_pmf_single_eq_zero_iff AE_iff_measurable[OF _ refl]) }
+  then show ?thesis
+    using AE_measure_pmf[of M] by auto
+qed
+
+lemma measure_pmf_eq_density: "measure_pmf p = density (count_space UNIV) (pmf p)"
+proof (transfer, elim conjE)
+  fix M :: "'a measure" assume [simp]: "sets M = UNIV" and ae: "AE x in M. measure M {x} \<noteq> 0"
+  assume "prob_space M" then interpret prob_space M .
+  show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
+  proof (rule measure_eqI)
+    fix A :: "'a set"
+    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
+      (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
+      by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
+    also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
+      by (subst nn_integral_restrict_space[symmetric]) (auto simp: restrict_count_space)
+    also have "\<dots> = emeasure M (\<Union>x\<in>(A \<inter> {x. measure M {x} \<noteq> 0}). {x})"
+      by (intro emeasure_UN_countable[symmetric] countable_Int2 countable_support)
+         (auto simp: disjoint_family_on_def)
+    also have "\<dots> = emeasure M A"
+      using ae by (intro emeasure_eq_AE) auto
+    finally show " emeasure M A = emeasure (density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))) A"
+      using emeasure_space_1 by (simp add: emeasure_density)
+  qed simp
+qed
+
+lemma set_pmf_not_empty: "set_pmf M \<noteq> {}"
+  using AE_measure_pmf[of M] by (intro notI) simp
+
+lemma set_pmf_iff: "x \<in> set_pmf M \<longleftrightarrow> pmf M x \<noteq> 0"
+  by transfer simp
+
+lemma emeasure_pmf: "emeasure (M::'a pmf) M = 1"
+proof -
+  have "emeasure (M::'a pmf) M = emeasure (M::'a pmf) (space M)"
+    by (intro emeasure_eq_AE) (simp_all add: AE_measure_pmf)
+  then show ?thesis
+    using measure_pmf.emeasure_space_1 by simp
+qed
+
+lemma map_pmf_id[simp]: "map_pmf id = id"
+  by (rule, transfer) (auto simp: emeasure_distr measurable_def intro!: measure_eqI)
+
+lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g"
+  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) 
+
+lemma map_pmf_cong:
+  assumes "p = q"
+  shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g q"
+  unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq
+  by (auto simp add: emeasure_distr AE_measure_pmf_iff intro!: emeasure_eq_AE measure_eqI)
+
+lemma pmf_set_map: 
+  fixes f :: "'a \<Rightarrow> 'b"
+  shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
+proof (rule, transfer, clarsimp simp add: measure_distr measurable_def)
+  fix f :: "'a \<Rightarrow> 'b" and M :: "'a measure"
+  assume "prob_space M" and ae: "AE x in M. measure M {x} \<noteq> 0" and [simp]: "sets M = UNIV"
+  interpret prob_space M by fact
+  show "{x. measure M (f -` {x}) \<noteq> 0} = f ` {x. measure M {x} \<noteq> 0}"
+  proof safe
+    fix x assume "measure M (f -` {x}) \<noteq> 0"
+    moreover have "measure M (f -` {x}) = measure M {y. f y = x \<and> measure M {y} \<noteq> 0}"
+      using ae by (intro finite_measure_eq_AE) auto
+    ultimately have "{y. f y = x \<and> measure M {y} \<noteq> 0} \<noteq> {}"
+      by (metis measure_empty)
+    then show "x \<in> f ` {x. measure M {x} \<noteq> 0}"
+      by auto
+  next
+    fix x assume "measure M {x} \<noteq> 0"
+    then have "0 < measure M {x}"
+      using measure_nonneg[of M "{x}"] by auto
+    also have "measure M {x} \<le> measure M (f -` {f x})"
+      by (intro finite_measure_mono) auto
+    finally show "measure M (f -` {f x}) = 0 \<Longrightarrow> False"
+      by simp
+  qed
+qed
+
+context
+  fixes f :: "'a \<Rightarrow> real"
+  assumes nonneg: "\<And>x. 0 \<le> f x"
+  assumes prob: "(\<integral>\<^sup>+x. f x \<partial>count_space UNIV) = 1"
+begin
+
+lift_definition embed_pmf :: "'a pmf" is "density (count_space UNIV) (ereal \<circ> f)"
+proof (intro conjI)
+  have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
+    by (simp split: split_indicator)
+  show "AE x in density (count_space UNIV) (ereal \<circ> f).
+    measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
+    by (simp add: AE_density nonneg emeasure_density measure_def nn_integral_cmult_indicator)
+  show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
+    by default (simp add: emeasure_density prob)
+qed simp
+
+lemma pmf_embed_pmf: "pmf embed_pmf x = f x"
+proof transfer
+  have *[simp]: "\<And>x y. ereal (f y) * indicator {x} y = ereal (f x) * indicator {x} y"
+    by (simp split: split_indicator)
+  fix x show "measure (density (count_space UNIV) (ereal \<circ> f)) {x} = f x"
+    by transfer (simp add: measure_def emeasure_density nn_integral_cmult_indicator nonneg)
+qed
+
+end
+
+lemma embed_pmf_transfer:
+  "rel_fun (eq_onp (\<lambda>f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1)) pmf_as_measure.cr_pmf (\<lambda>f. density (count_space UNIV) (ereal \<circ> f)) embed_pmf"
+  by (auto simp: rel_fun_def eq_onp_def embed_pmf.transfer)
+
+lemma td_pmf_embed_pmf:
+  "type_definition pmf embed_pmf {f::'a \<Rightarrow> real. (\<forall>x. 0 \<le> f x) \<and> (\<integral>\<^sup>+x. ereal (f x) \<partial>count_space UNIV) = 1}"
+  unfolding type_definition_def
+proof safe
+  fix p :: "'a pmf"
+  have "(\<integral>\<^sup>+ x. 1 \<partial>measure_pmf p) = 1"
+    using measure_pmf.emeasure_space_1[of p] by simp
+  then show *: "(\<integral>\<^sup>+ x. ereal (pmf p x) \<partial>count_space UNIV) = 1"
+    by (simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg del: nn_integral_const)
+
+  show "embed_pmf (pmf p) = p"
+    by (intro measure_pmf_inject[THEN iffD1])
+       (simp add: * embed_pmf.rep_eq pmf_nonneg measure_pmf_eq_density[of p] comp_def)
+next
+  fix f :: "'a \<Rightarrow> real" assume "\<forall>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>count_space UNIV) = 1"
+  then show "pmf (embed_pmf f) = f"
+    by (auto intro!: pmf_embed_pmf)
+qed (rule pmf_nonneg)
+
+end
+
+locale pmf_as_function
+begin
+
+setup_lifting td_pmf_embed_pmf
+
+end 
+
+(*
+
+definition
+  "rel_pmf P d1 d2 \<longleftrightarrow> (\<exists>p3. (\<forall>(x, y) \<in> set_pmf p3. P x y) \<and> map_pmf fst p3 = d1 \<and> map_pmf snd p3 = d2)"
+
+lift_definition pmf_join :: "real \<Rightarrow> 'a pmf \<Rightarrow> 'a pmf \<Rightarrow> 'a pmf" is
+  "\<lambda>p M1 M2. density (count_space UNIV) (\<lambda>x. p * measure M1 {x} + (1 - p) * measure M2 {x})"
+sorry
+
+lift_definition pmf_single :: "'a \<Rightarrow> 'a pmf" is
+  "\<lambda>x. uniform_measure (count_space UNIV) {x}"
+sorry
+
+bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: pmf_rel
+proof -
+  show "map_pmf id = id" by (rule map_pmf_id)
+  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
+  show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p"
+    by (intro map_pmg_cong refl)
+
+  show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
+    by (rule pmf_set_map)
+
+  { fix p :: "'s pmf"
+    have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq"
+      by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
+         (auto intro: countable_set_pmf inj_on_to_nat_on)
+    also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq"
+      by (metis Field_natLeq card_of_least natLeq_Well_order)
+    finally show "(card_of (set_pmf p), natLeq) \<in> ordLeq" . }
+
+  show "\<And>R. pmf_rel R =
+         (BNF_Util.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
+         BNF_Util.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
+     by (auto simp add: fun_eq_iff pmf_rel_def BNF_Util.Grp_def OO_def)
+
+  { let ?f = "map_pmf fst" and ?s = "map_pmf snd"
+    fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and A assume "\<And>x y. (x, y) \<in> set_pmf A \<Longrightarrow> R x y"
+    fix S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" and B assume "\<And>y z. (y, z) \<in> set_pmf B \<Longrightarrow> S y z"
+    assume "?f B = ?s A"
+    have "\<exists>C. (\<forall>(x, z)\<in>set_pmf C. \<exists>y. R x y \<and> S y z) \<and> ?f C = ?f A \<and> ?s C = ?s B"
+      sorry }
+oops
+  then show "\<And>R::'a \<Rightarrow> 'b \<Rightarrow> bool. \<And>S::'b \<Rightarrow> 'c \<Rightarrow> bool. pmf_rel R OO pmf_rel S \<le> pmf_rel (R OO S)"
+      by (auto simp add: subset_eq pmf_rel_def fun_eq_iff OO_def Ball_def)
+qed (fact natLeq_card_order natLeq_cinfinite)+
+
+notepad
+begin
+  fix x y :: "nat \<Rightarrow> real"
+  def IJz \<equiv> "rec_nat ((0, 0), \<lambda>_. 0) (\<lambda>n ((I, J), z).
+    let a = x I - (\<Sum>j<J. z (I, j)) ; b = y J - (\<Sum>i<I. z (i, J)) in
+      ((if a \<le> b then I + 1 else I, if b \<le> a then J + 1 else J), z((I, J) := min a b)))"
+  def I == "fst \<circ> fst \<circ> IJz" def J == "snd \<circ> fst \<circ> IJz" def z == "snd \<circ> IJz"
+  let ?a = "\<lambda>n. x (I n) - (\<Sum>j<J n. z n (I n, j))" and ?b = "\<lambda>n. y (J n) - (\<Sum>i<I n. z n (i, J n))"
+  have IJz_0[simp]: "\<And>p. z 0 p = 0" "I 0 = 0" "J 0 = 0"
+    by (simp_all add: I_def J_def z_def IJz_def)
+  have z_Suc[simp]: "\<And>n. z (Suc n) = (z n)((I n, J n) := min (?a n) (?b n))"
+    by (simp add: z_def I_def J_def IJz_def Let_def split_beta)
+  have I_Suc[simp]: "\<And>n. I (Suc n) = (if ?a n \<le> ?b n then I n + 1 else I n)"
+    by (simp add: z_def I_def J_def IJz_def Let_def split_beta)
+  have J_Suc[simp]: "\<And>n. J (Suc n) = (if ?b n \<le> ?a n then J n + 1 else J n)"
+    by (simp add: z_def I_def J_def IJz_def Let_def split_beta)
+  
+  { fix N have "\<And>p. z N p \<noteq> 0 \<Longrightarrow> \<exists>n<N. p = (I n, J n)"
+      by (induct N) (auto simp add: less_Suc_eq split: split_if_asm) }
+  
+  { fix i n assume "i < I n"
+    then have "(\<Sum>j. z n (i, j)) = x i" 
+    oops
+*)
+
+end
+

--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Oct 06 17:27:27 2014 +0200
@@ -2214,122 +2214,101 @@
   using emeasure_extend_measure[OF M _ _ ms(2,3), of "(i,j)"] eq ms(1) `I i j`
   by (auto simp: subset_eq)
 
-subsubsection {* Sigma algebra generated by function preimages *}
+subsubsection {* Supremum of a set of \sigma-algebras *}
+
+definition "Sup_sigma M = sigma (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
+
+syntax
+  "_SUP_sigma"   :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>\<^sub>\<sigma> _\<in>_./ _)" [0, 0, 10] 10)
 
-definition
-  "vimage_algebra M S X = sigma S ((\<lambda>A. X -` A \<inter> S) ` sets M)"
+translations
+  "\<Squnion>\<^sub>\<sigma> x\<in>A. B"   == "CONST Sup_sigma ((\<lambda>x. B) ` A)"
+
+lemma space_Sup_sigma: "space (Sup_sigma M) = (\<Union>x\<in>M. space x)"
+  unfolding Sup_sigma_def by (rule space_measure_of) (auto dest: sets.sets_into_space)
+
+lemma sets_Sup_sigma: "sets (Sup_sigma M) = sigma_sets (\<Union>x\<in>M. space x) (\<Union>x\<in>M. sets x)"
+  unfolding Sup_sigma_def by (rule sets_measure_of) (auto dest: sets.sets_into_space)
+
+lemma in_Sup_sigma: "m \<in> M \<Longrightarrow> A \<in> sets m \<Longrightarrow> A \<in> sets (Sup_sigma M)"
+  unfolding sets_Sup_sigma by auto
 
-lemma sigma_algebra_preimages:
-  fixes f :: "'x \<Rightarrow> 'a"
-  assumes "f \<in> S \<rightarrow> space M"
-  shows "sigma_algebra S ((\<lambda>A. f -` A \<inter> S) ` sets M)"
-    (is "sigma_algebra _ (?F ` sets M)")
-proof (simp add: sigma_algebra_iff2, safe)
-  show "{} \<in> ?F ` sets M" by blast
-next
-  fix A assume "A \<in> sets M"
-  moreover have "S - ?F A = ?F (space M - A)"
+lemma sets_Sup_in_sets: 
+  assumes "M \<noteq> {}"
+  assumes "\<And>m. m \<in> M \<Longrightarrow> space m = space N"
+  assumes "\<And>m. m \<in> M \<Longrightarrow> sets m \<subseteq> sets N"
+  shows "sets (Sup_sigma M) \<subseteq> sets N"
+proof -
+  have *: "UNION M space = space N"
     using assms by auto
-  ultimately show "S - ?F A \<in> ?F ` sets M"
-    by blast
-next
-  fix A :: "nat \<Rightarrow> 'x set" assume *: "range A \<subseteq> ?F ` M"
-  have "\<forall>i. \<exists>b. b \<in> M \<and> A i = ?F b"
-  proof safe
-    fix i
-    have "A i \<in> ?F ` M" using * by auto
-    then show "\<exists>b. b \<in> M \<and> A i = ?F b" by auto
-  qed
-  from choice[OF this] obtain b where b: "range b \<subseteq> M" "\<And>i. A i = ?F (b i)"
-    by auto
-  then have "(\<Union>i. A i) = ?F (\<Union>i. b i)" by auto
-  then show "(\<Union>i. A i) \<in> ?F ` M" using b(1) by blast
+  show ?thesis
+    unfolding sets_Sup_sigma * using assms by (auto intro!: sets.sigma_sets_subset)
+qed
+
+lemma measurable_Sup_sigma1:
+  assumes m: "m \<in> M" and f: "f \<in> measurable m N"
+    and const_space: "\<And>m n. m \<in> M \<Longrightarrow> n \<in> M \<Longrightarrow> space m = space n"
+  shows "f \<in> measurable (Sup_sigma M) N"
+proof -
+  have "space (Sup_sigma M) = space m"
+    using m by (auto simp add: space_Sup_sigma dest: const_space)
+  then show ?thesis
+    using m f unfolding measurable_def by (auto intro: in_Sup_sigma)
 qed
 
-lemma sets_vimage_algebra[simp]:
-  "f \<in> S \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra M S f) = (\<lambda>A. f -` A \<inter> S) ` sets M"
-  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_preimages, of f S M]
-  by (simp add: vimage_algebra_def)
+lemma measurable_Sup_sigma2:
+  assumes M: "M \<noteq> {}"
+  assumes f: "\<And>m. m \<in> M \<Longrightarrow> f \<in> measurable N m"
+  shows "f \<in> measurable N (Sup_sigma M)"
+  unfolding Sup_sigma_def
+proof (rule measurable_measure_of)
+  show "f \<in> space N \<rightarrow> UNION M space"
+    using measurable_space[OF f] M by auto
+qed (auto intro: measurable_sets f dest: sets.sets_into_space)
 
-lemma space_vimage_algebra[simp]:
-  "f \<in> S \<rightarrow> space M \<Longrightarrow> space (vimage_algebra M S f) = S"
-  using sigma_algebra.space_measure_of_eq[OF sigma_algebra_preimages, of f S M]
-  by (simp add: vimage_algebra_def)
-
-lemma in_vimage_algebra[simp]:
-  "f \<in> S \<rightarrow> space M \<Longrightarrow> A \<in> sets (vimage_algebra M S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f -` B \<inter> S)"
-  by (simp add: image_iff)
+subsection {* The smallest \sigma-algebra regarding a function *}
 
-lemma measurable_vimage_algebra:
-  fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M"
-  shows "f \<in> measurable (vimage_algebra M S f) M"
-  unfolding measurable_def using assms by force
+definition
+  "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
+
+lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
+  unfolding vimage_algebra_def by (rule space_measure_of) auto
 
-lemma measurable_vimage:
-  fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a"
-  assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M"
-  shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra M S f) M2"
-proof -
-  note measurable_vimage_algebra[OF assms(2)]
-  from measurable_comp[OF this assms(1)]
-  show ?thesis by (simp add: comp_def)
-qed
+lemma sets_vimage_algebra: "sets (vimage_algebra X f M) = sigma_sets X {f -` A \<inter> X | A. A \<in> sets M}"
+  unfolding vimage_algebra_def by (rule sets_measure_of) auto
+
+lemma sets_vimage_algebra2:
+  "f \<in> X \<rightarrow> space M \<Longrightarrow> sets (vimage_algebra X f M) = {f -` A \<inter> X | A. A \<in> sets M}"
+  using sigma_sets_vimage_commute[of f X "space M" "sets M"]
+  unfolding sets_vimage_algebra sets.sigma_sets_eq by simp
 
-lemma sigma_sets_vimage:
-  assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S"
-  shows "sigma_sets S' ((\<lambda>X. f -` X \<inter> S') ` A) = (\<lambda>X. f -` X \<inter> S') ` sigma_sets S A"
-proof (intro set_eqI iffI)
-  let ?F = "\<lambda>X. f -` X \<inter> S'"
-  fix X assume "X \<in> sigma_sets S' (?F ` A)"
-  then show "X \<in> ?F ` sigma_sets S A"
-  proof induct
-    case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A"
-      by auto
-    then show ?case by auto
-  next
-    case Empty then show ?case
-      by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty)
-  next
-    case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A"
-      by auto
-    then have "S - X' \<in> sigma_sets S A"
-      by (auto intro!: sigma_sets.Compl)
-    then show ?case
-      using X assms by (auto intro!: image_eqI[where x="S - X'"])
-  next
-    case (Union F)
-    then have "\<forall>i. \<exists>F'.  F' \<in> sigma_sets S A \<and> F i = f -` F' \<inter> S'"
-      by (auto simp: image_iff Bex_def)
-    from choice[OF this] obtain F' where
-      "\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f -` F' i \<inter> S'"
-      by auto
-    then show ?case
-      by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"])
-  qed
-next
-  let ?F = "\<lambda>X. f -` X \<inter> S'"
-  fix X assume "X \<in> ?F ` sigma_sets S A"
-  then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto
-  then show "X \<in> sigma_sets S' (?F ` A)"
-  proof (induct arbitrary: X)
-    case Empty then show ?case by (auto intro: sigma_sets.Empty)
-  next
-    case (Compl X')
-    have "S' - (S' - X) \<in> sigma_sets S' (?F ` A)"
-      apply (rule sigma_sets.Compl)
-      using assms by (auto intro!: Compl.hyps simp: Compl.prems)
-    also have "S' - (S' - X) = X"
-      using assms Compl by auto
-    finally show ?case .
-  next
-    case (Union F)
-    have "(\<Union>i. f -` F i \<inter> S') \<in> sigma_sets S' (?F ` A)"
-      by (intro sigma_sets.Union Union.hyps) simp
-    also have "(\<Union>i. f -` F i \<inter> S') = X"
-      using assms Union by auto
-    finally show ?case .
-  qed auto
-qed
+lemma in_vimage_algebra: "A \<in> sets M \<Longrightarrow> f -` A \<inter> X \<in> sets (vimage_algebra X f M)"
+  by (auto simp: vimage_algebra_def)
+
+lemma sets_image_in_sets:
+  assumes N: "space N = X"
+  assumes f: "f \<in> measurable N M"
+  shows "sets (vimage_algebra X f M) \<subseteq> sets N"
+  unfolding sets_vimage_algebra N[symmetric]
+  by (rule sets.sigma_sets_subset) (auto intro!: measurable_sets f)
+
+lemma measurable_vimage_algebra1: "f \<in> X \<rightarrow> space M \<Longrightarrow> f \<in> measurable (vimage_algebra X f M) M"
+  unfolding measurable_def by (auto intro: in_vimage_algebra)
+
+lemma measurable_vimage_algebra2:
+  assumes g: "g \<in> space N \<rightarrow> X" and f: "(\<lambda>x. f (g x)) \<in> measurable N M"
+  shows "g \<in> measurable N (vimage_algebra X f M)"
+  unfolding vimage_algebra_def
+proof (rule measurable_measure_of)
+  fix A assume "A \<in> {f -` A \<inter> X | A. A \<in> sets M}"
+  then obtain Y where Y: "Y \<in> sets M" and A: "A = f -` Y \<inter> X"
+    by auto
+  then have "g -` A \<inter> space N = (\<lambda>x. f (g x)) -` Y \<inter> space N"
+    using g by auto
+  also have "\<dots> \<in> sets N"
+    using f Y by (rule measurable_sets)
+  finally show "g -` A \<inter> space N \<in> sets N" .
+qed (insert g, auto)
 
 subsubsection {* Restricted Space Sigma Algebra *}
 
@@ -2343,16 +2322,20 @@
   by (simp add: space_restrict_space sets.sets_into_space)
 
 lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
-proof -
-  have "sigma_sets (\<Omega> \<inter> space M) ((\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M) =
+  unfolding restrict_space_def
+proof (subst sets_measure_of)
+  show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)"
+    by (auto dest: sets.sets_into_space)
+  have "sigma_sets (\<Omega> \<inter> space M) {((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} =
     (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
-    using sigma_sets_vimage[of "\<lambda>x. x" "\<Omega> \<inter> space M" "space M" "sets M"] sets.space_closed[of M]
-    by (simp add: sets.sigma_sets_eq)
-  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
-    using sets.sets_into_space by (intro image_cong) auto
-  ultimately show ?thesis
-    using sets.sets_into_space[of _ M] unfolding restrict_space_def
-    by (subst sets_measure_of) fastforce+
+    by (subst sigma_sets_vimage_commute[symmetric, where \<Omega>' = "space M"])
+       (auto simp add: sets.sigma_sets_eq)
+  moreover have "{((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) `  sets M"
+    by auto
+  moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) `  sets M = (op \<inter> \<Omega>) ` sets M"
+    by (intro image_cong) (auto dest: sets.sets_into_space)
+  ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M"
+    by simp
 qed
 
 lemma sets_restrict_space_iff:

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Stream_Space.thy	Mon Oct 06 17:27:27 2014 +0200
@@ -0,0 +1,198 @@
+theory Stream_Space
+imports
+  Infinite_Product_Measure
+  "~~/src/HOL/Datatype_Examples/Stream"
+begin
+
+lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"
+  by (cases s) simp
+
+lemma Stream_snth: "(x ## s) !! n = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> s !! n)"
+  by (cases n) simp_all
+
+lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
+  using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
+
+lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \<le> 0 \<longleftrightarrow> integral\<^sup>N M f = 0"
+  using nn_integral_nonneg[of M f] by auto
+
+lemma restrict_UNIV: "restrict f UNIV = f"
+  by (simp add: restrict_def)
+
+definition to_stream :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a stream" where
+  "to_stream X = smap X nats"
+
+lemma to_stream_nat_case: "to_stream (case_nat x X) = x ## to_stream X"
+  unfolding to_stream_def
+  by (subst siterate.ctr) (simp add: smap_siterate[symmetric] stream.map_comp comp_def)
+
+definition stream_space :: "'a measure \<Rightarrow> 'a stream measure" where
+  "stream_space M =
+    distr (\<Pi>\<^sub>M i\<in>UNIV. M) (vimage_algebra (streams (space M)) snth (\<Pi>\<^sub>M i\<in>UNIV. M)) to_stream"
+
+lemma space_stream_space: "space (stream_space M) = streams (space M)"
+  by (simp add: stream_space_def)
+
+lemma streams_stream_space[intro]: "streams (space M) \<in> sets (stream_space M)"
+  using sets.top[of "stream_space M"] by (simp add: space_stream_space)
+
+lemma stream_space_Stream:
+  "x ## \<omega> \<in> space (stream_space M) \<longleftrightarrow> x \<in> space M \<and> \<omega> \<in> space (stream_space M)"
+  by (simp add: space_stream_space streams_Stream)
+
+lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
+  unfolding stream_space_def by (rule distr_cong) auto
+
+lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
+  using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
+
+lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"
+  by (auto intro!: measurable_vimage_algebra1
+           simp: space_PiM streams_iff_sset sset_range image_subset_iff stream_space_def)
+
+lemma measurable_snth[measurable]: "(\<lambda>\<omega>. \<omega> !! n) \<in> measurable (stream_space M) M"
+  using measurable_snth_PiM measurable_component_singleton by (rule measurable_compose) simp
+
+lemma measurable_shd[measurable]: "shd \<in> measurable (stream_space M) M"
+  using measurable_snth[of 0] by simp
+
+lemma measurable_stream_space2:
+  assumes f_snth: "\<And>n. (\<lambda>x. f x !! n) \<in> measurable N M"
+  shows "f \<in> measurable N (stream_space M)"
+  unfolding stream_space_def measurable_distr_eq2
+proof (rule measurable_vimage_algebra2)
+  show "f \<in> space N \<rightarrow> streams (space M)"
+    using f_snth[THEN measurable_space] by (auto simp add: streams_iff_sset sset_range)
+  show "(\<lambda>x. op !! (f x)) \<in> measurable N (Pi\<^sub>M UNIV (\<lambda>i. M))"
+  proof (rule measurable_PiM_single')
+    show "(\<lambda>x. op !! (f x)) \<in> space N \<rightarrow> UNIV \<rightarrow>\<^sub>E space M"
+      using f_snth[THEN measurable_space] by auto
+  qed (rule f_snth)
+qed
+
+lemma measurable_stream_coinduct[consumes 1, case_names shd stl, coinduct set: measurable]:
+  assumes "F f"
+  assumes h: "\<And>f. F f \<Longrightarrow> (\<lambda>x. shd (f x)) \<in> measurable N M"
+  assumes t: "\<And>f. F f \<Longrightarrow> F (\<lambda>x. stl (f x))"
+  shows "f \<in> measurable N (stream_space M)"
+proof (rule measurable_stream_space2)
+  fix n show "(\<lambda>x. f x !! n) \<in> measurable N M"
+    using `F f` by (induction n arbitrary: f) (auto intro: h t)
+qed
+
+lemma measurable_sdrop[measurable]: "sdrop n \<in> measurable (stream_space M) (stream_space M)"
+  by (rule measurable_stream_space2) (simp add: sdrop_snth)
+
+lemma measurable_stl[measurable]: "(\<lambda>\<omega>. stl \<omega>) \<in> measurable (stream_space M) (stream_space M)"
+  by (rule measurable_stream_space2) (simp del: snth.simps add: snth.simps[symmetric])
+
+lemma measurable_to_stream[measurable]: "to_stream \<in> measurable (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M)"
+  by (rule measurable_stream_space2) (simp add: to_stream_def)
+
+lemma measurable_Stream[measurable (raw)]:
+  assumes f[measurable]: "f \<in> measurable N M"
+  assumes g[measurable]: "g \<in> measurable N (stream_space M)"
+  shows "(\<lambda>x. f x ## g x) \<in> measurable N (stream_space M)"
+  by (rule measurable_stream_space2) (simp add: Stream_snth)
+
+lemma measurable_smap[measurable]: 
+  assumes X[measurable]: "X \<in> measurable N M"
+  shows "smap X \<in> measurable (stream_space N) (stream_space M)"
+  by (rule measurable_stream_space2) simp
+
+lemma measurable_stake[measurable]: 
+  "stake i \<in> measurable (stream_space (count_space UNIV)) (count_space (UNIV :: 'a::countable list set))"
+  by (induct i) auto
+
+lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
+proof -
+  interpret product_prob_space "\<lambda>_. M" UNIV by default
+  show ?thesis
+    by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
+qed
+
+lemma (in prob_space) nn_integral_stream_space:
+  assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
+  shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)"
+proof -                  
+  interpret S: sequence_space M
+    by default
+  interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
+    by default
+
+  have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)"
+    by (subst stream_space_eq_distr) (simp add: nn_integral_distr)
+  also have "\<dots> = (\<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) X)) \<partial>(M \<Otimes>\<^sub>M S.S))"
+    by (subst S.PiM_iter[symmetric]) (simp add: nn_integral_distr)
+  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (to_stream ((\<lambda>(s, \<omega>). case_nat s \<omega>) (x, X))) \<partial>S.S \<partial>M)"
+    by (subst S.nn_integral_fst) simp_all
+  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## to_stream X) \<partial>S.S \<partial>M)"
+    by (auto intro!: nn_integral_cong simp: to_stream_nat_case)
+  also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M \<partial>M)"
+    by (subst stream_space_eq_distr)
+       (simp add: nn_integral_distr cong: nn_integral_cong)
+  finally show ?thesis .
+qed
+
+lemma (in prob_space) emeasure_stream_space:
+  assumes X[measurable]: "X \<in> sets (stream_space M)"
+  shows "emeasure (stream_space M) X = (\<integral>\<^sup>+t. emeasure (stream_space M) {x\<in>space (stream_space M). t ## x \<in> X } \<partial>M)"
+proof -
+  have eq: "\<And>x xs. xs \<in> space (stream_space M) \<Longrightarrow> x \<in> space M \<Longrightarrow>
+      indicator X (x ## xs) = indicator {xs\<in>space (stream_space M). x ## xs \<in> X } xs"
+    by (auto split: split_indicator)
+  show ?thesis
+    using nn_integral_stream_space[of "indicator X"]
+    apply (auto intro!: nn_integral_cong)
+    apply (subst nn_integral_cong)
+    apply (rule eq)
+    apply simp_all
+    done
+qed
+
+lemma (in prob_space) prob_stream_space:
+  assumes P[measurable]: "{x\<in>space (stream_space M). P x} \<in> sets (stream_space M)"
+  shows "\<P>(x in stream_space M. P x) = (\<integral>\<^sup>+t. \<P>(x in stream_space M. P (t ## x)) \<partial>M)"
+proof -
+  interpret S: prob_space "stream_space M"
+    by (rule prob_space_stream_space)
+  show ?thesis
+    unfolding S.emeasure_eq_measure[symmetric]
+    by (subst emeasure_stream_space) (auto simp: stream_space_Stream intro!: nn_integral_cong)
+qed
+
+lemma (in prob_space) AE_stream_space:
+  assumes [measurable]: "Measurable.pred (stream_space M) P"
+  shows "(AE X in stream_space M. P X) = (AE x in M. AE X in stream_space M. P (x ## X))"
+proof -
+  interpret stream: prob_space "stream_space M"
+    by (rule prob_space_stream_space)
+
+  have eq: "\<And>x X. indicator {x. \<not> P x} (x ## X) = indicator {X. \<not> P (x ## X)} X"
+    by (auto split: split_indicator)
+  show ?thesis
+    apply (subst AE_iff_nn_integral, simp)
+    apply (subst nn_integral_stream_space, simp)
+    apply (subst eq)
+    apply (subst nn_integral_0_iff_AE, simp)
+    apply (simp add: AE_iff_nn_integral[symmetric])
+    done
+qed
+  
+lemma (in prob_space) AE_stream_all:
+  assumes [measurable]: "Measurable.pred M P" and P: "AE x in M. P x"
+  shows "AE x in stream_space M. stream_all P x"
+proof -
+  { fix n have "AE x in stream_space M. P (x !! n)"
+    proof (induct n)
+      case 0 with P show ?case
+        by (subst AE_stream_space) (auto elim!: eventually_elim1)
+    next
+      case (Suc n) then show ?case
+        by (subst AE_stream_space) auto
+    qed }
+  then show ?thesis
+    unfolding stream_all_def by (simp add: AE_all_countable)
+qed
+
+end

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -11,12 +11,24 @@
   type fp_ctr_sugar =
     {ctrXs_Tss: typ list list,
      ctr_defs: thm list,
-     ctr_sugar: Ctr_Sugar.ctr_sugar}
+     ctr_sugar: Ctr_Sugar.ctr_sugar,
+     ctr_transfers: thm list,
+     case_transfers: thm list,
+     disc_transfers: thm list}
 
   type fp_bnf_sugar =
     {map_thms: thm list,
+     map_disc_iffs: thm list,
+     map_sels: thm list,
      rel_injects: thm list,
-     rel_distincts: thm list}
+     rel_distincts: thm list,
+     rel_sels: thm list,
+     rel_intros: thm list,
+     rel_cases: thm list,
+     set_thms: thm list,
+     set_sels: thm list,
+     set_intros: thm list,
+     set_cases: thm list}
 
   type fp_co_induct_sugar =
     {co_rec: term,
@@ -25,7 +37,14 @@
      co_rec_def: thm,
      co_rec_thms: thm list,
      co_rec_discs: thm list,
-     co_rec_selss: thm list list}
+     co_rec_disc_iffs: thm list,
+     co_rec_selss: thm list list,
+     co_rec_codes: thm list,
+     co_rec_transfers: thm list,
+     common_rel_co_inducts: thm list,
+     rel_co_inducts: thm list,
+     common_set_inducts: thm list,
+     set_inducts: thm list}
 
   type fp_sugar =
     {T: typ,
@@ -163,12 +182,24 @@
 type fp_ctr_sugar =
   {ctrXs_Tss: typ list list,
    ctr_defs: thm list,
-   ctr_sugar: Ctr_Sugar.ctr_sugar};
+   ctr_sugar: Ctr_Sugar.ctr_sugar,
+   ctr_transfers: thm list,
+   case_transfers: thm list,
+   disc_transfers: thm list};
 
 type fp_bnf_sugar =
   {map_thms: thm list,
+   map_disc_iffs: thm list,
+   map_sels: thm list,
    rel_injects: thm list,
-   rel_distincts: thm list};
+   rel_distincts: thm list,
+   rel_sels: thm list,
+   rel_intros: thm list,
+   rel_cases: thm list,
+   set_thms: thm list,
+   set_sels: thm list,
+   set_intros: thm list,
+   set_cases: thm list};
 
 type fp_co_induct_sugar =
   {co_rec: term,
@@ -177,7 +208,14 @@
    co_rec_def: thm,
    co_rec_thms: thm list,
    co_rec_discs: thm list,
-   co_rec_selss: thm list list};
+   co_rec_disc_iffs: thm list,
+   co_rec_selss: thm list list,
+   co_rec_codes: thm list,
+   co_rec_transfers: thm list,
+   common_rel_co_inducts: thm list,
+   rel_co_inducts: thm list,
+   common_set_inducts: thm list,
+   set_inducts: thm list};
 
 type fp_sugar =
   {T: typ,
@@ -194,25 +232,47 @@
    fp_bnf_sugar: fp_bnf_sugar,
    fp_co_induct_sugar: fp_co_induct_sugar};
 
-fun morph_fp_bnf_sugar phi ({map_thms, rel_injects, rel_distincts} : fp_bnf_sugar) =
+fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts,
+    rel_sels, rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases} : fp_bnf_sugar) =
   {map_thms = map (Morphism.thm phi) map_thms,
+   map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
+   map_sels = map (Morphism.thm phi) map_sels,
    rel_injects = map (Morphism.thm phi) rel_injects,
-   rel_distincts = map (Morphism.thm phi) rel_distincts};
+   rel_distincts = map (Morphism.thm phi) rel_distincts,
+   rel_sels = map (Morphism.thm phi) rel_sels,
+   rel_intros = map (Morphism.thm phi) rel_intros,
+   rel_cases = map (Morphism.thm phi) rel_cases,
+   set_thms = map (Morphism.thm phi) set_thms,
+   set_sels = map (Morphism.thm phi) set_sels,
+   set_intros = map (Morphism.thm phi) set_intros,
+   set_cases = map (Morphism.thm phi) set_cases};
 
 fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
-    co_rec_discs, co_rec_selss} : fp_co_induct_sugar) =
+    co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers,
+    common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) =
   {co_rec = Morphism.term phi co_rec,
    common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    co_inducts = map (Morphism.thm phi) co_inducts,
    co_rec_def = Morphism.thm phi co_rec_def,
    co_rec_thms = map (Morphism.thm phi) co_rec_thms,
    co_rec_discs = map (Morphism.thm phi) co_rec_discs,
-   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss};
+   co_rec_disc_iffs = map (Morphism.thm phi) co_rec_disc_iffs,
+   co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
+   co_rec_codes = map (Morphism.thm phi) co_rec_codes,
+   co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
+   common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
+   rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
+   common_set_inducts = map (Morphism.thm phi) common_set_inducts,
+   set_inducts = map (Morphism.thm phi) set_inducts};
 
-fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : fp_ctr_sugar) =
+fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers,
+    disc_transfers} : fp_ctr_sugar) =
   {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    ctr_defs = map (Morphism.thm phi) ctr_defs,
-   ctr_sugar = morph_ctr_sugar phi ctr_sugar};
+   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+   ctr_transfers = map (Morphism.thm phi) ctr_transfers,
+   case_transfers = map (Morphism.thm phi) case_transfers,
+   disc_transfers = map (Morphism.thm phi) disc_transfers};
 
 fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
     live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar,
@@ -281,7 +341,10 @@
 fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
     live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss
     common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
-    rel_distinctss noted =
+    rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss
+    set_intross set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
+    co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
+    set_inductss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -291,11 +354,23 @@
          fp_ctr_sugar =
            {ctrXs_Tss = nth ctrXs_Tsss kk,
             ctr_defs = nth ctr_defss kk,
-            ctr_sugar = nth ctr_sugars kk},
+            ctr_sugar = nth ctr_sugars kk,
+            ctr_transfers = nth ctr_transferss kk,
+            case_transfers = nth case_transferss kk,
+            disc_transfers = nth disc_transferss kk},
          fp_bnf_sugar =
            {map_thms = nth map_thmss kk,
+            map_disc_iffs = nth map_disc_iffss kk,
+            map_sels = nth map_selss kk,
             rel_injects = nth rel_injectss kk,
-            rel_distincts = nth rel_distinctss kk},
+            rel_distincts = nth rel_distinctss kk,
+            rel_sels = nth rel_selss kk,
+            rel_intros = nth rel_intross kk,
+            rel_cases = nth rel_casess kk,
+            set_thms = nth set_thmss kk,
+            set_sels = nth set_selss kk,
+            set_intros = nth set_intross kk,
+            set_cases = nth set_casess kk},
          fp_co_induct_sugar =
            {co_rec = nth co_recs kk,
             common_co_inducts = common_co_inducts,
@@ -303,7 +378,14 @@
             co_rec_def = nth co_rec_defs kk,
             co_rec_thms = nth co_rec_thmss kk,
             co_rec_discs = nth co_rec_discss kk,
-            co_rec_selss = nth co_rec_selsss kk}}
+            co_rec_disc_iffs = nth co_rec_disc_iffss kk,
+            co_rec_selss = nth co_rec_selsss kk,
+            co_rec_codes = nth co_rec_codess kk,
+            co_rec_transfers = nth co_rec_transferss kk,
+            common_rel_co_inducts = common_rel_co_inducts,
+            rel_co_inducts = nth rel_co_inductss kk,
+            common_set_inducts = common_set_inducts,
+            set_inducts = nth set_inductss kk}}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
@@ -455,7 +537,7 @@
       distincts, distinct_discsss, ...} : ctr_sugar)
     lthy =
   if live = 0 then
-    (([], [], [], []), lthy)
+    (([], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
   else
     let
       val n = length ctr_Tss;
@@ -487,7 +569,6 @@
       val discAs = map (mk_disc_or_sel As) discs;
       val discBs = map (mk_disc_or_sel Bs) discs;
       val selAss = map (map (mk_disc_or_sel As)) selss;
-      val discAs_selAss = flat (map2 (map o pair) discAs selAss);
 
       val ctor_cong =
         if fp = Least_FP then
@@ -567,7 +648,7 @@
       val (rel_distinct_thms, _) =
         join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
 
-      val rel_eq_thms =
+      val rel_code_thms =
         map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
         map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms;
 
@@ -760,7 +841,7 @@
           (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
         end;
 
-      val case_transfer_thms =
+      val case_transfer_thm =
         let
           val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
           val caseA = mk_case As C casex;
@@ -804,8 +885,7 @@
           else
             Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
               (fn {context = ctxt, prems = _} =>
-                 mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
-                   map_thms)
+                 mk_map_disc_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) map_thms)
             |> Conjunction.elim_balanced (length goals)
             |> Proof_Context.export names_lthy lthy
             |> map Thm.close_derivation
@@ -813,7 +893,7 @@
 
       val map_sel_thms =
         let
-          fun mk_goal (discA, selA) =
+          fun mk_goal discA selA =
             let
               val prem = Term.betapply (discA, ta);
               val selB = mk_disc_or_sel Bs selA;
@@ -832,7 +912,7 @@
               else Logic.mk_implies (HOLogic.mk_Trueprop prem, concl)
             end;
 
-          val goals = map mk_goal discAs_selAss;
+          val goals = flat (map2 (map o mk_goal) discAs selAss);
         in
           if null goals then
             []
@@ -887,8 +967,10 @@
               else
                 ([], ctxt)
             end;
-          val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) =>
-            fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy);
+          val (goals, names_lthy) = apfst (flat o flat o flat)
+            (fold_map2 (fn disc =>
+                 fold_map (fn sel => fold_map (mk_goal disc sel) setAs))
+               discAs selAss names_lthy);
         in
           if null goals then
             []
@@ -905,11 +987,11 @@
       val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
       val anonymous_notes =
-        [(rel_eq_thms, code_attrs @ nitpicksimp_attrs)]
+        [(rel_code_thms, code_attrs @ nitpicksimp_attrs)]
         |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
       val notes =
-        [(case_transferN, [case_transfer_thms], K []),
+        [(case_transferN, [case_transfer_thm], K []),
          (ctr_transferN, ctr_transfer_thms, K []),
          (disc_transferN, disc_transfer_thms, K []),
          (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
@@ -930,14 +1012,27 @@
         lthy
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
         |> fp = Least_FP
-          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
+          ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_code_thms)
         |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
         |> Local_Theory.notes (anonymous_notes @ notes);
 
       val subst = Morphism.thm (substitute_noted_thm noted);
     in
-      ((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms,
-        map (map subst) set0_thmss), lthy')
+      ((map subst map_thms,
+        map subst map_disc_iff_thms,
+        map subst map_sel_thms,
+        map subst rel_inject_thms,
+        map subst rel_distinct_thms,
+        map subst rel_sel_thms,
+        map subst rel_intro_thms,
+        [subst rel_cases_thm],
+        map subst set_thms,
+        map subst set_sel_thms,
+        map subst set_intros_thms,
+        map subst set_cases_thms,
+        map subst ctr_transfer_thms,
+        [subst case_transfer_thm],
+        map subst disc_transfer_thms), lthy')
     end;
 
 type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list);
@@ -1840,9 +1935,9 @@
 
     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_transfer_thms, ...},
+             ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
+             xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
+             xtor_co_rec_transfers, ...},
            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
@@ -2041,12 +2136,13 @@
 
     fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
       fold_map I wrap_one_etc lthy
-      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
+      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list15 o split_list)
         o split_list;
 
     fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
-        rel_distincts setss =
-      injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss;
+        rel_distincts set_thmss =
+      injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @
+      set_thmss;
 
     fun mk_co_rec_transfer_goals lthy co_recs =
       let
@@ -2067,14 +2163,17 @@
         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)
+               xtor_co_rec_transfers 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
-        ((((map_thmss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
+            rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss,
+            case_transferss, disc_transferss),
+           (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
       let
         val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -2097,7 +2196,7 @@
             let
               val ((rel_induct_thms, common_rel_induct_thm), rel_induct_attrs) =
                 derive_rel_induct_thms_for_types lthy fpTs As Bs ctrss ctr_Tsss
-                  (map #exhaust ctr_sugars) rel_xtor_co_induct_thm ctr_defss ctor_injects
+                  (map #exhaust ctr_sugars) xtor_rel_co_induct ctr_defss ctor_injects
                   pre_rel_defs abs_inverses live_nesting_rel_eqs;
             in
               ((map single rel_induct_thms, single common_rel_induct_thm),
@@ -2105,7 +2204,7 @@
             end;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss;
+          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (if nn > 1 then
@@ -2131,8 +2230,11 @@
           (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
         |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
-          map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
-          rel_injectss rel_distinctss
+          map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
+          (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
+          rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
+          case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
+          common_rel_induct_thms rel_induct_thmss [] (replicate nn [])
       end;
 
     fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2143,7 +2245,7 @@
         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
+               type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
                live_nesting_rel_eqs (flat pgss) pss qssss gssss)
         |> Conjunction.elim_balanced (length goals)
         |> Proof_Context.export names_lthy lthy
@@ -2151,7 +2253,10 @@
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
-        ((((map_thmss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
+        ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
+            rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss,
+            case_transferss, disc_transferss),
+           (_, _, ctr_defss, ctr_sugars)),
           (corecs, corec_defs)), lthy) =
       let
         val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
@@ -2195,7 +2300,7 @@
               val ((rel_coinduct_thms, common_rel_coinduct_thm),
                    (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
                 derive_rel_coinduct_thm_for_types lthy fpTs ns As Bs mss ctr_sugars abs_inverses
-                  abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss rel_xtor_co_induct_thm
+                  abs_injects ctor_injects dtor_ctors pre_rel_defs ctr_defss xtor_rel_co_induct
                   live_nesting_rel_eqs;
             in
               ((map single rel_coinduct_thms, single common_rel_coinduct_thm),
@@ -2204,7 +2309,7 @@
 
         val (set_induct_thms, set_induct_attrss) =
           derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
-            (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_induct_thms
+            (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
             (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
             dtor_ctors abs_inverses
           |> split_list;
@@ -2212,7 +2317,7 @@
         val simp_thmss =
           map6 mk_simp_thms ctr_sugars
             (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
-            map_thmss rel_injectss rel_distinctss setss;
+            map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (set_inductN, set_induct_thms, nth set_induct_attrss) ::
@@ -2245,14 +2350,18 @@
           fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
           map_thmss [coinduct_thm, coinduct_strong_thm]
           (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
-          corec_sel_thmsss rel_injectss rel_distinctss
+          corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss
+          rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss
+          case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
+          corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
+          (replicate nn (if nn = 1 then set_induct_thms else []))
       end;
 
     val lthy'' = lthy'
       |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
       |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
         xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
-        pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
+        pre_rel_defs ~~ xtor_maps ~~ xtor_setss ~~ xtor_rels ~~ ns ~~ kss ~~ mss ~~
         abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
         ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_default_eqss)
       |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types

--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -164,7 +164,7 @@
     val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
 
     val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
-    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
+    val rel_xtor_co_inducts = of_fp_res (split_conj_thm o #xtor_rel_co_induct)
       |> map (unfold_thms lthy (id_apply :: rel_unfolds));
 
     val rel_defs = map rel_def_of_bnf bnfs;
@@ -185,8 +185,8 @@
     val fp_or_nesting_rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
     val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
 
-    val rel_xtor_co_induct_thm =
-      mk_rel_xtor_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
+    val xtor_rel_co_induct =
+      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
         xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
           rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
         lthy;
@@ -208,7 +208,7 @@
             fun mk_type_copy_thms thm = map (curry op RS thm)
               @{thms type_copy_Rep_o_Abs type_copy_vimage2p_Grp_Abs};
           in
-            cterm_instantiate_pos cts rel_xtor_co_induct_thm
+            cterm_instantiate_pos cts xtor_rel_co_induct
             |> singleton (Proof_Context.export names_lthy lthy)
             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @
                 fp_or_nesting_rel_eqs)
@@ -225,7 +225,7 @@
           let
             val cts = NONE :: map (SOME o certify lthy) (map HOLogic.eq_const As);
           in
-            cterm_instantiate_pos cts rel_xtor_co_induct_thm
+            cterm_instantiate_pos cts xtor_rel_co_induct
             |> unfold_thms lthy (@{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} @
                 fp_or_nesting_rel_eqs)
             |> funpow (2 * n) (fn thm => thm RS spec)
@@ -388,7 +388,7 @@
 
     val co_recs = map (Morphism.term phi) raw_co_recs;
 
-    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
+    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
       |> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
 
     val xtor_co_rec_thms =
@@ -471,14 +471,14 @@
         ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
         ctor_injects = of_fp_res #ctor_injects (*too general types*),
         dtor_injects = of_fp_res #dtor_injects (*too general types*),
-        xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
-        xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
-        xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
+        xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
+        xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
+        xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
         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 = [],
-        xtor_co_rec_transfer_thms = []}
+        xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
+        xtor_rel_co_induct = xtor_rel_co_induct,
+        dtor_set_inducts = [],
+        xtor_co_rec_transfers = []}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -293,18 +293,35 @@
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
             co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
-            ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) =
+            ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...},
+              fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels,
+                rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...},
+              fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
+                common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
+              ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
            pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
            live_nesting_bnfs = live_nesting_bnfs,
            fp_ctr_sugar =
              {ctrXs_Tss = ctrXs_Tss,
               ctr_defs = ctr_defs,
-              ctr_sugar = ctr_sugar},
+              ctr_sugar = ctr_sugar,
+              ctr_transfers = ctr_transfers,
+              case_transfers = case_transfers,
+              disc_transfers = disc_transfers},
            fp_bnf_sugar =
              {map_thms = map_thms,
+              map_disc_iffs = map_disc_iffs,
+              map_sels = map_sels,
               rel_injects = rel_injects,
-              rel_distincts = rel_distincts},
+              rel_distincts = rel_distincts,
+              rel_sels = rel_sels,
+              rel_intros = rel_intros,
+              rel_cases = rel_cases,
+              set_thms = set_thms,
+              set_sels = set_sels,
+              set_intros = set_intros,
+              set_cases = set_cases},
            fp_co_induct_sugar =
              {co_rec = co_rec,
               common_co_inducts = common_co_inducts,
@@ -312,7 +329,14 @@
               co_rec_def = co_rec_def, 
               co_rec_thms = co_rec_thms,
               co_rec_discs = co_rec_disc_thms,
-              co_rec_selss = co_rec_sel_thmss}}
+              co_rec_disc_iffs = co_rec_disc_iffs,
+              co_rec_selss = co_rec_sel_thmss,
+              co_rec_codes = co_rec_codes,
+              co_rec_transfers = co_rec_transfers,
+              common_rel_co_inducts = common_rel_co_inducts,
+              rel_co_inducts = rel_co_inducts,
+              common_set_inducts = common_set_inducts,
+              set_inducts = set_inducts}}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -21,14 +21,14 @@
      ctor_dtors: thm list,
      ctor_injects: thm list,
      dtor_injects: thm list,
-     xtor_map_thms: thm list,
-     xtor_set_thmss: thm list list,
-     xtor_rel_thms: thm list,
+     xtor_maps: thm list,
+     xtor_setss: thm list list,
+     xtor_rels: thm list,
      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,
-     xtor_co_rec_transfer_thms: thm list}
+     xtor_co_rec_o_maps: thm list,
+     xtor_rel_co_induct: thm,
+     dtor_set_inducts: thm list,
+     xtor_co_rec_transfers: thm list}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
 
@@ -176,7 +176,7 @@
   val mk_sum_Cinfinite: thm list -> thm
   val mk_sum_card_order: thm list -> thm
 
-  val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
+  val mk_xtor_rel_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_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
@@ -213,19 +213,19 @@
    ctor_dtors: thm list,
    ctor_injects: thm list,
    dtor_injects: thm list,
-   xtor_map_thms: thm list,
-   xtor_set_thmss: thm list list,
-   xtor_rel_thms: thm list,
+   xtor_maps: thm list,
+   xtor_setss: thm list list,
+   xtor_rels: thm list,
    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,
-   xtor_co_rec_transfer_thms: thm list};
+   xtor_co_rec_o_maps: thm list,
+   xtor_rel_co_induct: thm,
+   dtor_set_inducts: thm list,
+   xtor_co_rec_transfers: 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_co_rec_transfer_thms} =
+    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss,
+    xtor_rels, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
+    dtor_set_inducts, xtor_co_rec_transfers} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
@@ -236,14 +236,14 @@
    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    ctor_injects = map (Morphism.thm phi) ctor_injects,
    dtor_injects = map (Morphism.thm phi) dtor_injects,
-   xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
-   xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
-   xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
+   xtor_maps = map (Morphism.thm phi) xtor_maps,
+   xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
+   xtor_rels = map (Morphism.thm phi) xtor_rels,
    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,
-   xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
+   xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
+   xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
+   dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts,
+   xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers};
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
@@ -500,7 +500,7 @@
 fun mk_sum_card_order [thm] = thm
   | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
 
-fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
+fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   let
     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -1659,7 +1659,7 @@
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
     fun mk_Jrel_DEADID_coinduct_thm () =
-      mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
+      mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
         Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
           (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
           REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
@@ -2255,7 +2255,7 @@
         end;
 
       val Jrel_coinduct_thm =
-        mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
+        mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
           Jrel_coinduct_tac lthy;
 
         val le_Jrel_OO_thm =
@@ -2539,11 +2539,11 @@
       {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_recs = corecs,
        xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
        ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
-       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,
-       xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
+       xtor_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss',
+       xtor_rels = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
+       xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
+       dtor_set_inducts = dtor_Jset_induct_thms,
+       xtor_co_rec_transfers = dtor_corec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -1766,7 +1766,7 @@
     val Irels = if m = 0 then map HOLogic.eq_const Ts
       else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
     val Irel_induct_thm =
-      mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
+      mk_xtor_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
         (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
            ctor_Irel_thms rel_mono_strong0s) lthy;
 
@@ -1826,10 +1826,10 @@
       {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_recs = recs,
        xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
        ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
-       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 = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
+       xtor_maps = ctor_Imap_thms, xtor_setss = ctor_Iset_thmss',
+       xtor_rels = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
+       xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
+       dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;

--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -41,14 +41,14 @@
    ctor_dtors = @{thms xtor_xtor},
    ctor_injects = @{thms xtor_inject},
    dtor_injects = @{thms xtor_inject},
-   xtor_map_thms = [xtor_map],
-   xtor_set_thmss = [xtor_sets],
-   xtor_rel_thms = [xtor_rel],
+   xtor_maps = [xtor_map],
+   xtor_setss = [xtor_sets],
+   xtor_rels = [xtor_rel],
    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 = [],
-   xtor_co_rec_transfer_thms = []};
+   xtor_co_rec_o_maps = [ctor_rec_o_map],
+   xtor_rel_co_induct = xtor_rel_induct,
+   dtor_set_inducts = [],
+   xtor_co_rec_transfers = []};
 
 fun fp_sugar_of_sum ctxt =
   let
@@ -79,11 +79,23 @@
      fp_ctr_sugar =
        {ctrXs_Tss = ctr_Tss,
         ctr_defs = @{thms Inl_def_alt Inr_def_alt},
-        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
+        ctr_transfers = [],
+        case_transfers = [],
+        disc_transfers = []},
      fp_bnf_sugar =
        {map_thms = @{thms map_sum.simps},
+        map_disc_iffs = [],
+        map_sels = [],
         rel_injects = @{thms rel_sum_simps(1,4)},
-        rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
+        rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
+        rel_sels = [],
+        rel_intros = [],
+        rel_cases = [],
+        set_thms = [],
+        set_sels = [],
+        set_intros = [],
+        set_cases = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
         common_co_inducts = @{thms sum.induct},
@@ -91,7 +103,14 @@
         co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
         co_rec_thms = @{thms sum.case},
         co_rec_discs = [],
-        co_rec_selss = []}}
+        co_rec_disc_iffs = [],
+        co_rec_selss = [],
+        co_rec_codes = [],
+        co_rec_transfers = [],
+        common_rel_co_inducts = [],
+        rel_co_inducts = [],
+        common_set_inducts = [],
+        set_inducts = []}}
   end;
 
 fun fp_sugar_of_prod ctxt =
@@ -123,11 +142,23 @@
      fp_ctr_sugar =
        {ctrXs_Tss = [ctr_Ts],
         ctr_defs = @{thms Pair_def_alt},
-        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+        ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
+        ctr_transfers = [],
+        case_transfers = [],
+        disc_transfers = []},
      fp_bnf_sugar =
        {map_thms = @{thms map_prod_simp},
+        map_disc_iffs = [],
+        map_sels = [],
         rel_injects = @{thms rel_prod_apply},
-        rel_distincts = []},
+        rel_distincts = [],
+        rel_sels = [],
+        rel_intros = [],
+        rel_cases = [],
+        set_thms = [],
+        set_sels = [],
+        set_intros = [],
+        set_cases = []},
      fp_co_induct_sugar =
        {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
         common_co_inducts = @{thms prod.induct},
@@ -135,7 +166,14 @@
         co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
         co_rec_thms = @{thms prod.case},
         co_rec_discs = [],
-        co_rec_selss = []}}
+        co_rec_disc_iffs = [],
+        co_rec_selss = [],
+        co_rec_codes = [],
+        co_rec_transfers = [],
+        common_rel_co_inducts = [],
+        rel_co_inducts = [],
+        common_set_inducts = [],
+        set_inducts = []}}
   end;
 
 val _ = Theory.setup (map_local_theory (fn lthy =>

--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -82,7 +82,7 @@
   IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
 
 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
-      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
+      fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_maps = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
       live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
     let
       val data = Data.get (Context.Proof lthy0);

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 06 17:26:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Oct 06 17:27:27 2014 +0200
@@ -59,6 +59,32 @@
     'i list -> 'j -> 'k list * 'j
   val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
+  val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list *
+    'e list * 'f list
+  val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list *
+    'd list * 'e list * 'f list * 'g list
+  val split_list8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list -> 'a list * 'b list * 'c list *
+    'd list * 'e list * 'f list * 'g list * 'h list
+  val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list *
+    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list
+  val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list *
+    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list
+  val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list *
+    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
+    'k list
+  val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) list -> 'a list *
+    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
+    'k list * 'l list
+  val split_list13: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm) list ->
+    '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
+  val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) list ->
+    '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
+  val split_list15:
+    ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o) list ->
+    '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 mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
@@ -294,6 +320,66 @@
     let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
 
+fun split_list6 [] = ([], [], [], [], [], [])
+  | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end;
+
+fun split_list7 [] = ([], [], [], [], [], [], [])
+  | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end;
+
+fun split_list8 [] = ([], [], [], [], [], [], [], [])
+  | split_list8 ((x1, x2, x3, x4, x5, x6, x7, x8) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8) = split_list8 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8) end;
+
+fun split_list9 [] = ([], [], [], [], [], [], [], [], [])
+  | split_list9 ((x1, x2, x3, x4, x5, x6, x7, x8, x9) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9) = split_list9 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9) end;
+
+fun split_list10 [] = ([], [], [], [], [], [], [], [], [], [])
+  | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10) end;
+
+fun split_list11 [] = ([], [], [], [], [], [], [], [], [], [], [])
+  | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11) end;
+
+fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], [])
+  | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12) end;
+
+fun split_list13 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [])
+  | split_list13 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13) = split_list13 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13) end;
+
+fun split_list14 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [])
+  | split_list14 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14) =
+      split_list14 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14) end;
+
+fun split_list15 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+  | split_list15 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) :: xs) =
+    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14, xs15) =
+      split_list15 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14, x15 :: xs15)
+    end;
+
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);