author hoelzl Mon Jul 13 14:39:50 2015 +0200 (2015-07-13) changeset 60714 ff8aa76d6d1c parent 60713 5240b2ed5189 child 60715 ee0afee54b1d
stronger induction assumption in lfp_transfer and emeasure_lfp
```     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.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)"
```