generalized inf and sup_continuous; added intro rules
authorhoelzl
Tue Jun 30 13:30:04 2015 +0200 (2015-06-30)
changeset 60614e39e6881985c
parent 60613 f11e9fd70b7d
child 60616 5a65c496d96f
generalized inf and sup_continuous; added intro rules
src/HOL/Library/Order_Continuity.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Tue Jun 30 13:29:30 2015 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Tue Jun 30 13:30:04 2015 +0200
     1.3 @@ -37,14 +37,13 @@
     1.4  subsection \<open>Continuity for complete lattices\<close>
     1.5  
     1.6  definition
     1.7 -  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
     1.8 +  sup_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
     1.9    "sup_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. mono M \<longrightarrow> F (SUP i. M i) = (SUP i. F (M i)))"
    1.10  
    1.11  lemma sup_continuousD: "sup_continuous F \<Longrightarrow> mono M \<Longrightarrow> F (SUP i::nat. M i) = (SUP i. F (M i))"
    1.12    by (auto simp: sup_continuous_def)
    1.13  
    1.14  lemma sup_continuous_mono:
    1.15 -  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.16    assumes [simp]: "sup_continuous F" shows "mono F"
    1.17  proof
    1.18    fix A B :: "'a" assume [simp]: "A \<le> B"
    1.19 @@ -56,6 +55,25 @@
    1.20      by (simp add: SUP_nat_binary le_iff_sup)
    1.21  qed
    1.22  
    1.23 +lemma sup_continuous_intros:
    1.24 +  shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
    1.25 +    and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
    1.26 +    and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
    1.27 +    and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
    1.28 + by (auto simp: sup_continuous_def)
    1.29 +
    1.30 +lemma sup_continuous_compose:
    1.31 +  assumes f: "sup_continuous f" and g: "sup_continuous g"
    1.32 +  shows "sup_continuous (\<lambda>x. f (g x))"
    1.33 +  unfolding sup_continuous_def
    1.34 +proof safe
    1.35 +  fix M :: "nat \<Rightarrow> 'c" assume "mono M"
    1.36 +  moreover then have "mono (\<lambda>i. g (M i))"
    1.37 +    using sup_continuous_mono[OF g] by (auto simp: mono_def)
    1.38 +  ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
    1.39 +    by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
    1.40 +qed
    1.41 +
    1.42  lemma sup_continuous_lfp:
    1.43    assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
    1.44  proof (rule antisym)
    1.45 @@ -105,14 +123,13 @@
    1.46  qed
    1.47  
    1.48  definition
    1.49 -  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'a::complete_lattice) \<Rightarrow> bool" where
    1.50 +  inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
    1.51    "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
    1.52  
    1.53  lemma inf_continuousD: "inf_continuous F \<Longrightarrow> antimono M \<Longrightarrow> F (INF i::nat. M i) = (INF i. F (M i))"
    1.54    by (auto simp: inf_continuous_def)
    1.55  
    1.56  lemma inf_continuous_mono:
    1.57 -  fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    1.58    assumes [simp]: "inf_continuous F" shows "mono F"
    1.59  proof
    1.60    fix A B :: "'a" assume [simp]: "A \<le> B"
    1.61 @@ -124,6 +141,25 @@
    1.62      by (simp add: INF_nat_binary le_iff_inf inf_commute)
    1.63  qed
    1.64  
    1.65 +lemma inf_continuous_intros:
    1.66 +  shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
    1.67 +    and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
    1.68 +    and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
    1.69 +    and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
    1.70 + by (auto simp: inf_continuous_def)
    1.71 +
    1.72 +lemma inf_continuous_compose:
    1.73 +  assumes f: "inf_continuous f" and g: "inf_continuous g"
    1.74 +  shows "inf_continuous (\<lambda>x. f (g x))"
    1.75 +  unfolding inf_continuous_def
    1.76 +proof safe
    1.77 +  fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
    1.78 +  moreover then have "antimono (\<lambda>i. g (M i))"
    1.79 +    using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
    1.80 +  ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
    1.81 +    by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
    1.82 +qed
    1.83 +
    1.84  lemma inf_continuous_gfp:
    1.85    assumes "inf_continuous F" shows "gfp F = (INF i. (F ^^ i) top)" (is "gfp F = ?U")
    1.86  proof (rule antisym)
     2.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Jun 30 13:29:30 2015 +0200
     2.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Jun 30 13:30:04 2015 +0200
     2.3 @@ -1547,25 +1547,25 @@
     2.4  
     2.5  lemma sup_continuous_nn_integral:
     2.6    assumes f: "\<And>y. sup_continuous (f y)"
     2.7 -  assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
     2.8 -  shows "sup_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
     2.9 +  assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
    2.10 +  shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))"
    2.11    unfolding sup_continuous_def
    2.12  proof safe
    2.13 -  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "incseq C"
    2.14 -  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))"
    2.15 -    using sup_continuous_mono[OF f]
    2.16 -    by (simp add: sup_continuousD[OF f C] fun_eq_iff nn_integral_monotone_convergence_SUP mono_def le_fun_def)
    2.17 +  fix C :: "nat \<Rightarrow> 'b" assume C: "incseq C"
    2.18 +  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)"
    2.19 +    unfolding sup_continuousD[OF f C]
    2.20 +    by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
    2.21  qed
    2.22  
    2.23  lemma inf_continuous_nn_integral:
    2.24    assumes f: "\<And>y. inf_continuous (f y)"
    2.25 -  assumes [measurable]: "\<And>F x. (\<lambda>y. f y F x) \<in> borel_measurable (M x)"
    2.26 -  assumes bnd: "\<And>x F. (\<integral>\<^sup>+ y. f y F x \<partial>M x) \<noteq> \<infinity>"
    2.27 -  shows "inf_continuous (\<lambda>F x. (\<integral>\<^sup>+y. f y F x \<partial>M x))"
    2.28 +  assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
    2.29 +  assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>"
    2.30 +  shows "inf_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))"
    2.31    unfolding inf_continuous_def
    2.32  proof safe
    2.33 -  fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume C: "decseq C"
    2.34 -  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))"
    2.35 +  fix C :: "nat \<Rightarrow> 'b" assume C: "decseq C"
    2.36 +  then show "(\<integral>\<^sup>+ y. f y (INFIMUM UNIV C) \<partial>M) = (INF i. \<integral>\<^sup>+ y. f y (C i) \<partial>M)"
    2.37      using inf_continuous_mono[OF f]
    2.38      by (auto simp add: inf_continuousD[OF f C] fun_eq_iff antimono_def mono_def le_fun_def bnd
    2.39               intro!:  nn_integral_monotone_convergence_INF)