src/HOL/Probability/Measurable.thy
 author hoelzl Tue May 20 19:24:39 2014 +0200 (2014-05-20) changeset 57025 e7fd64f82876 parent 56993 e5366291d6aa child 58965 a62cdcc5344b permissions -rw-r--r--
 wenzelm@50530 ` 1` ```(* Title: HOL/Probability/Measurable.thy ``` hoelzl@50387 ` 2` ``` Author: Johannes Hölzl ``` hoelzl@50387 ` 3` ```*) ``` hoelzl@50387 ` 4` ```theory Measurable ``` hoelzl@56021 ` 5` ``` imports ``` hoelzl@56021 ` 6` ``` Sigma_Algebra ``` hoelzl@56021 ` 7` ``` "~~/src/HOL/Library/Order_Continuity" ``` hoelzl@50387 ` 8` ```begin ``` hoelzl@50387 ` 9` hoelzl@56021 ` 10` ```hide_const (open) Order_Continuity.continuous ``` hoelzl@56021 ` 11` hoelzl@50387 ` 12` ```subsection {* Measurability prover *} ``` hoelzl@50387 ` 13` hoelzl@50387 ` 14` ```lemma (in algebra) sets_Collect_finite_All: ``` hoelzl@50387 ` 15` ``` assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S" ``` hoelzl@50387 ` 16` ``` shows "{x\\. \i\S. P i x} \ M" ``` hoelzl@50387 ` 17` ```proof - ``` hoelzl@50387 ` 18` ``` have "{x\\. \i\S. P i x} = (if S = {} then \ else \i\S. {x\\. P i x})" ``` hoelzl@50387 ` 19` ``` by auto ``` hoelzl@50387 ` 20` ``` with assms show ?thesis by (auto intro!: sets_Collect_finite_All') ``` hoelzl@50387 ` 21` ```qed ``` hoelzl@50387 ` 22` hoelzl@50387 ` 23` ```abbreviation "pred M P \ P \ measurable M (count_space (UNIV::bool set))" ``` hoelzl@50387 ` 24` hoelzl@50387 ` 25` ```lemma pred_def: "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 26` ```proof ``` hoelzl@50387 ` 27` ``` assume "pred M P" ``` hoelzl@50387 ` 28` ``` then have "P -` {True} \ space M \ sets M" ``` hoelzl@50387 ` 29` ``` by (auto simp: measurable_count_space_eq2) ``` hoelzl@50387 ` 30` ``` also have "P -` {True} \ space M = {x\space M. P x}" by auto ``` hoelzl@50387 ` 31` ``` finally show "{x\space M. P x} \ sets M" . ``` hoelzl@50387 ` 32` ```next ``` hoelzl@50387 ` 33` ``` assume P: "{x\space M. P x} \ sets M" ``` hoelzl@50387 ` 34` ``` moreover ``` hoelzl@50387 ` 35` ``` { fix X ``` hoelzl@50387 ` 36` ``` have "X \ Pow (UNIV :: bool set)" by simp ``` hoelzl@50387 ` 37` ``` then have "P -` X \ space M = {x\space M. ((X = {True} \ P x) \ (X = {False} \ \ P x) \ X \ {})}" ``` hoelzl@50387 ` 38` ``` unfolding UNIV_bool Pow_insert Pow_empty by auto ``` hoelzl@50387 ` 39` ``` then have "P -` X \ space M \ sets M" ``` hoelzl@50387 ` 40` ``` by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } ``` hoelzl@50387 ` 41` ``` then show "pred M P" ``` hoelzl@50387 ` 42` ``` by (auto simp: measurable_def) ``` hoelzl@50387 ` 43` ```qed ``` hoelzl@50387 ` 44` hoelzl@50387 ` 45` ```lemma pred_sets1: "{x\space M. P x} \ sets M \ f \ measurable N M \ pred N (\x. P (f x))" ``` hoelzl@50387 ` 46` ``` by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) ``` hoelzl@50387 ` 47` hoelzl@50387 ` 48` ```lemma pred_sets2: "A \ sets N \ f \ measurable M N \ pred M (\x. f x \ A)" ``` hoelzl@50387 ` 49` ``` by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) ``` hoelzl@50387 ` 50` hoelzl@50387 ` 51` ```ML_file "measurable.ML" ``` hoelzl@50387 ` 52` wenzelm@53043 ` 53` ```attribute_setup measurable = {* ``` wenzelm@53043 ` 54` ``` Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.\$\$\$ "raw" >> K true) false -- ``` wenzelm@53043 ` 55` ``` Scan.optional (Args.\$\$\$ "generic" >> K Measurable.Generic) Measurable.Concrete)) ``` wenzelm@53043 ` 56` ``` (false, Measurable.Concrete) >> (Thm.declaration_attribute o Measurable.add_thm)) ``` wenzelm@53043 ` 57` ```*} "declaration of measurability theorems" ``` wenzelm@53043 ` 58` wenzelm@53043 ` 59` ```attribute_setup measurable_dest = {* ``` wenzelm@53043 ` 60` ``` Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest)) ``` wenzelm@53043 ` 61` ```*} "add dest rule for measurability prover" ``` wenzelm@53043 ` 62` wenzelm@53043 ` 63` ```attribute_setup measurable_app = {* ``` wenzelm@53043 ` 64` ``` Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app)) ``` wenzelm@53043 ` 65` ```*} "add application rule for measurability prover" ``` wenzelm@53043 ` 66` wenzelm@53043 ` 67` ```method_setup measurable = {* ``` wenzelm@53043 ` 68` ``` Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts))) ``` wenzelm@53043 ` 69` ```*} "measurability prover" ``` wenzelm@53043 ` 70` hoelzl@50387 ` 71` ```simproc_setup measurable ("A \ sets M" | "f \ measurable M N") = {* K Measurable.simproc *} ``` hoelzl@50387 ` 72` hoelzl@50387 ` 73` ```declare ``` hoelzl@50387 ` 74` ``` measurable_compose_rev[measurable_dest] ``` hoelzl@50387 ` 75` ``` pred_sets1[measurable_dest] ``` hoelzl@50387 ` 76` ``` pred_sets2[measurable_dest] ``` hoelzl@50387 ` 77` ``` sets.sets_into_space[measurable_dest] ``` hoelzl@50387 ` 78` hoelzl@50387 ` 79` ```declare ``` hoelzl@50387 ` 80` ``` sets.top[measurable] ``` hoelzl@50387 ` 81` ``` sets.empty_sets[measurable (raw)] ``` hoelzl@50387 ` 82` ``` sets.Un[measurable (raw)] ``` hoelzl@50387 ` 83` ``` sets.Diff[measurable (raw)] ``` hoelzl@50387 ` 84` hoelzl@50387 ` 85` ```declare ``` hoelzl@50387 ` 86` ``` measurable_count_space[measurable (raw)] ``` hoelzl@50387 ` 87` ``` measurable_ident[measurable (raw)] ``` hoelzl@50387 ` 88` ``` measurable_ident_sets[measurable (raw)] ``` hoelzl@50387 ` 89` ``` measurable_const[measurable (raw)] ``` hoelzl@50387 ` 90` ``` measurable_If[measurable (raw)] ``` hoelzl@50387 ` 91` ``` measurable_comp[measurable (raw)] ``` hoelzl@50387 ` 92` ``` measurable_sets[measurable (raw)] ``` hoelzl@50387 ` 93` hoelzl@50387 ` 94` ```lemma predE[measurable (raw)]: ``` hoelzl@50387 ` 95` ``` "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 96` ``` unfolding pred_def . ``` hoelzl@50387 ` 97` hoelzl@50387 ` 98` ```lemma pred_intros_imp'[measurable (raw)]: ``` hoelzl@50387 ` 99` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 100` ``` by (cases K) auto ``` hoelzl@50387 ` 101` hoelzl@50387 ` 102` ```lemma pred_intros_conj1'[measurable (raw)]: ``` hoelzl@50387 ` 103` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 104` ``` by (cases K) auto ``` hoelzl@50387 ` 105` hoelzl@50387 ` 106` ```lemma pred_intros_conj2'[measurable (raw)]: ``` hoelzl@50387 ` 107` ``` "(K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 108` ``` by (cases K) auto ``` hoelzl@50387 ` 109` hoelzl@50387 ` 110` ```lemma pred_intros_disj1'[measurable (raw)]: ``` hoelzl@50387 ` 111` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 112` ``` by (cases K) auto ``` hoelzl@50387 ` 113` hoelzl@50387 ` 114` ```lemma pred_intros_disj2'[measurable (raw)]: ``` hoelzl@50387 ` 115` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 116` ``` by (cases K) auto ``` hoelzl@50387 ` 117` hoelzl@50387 ` 118` ```lemma pred_intros_logic[measurable (raw)]: ``` hoelzl@50387 ` 119` ``` "pred M (\x. x \ space M)" ``` hoelzl@50387 ` 120` ``` "pred M (\x. P x) \ pred M (\x. \ P x)" ``` hoelzl@50387 ` 121` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 122` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 123` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 124` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x = P x)" ``` hoelzl@50387 ` 125` ``` "pred M (\x. f x \ UNIV)" ``` hoelzl@50387 ` 126` ``` "pred M (\x. f x \ {})" ``` hoelzl@50387 ` 127` ``` "pred M (\x. P' (f x) x) \ pred M (\x. f x \ {y. P' y x})" ``` hoelzl@50387 ` 128` ``` "pred M (\x. f x \ (B x)) \ pred M (\x. f x \ - (B x))" ``` hoelzl@50387 ` 129` ``` "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) - (B x))" ``` hoelzl@50387 ` 130` ``` "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) \ (B x))" ``` hoelzl@50387 ` 131` ``` "pred M (\x. f x \ (A x)) \ pred M (\x. f x \ (B x)) \ pred M (\x. f x \ (A x) \ (B x))" ``` hoelzl@50387 ` 132` ``` "pred M (\x. g x (f x) \ (X x)) \ pred M (\x. f x \ (g x) -` (X x))" ``` hoelzl@50387 ` 133` ``` by (auto simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 134` hoelzl@50387 ` 135` ```lemma pred_intros_countable[measurable (raw)]: ``` hoelzl@50387 ` 136` ``` fixes P :: "'a \ 'i :: countable \ bool" ``` hoelzl@50387 ` 137` ``` shows ``` hoelzl@50387 ` 138` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 139` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 140` ``` by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) ``` hoelzl@50387 ` 141` hoelzl@50387 ` 142` ```lemma pred_intros_countable_bounded[measurable (raw)]: ``` hoelzl@50387 ` 143` ``` fixes X :: "'i :: countable set" ``` hoelzl@50387 ` 144` ``` shows ``` hoelzl@50387 ` 145` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 146` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 147` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 148` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 149` ``` by (auto simp: Bex_def Ball_def) ``` hoelzl@50387 ` 150` hoelzl@50387 ` 151` ```lemma pred_intros_finite[measurable (raw)]: ``` hoelzl@50387 ` 152` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 153` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 154` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 155` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 156` ``` by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 157` hoelzl@50387 ` 158` ```lemma countable_Un_Int[measurable (raw)]: ``` hoelzl@50387 ` 159` ``` "(\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 160` ``` "I \ {} \ (\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 161` ``` by auto ``` hoelzl@50387 ` 162` hoelzl@50387 ` 163` ```declare ``` hoelzl@50387 ` 164` ``` finite_UN[measurable (raw)] ``` hoelzl@50387 ` 165` ``` finite_INT[measurable (raw)] ``` hoelzl@50387 ` 166` hoelzl@50387 ` 167` ```lemma sets_Int_pred[measurable (raw)]: ``` hoelzl@50387 ` 168` ``` assumes space: "A \ B \ space M" and [measurable]: "pred M (\x. x \ A)" "pred M (\x. x \ B)" ``` hoelzl@50387 ` 169` ``` shows "A \ B \ sets M" ``` hoelzl@50387 ` 170` ```proof - ``` hoelzl@50387 ` 171` ``` have "{x\space M. x \ A \ B} \ sets M" by auto ``` hoelzl@50387 ` 172` ``` also have "{x\space M. x \ A \ B} = A \ B" ``` hoelzl@50387 ` 173` ``` using space by auto ``` hoelzl@50387 ` 174` ``` finally show ?thesis . ``` hoelzl@50387 ` 175` ```qed ``` hoelzl@50387 ` 176` hoelzl@50387 ` 177` ```lemma [measurable (raw generic)]: ``` hoelzl@50387 ` 178` ``` assumes f: "f \ measurable M N" and c: "c \ space N \ {c} \ sets N" ``` hoelzl@50387 ` 179` ``` shows pred_eq_const1: "pred M (\x. f x = c)" ``` hoelzl@50387 ` 180` ``` and pred_eq_const2: "pred M (\x. c = f x)" ``` hoelzl@50387 ` 181` ```proof - ``` hoelzl@50387 ` 182` ``` show "pred M (\x. f x = c)" ``` hoelzl@50387 ` 183` ``` proof cases ``` hoelzl@50387 ` 184` ``` assume "c \ space N" ``` hoelzl@50387 ` 185` ``` with measurable_sets[OF f c] show ?thesis ``` hoelzl@50387 ` 186` ``` by (auto simp: Int_def conj_commute pred_def) ``` hoelzl@50387 ` 187` ``` next ``` hoelzl@50387 ` 188` ``` assume "c \ space N" ``` hoelzl@50387 ` 189` ``` with f[THEN measurable_space] have "{x \ space M. f x = c} = {}" by auto ``` hoelzl@50387 ` 190` ``` then show ?thesis by (auto simp: pred_def cong: conj_cong) ``` hoelzl@50387 ` 191` ``` qed ``` hoelzl@50387 ` 192` ``` then show "pred M (\x. c = f x)" ``` hoelzl@50387 ` 193` ``` by (simp add: eq_commute) ``` hoelzl@50387 ` 194` ```qed ``` hoelzl@50387 ` 195` hoelzl@50387 ` 196` ```lemma pred_le_const[measurable (raw generic)]: ``` hoelzl@50387 ` 197` ``` assumes f: "f \ measurable M N" and c: "{.. c} \ sets N" shows "pred M (\x. f x \ c)" ``` hoelzl@50387 ` 198` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 199` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 200` hoelzl@50387 ` 201` ```lemma pred_const_le[measurable (raw generic)]: ``` hoelzl@50387 ` 202` ``` assumes f: "f \ measurable M N" and c: "{c ..} \ sets N" shows "pred M (\x. c \ f x)" ``` hoelzl@50387 ` 203` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 204` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 205` hoelzl@50387 ` 206` ```lemma pred_less_const[measurable (raw generic)]: ``` hoelzl@50387 ` 207` ``` assumes f: "f \ measurable M N" and c: "{..< c} \ sets N" shows "pred M (\x. f x < c)" ``` hoelzl@50387 ` 208` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 209` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 210` hoelzl@50387 ` 211` ```lemma pred_const_less[measurable (raw generic)]: ``` hoelzl@50387 ` 212` ``` assumes f: "f \ measurable M N" and c: "{c <..} \ sets N" shows "pred M (\x. c < f x)" ``` hoelzl@50387 ` 213` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 214` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 215` hoelzl@50387 ` 216` ```declare ``` hoelzl@50387 ` 217` ``` sets.Int[measurable (raw)] ``` hoelzl@50387 ` 218` hoelzl@50387 ` 219` ```lemma pred_in_If[measurable (raw)]: ``` hoelzl@50387 ` 220` ``` "(P \ pred M (\x. x \ A x)) \ (\ P \ pred M (\x. x \ B x)) \ ``` hoelzl@50387 ` 221` ``` pred M (\x. x \ (if P then A x else B x))" ``` hoelzl@50387 ` 222` ``` by auto ``` hoelzl@50387 ` 223` hoelzl@50387 ` 224` ```lemma sets_range[measurable_dest]: ``` hoelzl@50387 ` 225` ``` "A ` I \ sets M \ i \ I \ A i \ sets M" ``` hoelzl@50387 ` 226` ``` by auto ``` hoelzl@50387 ` 227` hoelzl@50387 ` 228` ```lemma pred_sets_range[measurable_dest]: ``` hoelzl@50387 ` 229` ``` "A ` I \ sets N \ i \ I \ f \ measurable M N \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 230` ``` using pred_sets2[OF sets_range] by auto ``` hoelzl@50387 ` 231` hoelzl@50387 ` 232` ```lemma sets_All[measurable_dest]: ``` hoelzl@50387 ` 233` ``` "\i. A i \ sets (M i) \ A i \ sets (M i)" ``` hoelzl@50387 ` 234` ``` by auto ``` hoelzl@50387 ` 235` hoelzl@50387 ` 236` ```lemma pred_sets_All[measurable_dest]: ``` hoelzl@50387 ` 237` ``` "\i. A i \ sets (N i) \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 238` ``` using pred_sets2[OF sets_All, of A N f] by auto ``` hoelzl@50387 ` 239` hoelzl@50387 ` 240` ```lemma sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 241` ``` "\i\I. A i \ sets (M i) \ i\I \ A i \ sets (M i)" ``` hoelzl@50387 ` 242` ``` by auto ``` hoelzl@50387 ` 243` hoelzl@50387 ` 244` ```lemma pred_sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 245` ``` "\i\I. A i \ sets (N i) \ i\I \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 246` ``` using pred_sets2[OF sets_Ball, of _ _ _ f] by auto ``` hoelzl@50387 ` 247` hoelzl@50387 ` 248` ```lemma measurable_finite[measurable (raw)]: ``` hoelzl@50387 ` 249` ``` fixes S :: "'a \ nat set" ``` hoelzl@50387 ` 250` ``` assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M" ``` hoelzl@50387 ` 251` ``` shows "pred M (\x. finite (S x))" ``` hoelzl@50387 ` 252` ``` unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) ``` hoelzl@50387 ` 253` hoelzl@50387 ` 254` ```lemma measurable_Least[measurable]: ``` hoelzl@50387 ` 255` ``` assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))"q ``` hoelzl@50387 ` 256` ``` shows "(\x. LEAST i. P i x) \ measurable M (count_space UNIV)" ``` hoelzl@50387 ` 257` ``` unfolding measurable_def by (safe intro!: sets_Least) simp_all ``` hoelzl@50387 ` 258` hoelzl@56993 ` 259` ```lemma measurable_Max_nat[measurable (raw)]: ``` hoelzl@56993 ` 260` ``` fixes P :: "nat \ 'a \ bool" ``` hoelzl@56993 ` 261` ``` assumes [measurable]: "\i. Measurable.pred M (P i)" ``` hoelzl@56993 ` 262` ``` shows "(\x. Max {i. P i x}) \ measurable M (count_space UNIV)" ``` hoelzl@56993 ` 263` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@56993 ` 264` ```proof safe ``` hoelzl@56993 ` 265` ``` fix n ``` hoelzl@56993 ` 266` hoelzl@56993 ` 267` ``` { fix x assume "\i. \n\i. P n x" ``` hoelzl@56993 ` 268` ``` then have "infinite {i. P i x}" ``` hoelzl@56993 ` 269` ``` unfolding infinite_nat_iff_unbounded_le by auto ``` hoelzl@56993 ` 270` ``` then have "Max {i. P i x} = the None" ``` hoelzl@56993 ` 271` ``` by (rule Max.infinite) } ``` hoelzl@56993 ` 272` ``` note 1 = this ``` hoelzl@56993 ` 273` hoelzl@56993 ` 274` ``` { fix x i j assume "P i x" "\n\j. \ P n x" ``` hoelzl@56993 ` 275` ``` then have "finite {i. P i x}" ``` hoelzl@56993 ` 276` ``` by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) ``` hoelzl@56993 ` 277` ``` with `P i x` have "P (Max {i. P i x}) x" "i \ Max {i. P i x}" "finite {i. P i x}" ``` hoelzl@56993 ` 278` ``` using Max_in[of "{i. P i x}"] by auto } ``` hoelzl@56993 ` 279` ``` note 2 = this ``` hoelzl@56993 ` 280` hoelzl@56993 ` 281` ``` have "(\x. Max {i. P i x}) -` {n} \ space M = {x\space M. Max {i. P i x} = n}" ``` hoelzl@56993 ` 282` ``` by auto ``` hoelzl@56993 ` 283` ``` also have "\ = ``` hoelzl@56993 ` 284` ``` {x\space M. if (\i. \n\i. P n x) then the None = n else ``` hoelzl@56993 ` 285` ``` if (\i. P i x) then P n x \ (\i>n. \ P i x) ``` hoelzl@56993 ` 286` ``` else Max {} = n}" ``` hoelzl@56993 ` 287` ``` by (intro arg_cong[where f=Collect] ext conj_cong) ``` hoelzl@56993 ` 288` ``` (auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI) ``` hoelzl@56993 ` 289` ``` also have "\ \ sets M" ``` hoelzl@56993 ` 290` ``` by measurable ``` hoelzl@56993 ` 291` ``` finally show "(\x. Max {i. P i x}) -` {n} \ space M \ sets M" . ``` hoelzl@56993 ` 292` ```qed simp ``` hoelzl@56993 ` 293` hoelzl@56993 ` 294` ```lemma measurable_Min_nat[measurable (raw)]: ``` hoelzl@56993 ` 295` ``` fixes P :: "nat \ 'a \ bool" ``` hoelzl@56993 ` 296` ``` assumes [measurable]: "\i. Measurable.pred M (P i)" ``` hoelzl@56993 ` 297` ``` shows "(\x. Min {i. P i x}) \ measurable M (count_space UNIV)" ``` hoelzl@56993 ` 298` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@56993 ` 299` ```proof safe ``` hoelzl@56993 ` 300` ``` fix n ``` hoelzl@56993 ` 301` hoelzl@56993 ` 302` ``` { fix x assume "\i. \n\i. P n x" ``` hoelzl@56993 ` 303` ``` then have "infinite {i. P i x}" ``` hoelzl@56993 ` 304` ``` unfolding infinite_nat_iff_unbounded_le by auto ``` hoelzl@56993 ` 305` ``` then have "Min {i. P i x} = the None" ``` hoelzl@56993 ` 306` ``` by (rule Min.infinite) } ``` hoelzl@56993 ` 307` ``` note 1 = this ``` hoelzl@56993 ` 308` hoelzl@56993 ` 309` ``` { fix x i j assume "P i x" "\n\j. \ P n x" ``` hoelzl@56993 ` 310` ``` then have "finite {i. P i x}" ``` hoelzl@56993 ` 311` ``` by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) ``` hoelzl@56993 ` 312` ``` with `P i x` have "P (Min {i. P i x}) x" "Min {i. P i x} \ i" "finite {i. P i x}" ``` hoelzl@56993 ` 313` ``` using Min_in[of "{i. P i x}"] by auto } ``` hoelzl@56993 ` 314` ``` note 2 = this ``` hoelzl@56993 ` 315` hoelzl@56993 ` 316` ``` have "(\x. Min {i. P i x}) -` {n} \ space M = {x\space M. Min {i. P i x} = n}" ``` hoelzl@56993 ` 317` ``` by auto ``` hoelzl@56993 ` 318` ``` also have "\ = ``` hoelzl@56993 ` 319` ``` {x\space M. if (\i. \n\i. P n x) then the None = n else ``` hoelzl@56993 ` 320` ``` if (\i. P i x) then P n x \ (\i P i x) ``` hoelzl@56993 ` 321` ``` else Min {} = n}" ``` hoelzl@56993 ` 322` ``` by (intro arg_cong[where f=Collect] ext conj_cong) ``` hoelzl@56993 ` 323` ``` (auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI) ``` hoelzl@56993 ` 324` ``` also have "\ \ sets M" ``` hoelzl@56993 ` 325` ``` by measurable ``` hoelzl@56993 ` 326` ``` finally show "(\x. Min {i. P i x}) -` {n} \ space M \ sets M" . ``` hoelzl@56993 ` 327` ```qed simp ``` hoelzl@56993 ` 328` hoelzl@50387 ` 329` ```lemma measurable_count_space_insert[measurable (raw)]: ``` hoelzl@50387 ` 330` ``` "s \ S \ A \ sets (count_space S) \ insert s A \ sets (count_space S)" ``` hoelzl@50387 ` 331` ``` by simp ``` hoelzl@50387 ` 332` hoelzl@57025 ` 333` ```lemma measurable_card[measurable]: ``` hoelzl@57025 ` 334` ``` fixes S :: "'a \ nat set" ``` hoelzl@57025 ` 335` ``` assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M" ``` hoelzl@57025 ` 336` ``` shows "(\x. card (S x)) \ measurable M (count_space UNIV)" ``` hoelzl@57025 ` 337` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@57025 ` 338` ```proof safe ``` hoelzl@57025 ` 339` ``` fix n show "(\x. card (S x)) -` {n} \ space M \ sets M" ``` hoelzl@57025 ` 340` ``` proof (cases n) ``` hoelzl@57025 ` 341` ``` case 0 ``` hoelzl@57025 ` 342` ``` then have "(\x. card (S x)) -` {n} \ space M = {x\space M. infinite (S x) \ (\i. i \ S x)}" ``` hoelzl@57025 ` 343` ``` by auto ``` hoelzl@57025 ` 344` ``` also have "\ \ sets M" ``` hoelzl@57025 ` 345` ``` by measurable ``` hoelzl@57025 ` 346` ``` finally show ?thesis . ``` hoelzl@57025 ` 347` ``` next ``` hoelzl@57025 ` 348` ``` case (Suc i) ``` hoelzl@57025 ` 349` ``` then have "(\x. card (S x)) -` {n} \ space M = ``` hoelzl@57025 ` 350` ``` (\F\{A\{A. finite A}. card A = n}. {x\space M. (\i. i \ S x \ i \ F)})" ``` hoelzl@57025 ` 351` ``` unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite) ``` hoelzl@57025 ` 352` ``` also have "\ \ sets M" ``` hoelzl@57025 ` 353` ``` by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto ``` hoelzl@57025 ` 354` ``` finally show ?thesis . ``` hoelzl@57025 ` 355` ``` qed ``` hoelzl@57025 ` 356` ```qed rule ``` hoelzl@57025 ` 357` hoelzl@56021 ` 358` ```subsection {* Measurability for (co)inductive predicates *} ``` hoelzl@56021 ` 359` hoelzl@56021 ` 360` ```lemma measurable_lfp: ``` hoelzl@56021 ` 361` ``` assumes "Order_Continuity.continuous F" ``` hoelzl@56021 ` 362` ``` assumes *: "\A. pred M A \ pred M (F A)" ``` hoelzl@56045 ` 363` ``` shows "pred M (lfp F)" ``` hoelzl@56021 ` 364` ```proof - ``` hoelzl@56021 ` 365` ``` { fix i have "Measurable.pred M (\x. (F ^^ i) (\x. False) x)" ``` hoelzl@56021 ` 366` ``` by (induct i) (auto intro!: *) } ``` hoelzl@56021 ` 367` ``` then have "Measurable.pred M (\x. \i. (F ^^ i) (\x. False) x)" ``` hoelzl@56021 ` 368` ``` by measurable ``` hoelzl@56021 ` 369` ``` also have "(\x. \i. (F ^^ i) (\x. False) x) = (SUP i. (F ^^ i) bot)" ``` hoelzl@56021 ` 370` ``` by (auto simp add: bot_fun_def) ``` hoelzl@56045 ` 371` ``` also have "\ = lfp F" ``` hoelzl@56045 ` 372` ``` by (rule continuous_lfp[symmetric]) fact ``` hoelzl@56021 ` 373` ``` finally show ?thesis . ``` hoelzl@56021 ` 374` ```qed ``` hoelzl@56021 ` 375` hoelzl@56021 ` 376` ```lemma measurable_gfp: ``` hoelzl@56021 ` 377` ``` assumes "Order_Continuity.down_continuous F" ``` hoelzl@56021 ` 378` ``` assumes *: "\A. pred M A \ pred M (F A)" ``` hoelzl@56045 ` 379` ``` shows "pred M (gfp F)" ``` hoelzl@56021 ` 380` ```proof - ``` hoelzl@56021 ` 381` ``` { fix i have "Measurable.pred M (\x. (F ^^ i) (\x. True) x)" ``` hoelzl@56021 ` 382` ``` by (induct i) (auto intro!: *) } ``` hoelzl@56021 ` 383` ``` then have "Measurable.pred M (\x. \i. (F ^^ i) (\x. True) x)" ``` hoelzl@56021 ` 384` ``` by measurable ``` hoelzl@56021 ` 385` ``` also have "(\x. \i. (F ^^ i) (\x. True) x) = (INF i. (F ^^ i) top)" ``` hoelzl@56021 ` 386` ``` by (auto simp add: top_fun_def) ``` hoelzl@56045 ` 387` ``` also have "\ = gfp F" ``` hoelzl@56045 ` 388` ``` by (rule down_continuous_gfp[symmetric]) fact ``` hoelzl@56021 ` 389` ``` finally show ?thesis . ``` hoelzl@56021 ` 390` ```qed ``` hoelzl@56021 ` 391` hoelzl@50387 ` 392` ```hide_const (open) pred ``` hoelzl@50387 ` 393` hoelzl@50387 ` 394` ```end ```