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