summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Measurable.thy

changeset 61808 | fc1556774cfe |

parent 60172 | 423273355b55 |

child 62343 | 24106dc44def |

1.1 --- a/src/HOL/Probability/Measurable.thy Mon Dec 07 16:48:10 2015 +0000 1.2 +++ b/src/HOL/Probability/Measurable.thy Mon Dec 07 20:19:59 2015 +0100 1.3 @@ -7,7 +7,7 @@ 1.4 "~~/src/HOL/Library/Order_Continuity" 1.5 begin 1.6 1.7 -subsection {* Measurability prover *} 1.8 +subsection \<open>Measurability prover\<close> 1.9 1.10 lemma (in algebra) sets_Collect_finite_All: 1.11 assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>\<Omega>. P i x} \<in> M" "finite S" 1.12 @@ -48,7 +48,7 @@ 1.13 1.14 ML_file "measurable.ML" 1.15 1.16 -attribute_setup measurable = {* 1.17 +attribute_setup measurable = \<open> 1.18 Scan.lift ( 1.19 (Args.add >> K true || Args.del >> K false || Scan.succeed true) -- 1.20 Scan.optional (Args.parens ( 1.21 @@ -56,7 +56,7 @@ 1.22 Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete)) 1.23 (false, Measurable.Concrete) >> 1.24 Measurable.measurable_thm_attr) 1.25 -*} "declaration of measurability theorems" 1.26 +\<close> "declaration of measurability theorems" 1.27 1.28 attribute_setup measurable_dest = Measurable.dest_thm_attr 1.29 "add dest rule to measurability prover" 1.30 @@ -67,11 +67,11 @@ 1.31 method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close> 1.32 "measurability prover" 1.33 1.34 -simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *} 1.35 +simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = \<open>K Measurable.simproc\<close> 1.36 1.37 -setup {* 1.38 +setup \<open> 1.39 Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all) 1.40 -*} 1.41 +\<close> 1.42 1.43 declare 1.44 pred_sets1[measurable_dest] 1.45 @@ -288,7 +288,7 @@ 1.46 { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" 1.47 then have "finite {i. P i x}" 1.48 by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) 1.49 - with `P i x` have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}" 1.50 + with \<open>P i x\<close> have "P (Max {i. P i x}) x" "i \<le> Max {i. P i x}" "finite {i. P i x}" 1.51 using Max_in[of "{i. P i x}"] by auto } 1.52 note 2 = this 1.53 1.54 @@ -323,7 +323,7 @@ 1.55 { fix x i j assume "P i x" "\<forall>n\<ge>j. \<not> P n x" 1.56 then have "finite {i. P i x}" 1.57 by (auto simp: subset_eq not_le[symmetric] finite_nat_iff_bounded) 1.58 - with `P i x` have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}" 1.59 + with \<open>P i x\<close> have "P (Min {i. P i x}) x" "Min {i. P i x} \<le> i" "finite {i. P i x}" 1.60 using Min_in[of "{i. P i x}"] by auto } 1.61 note 2 = this 1.62 1.63 @@ -380,7 +380,7 @@ 1.64 unfolding pred_def 1.65 by (auto intro!: sets.sets_Collect_countable_All' sets.sets_Collect_countable_Ex' assms) 1.66 1.67 -subsection {* Measurability for (co)inductive predicates *} 1.68 +subsection \<open>Measurability for (co)inductive predicates\<close> 1.69 1.70 lemma measurable_bot[measurable]: "bot \<in> measurable M (count_space UNIV)" 1.71 by (simp add: bot_fun_def) 1.72 @@ -427,7 +427,7 @@ 1.73 assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.74 shows "lfp F \<in> measurable M (count_space UNIV)" 1.75 proof - 1.76 - { fix i from `P M` have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)" 1.77 + { fix i from \<open>P M\<close> have "((F ^^ i) bot) \<in> measurable M (count_space UNIV)" 1.78 by (induct i arbitrary: M) (auto intro!: *) } 1.79 then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)" 1.80 by measurable 1.81 @@ -450,7 +450,7 @@ 1.82 assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> A \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A \<in> measurable M (count_space UNIV)" 1.83 shows "gfp F \<in> measurable M (count_space UNIV)" 1.84 proof - 1.85 - { fix i from `P M` have "((F ^^ i) top) \<in> measurable M (count_space UNIV)" 1.86 + { fix i from \<open>P M\<close> have "((F ^^ i) top) \<in> measurable M (count_space UNIV)" 1.87 by (induct i arbitrary: M) (auto intro!: *) } 1.88 then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)" 1.89 by measurable 1.90 @@ -473,7 +473,7 @@ 1.91 assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" 1.92 shows "lfp F s \<in> measurable M (count_space UNIV)" 1.93 proof - 1.94 - { fix i from `P M s` have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 1.95 + { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 1.96 by (induct i arbitrary: M s) (auto intro!: *) } 1.97 then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)" 1.98 by measurable 1.99 @@ -489,7 +489,7 @@ 1.100 assumes *: "\<And>M A s. P M s \<Longrightarrow> (\<And>N t. P N t \<Longrightarrow> A t \<in> measurable N (count_space UNIV)) \<Longrightarrow> F A s \<in> measurable M (count_space UNIV)" 1.101 shows "gfp F s \<in> measurable M (count_space UNIV)" 1.102 proof - 1.103 - { fix i from `P M s` have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 1.104 + { fix i from \<open>P M s\<close> have "(\<lambda>x. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 1.105 by (induct i arbitrary: M s) (auto intro!: *) } 1.106 then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)" 1.107 by measurable 1.108 @@ -511,7 +511,7 @@ 1.109 have "f -` {a} \<inter> space M = {x\<in>space M. f x = a}" 1.110 by auto 1.111 { fix i :: nat 1.112 - from `R f` have "Measurable.pred M (\<lambda>x. f x = enat i)" 1.113 + from \<open>R f\<close> have "Measurable.pred M (\<lambda>x. f x = enat i)" 1.114 proof (induction i arbitrary: f) 1.115 case 0 1.116 from *[OF this] obtain g h i P 1.117 @@ -533,7 +533,7 @@ 1.118 (\<lambda>x. (P x \<longrightarrow> h x = enat (Suc n)) \<and> (\<not> P x \<longrightarrow> g (i x) = enat n))" 1.119 by (auto simp: f zero_enat_def[symmetric] eSuc_enat[symmetric]) 1.120 also have "Measurable.pred M \<dots>" 1.121 - by (intro pred_intros_logic measurable_compose[OF M(2)] Suc `R g`) measurable 1.122 + by (intro pred_intros_logic measurable_compose[OF M(2)] Suc \<open>R g\<close>) measurable 1.123 finally show ?case . 1.124 qed 1.125 then have "f -` {enat i} \<inter> space M \<in> sets M"