--- a/src/HOL/Library/Order_Continuity.thy Tue Jun 30 13:29:30 2015 +0200
+++ b/src/HOL/Library/Order_Continuity.thy Tue Jun 30 13:30:04 2015 +0200
@@ -37,14 +37,13 @@
subsection \<open>Continuity for complete lattices\<close>
definition
- sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+ sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
"sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
by (auto simp: sup_continuous_def)
lemma sup_continuous_mono:
- fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
assumes [simp]: "sup_continuous F" shows "mono F"
proof
fix A B :: "'a" assume [simp]: "A \<le> B"
@@ -56,6 +55,25 @@
by (simp add: SUP_nat_binary le_iff_sup)
qed
+lemma sup_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)
+
+lemma sup_continuous_compose:
+ assumes f: "sup_continuous f" and g: "sup_continuous g"
+ shows "sup_continuous (\<lambda>x. f (g x))"
+ unfolding sup_continuous_def
+proof safe
+ fix M :: "nat \<Rightarrow> 'c" assume "mono M"
+ moreover then have "mono (\<lambda>i. g (M i))"
+ using sup_continuous_mono[OF g] by (auto simp: mono_def)
+ ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
+ by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
+qed
+
lemma sup_continuous_lfp:
assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
proof (rule antisym)
@@ -105,14 +123,13 @@
qed
definition
- inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
+ 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)))"
lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
by (auto simp: inf_continuous_def)
lemma inf_continuous_mono:
- fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
assumes [simp]: "inf_continuous F" shows "mono F"
proof
fix A B :: "'a" assume [simp]: "A \<le> B"
@@ -124,6 +141,25 @@
by (simp add: INF_nat_binary le_iff_inf inf_commute)
qed
+lemma inf_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)
+
+lemma inf_continuous_compose:
+ assumes f: "inf_continuous f" and g: "inf_continuous g"
+ shows "inf_continuous (\<lambda>x. f (g x))"
+ unfolding inf_continuous_def
+proof safe
+ fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
+ moreover then have "antimono (\<lambda>i. g (M i))"
+ using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
+ ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
+ by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
+qed
+
lemma inf_continuous_gfp:
assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
proof (rule antisym)
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Jun 30 13:29:30 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Jun 30 13:30:04 2015 +0200
@@ -1547,25 +1547,25 @@
lemma sup_continuous_nn_integral:
assumes f: "\<And>y. sup_continuous (f y)"
- assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
- shows "sup_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
+ 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))"
unfolding sup_continuous_def
proof safe
- fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "incseq C"
- then show "(\<lambda>x. \<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) x \<partial>M x) = (SUP i. (\<lambda>x. \<integral>\<^sup>+ y. f y (C i) x \<partial>M x))"
- using sup_continuous_mono[OF f]
- by (simp add: sup_continuousD[OF f C] fun_eq_iff nn_integral_monotone_convergence_SUP mono_def le_fun_def)
+ fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C"
+ with sup_continuous_mono[OF f] show "(\<integral>\<^sup>+ y. f y (SUPREMUM UNIV C) \<partial>M) = (SUP i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
+ unfolding sup_continuousD[OF f C]
+ by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
qed
lemma inf_continuous_nn_integral:
assumes f: "\<And>y. inf_continuous (f y)"
- assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
- assumes bnd: "\<And>x F. (\<integral>\<^sup>+ y. f y F x \<partial>M x) \<noteq> \<infinity>"
- shows "inf_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
+ 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>"
+ shows "inf_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))"
unfolding inf_continuous_def
proof safe
- fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "decseq C"
- then show "(\<lambda>x. \<integral>\<^sup>+ y. f y (INFIMUM UNIV C) x \<partial>M x) = (INF i. (\<lambda>x. \<integral>\<^sup>+ y. f y (C i) x \<partial>M x))"
+ fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C"
+ then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
using inf_continuous_mono[OF f]
by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def bnd
intro!: nn_integral_monotone_convergence_INF)