# 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 (\x. f (f x))" -proof (rule antisym) - show "lfp f \ lfp (\x. f (f x))" - by (intro lfp_lowerbound) (simp add: assms lfp_rolling) - show "lfp (\x. f (f x)) \ lfp f" - by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric]) -qed - lemma lfp_lfp: assumes f: "\x y w z. x \ y \ w \ z \ f x w \ f y z" shows "lfp (\x. lfp (f x)) = lfp (\x. f x x)" @@ -330,15 +320,6 @@ qed qed -lemma gfp_square: - assumes "mono f" shows "gfp f = gfp (\x. f (f x))" -proof (rule antisym) - show "gfp (\x. f (f x)) \ gfp f" - by (intro gfp_upperbound) (simp add: assms gfp_rolling) - show "gfp f \ gfp (\x. f (f x))" - by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric]) -qed - lemma gfp_gfp: assumes f: "\x y w z. x \ y \ w \ z \ f x w \ f y z" shows "gfp (\x. gfp (f x)) = gfp (\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 \Extended natural numbers (i.e. with infinity)\ 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 \ {}" + 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 \ {} \ 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 \ sup_continuous (\x. eSuc (f x))" + using eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def) + subsection \Traditional theorem names\ 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 \Extended real number line\ theory Extended_Real -imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity +imports Complex_Main Extended_Nat Liminf_Limsup begin text \ @@ -2768,6 +2768,18 @@ qed qed +lemma not_MInfty_nonneg[simp]: "0 \ (x::ereal) \ x \ - \" + by auto + +lemma sup_continuous_add_left[order_continuous_intros]: "0 \ c \ sup_continuous f \ sup_continuous (\x. f x + c :: ereal)" + by (auto simp: sup_continuous_def SUP_ereal_add_left) + +lemma sup_continuous_add_right[order_continuous_intros]: "0 \ c \ sup_continuous f \ sup_continuous (\x. c + f x :: ereal)" + using sup_continuous_add_left by (simp add: ac_simps) + +lemma sup_continuous_multc[order_continuous_intros]: "0 \ c \ c < \ \ sup_continuous (\f s. f s * c :: ereal)" + by (cases c) (auto simp: sup_continuous_def fun_eq_iff Sup_ereal_mult_right') + subsubsection \Tests for code generator\ (* 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 \Continuity and iterations (of set transformers)\ 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. \ +named_theorems order_continuous_intros + subsection \Continuity for complete lattices\ 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 (\x. c)" and sup_continuous_id: "sup_continuous (\x. x)" and sup_continuous_apply: "sup_continuous (\f. f x)" and sup_continuous_fun: "(\s. sup_continuous (\x. P x s)) \ sup_continuous P" - by (auto simp: sup_continuous_def) + and sup_continuous_If: "sup_continuous F \ sup_continuous G \ sup_continuous (\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 \ sup_continuous g \ sup_continuous (\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 \ 'b :: complete_distrib_lattice" + assumes P: "sup_continuous P" and Q: "sup_continuous Q" + shows "sup_continuous (\x. inf (P x) (Q x))" + unfolding sup_continuous_def +proof (safe intro!: antisym) + fix M :: "nat \ 'a" assume M: "incseq M" + have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \ (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 "\ \ (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)) \ (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)) \ (SUP i. inf (P (M i)) (Q (M i)))" . + + show "(SUP i. inf (P (M i)) (Q (M i))) \ 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 \ sup_continuous Q \ sup_continuous (\x. P x \ Q x)" + using sup_continuous_inf[of P Q] by simp + +lemma sup_continuous_or[order_continuous_intros]: + "sup_continuous P \ sup_continuous Q \ sup_continuous (\x. P x \ 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" "\x. P x \ P (f x)" "\M. (\i. P (M i)) \ P (SUP i::nat. M i)" + assumes \: "\M. mono M \ (\i::nat. P (M i)) \ \ (SUP i. M i) = (SUP i. \ (M i))" + assumes f: "sup_continuous f" and g: "sup_continuous g" + assumes [simp]: "\x. P x \ \ (f x) = g (\ x)" + assumes g_bound: "\x. \ bot \ g x" + shows "\ (lfp f) = lfp g" +proof (rule antisym) + note mono_g = sup_continuous_mono[OF g] + have lfp_bound: "\ bot \ 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 (\i. (f ^^ i) bot)" + unfolding mono_iff_le_Suc + proof + fix i show "(f ^^ i) bot \ (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 "\ (lfp f) = (SUP i. \ ((f^^i) bot))" + unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \) + also have "\ \ lfp g" + proof (rule SUP_least) + fix i show "\ ((f^^i) bot) \ 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 "\ (lfp f) \ lfp g" . + + show "lfp g \ \ (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 \ 'b::complete_lattice) \ bool" where "inf_continuous F \ (\M::nat \ 'a. antimono M \ 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 (\x. c)" and inf_continuous_id: "inf_continuous (\x. x)" and inf_continuous_apply: "inf_continuous (\f. f x)" and inf_continuous_fun: "(\s. inf_continuous (\x. P x s)) \ inf_continuous P" - by (auto simp: inf_continuous_def) + and inf_continuous_If: "inf_continuous F \ inf_continuous G \ inf_continuous (\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 \ inf_continuous g \ inf_continuous (\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 \ 'b :: complete_distrib_lattice" + assumes P: "inf_continuous P" and Q: "inf_continuous Q" + shows "inf_continuous (\x. sup (P x) (Q x))" + unfolding inf_continuous_def +proof (safe intro!: antisym) + fix M :: "nat \ 'a" assume M: "decseq M" + show "sup (P (INF i. M i)) (Q (INF i. M i)) \ (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))) \ (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)) \ (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 "\ \ 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)) \ (INF i. sup (P (M i)) (Q (M i)))" . +qed + +lemma inf_continuous_and[order_continuous_intros]: + "inf_continuous P \ inf_continuous Q \ inf_continuous (\x. P x \ Q x)" + using inf_continuous_inf[of P Q] by simp + +lemma inf_continuous_or[order_continuous_intros]: + "inf_continuous P \ inf_continuous Q \ inf_continuous (\x. P x \ 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)" "\x. P x \ P (f x)" "\M. antimono M \ (\i. P (M i)) \ P (INF i::nat. M i)" + assumes \: "\M. antimono M \ (\i::nat. P (M i)) \ \ (INF i. M i) = (INF i. \ (M i))" + assumes f: "inf_continuous f" and g: "inf_continuous g" + assumes [simp]: "\x. P x \ \ (f x) = g (\ x)" + assumes g_bound: "\x. g x \ \ (f top)" + shows "\ (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 (\i. (f ^^ i) top)" + unfolding antimono_iff_le_Suc + proof + fix i show "(f ^^ Suc i) top \ (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 (\i. (f ^^ i) (f top))" + proof + show "x \ y \ (f ^^ y) (f top) \ (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 "\j\UNIV. (f ^^ j) (f top) \ (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 "\j\UNIV. (f ^^ j) top \ (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 "\ (gfp f) = (INF i. \ ((f^^i) (f top)))" + unfolding gfp_f by (rule \) (auto intro!: P_pow antimono_pow2) + also have "\ \ gfp g" + proof (rule INF_greatest) + fix i show "gfp g \ \ ((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 \ \ (f top)" + by (subst gfp_unfold[OF mono_g]) (rule g_bound) + then show ?case + by simp + qed + qed + finally show "gfp g \ \ (gfp f)" . + + show "\ (gfp f) \ 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 \ 'a::complete_lattice" + shows "mono f \ 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 \ lfp (f ^^ Suc n)" + proof (rule lfp_lowerbound) + have "f (lfp (f ^^ Suc n)) = lfp (\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)) \ 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) \ 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 \ gfp (f ^^ Suc n)" + proof (rule gfp_upperbound) + have "f (gfp (f ^^ Suc n)) = gfp (\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)) \ 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) \ 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 *: "\M A. P M \ (\N. P N \ Measurable.pred N A) \ Measurable.pred M (F A)" @@ -574,6 +574,20 @@ by (subst SUP_emeasure_incseq) auto qed +lemma emeasure_lfp: + assumes [simp]: "\s. sets (M s) = sets N" + assumes cont: "sup_continuous F" "sup_continuous f" + assumes nonneg: "\P s. 0 \ f P s" + assumes meas: "\P. Measurable.pred N P \ Measurable.pred N (F P)" + assumes iter: "\P s. Measurable.pred N P \ emeasure (M s) {x\space N. F P x} = f (\s. emeasure (M s) {x\space N. P x}) s" + shows "emeasure (M s) {x\space N. lfp F x} = lfp f s" +proof (subst lfp_transfer_bounded[where \="\F s. emeasure (M s) {x\space N. F x}" and g=f and f=F and P="Measurable.pred N", symmetric]) + fix C assume "incseq C" "\i. Measurable.pred N (C i)" + then show "(\s. emeasure (M s) {x \ space N. (SUP i. C i) x}) = (SUP i. (\s. emeasure (M s) {x \ 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 \ sets M" "B \ sets M" shows "emeasure M (A \ B) \ emeasure M A + emeasure M B" @@ -1254,7 +1268,7 @@ have "emeasure (distr M' M f) {x \ space (distr M' M f). lfp F x} = (SUP i. emeasure (distr M' M f) {x \ space (distr M' M f). (F ^^ i) (\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 "\N. P N \ Measurable.pred (distr M' N f) A" by metis then have "\N. P N \ Measurable.pred N A" @@ -1662,6 +1676,26 @@ with f show "emeasure (distr M M' f) (space (distr M M' f)) \ \" by (auto simp: emeasure_distr) qed +lemma emeasure_gfp[consumes 1, case_names cont measurable]: + assumes sets[simp]: "\s. sets (M s) = sets N" + assumes "\s. finite_measure (M s)" + assumes cont: "inf_continuous F" "inf_continuous f" + assumes meas: "\P. Measurable.pred N P \ Measurable.pred N (F P)" + assumes iter: "\P s. Measurable.pred N P \ emeasure (M s) {x\space N. F P x} = f (\s. emeasure (M s) {x\space N. P x}) s" + assumes bound: "\P. f P \ f (\s. emeasure (M s) (space (M s)))" + shows "emeasure (M s) {x\space N. gfp F x} = gfp f s" +proof (subst gfp_transfer_bounded[where \="\F s. emeasure (M s) {x\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" "\i. Measurable.pred N (C i)" + then show "(\s. emeasure (M s) {x \ space N. (INF i. C i) x}) = (INF i. (\s. emeasure (M s) {x \ 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 \ (\s. emeasure (M s) {x \ 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: "\y. sup_continuous (f y)" assumes [measurable]: "\x. (\y. f y x) \ borel_measurable M" shows "sup_continuous (\x. (\\<^sup>+y. f y x \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: "\y. inf_continuous (f y)" assumes [measurable]: "\x. (\y. f y x) \ borel_measurable M" assumes bnd: "\x. (\\<^sup>+ y. f y x \M) \ \" @@ -1739,122 +1739,57 @@ qed lemma nn_integral_lfp: - assumes sets: "\s. sets (M s) = sets N" + assumes sets[simp]: "\s. sets (M s) = sets N" assumes f: "sup_continuous f" + assumes g: "sup_continuous g" + assumes nonneg: "\F s. 0 \ g F s" assumes meas: "\F. F \ borel_measurable N \ f F \ borel_measurable N" - assumes nonneg: "\F s. 0 \ g F s" - assumes g: "sup_continuous g" assumes step: "\F s. F \ borel_measurable N \ integral\<^sup>N (M s) (f F) = g (\s. integral\<^sup>N (M s) F) s" shows "(\\<^sup>+\. lfp f \ \M s) = lfp g s" -proof (rule antisym) - show "lfp g s \ (\\<^sup>+\. lfp f \ \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: "\s. 0 \ lfp g s" - by (subst lfp_unfold[OF sup_continuous_mono[OF g]]) (rule nonneg) - - { fix i have "((f ^^ i) bot) \ borel_measurable N" - by (induction i) (simp_all add: meas) } - - have "(\\<^sup>+\. lfp f \ \M s) = (\\<^sup>+\. (SUP i. (f ^^ i) bot \) \M s)" - by (simp add: sup_continuous_lfp f) - also have "\ = (SUP i. \\<^sup>+\. (f ^^ i) bot \ \M s)" - proof (rule nn_integral_monotone_convergence_SUP) - show "incseq (\i. (f ^^ i) bot)" - using f[THEN sup_continuous_mono] by (rule mono_funpow) - show "\i. ((f ^^ i) bot) \ borel_measurable (M s)" - unfolding measurable_cong_sets[OF sets refl] by fact - qed - also have "\ \ lfp g s" - proof (rule SUP_least) - fix i show "integral\<^sup>N (M s) ((f ^^ i) bot) \ 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 "(\\<^sup>+\. lfp f \ \M s) \ lfp g s" . -qed +proof (subst lfp_transfer_bounded[where \="\F s. \\<^sup>+x. F x \M s" and g=g and f=f and P="\f. f \ borel_measurable N", symmetric]) + fix C :: "nat \ 'b \ ereal" assume "incseq C" "\i. C i \ borel_measurable N" + then show "(\s. \\<^sup>+x. (SUP i. C i) x \M s) = (SUP i. (\s. \\<^sup>+x. C i x \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 "\x. (\s. integral\<^sup>N (M s) bot) \ 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: "\s. sets (M s) = sets N" - assumes f: "inf_continuous f" + assumes sets[simp]: "\s. sets (M s) = sets N" + assumes f: "inf_continuous f" and g: "inf_continuous g" assumes meas: "\F. F \ borel_measurable N \ f F \ borel_measurable N" - assumes bound: "\F s. (\\<^sup>+x. f F x \M s) < \" + assumes bound: "\F s. F \ borel_measurable N \ (\\<^sup>+x. f F x \M s) < \" assumes non_zero: "\s. emeasure (M s) (space (M s)) \ 0" - assumes g: "inf_continuous g" assumes step: "\F s. F \ borel_measurable N \ integral\<^sup>N (M s) (f F) = g (\s. integral\<^sup>N (M s) F) s" shows "(\\<^sup>+\. gfp f \ \M s) = gfp g s" -proof (rule antisym) - show "(\\<^sup>+\. gfp f \ \M s) \ 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) \ borel_measurable N" - by (induction i) (simp_all add: meas) } - - have "(\\<^sup>+\. gfp f \ \M s) = (\\<^sup>+\. (INF i. (f ^^ i) top \) \M s)" - by (simp add: inf_continuous_gfp f) - also have "\ = (INF i. \\<^sup>+\. (f ^^ i) top \ \M s)" - proof (rule nn_integral_monotone_convergence_INF) - show "decseq (\i. (f ^^ i) top)" - using f[THEN inf_continuous_mono] by (rule antimono_funpow) - show "\i. ((f ^^ i) top) \ borel_measurable (M s)" - unfolding measurable_cong_sets[OF sets refl] by fact - show "integral\<^sup>N (M s) ((f ^^ 1) top) < \" - using bound[of s top] by simp - qed - also have "\ \ gfp g s" - proof (rule INF_greatest) - fix i show "gfp g s \ 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 \ (\\<^sup>+\. gfp f \ \M s)" . -qed +proof (subst gfp_transfer_bounded[where \="\F s. \\<^sup>+x. F x \M s" and g=g and f=f + and P="\F. F \ borel_measurable N \ (\s. (\\<^sup>+x. F x \M s) < \)", symmetric]) + fix C :: "nat \ 'b \ ereal" assume "decseq C" "\i. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" + then show "(\s. \\<^sup>+x. (INF i. C i) x \M s) = (INF i. (\s. \\<^sup>+x. C i x \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 "\x. g x \ (\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 "\i::nat. C i \ borel_measurable N \ (\s. integral\<^sup>N (M s) (C i) < \)" "decseq C" + with bound show "INFIMUM UNIV C \ borel_measurable N \ (\s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \)" + 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 "\x. x \ borel_measurable N \ (\s. integral\<^sup>N (M s) x < \) \ + (\s. integral\<^sup>N (M s) (f x)) = g (\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 "\ y \ x" hence "y > x" by simp hence "y \ - \" by auto hence y_fin: "\y\ \ \" using `y \ \` by auto have x_fin: "\x\ \ \" 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 \ "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 \ A" "x + e \ f i" by blast