stronger induction assumption in lfp_transfer and emeasure_lfp
authorhoelzl
Mon Jul 13 14:39:50 2015 +0200 (2015-07-13)
changeset 60714ff8aa76d6d1c
parent 60713 5240b2ed5189
child 60715 ee0afee54b1d
stronger induction assumption in lfp_transfer and emeasure_lfp
src/HOL/Library/Order_Continuity.thy
src/HOL/Probability/Measure_Space.thy
     1.1 --- a/src/HOL/Library/Order_Continuity.thy	Mon Jul 13 11:05:50 2015 +0200
     1.2 +++ b/src/HOL/Library/Order_Continuity.thy	Mon Jul 13 14:39:50 2015 +0200
     1.3 @@ -144,28 +144,16 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma lfp_transfer:
     1.8 -  assumes \<alpha>: "sup_continuous \<alpha>" and f: "sup_continuous f" and g: "sup_continuous g"
     1.9 -  assumes [simp]: "\<alpha> bot = bot" "\<And>x. \<alpha> (f x) = g (\<alpha> x)"
    1.10 -  shows "\<alpha> (lfp f) = lfp g"
    1.11 -proof -
    1.12 -  have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
    1.13 -    unfolding sup_continuous_lfp[OF f] by (intro f \<alpha> sup_continuousD mono_funpow sup_continuous_mono)
    1.14 -  moreover have "\<alpha> ((f^^i) bot) = (g^^i) bot" for i
    1.15 -    by (induction i; simp)
    1.16 -  ultimately show ?thesis
    1.17 -    unfolding sup_continuous_lfp[OF g] by simp
    1.18 -qed
    1.19 -
    1.20  lemma lfp_transfer_bounded:
    1.21    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)"
    1.22    assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
    1.23    assumes f: "sup_continuous f" and g: "sup_continuous g"
    1.24 -  assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
    1.25 +  assumes [simp]: "\<And>x. P x \<Longrightarrow> x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
    1.26    assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
    1.27    shows "\<alpha> (lfp f) = lfp g"
    1.28  proof (rule antisym)
    1.29    note mono_g = sup_continuous_mono[OF g]
    1.30 +  note mono_f = sup_continuous_mono[OF f]
    1.31    have lfp_bound: "\<alpha> bot \<le> lfp g"
    1.32      by (subst lfp_unfold[OF mono_g]) (rule g_bound)
    1.33  
    1.34 @@ -182,6 +170,13 @@
    1.35    have P_lfp: "P (lfp f)"
    1.36      using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
    1.37  
    1.38 +  have iter_le_lfp: "(f ^^ n) bot \<le> lfp f" for n
    1.39 +    apply (induction n)
    1.40 +    apply simp
    1.41 +    apply (subst lfp_unfold[OF mono_f])
    1.42 +    apply (auto intro!: monoD[OF mono_f])
    1.43 +    done
    1.44 +
    1.45    have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
    1.46      unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
    1.47    also have "\<dots> \<le> lfp g"
    1.48 @@ -189,7 +184,7 @@
    1.49      fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
    1.50      proof (induction i)
    1.51        case (Suc n) then show ?case
    1.52 -        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
    1.53 +        by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow iter_le_lfp)
    1.54      qed (simp add: lfp_bound)
    1.55    qed
    1.56    finally show "\<alpha> (lfp f) \<le> lfp g" .
    1.57 @@ -202,6 +197,11 @@
    1.58    qed (auto intro: Sup_least)
    1.59  qed
    1.60  
    1.61 +lemma lfp_transfer:
    1.62 +  "sup_continuous \<alpha> \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow>
    1.63 +    (\<And>x. \<alpha> bot \<le> g x) \<Longrightarrow> (\<And>x. x \<le> lfp f \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)) \<Longrightarrow> \<alpha> (lfp f) = lfp g"
    1.64 +  by (rule lfp_transfer_bounded[where P=top]) (auto dest: sup_continuousD)
    1.65 +
    1.66  definition
    1.67    inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
    1.68    "inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon Jul 13 11:05:50 2015 +0200
     2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon Jul 13 14:39:50 2015 +0200
     2.3 @@ -579,7 +579,7 @@
     2.4    assumes cont: "sup_continuous F" "sup_continuous f"
     2.5    assumes nonneg: "\<And>P s. 0 \<le> f P s"
     2.6    assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
     2.7 -  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"
     2.8 +  assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> P \<le> lfp F \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
     2.9    shows "emeasure (M s) {x\<in>space N. lfp F x} = lfp f s"
    2.10  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])
    2.11    fix C assume "incseq C" "\<And>i. Measurable.pred N (C i)"