src/HOL/Probability/Measurable.thy
 author hoelzl Wed Dec 05 15:59:08 2012 +0100 (2012-12-05) changeset 50387 3d8863c41fe8 child 50530 6266e44b3396 permissions -rw-r--r--
Move the measurability prover to its own file
 hoelzl@50387 ` 1` ```(* Title: HOL/Probability/measurable.ML ``` hoelzl@50387 ` 2` ``` Author: Johannes Hölzl ``` hoelzl@50387 ` 3` ```*) ``` hoelzl@50387 ` 4` ```theory Measurable ``` hoelzl@50387 ` 5` ``` imports Sigma_Algebra ``` hoelzl@50387 ` 6` ```begin ``` hoelzl@50387 ` 7` hoelzl@50387 ` 8` ```subsection {* Measurability prover *} ``` hoelzl@50387 ` 9` hoelzl@50387 ` 10` ```lemma (in algebra) sets_Collect_finite_All: ``` hoelzl@50387 ` 11` ``` assumes "\i. i \ S \ {x\\. P i x} \ M" "finite S" ``` hoelzl@50387 ` 12` ``` shows "{x\\. \i\S. P i x} \ M" ``` hoelzl@50387 ` 13` ```proof - ``` hoelzl@50387 ` 14` ``` have "{x\\. \i\S. P i x} = (if S = {} then \ else \i\S. {x\\. P i x})" ``` hoelzl@50387 ` 15` ``` by auto ``` hoelzl@50387 ` 16` ``` with assms show ?thesis by (auto intro!: sets_Collect_finite_All') ``` hoelzl@50387 ` 17` ```qed ``` hoelzl@50387 ` 18` hoelzl@50387 ` 19` ```abbreviation "pred M P \ P \ measurable M (count_space (UNIV::bool set))" ``` hoelzl@50387 ` 20` hoelzl@50387 ` 21` ```lemma pred_def: "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 22` ```proof ``` hoelzl@50387 ` 23` ``` assume "pred M P" ``` hoelzl@50387 ` 24` ``` then have "P -` {True} \ space M \ sets M" ``` hoelzl@50387 ` 25` ``` by (auto simp: measurable_count_space_eq2) ``` hoelzl@50387 ` 26` ``` also have "P -` {True} \ space M = {x\space M. P x}" by auto ``` hoelzl@50387 ` 27` ``` finally show "{x\space M. P x} \ sets M" . ``` hoelzl@50387 ` 28` ```next ``` hoelzl@50387 ` 29` ``` assume P: "{x\space M. P x} \ sets M" ``` hoelzl@50387 ` 30` ``` moreover ``` hoelzl@50387 ` 31` ``` { fix X ``` hoelzl@50387 ` 32` ``` have "X \ Pow (UNIV :: bool set)" by simp ``` hoelzl@50387 ` 33` ``` then have "P -` X \ space M = {x\space M. ((X = {True} \ P x) \ (X = {False} \ \ P x) \ X \ {})}" ``` hoelzl@50387 ` 34` ``` unfolding UNIV_bool Pow_insert Pow_empty by auto ``` hoelzl@50387 ` 35` ``` then have "P -` X \ space M \ sets M" ``` hoelzl@50387 ` 36` ``` by (auto intro!: sets.sets_Collect_neg sets.sets_Collect_imp sets.sets_Collect_conj sets.sets_Collect_const P) } ``` hoelzl@50387 ` 37` ``` then show "pred M P" ``` hoelzl@50387 ` 38` ``` by (auto simp: measurable_def) ``` hoelzl@50387 ` 39` ```qed ``` hoelzl@50387 ` 40` hoelzl@50387 ` 41` ```lemma pred_sets1: "{x\space M. P x} \ sets M \ f \ measurable N M \ pred N (\x. P (f x))" ``` hoelzl@50387 ` 42` ``` by (rule measurable_compose[where f=f and N=M]) (auto simp: pred_def) ``` hoelzl@50387 ` 43` hoelzl@50387 ` 44` ```lemma pred_sets2: "A \ sets N \ f \ measurable M N \ pred M (\x. f x \ A)" ``` hoelzl@50387 ` 45` ``` by (rule measurable_compose[where f=f and N=N]) (auto simp: pred_def Int_def[symmetric]) ``` hoelzl@50387 ` 46` hoelzl@50387 ` 47` ```ML_file "measurable.ML" ``` hoelzl@50387 ` 48` hoelzl@50387 ` 49` ```attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems" ``` hoelzl@50387 ` 50` ```attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover" ``` hoelzl@50387 ` 51` ```attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover" ``` hoelzl@50387 ` 52` ```method_setup measurable = {* Measurable.method *} "measurability prover" ``` hoelzl@50387 ` 53` ```simproc_setup measurable ("A \ sets M" | "f \ measurable M N") = {* K Measurable.simproc *} ``` hoelzl@50387 ` 54` hoelzl@50387 ` 55` ```declare ``` hoelzl@50387 ` 56` ``` measurable_compose_rev[measurable_dest] ``` hoelzl@50387 ` 57` ``` pred_sets1[measurable_dest] ``` hoelzl@50387 ` 58` ``` pred_sets2[measurable_dest] ``` hoelzl@50387 ` 59` ``` sets.sets_into_space[measurable_dest] ``` hoelzl@50387 ` 60` hoelzl@50387 ` 61` ```declare ``` hoelzl@50387 ` 62` ``` sets.top[measurable] ``` hoelzl@50387 ` 63` ``` sets.empty_sets[measurable (raw)] ``` hoelzl@50387 ` 64` ``` sets.Un[measurable (raw)] ``` hoelzl@50387 ` 65` ``` sets.Diff[measurable (raw)] ``` hoelzl@50387 ` 66` hoelzl@50387 ` 67` ```declare ``` hoelzl@50387 ` 68` ``` measurable_count_space[measurable (raw)] ``` hoelzl@50387 ` 69` ``` measurable_ident[measurable (raw)] ``` hoelzl@50387 ` 70` ``` measurable_ident_sets[measurable (raw)] ``` hoelzl@50387 ` 71` ``` measurable_const[measurable (raw)] ``` hoelzl@50387 ` 72` ``` measurable_If[measurable (raw)] ``` hoelzl@50387 ` 73` ``` measurable_comp[measurable (raw)] ``` hoelzl@50387 ` 74` ``` measurable_sets[measurable (raw)] ``` hoelzl@50387 ` 75` hoelzl@50387 ` 76` ```lemma predE[measurable (raw)]: ``` hoelzl@50387 ` 77` ``` "pred M P \ {x\space M. P x} \ sets M" ``` hoelzl@50387 ` 78` ``` unfolding pred_def . ``` hoelzl@50387 ` 79` hoelzl@50387 ` 80` ```lemma pred_intros_imp'[measurable (raw)]: ``` hoelzl@50387 ` 81` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 82` ``` by (cases K) auto ``` hoelzl@50387 ` 83` hoelzl@50387 ` 84` ```lemma pred_intros_conj1'[measurable (raw)]: ``` hoelzl@50387 ` 85` ``` "(K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 86` ``` by (cases K) auto ``` hoelzl@50387 ` 87` hoelzl@50387 ` 88` ```lemma pred_intros_conj2'[measurable (raw)]: ``` hoelzl@50387 ` 89` ``` "(K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 90` ``` by (cases K) auto ``` hoelzl@50387 ` 91` hoelzl@50387 ` 92` ```lemma pred_intros_disj1'[measurable (raw)]: ``` hoelzl@50387 ` 93` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. K \ P x)" ``` hoelzl@50387 ` 94` ``` by (cases K) auto ``` hoelzl@50387 ` 95` hoelzl@50387 ` 96` ```lemma pred_intros_disj2'[measurable (raw)]: ``` hoelzl@50387 ` 97` ``` "(\ K \ pred M (\x. P x)) \ pred M (\x. P x \ K)" ``` hoelzl@50387 ` 98` ``` by (cases K) auto ``` hoelzl@50387 ` 99` hoelzl@50387 ` 100` ```lemma pred_intros_logic[measurable (raw)]: ``` hoelzl@50387 ` 101` ``` "pred M (\x. x \ space M)" ``` hoelzl@50387 ` 102` ``` "pred M (\x. P x) \ pred M (\x. \ P x)" ``` hoelzl@50387 ` 103` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 104` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 105` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x \ P x)" ``` hoelzl@50387 ` 106` ``` "pred M (\x. Q x) \ pred M (\x. P x) \ pred M (\x. Q x = P x)" ``` hoelzl@50387 ` 107` ``` "pred M (\x. f x \ UNIV)" ``` hoelzl@50387 ` 108` ``` "pred M (\x. f x \ {})" ``` hoelzl@50387 ` 109` ``` "pred M (\x. P' (f x) x) \ pred M (\x. f x \ {y. P' y x})" ``` hoelzl@50387 ` 110` ``` "pred M (\x. f x \ (B x)) \ pred M (\x. f x \ - (B x))" ``` hoelzl@50387 ` 111` ``` "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 ` 112` ``` "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 ` 113` ``` "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 ` 114` ``` "pred M (\x. g x (f x) \ (X x)) \ pred M (\x. f x \ (g x) -` (X x))" ``` hoelzl@50387 ` 115` ``` by (auto simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 116` hoelzl@50387 ` 117` ```lemma pred_intros_countable[measurable (raw)]: ``` hoelzl@50387 ` 118` ``` fixes P :: "'a \ 'i :: countable \ bool" ``` hoelzl@50387 ` 119` ``` shows ``` hoelzl@50387 ` 120` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 121` ``` "(\i. pred M (\x. P x i)) \ pred M (\x. \i. P x i)" ``` hoelzl@50387 ` 122` ``` by (auto intro!: sets.sets_Collect_countable_All sets.sets_Collect_countable_Ex simp: pred_def) ``` hoelzl@50387 ` 123` hoelzl@50387 ` 124` ```lemma pred_intros_countable_bounded[measurable (raw)]: ``` hoelzl@50387 ` 125` ``` fixes X :: "'i :: countable set" ``` hoelzl@50387 ` 126` ``` shows ``` hoelzl@50387 ` 127` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 128` ``` "(\i. i \ X \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\X. N x i))" ``` hoelzl@50387 ` 129` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 130` ``` "(\i. i \ X \ pred M (\x. P x i)) \ pred M (\x. \i\X. P x i)" ``` hoelzl@50387 ` 131` ``` by (auto simp: Bex_def Ball_def) ``` hoelzl@50387 ` 132` hoelzl@50387 ` 133` ```lemma pred_intros_finite[measurable (raw)]: ``` hoelzl@50387 ` 134` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 135` ``` "finite I \ (\i. i \ I \ pred M (\x. x \ N x i)) \ pred M (\x. x \ (\i\I. N x i))" ``` hoelzl@50387 ` 136` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 137` ``` "finite I \ (\i. i \ I \ pred M (\x. P x i)) \ pred M (\x. \i\I. P x i)" ``` hoelzl@50387 ` 138` ``` by (auto intro!: sets.sets_Collect_finite_Ex sets.sets_Collect_finite_All simp: iff_conv_conj_imp pred_def) ``` hoelzl@50387 ` 139` hoelzl@50387 ` 140` ```lemma countable_Un_Int[measurable (raw)]: ``` hoelzl@50387 ` 141` ``` "(\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 142` ``` "I \ {} \ (\i :: 'i :: countable. i \ I \ N i \ sets M) \ (\i\I. N i) \ sets M" ``` hoelzl@50387 ` 143` ``` by auto ``` hoelzl@50387 ` 144` hoelzl@50387 ` 145` ```declare ``` hoelzl@50387 ` 146` ``` finite_UN[measurable (raw)] ``` hoelzl@50387 ` 147` ``` finite_INT[measurable (raw)] ``` hoelzl@50387 ` 148` hoelzl@50387 ` 149` ```lemma sets_Int_pred[measurable (raw)]: ``` hoelzl@50387 ` 150` ``` assumes space: "A \ B \ space M" and [measurable]: "pred M (\x. x \ A)" "pred M (\x. x \ B)" ``` hoelzl@50387 ` 151` ``` shows "A \ B \ sets M" ``` hoelzl@50387 ` 152` ```proof - ``` hoelzl@50387 ` 153` ``` have "{x\space M. x \ A \ B} \ sets M" by auto ``` hoelzl@50387 ` 154` ``` also have "{x\space M. x \ A \ B} = A \ B" ``` hoelzl@50387 ` 155` ``` using space by auto ``` hoelzl@50387 ` 156` ``` finally show ?thesis . ``` hoelzl@50387 ` 157` ```qed ``` hoelzl@50387 ` 158` hoelzl@50387 ` 159` ```lemma [measurable (raw generic)]: ``` hoelzl@50387 ` 160` ``` assumes f: "f \ measurable M N" and c: "c \ space N \ {c} \ sets N" ``` hoelzl@50387 ` 161` ``` shows pred_eq_const1: "pred M (\x. f x = c)" ``` hoelzl@50387 ` 162` ``` and pred_eq_const2: "pred M (\x. c = f x)" ``` hoelzl@50387 ` 163` ```proof - ``` hoelzl@50387 ` 164` ``` show "pred M (\x. f x = c)" ``` hoelzl@50387 ` 165` ``` proof cases ``` hoelzl@50387 ` 166` ``` assume "c \ space N" ``` hoelzl@50387 ` 167` ``` with measurable_sets[OF f c] show ?thesis ``` hoelzl@50387 ` 168` ``` by (auto simp: Int_def conj_commute pred_def) ``` hoelzl@50387 ` 169` ``` next ``` hoelzl@50387 ` 170` ``` assume "c \ space N" ``` hoelzl@50387 ` 171` ``` with f[THEN measurable_space] have "{x \ space M. f x = c} = {}" by auto ``` hoelzl@50387 ` 172` ``` then show ?thesis by (auto simp: pred_def cong: conj_cong) ``` hoelzl@50387 ` 173` ``` qed ``` hoelzl@50387 ` 174` ``` then show "pred M (\x. c = f x)" ``` hoelzl@50387 ` 175` ``` by (simp add: eq_commute) ``` hoelzl@50387 ` 176` ```qed ``` hoelzl@50387 ` 177` hoelzl@50387 ` 178` ```lemma pred_le_const[measurable (raw generic)]: ``` hoelzl@50387 ` 179` ``` assumes f: "f \ measurable M N" and c: "{.. c} \ sets N" shows "pred M (\x. f x \ c)" ``` hoelzl@50387 ` 180` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 181` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 182` hoelzl@50387 ` 183` ```lemma pred_const_le[measurable (raw generic)]: ``` hoelzl@50387 ` 184` ``` assumes f: "f \ measurable M N" and c: "{c ..} \ sets N" shows "pred M (\x. c \ f x)" ``` hoelzl@50387 ` 185` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 186` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 187` hoelzl@50387 ` 188` ```lemma pred_less_const[measurable (raw generic)]: ``` hoelzl@50387 ` 189` ``` assumes f: "f \ measurable M N" and c: "{..< c} \ sets N" shows "pred M (\x. f x < c)" ``` hoelzl@50387 ` 190` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 191` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 192` hoelzl@50387 ` 193` ```lemma pred_const_less[measurable (raw generic)]: ``` hoelzl@50387 ` 194` ``` assumes f: "f \ measurable M N" and c: "{c <..} \ sets N" shows "pred M (\x. c < f x)" ``` hoelzl@50387 ` 195` ``` using measurable_sets[OF f c] ``` hoelzl@50387 ` 196` ``` by (auto simp: Int_def conj_commute eq_commute pred_def) ``` hoelzl@50387 ` 197` hoelzl@50387 ` 198` ```declare ``` hoelzl@50387 ` 199` ``` sets.Int[measurable (raw)] ``` hoelzl@50387 ` 200` hoelzl@50387 ` 201` ```lemma pred_in_If[measurable (raw)]: ``` hoelzl@50387 ` 202` ``` "(P \ pred M (\x. x \ A x)) \ (\ P \ pred M (\x. x \ B x)) \ ``` hoelzl@50387 ` 203` ``` pred M (\x. x \ (if P then A x else B x))" ``` hoelzl@50387 ` 204` ``` by auto ``` hoelzl@50387 ` 205` hoelzl@50387 ` 206` ```lemma sets_range[measurable_dest]: ``` hoelzl@50387 ` 207` ``` "A ` I \ sets M \ i \ I \ A i \ sets M" ``` hoelzl@50387 ` 208` ``` by auto ``` hoelzl@50387 ` 209` hoelzl@50387 ` 210` ```lemma pred_sets_range[measurable_dest]: ``` hoelzl@50387 ` 211` ``` "A ` I \ sets N \ i \ I \ f \ measurable M N \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 212` ``` using pred_sets2[OF sets_range] by auto ``` hoelzl@50387 ` 213` hoelzl@50387 ` 214` ```lemma sets_All[measurable_dest]: ``` hoelzl@50387 ` 215` ``` "\i. A i \ sets (M i) \ A i \ sets (M i)" ``` hoelzl@50387 ` 216` ``` by auto ``` hoelzl@50387 ` 217` hoelzl@50387 ` 218` ```lemma pred_sets_All[measurable_dest]: ``` hoelzl@50387 ` 219` ``` "\i. A i \ sets (N i) \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 220` ``` using pred_sets2[OF sets_All, of A N f] by auto ``` hoelzl@50387 ` 221` hoelzl@50387 ` 222` ```lemma sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 223` ``` "\i\I. A i \ sets (M i) \ i\I \ A i \ sets (M i)" ``` hoelzl@50387 ` 224` ``` by auto ``` hoelzl@50387 ` 225` hoelzl@50387 ` 226` ```lemma pred_sets_Ball[measurable_dest]: ``` hoelzl@50387 ` 227` ``` "\i\I. A i \ sets (N i) \ i\I \ f \ measurable M (N i) \ pred M (\x. f x \ A i)" ``` hoelzl@50387 ` 228` ``` using pred_sets2[OF sets_Ball, of _ _ _ f] by auto ``` hoelzl@50387 ` 229` hoelzl@50387 ` 230` ```lemma measurable_finite[measurable (raw)]: ``` hoelzl@50387 ` 231` ``` fixes S :: "'a \ nat set" ``` hoelzl@50387 ` 232` ``` assumes [measurable]: "\i. {x\space M. i \ S x} \ sets M" ``` hoelzl@50387 ` 233` ``` shows "pred M (\x. finite (S x))" ``` hoelzl@50387 ` 234` ``` unfolding finite_nat_set_iff_bounded by (simp add: Ball_def) ``` hoelzl@50387 ` 235` hoelzl@50387 ` 236` ```lemma measurable_Least[measurable]: ``` hoelzl@50387 ` 237` ``` assumes [measurable]: "(\i::nat. (\x. P i x) \ measurable M (count_space UNIV))"q ``` hoelzl@50387 ` 238` ``` shows "(\x. LEAST i. P i x) \ measurable M (count_space UNIV)" ``` hoelzl@50387 ` 239` ``` unfolding measurable_def by (safe intro!: sets_Least) simp_all ``` hoelzl@50387 ` 240` hoelzl@50387 ` 241` ```lemma measurable_count_space_insert[measurable (raw)]: ``` hoelzl@50387 ` 242` ``` "s \ S \ A \ sets (count_space S) \ insert s A \ sets (count_space S)" ``` hoelzl@50387 ` 243` ``` by simp ``` hoelzl@50387 ` 244` hoelzl@50387 ` 245` ```hide_const (open) pred ``` hoelzl@50387 ` 246` hoelzl@50387 ` 247` ```end ```