src/HOL/Probability/Measurable.thy
 author haftmann Fri Jun 19 07:53:35 2015 +0200 (2015-06-19) changeset 60517 f16e4fb20652 parent 60172 423273355b55 child 61808 fc1556774cfe permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
 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@50387 ` 10` ```subsection {* Measurability prover *} ``` hoelzl@50387 ` 11` hoelzl@50387 ` 12` ```lemma (in algebra) sets_Collect_finite_All: ``` hoelzl@50387 ` 13` ``` assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S" ``` hoelzl@50387 ` 14` ``` shows "{x\\. \i\S. P i x} \ M" ``` hoelzl@50387 ` 15` ```proof - ``` hoelzl@50387 ` 16` ``` have "{x\\. \i\S. P i x} = (if S = {} then \ else \i\S. {x\\. P i x})" ``` hoelzl@50387 ` 17` ``` by auto ``` hoelzl@50387 ` 18` ``` with assms show ?thesis by (auto intro!: sets_Collect_finite_All') ``` hoelzl@50387 ` 19` ```qed ``` hoelzl@50387 ` 20` hoelzl@50387 ` 21` ```abbreviation "pred M P \ P \ measurable M (count_space (UNIV::bool set))" ``` hoelzl@50387 ` 22` hoelzl@50387 ` 23` ```lemma pred_def: "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 24` ```proof ``` hoelzl@50387 ` 25` ``` assume "pred M P" ``` hoelzl@50387 ` 26` ``` then have "P -` {True} \ space M \ sets M" ``` hoelzl@50387 ` 27` ``` by (auto simp: measurable_count_space_eq2) ``` hoelzl@50387 ` 28` ``` also have "P -` {True} \ space M = {x\space M. P x}" by auto ``` hoelzl@50387 ` 29` ``` finally show "{x\space M. P x} \ sets M" . ``` hoelzl@50387 ` 30` ```next ``` hoelzl@50387 ` 31` ``` assume P: "{x\space M. P x} \ sets M" ``` hoelzl@50387 ` 32` ``` moreover ``` hoelzl@50387 ` 33` ``` { fix X ``` hoelzl@50387 ` 34` ``` have "X \ Pow (UNIV :: bool set)" by simp ``` hoelzl@50387 ` 35` ``` then have "P -` X \ space M = {x\space M. ((X = {True} \ P x) \ (X = {False} \ \ P x) \ X \ {})}" ``` hoelzl@50387 ` 36` ``` unfolding UNIV_bool Pow_insert Pow_empty by auto ``` hoelzl@50387 ` 37` ``` then have "P -` X \ space M \ sets M" ``` hoelzl@50387 ` 38` ``` by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } ``` hoelzl@50387 ` 39` ``` then show "pred M P" ``` hoelzl@50387 ` 40` ``` by (auto simp: measurable_def) ``` hoelzl@50387 ` 41` ```qed ``` hoelzl@50387 ` 42` hoelzl@50387 ` 43` ```lemma pred_sets1: "{x\space M. P x} \ sets M \ f \ measurable N M \ pred N (\x. P (f x))" ``` hoelzl@50387 ` 44` ``` by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) ``` hoelzl@50387 ` 45` hoelzl@50387 ` 46` ```lemma pred_sets2: "A \ sets N \ f \ measurable M N \ pred M (\x. f x \ A)" ``` hoelzl@50387 ` 47` ``` by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) ``` hoelzl@50387 ` 48` hoelzl@50387 ` 49` ```ML_file "measurable.ML" ``` hoelzl@50387 ` 50` wenzelm@53043 ` 51` ```attribute_setup measurable = {* ``` hoelzl@59047 ` 52` ``` Scan.lift ( ``` hoelzl@59047 ` 53` ``` (Args.add >> K true || Args.del >> K false || Scan.succeed true) -- ``` hoelzl@59047 ` 54` ``` Scan.optional (Args.parens ( ``` hoelzl@59047 ` 55` ``` Scan.optional (Args.\$\$\$ "raw" >> K true) false -- ``` Andreas@58965 ` 56` ``` Scan.optional (Args.\$\$\$ "generic" >> K Measurable.Generic) Measurable.Concrete)) ``` hoelzl@59047 ` 57` ``` (false, Measurable.Concrete) >> ``` hoelzl@59047 ` 58` ``` Measurable.measurable_thm_attr) ``` wenzelm@53043 ` 59` ```*} "declaration of measurability theorems" ``` wenzelm@53043 ` 60` hoelzl@59047 ` 61` ```attribute_setup measurable_dest = Measurable.dest_thm_attr ``` hoelzl@59048 ` 62` ``` "add dest rule to measurability prover" ``` wenzelm@53043 ` 63` hoelzl@59048 ` 64` ```attribute_setup measurable_cong = Measurable.cong_thm_attr ``` hoelzl@59048 ` 65` ``` "add congurence rules to measurability prover" ``` wenzelm@53043 ` 66` hoelzl@59047 ` 67` ```method_setup measurable = \ Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \ ``` hoelzl@59047 ` 68` ``` "measurability prover" ``` wenzelm@53043 ` 69` hoelzl@50387 ` 70` ```simproc_setup measurable ("A \ sets M" | "f \ measurable M N") = {* K Measurable.simproc *} ``` hoelzl@50387 ` 71` Andreas@58965 ` 72` ```setup {* ``` hoelzl@59048 ` 73` ``` Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all) ``` Andreas@58965 ` 74` ```*} ``` hoelzl@59353 ` 75` ``` ``` hoelzl@50387 ` 76` ```declare ``` hoelzl@50387 ` 77` ``` pred_sets1[measurable_dest] ``` hoelzl@50387 ` 78` ``` pred_sets2[measurable_dest] ``` hoelzl@50387 ` 79` ``` sets.sets_into_space[measurable_dest] ``` hoelzl@50387 ` 80` hoelzl@50387 ` 81` ```declare ``` hoelzl@50387 ` 82` ``` sets.top[measurable] ``` hoelzl@50387 ` 83` ``` sets.empty_sets[measurable (raw)] ``` hoelzl@50387 ` 84` ``` sets.Un[measurable (raw)] ``` hoelzl@50387 ` 85` ``` sets.Diff[measurable (raw)] ``` hoelzl@50387 ` 86` hoelzl@50387 ` 87` ```declare ``` hoelzl@50387 ` 88` ``` measurable_count_space[measurable (raw)] ``` hoelzl@50387 ` 89` ``` measurable_ident[measurable (raw)] ``` hoelzl@59048 ` 90` ``` measurable_id[measurable (raw)] ``` hoelzl@50387 ` 91` ``` measurable_const[measurable (raw)] ``` hoelzl@50387 ` 92` ``` measurable_If[measurable (raw)] ``` hoelzl@50387 ` 93` ``` measurable_comp[measurable (raw)] ``` hoelzl@50387 ` 94` ``` measurable_sets[measurable (raw)] ``` hoelzl@50387 ` 95` hoelzl@59048 ` 96` ```declare measurable_cong_sets[measurable_cong] ``` hoelzl@59048 ` 97` ```declare sets_restrict_space_cong[measurable_cong] ``` hoelzl@59361 ` 98` ```declare sets_restrict_UNIV[measurable_cong] ``` hoelzl@59048 ` 99` hoelzl@50387 ` 100` ```lemma predE[measurable (raw)]: ``` hoelzl@50387 ` 101` ``` "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 102` ``` unfolding pred_def . ``` hoelzl@50387 ` 103` hoelzl@50387 ` 104` ```lemma pred_intros_imp'[measurable (raw)]: ``` hoelzl@50387 ` 105` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 106` ``` by (cases K) auto ``` hoelzl@50387 ` 107` hoelzl@50387 ` 108` ```lemma pred_intros_conj1'[measurable (raw)]: ``` hoelzl@50387 ` 109` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 110` ``` by (cases K) auto ``` hoelzl@50387 ` 111` hoelzl@50387 ` 112` ```lemma pred_intros_conj2'[measurable (raw)]: ``` hoelzl@50387 ` 113` ``` "(K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 114` ``` by (cases K) auto ``` hoelzl@50387 ` 115` hoelzl@50387 ` 116` ```lemma pred_intros_disj1'[measurable (raw)]: ``` hoelzl@50387 ` 117` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 118` ``` by (cases K) auto ``` hoelzl@50387 ` 119` hoelzl@50387 ` 120` ```lemma pred_intros_disj2'[measurable (raw)]: ``` hoelzl@50387 ` 121` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 122` ``` by (cases K) auto ``` hoelzl@50387 ` 123` hoelzl@50387 ` 124` ```lemma pred_intros_logic[measurable (raw)]: ``` hoelzl@50387 ` 125` ``` "pred M (\x. x \ space M)" ``` hoelzl@50387 ` 126` ``` "pred M (\x. P x) \ pred M (\x. \ P x)" ``` hoelzl@50387 ` 127` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 128` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 129` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 130` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x = P x)" ``` hoelzl@50387 ` 131` ``` "pred M (\x. f x \ UNIV)" ``` hoelzl@50387 ` 132` ``` "pred M (\x. f x \ {})" ``` hoelzl@50387 ` 133` ``` "pred M (\x. P' (f x) x) \ pred M (\x. f x \ {y. P' y x})" ``` hoelzl@50387 ` 134` ``` "pred M (\x. f x \ (B x)) \ pred M (\x. f x \ - (B x))" ``` hoelzl@50387 ` 135` ``` "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 ` 136` ``` "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 ` 137` ``` "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 ` 138` ``` "pred M (\x. g x (f x) \ (X x)) \ pred M (\x. f x \ (g x) -` (X x))" ``` hoelzl@50387 ` 139` ``` by (auto simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 140` hoelzl@50387 ` 141` ```lemma pred_intros_countable[measurable (raw)]: ``` hoelzl@50387 ` 142` ``` fixes P :: "'a \ 'i :: countable \ bool" ``` hoelzl@50387 ` 143` ``` shows ``` hoelzl@50387 ` 144` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 145` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 146` ``` by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) ``` hoelzl@50387 ` 147` hoelzl@50387 ` 148` ```lemma pred_intros_countable_bounded[measurable (raw)]: ``` hoelzl@50387 ` 149` ``` fixes X :: "'i :: countable set" ``` hoelzl@50387 ` 150` ``` shows ``` hoelzl@50387 ` 151` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 152` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 153` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 154` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 155` ``` by (auto simp: Bex_def Ball_def) ``` hoelzl@50387 ` 156` hoelzl@50387 ` 157` ```lemma pred_intros_finite[measurable (raw)]: ``` hoelzl@50387 ` 158` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 159` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 160` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 161` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 162` ``` by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 163` hoelzl@50387 ` 164` ```lemma countable_Un_Int[measurable (raw)]: ``` hoelzl@50387 ` 165` ``` "(\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 166` ``` "I \ {} \ (\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 167` ``` by auto ``` hoelzl@50387 ` 168` hoelzl@50387 ` 169` ```declare ``` hoelzl@50387 ` 170` ``` finite_UN[measurable (raw)] ``` hoelzl@50387 ` 171` ``` finite_INT[measurable (raw)] ``` hoelzl@50387 ` 172` hoelzl@50387 ` 173` ```lemma sets_Int_pred[measurable (raw)]: ``` hoelzl@50387 ` 174` ``` assumes space: "A \ B \ space M" and [measurable]: "pred M (\x. x \ A)" "pred M (\x. x \ B)" ``` hoelzl@50387 ` 175` ``` shows "A \ B \ sets M" ``` hoelzl@50387 ` 176` ```proof - ``` hoelzl@50387 ` 177` ``` have "{x\space M. x \ A \ B} \ sets M" by auto ``` hoelzl@50387 ` 178` ``` also have "{x\space M. x \ A \ B} = A \ B" ``` hoelzl@50387 ` 179` ``` using space by auto ``` hoelzl@50387 ` 180` ``` finally show ?thesis . ``` hoelzl@50387 ` 181` ```qed ``` hoelzl@50387 ` 182` hoelzl@50387 ` 183` ```lemma [measurable (raw generic)]: ``` hoelzl@50387 ` 184` ``` assumes f: "f \ measurable M N" and c: "c \ space N \ {c} \ sets N" ``` hoelzl@50387 ` 185` ``` shows pred_eq_const1: "pred M (\x. f x = c)" ``` hoelzl@50387 ` 186` ``` and pred_eq_const2: "pred M (\x. c = f x)" ``` hoelzl@50387 ` 187` ```proof - ``` hoelzl@50387 ` 188` ``` show "pred M (\x. f x = c)" ``` hoelzl@50387 ` 189` ``` proof cases ``` hoelzl@50387 ` 190` ``` assume "c \ space N" ``` hoelzl@50387 ` 191` ``` with measurable_sets[OF f c] show ?thesis ``` hoelzl@50387 ` 192` ``` by (auto simp: Int_def conj_commute pred_def) ``` hoelzl@50387 ` 193` ``` next ``` hoelzl@50387 ` 194` ``` assume "c \ space N" ``` hoelzl@50387 ` 195` ``` with f[THEN measurable_space] have "{x \ space M. f x = c} = {}" by auto ``` hoelzl@50387 ` 196` ``` then show ?thesis by (auto simp: pred_def cong: conj_cong) ``` hoelzl@50387 ` 197` ``` qed ``` hoelzl@50387 ` 198` ``` then show "pred M (\x. c = f x)" ``` hoelzl@50387 ` 199` ``` by (simp add: eq_commute) ``` hoelzl@50387 ` 200` ```qed ``` hoelzl@50387 ` 201` hoelzl@59000 ` 202` ```lemma pred_count_space_const1[measurable (raw)]: ``` hoelzl@59000 ` 203` ``` "f \ measurable M (count_space UNIV) \ Measurable.pred M (\x. f x = c)" ``` hoelzl@59000 ` 204` ``` by (intro pred_eq_const1[where N="count_space UNIV"]) (auto ) ``` hoelzl@59000 ` 205` hoelzl@59000 ` 206` ```lemma pred_count_space_const2[measurable (raw)]: ``` hoelzl@59000 ` 207` ``` "f \ measurable M (count_space UNIV) \ Measurable.pred M (\x. c = f x)" ``` hoelzl@59000 ` 208` ``` by (intro pred_eq_const2[where N="count_space UNIV"]) (auto ) ``` hoelzl@59000 ` 209` hoelzl@50387 ` 210` ```lemma pred_le_const[measurable (raw generic)]: ``` hoelzl@50387 ` 211` ``` assumes f: "f \ measurable M N" and c: "{.. c} \ sets N" shows "pred M (\x. f x \ c)" ``` hoelzl@50387 ` 212` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 213` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 214` hoelzl@50387 ` 215` ```lemma pred_const_le[measurable (raw generic)]: ``` hoelzl@50387 ` 216` ``` assumes f: "f \ measurable M N" and c: "{c ..} \ sets N" shows "pred M (\x. c \ f x)" ``` hoelzl@50387 ` 217` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 218` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 219` hoelzl@50387 ` 220` ```lemma pred_less_const[measurable (raw generic)]: ``` hoelzl@50387 ` 221` ``` assumes f: "f \ measurable M N" and c: "{..< c} \ sets N" shows "pred M (\x. f x < c)" ``` hoelzl@50387 ` 222` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 223` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 224` hoelzl@50387 ` 225` ```lemma pred_const_less[measurable (raw generic)]: ``` hoelzl@50387 ` 226` ``` assumes f: "f \ measurable M N" and c: "{c <..} \ sets N" shows "pred M (\x. c < f x)" ``` hoelzl@50387 ` 227` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 228` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 229` hoelzl@50387 ` 230` ```declare ``` hoelzl@50387 ` 231` ``` sets.Int[measurable (raw)] ``` hoelzl@50387 ` 232` hoelzl@50387 ` 233` ```lemma pred_in_If[measurable (raw)]: ``` hoelzl@50387 ` 234` ``` "(P \ pred M (\x. x \ A x)) \ (\ P \ pred M (\x. x \ B x)) \ ``` hoelzl@50387 ` 235` ``` pred M (\x. x \ (if P then A x else B x))" ``` hoelzl@50387 ` 236` ``` by auto ``` hoelzl@50387 ` 237` hoelzl@50387 ` 238` ```lemma sets_range[measurable_dest]: ``` hoelzl@50387 ` 239` ``` "A ` I \ sets M \ i \ I \ A i \ sets M" ``` hoelzl@50387 ` 240` ``` by auto ``` hoelzl@50387 ` 241` hoelzl@50387 ` 242` ```lemma pred_sets_range[measurable_dest]: ``` hoelzl@50387 ` 243` ``` "A ` I \ sets N \ i \ I \ f \ measurable M N \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 244` ``` using pred_sets2[OF sets_range] by auto ``` hoelzl@50387 ` 245` hoelzl@50387 ` 246` ```lemma sets_All[measurable_dest]: ``` hoelzl@50387 ` 247` ``` "\i. A i \ sets (M i) \ A i \ sets (M i)" ``` hoelzl@50387 ` 248` ``` by auto ``` hoelzl@50387 ` 249` hoelzl@50387 ` 250` ```lemma pred_sets_All[measurable_dest]: ``` hoelzl@50387 ` 251` ``` "\i. A i \ sets (N i) \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 252` ``` using pred_sets2[OF sets_All, of A N f] by auto ``` hoelzl@50387 ` 253` hoelzl@50387 ` 254` ```lemma sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 255` ``` "\i\I. A i \ sets (M i) \ i\I \ A i \ sets (M i)" ``` hoelzl@50387 ` 256` ``` by auto ``` hoelzl@50387 ` 257` hoelzl@50387 ` 258` ```lemma pred_sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 259` ``` "\i\I. A i \ sets (N i) \ i\I \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 260` ``` using pred_sets2[OF sets_Ball, of _ _ _ f] by auto ``` hoelzl@50387 ` 261` hoelzl@50387 ` 262` ```lemma measurable_finite[measurable (raw)]: ``` hoelzl@50387 ` 263` ``` fixes S :: "'a \ nat set" ``` hoelzl@50387 ` 264` ``` assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M" ``` hoelzl@50387 ` 265` ``` shows "pred M (\x. finite (S x))" ``` hoelzl@50387 ` 266` ``` unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) ``` hoelzl@50387 ` 267` hoelzl@50387 ` 268` ```lemma measurable_Least[measurable]: ``` hoelzl@50387 ` 269` ``` assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))"q ``` hoelzl@50387 ` 270` ``` shows "(\x. LEAST i. P i x) \ measurable M (count_space UNIV)" ``` hoelzl@50387 ` 271` ``` unfolding measurable_def by (safe intro!: sets_Least) simp_all ``` hoelzl@50387 ` 272` hoelzl@56993 ` 273` ```lemma measurable_Max_nat[measurable (raw)]: ``` hoelzl@56993 ` 274` ``` fixes P :: "nat \ 'a \ bool" ``` hoelzl@56993 ` 275` ``` assumes [measurable]: "\i. Measurable.pred M (P i)" ``` hoelzl@56993 ` 276` ``` shows "(\x. Max {i. P i x}) \ measurable M (count_space UNIV)" ``` hoelzl@56993 ` 277` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@56993 ` 278` ```proof safe ``` hoelzl@56993 ` 279` ``` fix n ``` hoelzl@56993 ` 280` hoelzl@56993 ` 281` ``` { fix x assume "\i. \n\i. P n x" ``` hoelzl@56993 ` 282` ``` then have "infinite {i. P i x}" ``` hoelzl@56993 ` 283` ``` unfolding infinite_nat_iff_unbounded_le by auto ``` hoelzl@56993 ` 284` ``` then have "Max {i. P i x} = the None" ``` hoelzl@56993 ` 285` ``` by (rule Max.infinite) } ``` hoelzl@56993 ` 286` ``` note 1 = this ``` hoelzl@56993 ` 287` hoelzl@56993 ` 288` ``` { fix x i j assume "P i x" "\n\j. \ P n x" ``` hoelzl@56993 ` 289` ``` then have "finite {i. P i x}" ``` hoelzl@56993 ` 290` ``` by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) ``` hoelzl@56993 ` 291` ``` 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 ` 292` ``` using Max_in[of "{i. P i x}"] by auto } ``` hoelzl@56993 ` 293` ``` note 2 = this ``` hoelzl@56993 ` 294` hoelzl@56993 ` 295` ``` have "(\x. Max {i. P i x}) -` {n} \ space M = {x\space M. Max {i. P i x} = n}" ``` hoelzl@56993 ` 296` ``` by auto ``` hoelzl@56993 ` 297` ``` also have "\ = ``` hoelzl@56993 ` 298` ``` {x\space M. if (\i. \n\i. P n x) then the None = n else ``` hoelzl@56993 ` 299` ``` if (\i. P i x) then P n x \ (\i>n. \ P i x) ``` hoelzl@56993 ` 300` ``` else Max {} = n}" ``` hoelzl@56993 ` 301` ``` by (intro arg_cong[where f=Collect] ext conj_cong) ``` hoelzl@56993 ` 302` ``` (auto simp add: 1 2 not_le[symmetric] intro!: Max_eqI) ``` hoelzl@56993 ` 303` ``` also have "\ \ sets M" ``` hoelzl@56993 ` 304` ``` by measurable ``` hoelzl@56993 ` 305` ``` finally show "(\x. Max {i. P i x}) -` {n} \ space M \ sets M" . ``` hoelzl@56993 ` 306` ```qed simp ``` hoelzl@56993 ` 307` hoelzl@56993 ` 308` ```lemma measurable_Min_nat[measurable (raw)]: ``` hoelzl@56993 ` 309` ``` fixes P :: "nat \ 'a \ bool" ``` hoelzl@56993 ` 310` ``` assumes [measurable]: "\i. Measurable.pred M (P i)" ``` hoelzl@56993 ` 311` ``` shows "(\x. Min {i. P i x}) \ measurable M (count_space UNIV)" ``` hoelzl@56993 ` 312` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@56993 ` 313` ```proof safe ``` hoelzl@56993 ` 314` ``` fix n ``` hoelzl@56993 ` 315` hoelzl@56993 ` 316` ``` { fix x assume "\i. \n\i. P n x" ``` hoelzl@56993 ` 317` ``` then have "infinite {i. P i x}" ``` hoelzl@56993 ` 318` ``` unfolding infinite_nat_iff_unbounded_le by auto ``` hoelzl@56993 ` 319` ``` then have "Min {i. P i x} = the None" ``` hoelzl@56993 ` 320` ``` by (rule Min.infinite) } ``` hoelzl@56993 ` 321` ``` note 1 = this ``` hoelzl@56993 ` 322` hoelzl@56993 ` 323` ``` { fix x i j assume "P i x" "\n\j. \ P n x" ``` hoelzl@56993 ` 324` ``` then have "finite {i. P i x}" ``` hoelzl@56993 ` 325` ``` by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) ``` hoelzl@56993 ` 326` ``` 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 ` 327` ``` using Min_in[of "{i. P i x}"] by auto } ``` hoelzl@56993 ` 328` ``` note 2 = this ``` hoelzl@56993 ` 329` hoelzl@56993 ` 330` ``` have "(\x. Min {i. P i x}) -` {n} \ space M = {x\space M. Min {i. P i x} = n}" ``` hoelzl@56993 ` 331` ``` by auto ``` hoelzl@56993 ` 332` ``` also have "\ = ``` hoelzl@56993 ` 333` ``` {x\space M. if (\i. \n\i. P n x) then the None = n else ``` hoelzl@56993 ` 334` ``` if (\i. P i x) then P n x \ (\i P i x) ``` hoelzl@56993 ` 335` ``` else Min {} = n}" ``` hoelzl@56993 ` 336` ``` by (intro arg_cong[where f=Collect] ext conj_cong) ``` hoelzl@56993 ` 337` ``` (auto simp add: 1 2 not_le[symmetric] intro!: Min_eqI) ``` hoelzl@56993 ` 338` ``` also have "\ \ sets M" ``` hoelzl@56993 ` 339` ``` by measurable ``` hoelzl@56993 ` 340` ``` finally show "(\x. Min {i. P i x}) -` {n} \ space M \ sets M" . ``` hoelzl@56993 ` 341` ```qed simp ``` hoelzl@56993 ` 342` hoelzl@50387 ` 343` ```lemma measurable_count_space_insert[measurable (raw)]: ``` hoelzl@50387 ` 344` ``` "s \ S \ A \ sets (count_space S) \ insert s A \ sets (count_space S)" ``` hoelzl@50387 ` 345` ``` by simp ``` hoelzl@50387 ` 346` hoelzl@59000 ` 347` ```lemma sets_UNIV [measurable (raw)]: "A \ sets (count_space UNIV)" ``` hoelzl@59000 ` 348` ``` by simp ``` hoelzl@59000 ` 349` hoelzl@57025 ` 350` ```lemma measurable_card[measurable]: ``` hoelzl@57025 ` 351` ``` fixes S :: "'a \ nat set" ``` hoelzl@57025 ` 352` ``` assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M" ``` hoelzl@57025 ` 353` ``` shows "(\x. card (S x)) \ measurable M (count_space UNIV)" ``` hoelzl@57025 ` 354` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@57025 ` 355` ```proof safe ``` hoelzl@57025 ` 356` ``` fix n show "(\x. card (S x)) -` {n} \ space M \ sets M" ``` hoelzl@57025 ` 357` ``` proof (cases n) ``` hoelzl@57025 ` 358` ``` case 0 ``` hoelzl@57025 ` 359` ``` then have "(\x. card (S x)) -` {n} \ space M = {x\space M. infinite (S x) \ (\i. i \ S x)}" ``` hoelzl@57025 ` 360` ``` by auto ``` hoelzl@57025 ` 361` ``` also have "\ \ sets M" ``` hoelzl@57025 ` 362` ``` by measurable ``` hoelzl@57025 ` 363` ``` finally show ?thesis . ``` hoelzl@57025 ` 364` ``` next ``` hoelzl@57025 ` 365` ``` case (Suc i) ``` hoelzl@57025 ` 366` ``` then have "(\x. card (S x)) -` {n} \ space M = ``` hoelzl@57025 ` 367` ``` (\F\{A\{A. finite A}. card A = n}. {x\space M. (\i. i \ S x \ i \ F)})" ``` hoelzl@57025 ` 368` ``` unfolding set_eq_iff[symmetric] Collect_bex_eq[symmetric] by (auto intro: card_ge_0_finite) ``` hoelzl@57025 ` 369` ``` also have "\ \ sets M" ``` hoelzl@57025 ` 370` ``` by (intro sets.countable_UN' countable_Collect countable_Collect_finite) auto ``` hoelzl@57025 ` 371` ``` finally show ?thesis . ``` hoelzl@57025 ` 372` ``` qed ``` hoelzl@57025 ` 373` ```qed rule ``` hoelzl@57025 ` 374` hoelzl@59088 ` 375` ```lemma measurable_pred_countable[measurable (raw)]: ``` hoelzl@59088 ` 376` ``` assumes "countable X" ``` hoelzl@59088 ` 377` ``` shows ``` hoelzl@59088 ` 378` ``` "(\i. i \ X \ Measurable.pred M (\x. P x i)) \ Measurable.pred M (\x. \i\X. P x i)" ``` hoelzl@59088 ` 379` ``` "(\i. i \ X \ Measurable.pred M (\x. P x i)) \ Measurable.pred M (\x. \i\X. P x i)" ``` hoelzl@59088 ` 380` ``` unfolding pred_def ``` hoelzl@59088 ` 381` ``` by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms) ``` hoelzl@59088 ` 382` hoelzl@56021 ` 383` ```subsection {* Measurability for (co)inductive predicates *} ``` hoelzl@56021 ` 384` hoelzl@59088 ` 385` ```lemma measurable_bot[measurable]: "bot \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 386` ``` by (simp add: bot_fun_def) ``` hoelzl@59088 ` 387` hoelzl@59088 ` 388` ```lemma measurable_top[measurable]: "top \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 389` ``` by (simp add: top_fun_def) ``` hoelzl@59088 ` 390` hoelzl@59088 ` 391` ```lemma measurable_SUP[measurable]: ``` hoelzl@59088 ` 392` ``` fixes F :: "'i \ 'a \ 'b::{complete_lattice, countable}" ``` hoelzl@59088 ` 393` ``` assumes [simp]: "countable I" ``` hoelzl@59088 ` 394` ``` assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 395` ``` shows "(\x. SUP i:I. F i x) \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 396` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@59088 ` 397` ```proof (safe intro!: UNIV_I) ``` hoelzl@59088 ` 398` ``` fix a ``` hoelzl@59088 ` 399` ``` have "(\x. SUP i:I. F i x) -` {a} \ space M = ``` hoelzl@59088 ` 400` ``` {x\space M. (\i\I. F i x \ a) \ (\b. (\i\I. F i x \ b) \ a \ b)}" ``` hoelzl@59088 ` 401` ``` unfolding SUP_le_iff[symmetric] by auto ``` hoelzl@59088 ` 402` ``` also have "\ \ sets M" ``` hoelzl@59088 ` 403` ``` by measurable ``` hoelzl@59088 ` 404` ``` finally show "(\x. SUP i:I. F i x) -` {a} \ space M \ sets M" . ``` hoelzl@59088 ` 405` ```qed ``` hoelzl@59088 ` 406` hoelzl@59088 ` 407` ```lemma measurable_INF[measurable]: ``` hoelzl@59088 ` 408` ``` fixes F :: "'i \ 'a \ 'b::{complete_lattice, countable}" ``` hoelzl@59088 ` 409` ``` assumes [simp]: "countable I" ``` hoelzl@59088 ` 410` ``` assumes [measurable]: "\i. i \ I \ F i \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 411` ``` shows "(\x. INF i:I. F i x) \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 412` ``` unfolding measurable_count_space_eq2_countable ``` hoelzl@59088 ` 413` ```proof (safe intro!: UNIV_I) ``` hoelzl@59088 ` 414` ``` fix a ``` hoelzl@59088 ` 415` ``` have "(\x. INF i:I. F i x) -` {a} \ space M = ``` hoelzl@59088 ` 416` ``` {x\space M. (\i\I. a \ F i x) \ (\b. (\i\I. b \ F i x) \ b \ a)}" ``` hoelzl@59088 ` 417` ``` unfolding le_INF_iff[symmetric] by auto ``` hoelzl@59088 ` 418` ``` also have "\ \ sets M" ``` hoelzl@59088 ` 419` ``` by measurable ``` hoelzl@59088 ` 420` ``` finally show "(\x. INF i:I. F i x) -` {a} \ space M \ sets M" . ``` hoelzl@59088 ` 421` ```qed ``` hoelzl@59088 ` 422` hoelzl@59088 ` 423` ```lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]: ``` hoelzl@59088 ` 424` ``` fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" ``` hoelzl@59088 ` 425` ``` assumes "P M" ``` hoelzl@60172 ` 426` ``` assumes F: "sup_continuous F" ``` hoelzl@59088 ` 427` ``` assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 428` ``` shows "lfp F \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 429` ```proof - ``` hoelzl@59088 ` 430` ``` { fix i from `P M` have "((F ^^ i) bot) \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 431` ``` by (induct i arbitrary: M) (auto intro!: *) } ``` hoelzl@59088 ` 432` ``` then have "(\x. SUP i. (F ^^ i) bot x) \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 433` ``` by measurable ``` hoelzl@59088 ` 434` ``` also have "(\x. SUP i. (F ^^ i) bot x) = lfp F" ``` hoelzl@60172 ` 435` ``` by (subst sup_continuous_lfp) (auto intro: F) ``` hoelzl@59088 ` 436` ``` finally show ?thesis . ``` hoelzl@59088 ` 437` ```qed ``` hoelzl@59088 ` 438` hoelzl@56021 ` 439` ```lemma measurable_lfp: ``` hoelzl@59088 ` 440` ``` fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" ``` hoelzl@60172 ` 441` ``` assumes F: "sup_continuous F" ``` hoelzl@59088 ` 442` ``` assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 443` ``` shows "lfp F \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 444` ``` by (coinduction rule: measurable_lfp_coinduct[OF _ F]) (blast intro: *) ``` hoelzl@59088 ` 445` hoelzl@59088 ` 446` ```lemma measurable_gfp_coinduct[consumes 1, case_names continuity step]: ``` hoelzl@59088 ` 447` ``` fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" ``` hoelzl@59088 ` 448` ``` assumes "P M" ``` hoelzl@60172 ` 449` ``` assumes F: "inf_continuous F" ``` hoelzl@59088 ` 450` ``` assumes *: "\M A. P M \ (\N. P N \ A \ measurable N (count_space UNIV)) \ F A \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 451` ``` shows "gfp F \ measurable M (count_space UNIV)" ``` hoelzl@56021 ` 452` ```proof - ``` hoelzl@59088 ` 453` ``` { fix i from `P M` have "((F ^^ i) top) \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 454` ``` by (induct i arbitrary: M) (auto intro!: *) } ``` hoelzl@59088 ` 455` ``` then have "(\x. INF i. (F ^^ i) top x) \ measurable M (count_space UNIV)" ``` hoelzl@56021 ` 456` ``` by measurable ``` hoelzl@59088 ` 457` ``` also have "(\x. INF i. (F ^^ i) top x) = gfp F" ``` hoelzl@60172 ` 458` ``` by (subst inf_continuous_gfp) (auto intro: F) ``` hoelzl@56021 ` 459` ``` finally show ?thesis . ``` hoelzl@56021 ` 460` ```qed ``` hoelzl@56021 ` 461` hoelzl@56021 ` 462` ```lemma measurable_gfp: ``` hoelzl@59088 ` 463` ``` fixes F :: "('a \ 'b) \ ('a \ 'b::{complete_lattice, countable})" ``` hoelzl@60172 ` 464` ``` assumes F: "inf_continuous F" ``` hoelzl@59088 ` 465` ``` assumes *: "\A. A \ measurable M (count_space UNIV) \ F A \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 466` ``` shows "gfp F \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 467` ``` by (coinduction rule: measurable_gfp_coinduct[OF _ F]) (blast intro: *) ``` hoelzl@59000 ` 468` hoelzl@59000 ` 469` ```lemma measurable_lfp2_coinduct[consumes 1, case_names continuity step]: ``` hoelzl@59088 ` 470` ``` fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})" ``` hoelzl@59000 ` 471` ``` assumes "P M s" ``` hoelzl@60172 ` 472` ``` assumes F: "sup_continuous F" ``` hoelzl@59088 ` 473` ``` assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 474` ``` shows "lfp F s \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 475` ```proof - ``` hoelzl@59088 ` 476` ``` { fix i from `P M s` have "(\x. (F ^^ i) bot s x) \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 477` ``` by (induct i arbitrary: M s) (auto intro!: *) } ``` hoelzl@59088 ` 478` ``` then have "(\x. SUP i. (F ^^ i) bot s x) \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 479` ``` by measurable ``` hoelzl@59088 ` 480` ``` also have "(\x. SUP i. (F ^^ i) bot s x) = lfp F s" ``` hoelzl@60172 ` 481` ``` by (subst sup_continuous_lfp) (auto simp: F) ``` hoelzl@59000 ` 482` ``` finally show ?thesis . ``` hoelzl@59000 ` 483` ```qed ``` hoelzl@59000 ` 484` hoelzl@59000 ` 485` ```lemma measurable_gfp2_coinduct[consumes 1, case_names continuity step]: ``` hoelzl@59088 ` 486` ``` fixes F :: "('a \ 'c \ 'b) \ ('a \ 'c \ 'b::{complete_lattice, countable})" ``` hoelzl@59000 ` 487` ``` assumes "P M s" ``` hoelzl@60172 ` 488` ``` assumes F: "inf_continuous F" ``` hoelzl@59088 ` 489` ``` assumes *: "\M A s. P M s \ (\N t. P N t \ A t \ measurable N (count_space UNIV)) \ F A s \ measurable M (count_space UNIV)" ``` hoelzl@59088 ` 490` ``` shows "gfp F s \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 491` ```proof - ``` hoelzl@59088 ` 492` ``` { fix i from `P M s` have "(\x. (F ^^ i) top s x) \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 493` ``` by (induct i arbitrary: M s) (auto intro!: *) } ``` hoelzl@59088 ` 494` ``` then have "(\x. INF i. (F ^^ i) top s x) \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 495` ``` by measurable ``` hoelzl@59088 ` 496` ``` also have "(\x. INF i. (F ^^ i) top s x) = gfp F s" ``` hoelzl@60172 ` 497` ``` by (subst inf_continuous_gfp) (auto simp: F) ``` hoelzl@59000 ` 498` ``` finally show ?thesis . ``` hoelzl@59000 ` 499` ```qed ``` hoelzl@59000 ` 500` hoelzl@59000 ` 501` ```lemma measurable_enat_coinduct: ``` hoelzl@59000 ` 502` ``` fixes f :: "'a \ enat" ``` hoelzl@59000 ` 503` ``` assumes "R f" ``` hoelzl@59000 ` 504` ``` assumes *: "\f. R f \ \g h i P. R g \ f = (\x. if P x then h x else eSuc (g (i x))) \ ``` hoelzl@59000 ` 505` ``` Measurable.pred M P \ ``` hoelzl@59000 ` 506` ``` i \ measurable M M \ ``` hoelzl@59000 ` 507` ``` h \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 508` ``` shows "f \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 509` ```proof (simp add: measurable_count_space_eq2_countable, rule ) ``` hoelzl@59000 ` 510` ``` fix a :: enat ``` hoelzl@59000 ` 511` ``` have "f -` {a} \ space M = {x\space M. f x = a}" ``` hoelzl@59000 ` 512` ``` by auto ``` hoelzl@59000 ` 513` ``` { fix i :: nat ``` hoelzl@59000 ` 514` ``` from `R f` have "Measurable.pred M (\x. f x = enat i)" ``` hoelzl@59000 ` 515` ``` proof (induction i arbitrary: f) ``` hoelzl@59000 ` 516` ``` case 0 ``` hoelzl@59000 ` 517` ``` from *[OF this] obtain g h i P ``` hoelzl@59000 ` 518` ``` where f: "f = (\x. if P x then h x else eSuc (g (i x)))" and ``` hoelzl@59000 ` 519` ``` [measurable]: "Measurable.pred M P" "i \ measurable M M" "h \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 520` ``` by auto ``` hoelzl@59000 ` 521` ``` have "Measurable.pred M (\x. P x \ h x = 0)" ``` hoelzl@59000 ` 522` ``` by measurable ``` hoelzl@59000 ` 523` ``` also have "(\x. P x \ h x = 0) = (\x. f x = enat 0)" ``` hoelzl@59000 ` 524` ``` by (auto simp: f zero_enat_def[symmetric]) ``` hoelzl@59000 ` 525` ``` finally show ?case . ``` hoelzl@59000 ` 526` ``` next ``` hoelzl@59000 ` 527` ``` case (Suc n) ``` hoelzl@59000 ` 528` ``` from *[OF Suc.prems] obtain g h i P ``` hoelzl@59000 ` 529` ``` where f: "f = (\x. if P x then h x else eSuc (g (i x)))" and "R g" and ``` hoelzl@59000 ` 530` ``` M[measurable]: "Measurable.pred M P" "i \ measurable M M" "h \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 531` ``` by auto ``` hoelzl@59000 ` 532` ``` have "(\x. f x = enat (Suc n)) = ``` hoelzl@59000 ` 533` ``` (\x. (P x \ h x = enat (Suc n)) \ (\ P x \ g (i x) = enat n))" ``` hoelzl@59000 ` 534` ``` by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric]) ``` hoelzl@59000 ` 535` ``` also have "Measurable.pred M \" ``` hoelzl@59000 ` 536` ``` by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable ``` hoelzl@59000 ` 537` ``` finally show ?case . ``` hoelzl@59000 ` 538` ``` qed ``` hoelzl@59000 ` 539` ``` then have "f -` {enat i} \ space M \ sets M" ``` hoelzl@59000 ` 540` ``` by (simp add: pred_def Int_def conj_commute) } ``` hoelzl@59000 ` 541` ``` note fin = this ``` hoelzl@59000 ` 542` ``` show "f -` {a} \ space M \ sets M" ``` hoelzl@59000 ` 543` ``` proof (cases a) ``` hoelzl@59000 ` 544` ``` case infinity ``` hoelzl@59000 ` 545` ``` then have "f -` {a} \ space M = space M - (\n. f -` {enat n} \ space M)" ``` hoelzl@59000 ` 546` ``` by auto ``` hoelzl@59000 ` 547` ``` also have "\ \ sets M" ``` hoelzl@59000 ` 548` ``` by (intro sets.Diff sets.top sets.Un sets.countable_UN) (auto intro!: fin) ``` hoelzl@59000 ` 549` ``` finally show ?thesis . ``` hoelzl@59000 ` 550` ``` qed (simp add: fin) ``` hoelzl@59000 ` 551` ```qed ``` hoelzl@59000 ` 552` hoelzl@59000 ` 553` ```lemma measurable_THE: ``` hoelzl@59000 ` 554` ``` fixes P :: "'a \ 'b \ bool" ``` hoelzl@59000 ` 555` ``` assumes [measurable]: "\i. Measurable.pred M (P i)" ``` hoelzl@59000 ` 556` ``` assumes I[simp]: "countable I" "\i x. x \ space M \ P i x \ i \ I" ``` hoelzl@59000 ` 557` ``` assumes unique: "\x i j. x \ space M \ P i x \ P j x \ i = j" ``` hoelzl@59000 ` 558` ``` shows "(\x. THE i. P i x) \ measurable M (count_space UNIV)" ``` hoelzl@59000 ` 559` ``` unfolding measurable_def ``` hoelzl@59000 ` 560` ```proof safe ``` hoelzl@59000 ` 561` ``` fix X ``` hoelzl@59000 ` 562` ``` def f \ "\x. THE i. P i x" def undef \ "THE i::'a. False" ``` hoelzl@59000 ` 563` ``` { fix i x assume "x \ space M" "P i x" then have "f x = i" ``` hoelzl@59000 ` 564` ``` unfolding f_def using unique by auto } ``` hoelzl@59000 ` 565` ``` note f_eq = this ``` hoelzl@59000 ` 566` ``` { fix x assume "x \ space M" "\i\I. \ P i x" ``` hoelzl@59000 ` 567` ``` then have "\i. \ P i x" ``` hoelzl@59000 ` 568` ``` using I(2)[of x] by auto ``` hoelzl@59000 ` 569` ``` then have "f x = undef" ``` hoelzl@59000 ` 570` ``` by (auto simp: undef_def f_def) } ``` hoelzl@59000 ` 571` ``` then have "f -` X \ space M = (\i\I \ X. {x\space M. P i x}) \ ``` hoelzl@59000 ` 572` ``` (if undef \ X then space M - (\i\I. {x\space M. P i x}) else {})" ``` hoelzl@59000 ` 573` ``` by (auto dest: f_eq) ``` hoelzl@59000 ` 574` ``` also have "\ \ sets M" ``` hoelzl@59000 ` 575` ``` by (auto intro!: sets.Diff sets.countable_UN') ``` hoelzl@59000 ` 576` ``` finally show "f -` X \ space M \ sets M" . ``` hoelzl@59000 ` 577` ```qed simp ``` hoelzl@59000 ` 578` hoelzl@59000 ` 579` ```lemma measurable_Ex1[measurable (raw)]: ``` hoelzl@59000 ` 580` ``` assumes [simp]: "countable I" and [measurable]: "\i. i \ I \ Measurable.pred M (P i)" ``` hoelzl@59000 ` 581` ``` shows "Measurable.pred M (\x. \!i\I. P i x)" ``` hoelzl@59000 ` 582` ``` unfolding bex1_def by measurable ``` hoelzl@59000 ` 583` hoelzl@59000 ` 584` ```lemma measurable_split_if[measurable (raw)]: ``` hoelzl@59000 ` 585` ``` "(c \ Measurable.pred M f) \ (\ c \ Measurable.pred M g) \ ``` hoelzl@59000 ` 586` ``` Measurable.pred M (if c then f else g)" ``` hoelzl@59000 ` 587` ``` by simp ``` hoelzl@59000 ` 588` hoelzl@59000 ` 589` ```lemma pred_restrict_space: ``` hoelzl@59000 ` 590` ``` assumes "S \ sets M" ``` hoelzl@59000 ` 591` ``` shows "Measurable.pred (restrict_space M S) P \ Measurable.pred M (\x. x \ S \ P x)" ``` hoelzl@59000 ` 592` ``` unfolding pred_def sets_Collect_restrict_space_iff[OF assms] .. ``` hoelzl@59000 ` 593` hoelzl@59000 ` 594` ```lemma measurable_predpow[measurable]: ``` hoelzl@59000 ` 595` ``` assumes "Measurable.pred M T" ``` hoelzl@59000 ` 596` ``` assumes "\Q. Measurable.pred M Q \ Measurable.pred M (R Q)" ``` hoelzl@59000 ` 597` ``` shows "Measurable.pred M ((R ^^ n) T)" ``` hoelzl@59000 ` 598` ``` by (induct n) (auto intro: assms) ``` hoelzl@59000 ` 599` hoelzl@50387 ` 600` ```hide_const (open) pred ``` hoelzl@50387 ` 601` hoelzl@50387 ` 602` ```end ``` hoelzl@59048 ` 603`