src/HOL/Probability/Probability_Mass_Function.thy
changeset 61808 fc1556774cfe
parent 61634 48e2de1b1df5
child 62026 ea3b1b0413b4
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Dec 07 16:48:10 2015 +0000
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Dec 07 20:19:59 2015 +0100
     1.3 @@ -54,16 +54,16 @@
     1.4      from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
     1.5        by auto
     1.6      { fix x assume "x \<in> X"
     1.7 -      from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
     1.8 +      from \<open>?M \<noteq> 0\<close> *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
     1.9        then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
    1.10      note singleton_sets = this
    1.11      have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
    1.12 -      using `?M \<noteq> 0`
    1.13 -      by (simp add: `card X = Suc (Suc n)` of_nat_Suc field_simps less_le measure_nonneg)
    1.14 +      using \<open>?M \<noteq> 0\<close>
    1.15 +      by (simp add: \<open>card X = Suc (Suc n)\<close> of_nat_Suc field_simps less_le measure_nonneg)
    1.16      also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
    1.17        by (rule setsum_mono) fact
    1.18      also have "\<dots> = measure M (\<Union>x\<in>X. {x})"
    1.19 -      using singleton_sets `finite X`
    1.20 +      using singleton_sets \<open>finite X\<close>
    1.21        by (intro finite_measure_finite_Union[symmetric]) (auto simp: disjoint_family_on_def)
    1.22      finally have "?M < measure M (\<Union>x\<in>X. {x})" .
    1.23      moreover have "measure M (\<Union>x\<in>X. {x}) \<le> ?M"
    1.24 @@ -399,7 +399,7 @@
    1.25  lemma bind_pmf_cong:
    1.26    assumes "p = q"
    1.27    shows "(\<And>x. x \<in> set_pmf q \<Longrightarrow> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
    1.28 -  unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq
    1.29 +  unfolding \<open>p = q\<close>[symmetric] measure_pmf_inject[symmetric] bind_pmf.rep_eq
    1.30    by (auto simp: AE_measure_pmf_iff Pi_iff space_subprob_algebra subprob_space_measure_pmf
    1.31                   sets_bind[where N="count_space UNIV"] emeasure_bind[where N="count_space UNIV"]
    1.32             intro!: nn_integral_cong_AE measure_eqI)
    1.33 @@ -736,7 +736,7 @@
    1.34  lemma set_pmf_transfer[transfer_rule]:
    1.35    assumes "bi_total A"
    1.36    shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"
    1.37 -  using `bi_total A`
    1.38 +  using \<open>bi_total A\<close>
    1.39    by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
    1.40       metis+
    1.41  
    1.42 @@ -1079,9 +1079,9 @@
    1.43      with in_set eq have "measure p {x. R x y} = measure q {y. R x y}"
    1.44        by auto
    1.45      moreover have "{y. R x y} = C"
    1.46 -      using assms `x \<in> C` C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
    1.47 +      using assms \<open>x \<in> C\<close> C quotientD[of UNIV ?R C x] by (simp add: equivp_equiv)
    1.48      moreover have "{x. R x y} = C"
    1.49 -      using assms `y \<in> C` C quotientD[of UNIV "?R" C y] sympD[of R]
    1.50 +      using assms \<open>y \<in> C\<close> C quotientD[of UNIV "?R" C y] sympD[of R]
    1.51        by (auto simp add: equivp_equiv elim: equivpE)
    1.52      ultimately show ?thesis
    1.53        by auto
    1.54 @@ -1114,7 +1114,7 @@
    1.55  
    1.56    fix x y assume "x \<in> set_pmf p" "y \<in> set_pmf q" "R x y"
    1.57    have "{y. R x y} \<in> UNIV // ?R" "{x. R x y} = {y. R x y}"
    1.58 -    using assms `R x y` by (auto simp: quotient_def dest: equivp_symp equivp_transp)
    1.59 +    using assms \<open>R x y\<close> by (auto simp: quotient_def dest: equivp_symp equivp_transp)
    1.60    with eq show "measure p {x. R x y} = measure q {y. R x y}"
    1.61      by auto
    1.62  qed
    1.63 @@ -1198,7 +1198,7 @@
    1.64      by (force elim: rel_pmf.cases)
    1.65    moreover have "set_pmf (return_pmf x) = {x}"
    1.66      by simp
    1.67 -  with `a \<in> M` have "(x, a) \<in> pq"
    1.68 +  with \<open>a \<in> M\<close> have "(x, a) \<in> pq"
    1.69      by (force simp: eq)
    1.70    with * show "R x a"
    1.71      by auto
    1.72 @@ -1366,12 +1366,12 @@
    1.73    by (rule rel_pmf_joinI)
    1.74       (auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg)
    1.75  
    1.76 -text {*
    1.77 +text \<open>
    1.78    Proof that @{const rel_pmf} preserves orders.
    1.79    Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
    1.80    Theoretical Computer Science 12(1):19--37, 1980,
    1.81    @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
    1.82 -*}
    1.83 +\<close>
    1.84  
    1.85  lemma
    1.86    assumes *: "rel_pmf R p q"