src/HOL/Probability/SPMF.thy
changeset 63343 fb5d8a50c641
parent 63333 158ab2239496
child 63540 f8652d0534fa
     1.1 --- a/src/HOL/Probability/SPMF.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Probability/SPMF.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -158,7 +158,9 @@
     1.4  
     1.5  subsubsection \<open>A relator for sets that treats sets like predicates\<close>
     1.6  
     1.7 -context begin interpretation lifting_syntax .
     1.8 +context includes lifting_syntax
     1.9 +begin
    1.10 +
    1.11  definition rel_pred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
    1.12  where "rel_pred R A B = (R ===> op =) (\<lambda>x. x \<in> A) (\<lambda>y. y \<in> B)"
    1.13  
    1.14 @@ -173,6 +175,7 @@
    1.15        because it blows up the search space for @{method transfer}
    1.16        (in combination with @{thm [source] Collect_transfer})\<close>
    1.17  by(simp add: rel_funI rel_predI)
    1.18 +
    1.19  end
    1.20  
    1.21  subsubsection \<open>Monotonicity rules\<close>
    1.22 @@ -720,7 +723,8 @@
    1.23  lemma spmf_rel_eq: "rel_spmf op = = op ="
    1.24  by(simp add: pmf.rel_eq option.rel_eq)
    1.25  
    1.26 -context begin interpretation lifting_syntax .
    1.27 +context includes lifting_syntax
    1.28 +begin
    1.29  
    1.30  lemma bind_spmf_parametric [transfer_rule]:
    1.31    "(rel_spmf A ===> (A ===> rel_spmf B) ===> rel_spmf B) bind_spmf bind_spmf"
    1.32 @@ -758,7 +762,9 @@
    1.33  lemma rel_pmf_return_pmfI: "P x y \<Longrightarrow> rel_pmf P (return_pmf x) (return_pmf y)"
    1.34  by(rule rel_pmf.intros[where pq="return_pmf (x, y)"])(simp_all)
    1.35  
    1.36 -context begin interpretation lifting_syntax .
    1.37 +context includes lifting_syntax
    1.38 +begin
    1.39 +
    1.40  text \<open>We do not yet have a relator for @{typ "'a measure"}, so we combine @{const measure} and @{const measure_pmf}\<close>
    1.41  lemma measure_pmf_parametric:
    1.42    "(rel_pmf A ===> rel_pred A ===> op =) (\<lambda>p. measure (measure_pmf p)) (\<lambda>q. measure (measure_pmf q))"
    1.43 @@ -778,6 +784,7 @@
    1.44  apply(erule measure_pmf_parametric[THEN rel_funD, THEN rel_funD])
    1.45  apply(auto simp add: rel_pred_def rel_fun_def elim: option.rel_cases)
    1.46  done
    1.47 +
    1.48  end
    1.49  
    1.50  subsection \<open>From @{typ "'a pmf"} to @{typ "'a spmf"}\<close>
    1.51 @@ -1785,7 +1792,8 @@
    1.52    \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. rel_spmf R (f x) (g x))"
    1.53  by(rule admissible_subst[OF admissible_rel_spmf, where f="\<lambda>x. (f x, g x)", simplified])(rule mcont_Pair)
    1.54  
    1.55 -context begin interpretation lifting_syntax .
    1.56 +context includes lifting_syntax
    1.57 +begin
    1.58  
    1.59  lemma fixp_spmf_parametric':
    1.60    assumes f: "\<And>x. monotone (ord_spmf op =) (ord_spmf op =) F"
    1.61 @@ -2032,7 +2040,9 @@
    1.62      by(auto simp add: spmf_of_set_def simp del: spmf_of_pmf_pmf_of_set intro: rel_pmf_of_set_bij)
    1.63  qed
    1.64  
    1.65 -context begin interpretation lifting_syntax .
    1.66 +context includes lifting_syntax
    1.67 +begin
    1.68 +
    1.69  lemma rel_spmf_of_set:
    1.70    assumes "bi_unique R"
    1.71    shows "(rel_set R ===> rel_spmf R) spmf_of_set spmf_of_set"
    1.72 @@ -2043,6 +2053,7 @@
    1.73      by(auto dest: bi_unique_rel_set_bij_betw)
    1.74    then show "rel_spmf R (spmf_of_set A) (spmf_of_set B)" by(rule rel_spmf_of_set_bij)
    1.75  qed
    1.76 +
    1.77  end
    1.78  
    1.79  lemma map_mem_spmf_of_set:
    1.80 @@ -2637,10 +2648,13 @@
    1.81    "lossless_spmf (TRY p ELSE q) \<longleftrightarrow> lossless_spmf p \<or> lossless_spmf q"
    1.82  by(auto simp add: try_spmf_def in_set_spmf lossless_iff_set_pmf_None split: option.splits)
    1.83  
    1.84 -context begin interpretation lifting_syntax .
    1.85 +context includes lifting_syntax
    1.86 +begin
    1.87 +
    1.88  lemma try_spmf_parametric [transfer_rule]:
    1.89    "(rel_spmf A ===> rel_spmf A ===> rel_spmf A) try_spmf try_spmf"
    1.90  unfolding try_spmf_def[abs_def] by transfer_prover
    1.91 +
    1.92  end
    1.93  
    1.94  lemma try_spmf_cong: