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"