# HG changeset patch
# User hoelzl
# Date 1435904794 -7200
# Node ID ee18efe9b2462c44f81441aaae2a0a9193fe2f53
# Parent  22830a64358f2c7ba5a6ab2e2da6e94934c480a6
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer

diff -r 22830a64358f -r ee18efe9b246 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Inductive.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -230,7 +230,6 @@
 apply (simp_all)
 done
 
-
 text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, 
     to control unfolding*}
 
@@ -283,15 +282,6 @@
   qed
 qed
 
-lemma lfp_square:
-  assumes "mono f" shows "lfp f = lfp (\<lambda>x. f (f x))"
-proof (rule antisym)
-  show "lfp f \<le> lfp (\<lambda>x. f (f x))"
-    by (intro lfp_lowerbound) (simp add: assms lfp_rolling)
-  show "lfp (\<lambda>x. f (f x)) \<le> lfp f"
-    by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric])
-qed
-
 lemma lfp_lfp:
   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
   shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
@@ -330,15 +320,6 @@
   qed
 qed
 
-lemma gfp_square:
-  assumes "mono f" shows "gfp f = gfp (\<lambda>x. f (f x))"
-proof (rule antisym)
-  show "gfp (\<lambda>x. f (f x)) \<le> gfp f"
-    by (intro gfp_upperbound) (simp add: assms gfp_rolling)
-  show "gfp f \<le> gfp (\<lambda>x. f (f x))"
-    by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric])
-qed
-
 lemma gfp_gfp:
   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
   shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -6,7 +6,7 @@
 section \<open>Extended natural numbers (i.e. with infinity)\<close>
 
 theory Extended_Nat
-imports Main Countable
+imports Main Countable Order_Continuity
 begin
 
 class infinity =
@@ -472,6 +472,17 @@
 apply (erule (1) le_less_trans)
 done
 
+lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
+  by (simp add: eSuc_def split: enat.split)
+
+lemma eSuc_Max: 
+  assumes "finite A" "A \<noteq> {}"
+  shows "eSuc (Max A) = Max (eSuc ` A)"
+using assms proof induction
+  case (insert x A)
+  thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
+qed simp
+
 instantiation enat :: "{order_bot, order_top}"
 begin
 
@@ -647,6 +658,12 @@
 
 instance enat :: complete_linorder ..
 
+lemma eSuc_Sup: "A \<noteq> {} \<Longrightarrow> eSuc (Sup A) = Sup (eSuc ` A)"
+  by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
+
+lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
+  using  eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
+
 subsection \<open>Traditional theorem names\<close>
 
 lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -8,7 +8,7 @@
 section \<open>Extended real number line\<close>
 
 theory Extended_Real
-imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity
+imports Complex_Main Extended_Nat Liminf_Limsup
 begin
 
 text \<open>
@@ -2768,6 +2768,18 @@
   qed
 qed
 
+lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
+  by auto
+
+lemma sup_continuous_add_left[order_continuous_intros]: "0 \<le> c \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x + c :: ereal)"
+  by (auto simp: sup_continuous_def SUP_ereal_add_left)
+
+lemma sup_continuous_add_right[order_continuous_intros]: "0 \<le> c \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. c + f x :: ereal)"
+  using sup_continuous_add_left by (simp add: ac_simps)
+
+lemma sup_continuous_multc[order_continuous_intros]: "0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> sup_continuous (\<lambda>f s. f s * c :: ereal)"
+  by (cases c) (auto simp: sup_continuous_def fun_eq_iff Sup_ereal_mult_right')
+
 subsubsection \<open>Tests for code generator\<close>
 
 (* A small list of simple arithmetic expressions *)
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Library/Order_Continuity.thy
--- a/src/HOL/Library/Order_Continuity.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Order_Continuity.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -5,7 +5,7 @@
 section \<open>Continuity and iterations (of set transformers)\<close>
 
 theory Order_Continuity
-imports Main
+imports Complex_Main
 begin
 
 (* TODO: Generalize theory to chain-complete partial orders *)
@@ -34,6 +34,8 @@
   and have the advantage that these names are duals.
 \<close>
 
+named_theorems order_continuous_intros
+
 subsection \<open>Continuity for complete lattices\<close>
 
 definition
@@ -55,12 +57,13 @@
     by (simp add: SUP_nat_binary le_iff_sup)
 qed
 
-lemma sup_continuous_intros:
+lemma [order_continuous_intros]:
   shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
     and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
     and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
     and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
- by (auto simp: sup_continuous_def)
+    and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
+  by (auto simp: sup_continuous_def)
 
 lemma sup_continuous_compose:
   assumes f: "sup_continuous f" and g: "sup_continuous g"
@@ -74,6 +77,38 @@
     by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
 qed
 
+lemma sup_continuous_sup[order_continuous_intros]:
+  "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
+  by (simp add: sup_continuous_def SUP_sup_distrib)
+
+lemma sup_continuous_inf[order_continuous_intros]:
+  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+  assumes P: "sup_continuous P" and Q: "sup_continuous Q"
+  shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
+  unfolding sup_continuous_def
+proof (safe intro!: antisym)
+  fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
+  have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
+    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
+  also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+  proof (intro SUP_least)
+    fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+      by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
+  qed
+  finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
+  
+  show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
+    unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
+qed
+
+lemma sup_continuous_and[order_continuous_intros]:
+  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
+  using sup_continuous_inf[of P Q] by simp
+
+lemma sup_continuous_or[order_continuous_intros]:
+  "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
+  by (auto simp: sup_continuous_def)
+
 lemma sup_continuous_lfp:
   assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
 proof (rule antisym)
@@ -122,6 +157,51 @@
     unfolding sup_continuous_lfp[OF g] by simp
 qed
 
+lemma lfp_transfer_bounded:
+  assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> P (SUP i::nat. M i)"
+  assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
+  assumes f: "sup_continuous f" and g: "sup_continuous g"
+  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+  assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
+  shows "\<alpha> (lfp f) = lfp g"
+proof (rule antisym)
+  note mono_g = sup_continuous_mono[OF g]
+  have lfp_bound: "\<alpha> bot \<le> lfp g"
+    by (subst lfp_unfold[OF mono_g]) (rule g_bound)
+
+  have P_pow: "P ((f ^^ i) bot)" for i
+    by (induction i) (auto intro!: P)
+  have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
+    unfolding mono_iff_le_Suc
+  proof
+    fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
+    proof (induct i)
+      case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
+    qed (simp add: le_fun_def)
+  qed
+  have P_lfp: "P (lfp f)"
+    using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
+
+  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
+    unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
+  also have "\<dots> \<le> lfp g"
+  proof (rule SUP_least)
+    fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
+    proof (induction i)
+      case (Suc n) then show ?case
+        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
+    qed (simp add: lfp_bound)
+  qed
+  finally show "\<alpha> (lfp f) \<le> lfp g" .
+
+  show "lfp g \<le> \<alpha> (lfp f)"
+  proof (induction rule: lfp_ordinal_induct[OF mono_g])
+    case (1 S) then show ?case
+      by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
+         (simp add: monoD[OF mono_g] P_lfp)
+  qed (auto intro: Sup_least)
+qed
+
 definition
   inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
   "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
@@ -141,12 +221,45 @@
     by (simp add: INF_nat_binary le_iff_inf inf_commute)
 qed
 
-lemma inf_continuous_intros:
+lemma [order_continuous_intros]:
   shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
     and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
     and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
     and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
- by (auto simp: inf_continuous_def)
+    and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
+  by (auto simp: inf_continuous_def)
+
+lemma inf_continuous_inf[order_continuous_intros]:
+  "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
+  by (simp add: inf_continuous_def INF_inf_distrib)
+
+lemma inf_continuous_sup[order_continuous_intros]:
+  fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+  assumes P: "inf_continuous P" and Q: "inf_continuous Q"
+  shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
+  unfolding inf_continuous_def
+proof (safe intro!: antisym)
+  fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
+  show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
+    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
+
+  have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
+  proof (intro INF_greatest)
+    fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
+      by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
+  qed
+  also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
+    unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
+  finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
+qed
+
+lemma inf_continuous_and[order_continuous_intros]:
+  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
+  using inf_continuous_inf[of P Q] by simp
+
+lemma inf_continuous_or[order_continuous_intros]:
+  "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
+  using inf_continuous_sup[of P Q] by simp
 
 lemma inf_continuous_compose:
   assumes f: "inf_continuous f" and g: "inf_continuous g"
@@ -208,4 +321,70 @@
     unfolding inf_continuous_gfp[OF g] by simp
 qed
 
+lemma gfp_transfer_bounded:
+  assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> P (INF i::nat. M i)"
+  assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
+  assumes f: "inf_continuous f" and g: "inf_continuous g"
+  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+  assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
+  shows "\<alpha> (gfp f) = gfp g"
+proof (rule antisym)
+  note mono_g = inf_continuous_mono[OF g]
+
+  have P_pow: "P ((f ^^ i) (f top))" for i
+    by (induction i) (auto intro!: P)
+
+  have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
+    unfolding antimono_iff_le_Suc
+  proof
+    fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
+    proof (induct i)
+      case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
+    qed (simp add: le_fun_def)
+  qed
+  have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
+  proof
+    show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
+      using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
+      unfolding funpow_Suc_right by simp
+  qed
+    
+  have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
+    unfolding inf_continuous_gfp[OF f]
+  proof (rule INF_eq)
+    show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
+      by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
+    show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
+      by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
+  qed
+
+  have P_lfp: "P (gfp f)"
+    unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
+
+  have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
+    unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
+  also have "\<dots> \<ge> gfp g"
+  proof (rule INF_greatest)
+    fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
+    proof (induction i)
+      case (Suc n) then show ?case
+        by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
+    next
+      case 0
+      have "gfp g \<le> \<alpha> (f top)"
+        by (subst gfp_unfold[OF mono_g]) (rule g_bound)
+      then show ?case
+        by simp
+    qed
+  qed
+  finally show "gfp g \<le> \<alpha> (gfp f)" .
+
+  show "\<alpha> (gfp f) \<le> gfp g"
+  proof (induction rule: gfp_ordinal_induct[OF mono_g])
+    case (1 S) then show ?case
+      by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
+         (simp add: monoD[OF mono_g] P_lfp)
+  qed (auto intro: Inf_greatest)
+qed
+
 end
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Nat.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -1416,6 +1416,42 @@
     using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
 qed
 
+lemma mono_pow:
+  fixes f :: "'a \<Rightarrow> 'a::complete_lattice"
+  shows "mono f \<Longrightarrow> mono (f ^^ n)"
+  by (induction n) (auto simp: mono_def)
+
+lemma lfp_funpow:
+  assumes f: "mono f" shows "lfp (f ^^ Suc n) = lfp f"
+proof (rule antisym)
+  show "lfp f \<le> lfp (f ^^ Suc n)"
+  proof (rule lfp_lowerbound)
+    have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))"
+      unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def)
+    then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)"
+      by (simp add: comp_def)
+  qed
+  have "(f^^n) (lfp f) = lfp f" for n
+    by (induction n) (auto intro: f lfp_unfold[symmetric])
+  then show "lfp (f^^Suc n) \<le> lfp f"
+    by (intro lfp_lowerbound) (simp del: funpow.simps)
+qed
+
+lemma gfp_funpow:
+  assumes f: "mono f" shows "gfp (f ^^ Suc n) = gfp f"
+proof (rule antisym)
+  show "gfp f \<ge> gfp (f ^^ Suc n)"
+  proof (rule gfp_upperbound)
+    have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))"
+      unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def)
+    then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)"
+      by (simp add: comp_def)
+  qed
+  have "(f^^n) (gfp f) = gfp f" for n
+    by (induction n) (auto intro: f gfp_unfold[symmetric])
+  then show "gfp (f^^Suc n) \<ge> gfp f"
+    by (intro gfp_upperbound) (simp del: funpow.simps)
+qed
 
 subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
 
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -548,7 +548,7 @@
   using LIMSEQ_INF[OF decseq_emeasure, OF A]
   using INF_emeasure_decseq[OF A fin] by simp
 
-lemma emeasure_lfp[consumes 1, case_names cont measurable]:
+lemma emeasure_lfp'[consumes 1, case_names cont measurable]:
   assumes "P M"
   assumes cont: "sup_continuous F"
   assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
@@ -574,6 +574,20 @@
     by (subst SUP_emeasure_incseq) auto
 qed
 
+lemma emeasure_lfp:
+  assumes [simp]: "\<And>s. sets (M s) = sets N"
+  assumes cont: "sup_continuous F" "sup_continuous f"
+  assumes nonneg: "\<And>P s. 0 \<le> f P s"
+  assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
+  assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
+  shows "emeasure (M s) {x\<in>space N. lfp F x} = lfp f s"
+proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and P="Measurable.pred N", symmetric])
+  fix C assume "incseq C" "\<And>i. Measurable.pred N (C i)"
+  then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (SUP i. C i) x}) = (SUP i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
+    unfolding SUP_apply[abs_def]
+    by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
+qed (auto simp add: iter nonneg le_fun_def SUP_apply[abs_def] intro!: meas cont)
+
 lemma emeasure_subadditive:
   assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
   shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
@@ -1254,7 +1268,7 @@
   have "emeasure (distr M' M f) {x \<in> space (distr M' M f). lfp F x} =
     (SUP i. emeasure (distr M' M f) {x \<in> space (distr M' M f). (F ^^ i) (\<lambda>x. False) x})"
     using `P M`
-  proof (coinduction arbitrary: M rule: emeasure_lfp)
+  proof (coinduction arbitrary: M rule: emeasure_lfp')
     case (measurable A N) then have "\<And>N. P N \<Longrightarrow> Measurable.pred (distr M' N f) A"
       by metis
     then have "\<And>N. P N \<Longrightarrow> Measurable.pred N A"
@@ -1662,6 +1676,26 @@
   with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
 qed
 
+lemma emeasure_gfp[consumes 1, case_names cont measurable]:
+  assumes sets[simp]: "\<And>s. sets (M s) = sets N"
+  assumes "\<And>s. finite_measure (M s)"
+  assumes cont: "inf_continuous F" "inf_continuous f"
+  assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
+  assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
+  assumes bound: "\<And>P. f P \<le> f (\<lambda>s. emeasure (M s) (space (M s)))"
+  shows "emeasure (M s) {x\<in>space N. gfp F x} = gfp f s"
+proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and
+    P="Measurable.pred N", symmetric])
+  interpret finite_measure "M s" for s by fact
+  fix C assume "decseq C" "\<And>i. Measurable.pred N (C i)"
+  then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (INF i. C i) x}) = (INF i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
+    unfolding INF_apply[abs_def]
+    by (subst INF_emeasure_decseq) (auto simp: antimono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
+next
+  show "f x \<le> (\<lambda>s. emeasure (M s) {x \<in> space N. F top x})" for x
+    using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
+qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
+
 subsection {* Counting space *}
 
 lemma strict_monoI_Suc:
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -1545,7 +1545,7 @@
   finally show ?thesis unfolding nn_integral_max_0 .
 qed
 
-lemma sup_continuous_nn_integral:
+lemma sup_continuous_nn_integral[order_continuous_intros]:
   assumes f: "\<And>y. sup_continuous (f y)"
   assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
   shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))"
@@ -1557,7 +1557,7 @@
     by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
 qed
 
-lemma inf_continuous_nn_integral:
+lemma inf_continuous_nn_integral[order_continuous_intros]:
   assumes f: "\<And>y. inf_continuous (f y)"
   assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
   assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>"
@@ -1739,122 +1739,57 @@
 qed
 
 lemma nn_integral_lfp:
-  assumes sets: "\<And>s. sets (M s) = sets N"
+  assumes sets[simp]: "\<And>s. sets (M s) = sets N"
   assumes f: "sup_continuous f"
+  assumes g: "sup_continuous g"
+  assumes nonneg: "\<And>F s. 0 \<le> g F s"
   assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
-  assumes nonneg: "\<And>F s. 0 \<le> g F s"
-  assumes g: "sup_continuous g"
   assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
   shows "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = lfp g s"
-proof (rule antisym)
-  show "lfp g s \<le> (\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s)"
-  proof (induction arbitrary: s rule: lfp_ordinal_induct[OF sup_continuous_mono[OF g]])
-    case (1 F) then show ?case
-      apply (subst lfp_unfold[OF sup_continuous_mono[OF f]])
-      apply (subst step)
-      apply (rule borel_measurable_lfp[OF f])
-      apply (rule meas)
-      apply assumption+
-      apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
-      apply (simp add: le_fun_def)
-      done
-  qed (auto intro: SUP_least)
-
-  have lfp_nonneg: "\<And>s. 0 \<le> lfp g s"
-    by (subst lfp_unfold[OF sup_continuous_mono[OF g]]) (rule nonneg)
-
-  { fix i have "((f ^^ i) bot) \<in> borel_measurable N"
-      by (induction i) (simp_all add: meas) }
-
-  have "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (SUP i. (f ^^ i) bot \<omega>) \<partial>M s)"
-    by (simp add: sup_continuous_lfp f)
-  also have "\<dots> = (SUP i. \<integral>\<^sup>+\<omega>. (f ^^ i) bot \<omega> \<partial>M s)"
-  proof (rule nn_integral_monotone_convergence_SUP)
-    show "incseq (\<lambda>i. (f ^^ i) bot)"
-      using f[THEN sup_continuous_mono] by (rule mono_funpow)
-    show "\<And>i. ((f ^^ i) bot) \<in> borel_measurable (M s)"
-      unfolding measurable_cong_sets[OF sets refl] by fact
-  qed
-  also have "\<dots> \<le> lfp g s"
-  proof (rule SUP_least)
-    fix i show "integral\<^sup>N (M s) ((f ^^ i) bot) \<le> lfp g s"
-    proof (induction i arbitrary: s)
-      case 0 then show ?case
-        by (simp add: nn_integral_const_nonpos lfp_nonneg)
-    next
-      case (Suc n)
-      show ?case
-        apply (simp del: bot_apply)
-        apply (subst step)
-        apply fact
-        apply (subst lfp_unfold[OF sup_continuous_mono[OF g]])
-        apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
-        apply (rule le_funI)
-        apply (rule Suc)
-        done
-    qed
-  qed
-  finally show "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) \<le> lfp g s" .
-qed
+proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f and P="\<lambda>f. f \<in> borel_measurable N", symmetric])
+  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume "incseq C" "\<And>i. C i \<in> borel_measurable N"
+  then show "(\<lambda>s. \<integral>\<^sup>+x. (SUP i. C i) x \<partial>M s) = (SUP i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))"
+    unfolding SUP_apply[abs_def]
+    by (subst nn_integral_monotone_convergence_SUP)
+       (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets)
+next
+  show "\<And>x. (\<lambda>s. integral\<^sup>N (M s) bot) \<le> g x"
+    by (subst nn_integral_max_0[symmetric])
+       (simp add: sup_ereal_def[symmetric] le_fun_def nonneg del: sup_ereal_def)
+qed (auto simp add: step nonneg le_fun_def SUP_apply[abs_def] bot_fun_def intro!: meas f g)
 
 lemma nn_integral_gfp:
-  assumes sets: "\<And>s. sets (M s) = sets N"
-  assumes f: "inf_continuous f"
+  assumes sets[simp]: "\<And>s. sets (M s) = sets N"
+  assumes f: "inf_continuous f" and g: "inf_continuous g"
   assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
-  assumes bound: "\<And>F s. (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>"
+  assumes bound: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>"
   assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0"
-  assumes g: "inf_continuous g"
   assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
   shows "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = gfp g s"
-proof (rule antisym)
-  show "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) \<le> gfp g s"
-  proof (induction arbitrary: s rule: gfp_ordinal_induct[OF inf_continuous_mono[OF g]])
-    case (1 F) then show ?case
-      apply (subst gfp_unfold[OF inf_continuous_mono[OF f]])
-      apply (subst step)
-      apply (rule borel_measurable_gfp[OF f])
-      apply (rule meas)
-      apply assumption+
-      apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
-      apply (simp add: le_fun_def)
-      done
-  qed (auto intro: INF_greatest)
-
-  { fix i have "((f ^^ i) top) \<in> borel_measurable N"
-      by (induction i) (simp_all add: meas) }
-
-  have "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (INF i. (f ^^ i) top \<omega>) \<partial>M s)"
-    by (simp add: inf_continuous_gfp f)
-  also have "\<dots> = (INF i. \<integral>\<^sup>+\<omega>. (f ^^ i) top \<omega> \<partial>M s)"
-  proof (rule nn_integral_monotone_convergence_INF)
-    show "decseq (\<lambda>i. (f ^^ i) top)"
-      using f[THEN inf_continuous_mono] by (rule antimono_funpow)
-    show "\<And>i. ((f ^^ i) top) \<in> borel_measurable (M s)"
-      unfolding measurable_cong_sets[OF sets refl] by fact
-    show "integral\<^sup>N (M s) ((f ^^ 1) top) < \<infinity>"
-      using bound[of s top] by simp
-  qed
-  also have "\<dots> \<ge> gfp g s"
-  proof (rule INF_greatest)
-    fix i show "gfp g s \<le> integral\<^sup>N (M s) ((f ^^ i) top)"
-    proof (induction i arbitrary: s)
-      case 0 with non_zero[of s] show ?case
-        by (simp add: top_ereal_def less_le emeasure_nonneg)
-    next
-      case (Suc n)
-      show ?case
-        apply (simp del: top_apply)
-        apply (subst step)
-        apply fact
-        apply (subst gfp_unfold[OF inf_continuous_mono[OF g]])
-        apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
-        apply (rule le_funI)
-        apply (rule Suc)
-        done
-    qed
-  qed
-  finally show "gfp g s \<le> (\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s)" .
-qed
+proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f
+    and P="\<lambda>F. F \<in> borel_measurable N \<and> (\<forall>s. (\<integral>\<^sup>+x. F x \<partial>M s) < \<infinity>)", symmetric])
+  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume "decseq C" "\<And>i. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)"
+  then show "(\<lambda>s. \<integral>\<^sup>+x. (INF i. C i) x \<partial>M s) = (INF i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))"
+    unfolding INF_apply[abs_def]
+    by (subst nn_integral_monotone_convergence_INF)
+       (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets)
+next
+  show "\<And>x. g x \<le> (\<lambda>s. integral\<^sup>N (M s) (f top))"
+    by (subst step)
+       (auto simp add: top_fun_def top_ereal_def less_le emeasure_nonneg non_zero le_fun_def
+             cong del: if_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD])
+next
+  fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C"
+  with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
+    unfolding INF_apply[abs_def]
+    by (subst nn_integral_monotone_convergence_INF)
+       (auto cong: measurable_cong_sets intro!: borel_measurable_INF
+             simp: INF_less_iff simp del: ereal_infty_less(1))
+next
+  show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow>
+         (\<lambda>s. integral\<^sup>N (M s) (f x)) = g (\<lambda>s. integral\<^sup>N (M s) x)"
+    by (subst step) auto
+qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g)
 
 subsection {* Integral under concrete measures *}
 
diff -r 22830a64358f -r ee18efe9b246 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Regularity.thy	Fri Jul 03 08:26:34 2015 +0200
@@ -55,7 +55,7 @@
     assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
     hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
     have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
-      apply auto by (metis ereal_infty_less_eq(2) f_le_y)
+      by auto
     def e \<equiv> "real ((y - x) / 2)"
     have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
     from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast