more symbols;
authorwenzelm
Fri Jan 01 14:44:52 2016 +0100 (2016-01-01)
changeset 62026ea3b1b0413b4
parent 62025 8007e4ff493a
child 62027 b270f2b9bef8
more symbols;
NEWS
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Predicate.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Projective_Family.thy
     1.1 --- a/NEWS	Fri Jan 01 11:27:29 2016 +0100
     1.2 +++ b/NEWS	Fri Jan 01 14:44:52 2016 +0100
     1.3 @@ -598,6 +598,8 @@
     1.4  terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
     1.5  "top". INCOMPATIBILITY.
     1.6  
     1.7 +* Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
     1.8 +
     1.9  * Library/Multiset:
    1.10    - Renamed multiset inclusion operators:
    1.11        < ~> <#
     2.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jan 01 11:27:29 2016 +0100
     2.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jan 01 14:44:52 2016 +0100
     2.3 @@ -338,7 +338,7 @@
     2.4    using assms by (rule effectE) (simp add: execute_simps)
     2.5  
     2.6  lemma upd_return:
     2.7 -  "upd i x a \<guillemotright> return a = upd i x a"
     2.8 +  "upd i x a \<then> return a = upd i x a"
     2.9    by (rule Heap_eqI) (simp add: bind_def guard_def upd_def execute_simps)
    2.10  
    2.11  lemma array_make:
    2.12 @@ -371,10 +371,10 @@
    2.13    by (simp add: make'_def o_def)
    2.14  
    2.15  definition len' where
    2.16 -  [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (of_nat n))"
    2.17 +  [code del]: "len' a = Array.len a \<bind> (\<lambda>n. return (of_nat n))"
    2.18  
    2.19  lemma [code]:
    2.20 -  "Array.len a = len' a \<guillemotright>= (\<lambda>i. return (nat_of_integer i))"
    2.21 +  "Array.len a = len' a \<bind> (\<lambda>i. return (nat_of_integer i))"
    2.22    by (simp add: len'_def)
    2.23  
    2.24  definition nth' where
    2.25 @@ -385,10 +385,10 @@
    2.26    by (simp add: nth'_def)
    2.27  
    2.28  definition upd' where
    2.29 -  [code del]: "upd' a i x = Array.upd (nat_of_integer i) x a \<guillemotright> return ()"
    2.30 +  [code del]: "upd' a i x = Array.upd (nat_of_integer i) x a \<then> return ()"
    2.31  
    2.32  lemma [code]:
    2.33 -  "Array.upd i x a = upd' a (of_nat i) x \<guillemotright> return a"
    2.34 +  "Array.upd i x a = upd' a (of_nat i) x \<then> return a"
    2.35    by (simp add: upd'_def upd_return)
    2.36  
    2.37  lemma [code]:
    2.38 @@ -497,4 +497,3 @@
    2.39  code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
    2.40  
    2.41  end
    2.42 -
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jan 01 11:27:29 2016 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jan 01 14:44:52 2016 +0100
     3.3 @@ -253,56 +253,56 @@
     3.4    Monad_Syntax.bind Heap_Monad.bind
     3.5  
     3.6  lemma execute_bind [execute_simps]:
     3.7 -  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g x) h'"
     3.8 -  "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
     3.9 +  "execute f h = Some (x, h') \<Longrightarrow> execute (f \<bind> g) h = execute (g x) h'"
    3.10 +  "execute f h = None \<Longrightarrow> execute (f \<bind> g) h = None"
    3.11    by (simp_all add: bind_def)
    3.12  
    3.13  lemma execute_bind_case:
    3.14 -  "execute (f \<guillemotright>= g) h = (case (execute f h) of
    3.15 +  "execute (f \<bind> g) h = (case (execute f h) of
    3.16      Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
    3.17    by (simp add: bind_def)
    3.18  
    3.19  lemma execute_bind_success:
    3.20 -  "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
    3.21 +  "success f h \<Longrightarrow> execute (f \<bind> g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
    3.22    by (cases f h rule: Heap_cases) (auto elim: successE simp add: bind_def)
    3.23  
    3.24  lemma success_bind_executeI:
    3.25 -  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
    3.26 +  "execute f h = Some (x, h') \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
    3.27    by (auto intro!: successI elim: successE simp add: bind_def)
    3.28  
    3.29  lemma success_bind_effectI [success_intros]:
    3.30 -  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<guillemotright>= g) h"
    3.31 +  "effect f h h' x \<Longrightarrow> success (g x) h' \<Longrightarrow> success (f \<bind> g) h"
    3.32    by (auto simp add: effect_def success_def bind_def)
    3.33  
    3.34  lemma effect_bindI [effect_intros]:
    3.35    assumes "effect f h h' r" "effect (g r) h' h'' r'"
    3.36 -  shows "effect (f \<guillemotright>= g) h h'' r'"
    3.37 +  shows "effect (f \<bind> g) h h'' r'"
    3.38    using assms
    3.39    apply (auto intro!: effectI elim!: effectE successE)
    3.40    apply (subst execute_bind, simp_all)
    3.41    done
    3.42  
    3.43  lemma effect_bindE [effect_elims]:
    3.44 -  assumes "effect (f \<guillemotright>= g) h h'' r'"
    3.45 +  assumes "effect (f \<bind> g) h h'' r'"
    3.46    obtains h' r where "effect f h h' r" "effect (g r) h' h'' r'"
    3.47    using assms by (auto simp add: effect_def bind_def split: option.split_asm)
    3.48  
    3.49  lemma execute_bind_eq_SomeI:
    3.50    assumes "execute f h = Some (x, h')"
    3.51      and "execute (g x) h' = Some (y, h'')"
    3.52 -  shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
    3.53 +  shows "execute (f \<bind> g) h = Some (y, h'')"
    3.54    using assms by (simp add: bind_def)
    3.55  
    3.56 -lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
    3.57 +lemma return_bind [simp]: "return x \<bind> f = f x"
    3.58    by (rule Heap_eqI) (simp add: execute_simps)
    3.59  
    3.60 -lemma bind_return [simp]: "f \<guillemotright>= return = f"
    3.61 +lemma bind_return [simp]: "f \<bind> return = f"
    3.62    by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
    3.63  
    3.64 -lemma bind_bind [simp]: "(f \<guillemotright>= g) \<guillemotright>= k = (f :: 'a Heap) \<guillemotright>= (\<lambda>x. g x \<guillemotright>= k)"
    3.65 +lemma bind_bind [simp]: "(f \<bind> g) \<bind> k = (f :: 'a Heap) \<bind> (\<lambda>x. g x \<bind> k)"
    3.66    by (rule Heap_eqI) (simp add: bind_def execute_simps split: option.splits)
    3.67  
    3.68 -lemma raise_bind [simp]: "raise e \<guillemotright>= f = raise e"
    3.69 +lemma raise_bind [simp]: "raise e \<bind> f = raise e"
    3.70    by (rule Heap_eqI) (simp add: execute_simps)
    3.71  
    3.72  
    3.73 @@ -334,7 +334,7 @@
    3.74  lemma assert_cong [fundef_cong]:
    3.75    assumes "P = P'"
    3.76    assumes "\<And>x. P' x \<Longrightarrow> f x = f' x"
    3.77 -  shows "(assert P x >>= f) = (assert P' x >>= f')"
    3.78 +  shows "(assert P x \<bind> f) = (assert P' x \<bind> f')"
    3.79    by (rule Heap_eqI) (insert assms, simp add: assert_def)
    3.80  
    3.81  
    3.82 @@ -348,7 +348,7 @@
    3.83    by (simp add: lift_def)
    3.84  
    3.85  lemma bind_lift:
    3.86 -  "(f \<guillemotright>= lift g) = (f \<guillemotright>= (\<lambda>x. return (g x)))"
    3.87 +  "(f \<bind> lift g) = (f \<bind> (\<lambda>x. return (g x)))"
    3.88    by (simp add: lift_def comp_def)
    3.89  
    3.90  
    3.91 @@ -363,7 +363,7 @@
    3.92     }"
    3.93  
    3.94  lemma fold_map_append:
    3.95 -  "fold_map f (xs @ ys) = fold_map f xs \<guillemotright>= (\<lambda>xs. fold_map f ys \<guillemotright>= (\<lambda>ys. return (xs @ ys)))"
    3.96 +  "fold_map f (xs @ ys) = fold_map f xs \<bind> (\<lambda>xs. fold_map f ys \<bind> (\<lambda>ys. return (xs @ ys)))"
    3.97    by (induct xs) simp_all
    3.98  
    3.99  lemma execute_fold_map_unchanged_heap [execute_simps]:
   3.100 @@ -476,7 +476,7 @@
   3.101  
   3.102  lemma bind_mono [partial_function_mono]:
   3.103    assumes mf: "mono_Heap B" and mg: "\<And>y. mono_Heap (\<lambda>f. C y f)"
   3.104 -  shows "mono_Heap (\<lambda>f. B f \<guillemotright>= (\<lambda>y. C y f))"
   3.105 +  shows "mono_Heap (\<lambda>f. B f \<bind> (\<lambda>y. C y f))"
   3.106  proof (rule monotoneI)
   3.107    fix f g :: "'a \<Rightarrow> 'b Heap" assume fg: "fun_ord Heap_ord f g"
   3.108    from mf
   3.109 @@ -484,7 +484,7 @@
   3.110    from mg
   3.111    have 2: "\<And>y'. Heap_ord (C y' f) (C y' g)" by (rule monotoneD) (rule fg)
   3.112  
   3.113 -  have "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y. C y f))"
   3.114 +  have "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y. C y f))"
   3.115      (is "Heap_ord ?L ?R")
   3.116    proof (rule Heap_ordI)
   3.117      fix h
   3.118 @@ -492,7 +492,7 @@
   3.119        by (rule Heap_ordE[where h = h]) (auto simp: execute_bind_case)
   3.120    qed
   3.121    also
   3.122 -  have "Heap_ord (B g \<guillemotright>= (\<lambda>y'. C y' f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))"
   3.123 +  have "Heap_ord (B g \<bind> (\<lambda>y'. C y' f)) (B g \<bind> (\<lambda>y'. C y' g))"
   3.124      (is "Heap_ord ?L ?R")
   3.125    proof (rule Heap_ordI)
   3.126      fix h
   3.127 @@ -512,7 +512,7 @@
   3.128      qed
   3.129    qed
   3.130    finally (heap.leq_trans)
   3.131 -  show "Heap_ord (B f \<guillemotright>= (\<lambda>y. C y f)) (B g \<guillemotright>= (\<lambda>y'. C y' g))" .
   3.132 +  show "Heap_ord (B f \<bind> (\<lambda>y. C y f)) (B g \<bind> (\<lambda>y'. C y' g))" .
   3.133  qed
   3.134  
   3.135  
     4.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 11:27:29 2016 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jan 01 14:44:52 2016 +0100
     4.3 @@ -208,11 +208,11 @@
     4.4    using assms by (rule effectE) (simp add: execute_simps)
     4.5  
     4.6  lemma lookup_chain:
     4.7 -  "(!r \<guillemotright> f) = f"
     4.8 +  "(!r \<then> f) = f"
     4.9    by (rule Heap_eqI) (auto simp add: lookup_def execute_simps intro: execute_bind)
    4.10  
    4.11  lemma update_change [code]:
    4.12 -  "r := e = change (\<lambda>_. e) r \<guillemotright> return ()"
    4.13 +  "r := e = change (\<lambda>_. e) r \<then> return ()"
    4.14    by (rule Heap_eqI) (simp add: change_def lookup_chain)
    4.15  
    4.16  
    4.17 @@ -320,4 +320,3 @@
    4.18  code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
    4.19  
    4.20  end
    4.21 -
     5.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jan 01 11:27:29 2016 +0100
     5.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jan 01 14:44:52 2016 +0100
     5.3 @@ -601,12 +601,12 @@
     5.4  lemma success_bindI' [success_intros]: (*FIXME move*)
     5.5    assumes "success f h"
     5.6    assumes "\<And>h' r. effect f h h' r \<Longrightarrow> success (g r) h'"
     5.7 -  shows "success (f \<guillemotright>= g) h"
     5.8 +  shows "success (f \<bind> g) h"
     5.9  using assms(1) proof (rule success_effectE)
    5.10    fix h' r
    5.11    assume *: "effect f h h' r"
    5.12    with assms(2) have "success (g r) h'" .
    5.13 -  with * show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
    5.14 +  with * show "success (f \<bind> g) h" by (rule success_bind_effectI)
    5.15  qed
    5.16  
    5.17  lemma success_partitionI:
     6.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jan 01 11:27:29 2016 +0100
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jan 01 14:44:52 2016 +0100
     6.3 @@ -110,7 +110,7 @@
     6.4        subarray_def rev.simps[where j=0] elim!: effect_elims)
     6.5    (drule sym[of "List.length (Array.get h a)"], simp)
     6.6  
     6.7 -definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
     6.8 +definition "example = (Array.make 10 id \<bind> (\<lambda>a. rev a 0 9))"
     6.9  
    6.10  export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
    6.11  
     7.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 01 11:27:29 2016 +0100
     7.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Fri Jan 01 14:44:52 2016 +0100
     7.3 @@ -507,7 +507,7 @@
     7.4  qed
     7.5  
     7.6  lemma traverse_make_llist':
     7.7 -  assumes effect: "effect (make_llist xs \<guillemotright>= traverse) h h' r"
     7.8 +  assumes effect: "effect (make_llist xs \<bind> traverse) h h' r"
     7.9    shows "r = xs"
    7.10  proof -
    7.11    from effect obtain h1 r1
    7.12 @@ -942,8 +942,8 @@
    7.13  
    7.14  text {* A simple example program *}
    7.15  
    7.16 -definition test_1 where "test_1 = (do { ll_xs <- make_llist [1..(15::int)]; xs <- traverse ll_xs; return xs })" 
    7.17 -definition test_2 where "test_2 = (do { ll_xs <- make_llist [1..(15::int)]; ll_ys <- rev ll_xs; ys <- traverse ll_ys; return ys })"
    7.18 +definition test_1 where "test_1 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; xs \<leftarrow> traverse ll_xs; return xs })" 
    7.19 +definition test_2 where "test_2 = (do { ll_xs \<leftarrow> make_llist [1..(15::int)]; ll_ys \<leftarrow> rev ll_xs; ys \<leftarrow> traverse ll_ys; return ys })"
    7.20  
    7.21  definition test_3 where "test_3 =
    7.22    (do {
    7.23 @@ -966,4 +966,3 @@
    7.24  export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala Scala_imp
    7.25  
    7.26  end
    7.27 -
     8.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jan 01 11:27:29 2016 +0100
     8.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Fri Jan 01 14:44:52 2016 +0100
     8.3 @@ -201,9 +201,9 @@
     8.4    "res_thm' l (x#xs) (y#ys) = 
     8.5    (if (x = l \<or> x = compl l) then resolve2 (compl x) xs (y#ys)
     8.6    else (if (y = l \<or> y = compl l) then resolve1 (compl y) (x#xs) ys
     8.7 -  else (if (x < y) then (res_thm' l xs (y#ys)) \<guillemotright>= (\<lambda>v. return (x # v))
     8.8 -  else (if (x > y) then (res_thm' l (x#xs) ys) \<guillemotright>= (\<lambda>v. return (y # v))
     8.9 -  else (res_thm' l xs ys) \<guillemotright>= (\<lambda>v. return (x # v))))))"
    8.10 +  else (if (x < y) then (res_thm' l xs (y#ys)) \<bind> (\<lambda>v. return (x # v))
    8.11 +  else (if (x > y) then (res_thm' l (x#xs) ys) \<bind> (\<lambda>v. return (y # v))
    8.12 +  else (res_thm' l xs ys) \<bind> (\<lambda>v. return (x # v))))))"
    8.13  | "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
    8.14  | "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
    8.15  
    8.16 @@ -432,7 +432,7 @@
    8.17    foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"
    8.18  where
    8.19    "foldM f [] s = return s"
    8.20 -  | "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"
    8.21 +  | "foldM f (x#xs) s = f x s \<bind> foldM f xs"
    8.22  
    8.23  fun doProofStep2 :: "Clause option array \<Rightarrow> ProofStep \<Rightarrow> Clause list \<Rightarrow> Clause list Heap"
    8.24  where
     9.1 --- a/src/HOL/Library/Monad_Syntax.thy	Fri Jan 01 11:27:29 2016 +0100
     9.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jan 01 14:44:52 2016 +0100
     9.3 @@ -15,28 +15,22 @@
     9.4  \<close>
     9.5  
     9.6  consts
     9.7 -  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<guillemotright>=" 54)
     9.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
     9.9  
    9.10  notation (ASCII)
    9.11    bind (infixr ">>=" 54)
    9.12  
    9.13 -notation (latex output)
    9.14 -  bind (infixr "\<bind>" 54)
    9.15 -
    9.16  
    9.17  abbreviation (do_notation)
    9.18    bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
    9.19    where "bind_do \<equiv> bind"
    9.20  
    9.21  notation (output)
    9.22 -  bind_do (infixr "\<guillemotright>=" 54)
    9.23 +  bind_do (infixr "\<bind>" 54)
    9.24  
    9.25  notation (ASCII output)
    9.26    bind_do (infixr ">>=" 54)
    9.27  
    9.28 -notation (latex output)
    9.29 -  bind_do (infixr "\<bind>" 54)
    9.30 -
    9.31  
    9.32  nonterminal do_binds and do_bind
    9.33  syntax
    9.34 @@ -46,15 +40,12 @@
    9.35    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    9.36    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    9.37    "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    9.38 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
    9.39 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    9.40  
    9.41  syntax (ASCII)
    9.42    "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
    9.43    "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    9.44  
    9.45 -syntax (latex output)
    9.46 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    9.47 -
    9.48  translations
    9.49    "_do_block (_do_cons (_do_then t) (_do_final e))"
    9.50      == "CONST bind_do t (\<lambda>_. e)"
    9.51 @@ -67,7 +58,7 @@
    9.52    "_do_cons (_do_let p t) (_do_final s)"
    9.53      == "_do_final (let p = t in s)"
    9.54    "_do_block (_do_final e)" => "e"
    9.55 -  "(m >> n)" => "(m >>= (\<lambda>_. n))"
    9.56 +  "(m \<then> n)" => "(m \<bind> (\<lambda>_. n))"
    9.57  
    9.58  adhoc_overloading
    9.59    bind Set.bind Predicate.bind Option.bind List.bind
    10.1 --- a/src/HOL/Predicate.thy	Fri Jan 01 11:27:29 2016 +0100
    10.2 +++ b/src/HOL/Predicate.thy	Fri Jan 01 14:44:52 2016 +0100
    10.3 @@ -120,35 +120,35 @@
    10.4    "eval (single x) = (op =) x"
    10.5    by (simp add: single_def)
    10.6  
    10.7 -definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<guillemotright>=" 70) where
    10.8 -  "P \<guillemotright>= f = (SUPREMUM {x. eval P x} f)"
    10.9 +definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where
   10.10 +  "P \<bind> f = (SUPREMUM {x. eval P x} f)"
   10.11  
   10.12  lemma eval_bind [simp]:
   10.13 -  "eval (P \<guillemotright>= f) = eval (SUPREMUM {x. eval P x} f)"
   10.14 +  "eval (P \<bind> f) = eval (SUPREMUM {x. eval P x} f)"
   10.15    by (simp add: bind_def)
   10.16  
   10.17  lemma bind_bind:
   10.18 -  "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
   10.19 +  "(P \<bind> Q) \<bind> R = P \<bind> (\<lambda>x. Q x \<bind> R)"
   10.20    by (rule pred_eqI) auto
   10.21  
   10.22  lemma bind_single:
   10.23 -  "P \<guillemotright>= single = P"
   10.24 +  "P \<bind> single = P"
   10.25    by (rule pred_eqI) auto
   10.26  
   10.27  lemma single_bind:
   10.28 -  "single x \<guillemotright>= P = P x"
   10.29 +  "single x \<bind> P = P x"
   10.30    by (rule pred_eqI) auto
   10.31  
   10.32  lemma bottom_bind:
   10.33 -  "\<bottom> \<guillemotright>= P = \<bottom>"
   10.34 +  "\<bottom> \<bind> P = \<bottom>"
   10.35    by (rule pred_eqI) auto
   10.36  
   10.37  lemma sup_bind:
   10.38 -  "(P \<squnion> Q) \<guillemotright>= R = P \<guillemotright>= R \<squnion> Q \<guillemotright>= R"
   10.39 +  "(P \<squnion> Q) \<bind> R = P \<bind> R \<squnion> Q \<bind> R"
   10.40    by (rule pred_eqI) auto
   10.41  
   10.42  lemma Sup_bind:
   10.43 -  "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
   10.44 +  "(\<Squnion>A \<bind> f) = \<Squnion>((\<lambda>x. x \<bind> f) ` A)"
   10.45    by (rule pred_eqI) auto
   10.46  
   10.47  lemma pred_iffI:
   10.48 @@ -169,10 +169,10 @@
   10.49  lemma singleE': "eval (single x) y \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   10.50    by simp
   10.51  
   10.52 -lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<guillemotright>= Q) y"
   10.53 +lemma bindI: "eval P x \<Longrightarrow> eval (Q x) y \<Longrightarrow> eval (P \<bind> Q) y"
   10.54    by auto
   10.55  
   10.56 -lemma bindE: "eval (R \<guillemotright>= Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   10.57 +lemma bindE: "eval (R \<bind> Q) y \<Longrightarrow> (\<And>x. eval R x \<Longrightarrow> eval (Q x) y \<Longrightarrow> P) \<Longrightarrow> P"
   10.58    by auto
   10.59  
   10.60  lemma botE: "eval \<bottom> x \<Longrightarrow> P"
   10.61 @@ -401,7 +401,7 @@
   10.62  by (rule unit_pred_cases) (auto elim: botE intro: singleI)
   10.63  
   10.64  definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a pred \<Rightarrow> 'b pred" where
   10.65 -  "map f P = P \<guillemotright>= (single o f)"
   10.66 +  "map f P = P \<bind> (single o f)"
   10.67  
   10.68  lemma eval_map [simp]:
   10.69    "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
   10.70 @@ -455,11 +455,11 @@
   10.71  
   10.72  primrec "apply" :: "('a \<Rightarrow> 'b pred) \<Rightarrow> 'a seq \<Rightarrow> 'b seq" where
   10.73    "apply f Empty = Empty"
   10.74 -| "apply f (Insert x P) = Join (f x) (Join (P \<guillemotright>= f) Empty)"
   10.75 -| "apply f (Join P xq) = Join (P \<guillemotright>= f) (apply f xq)"
   10.76 +| "apply f (Insert x P) = Join (f x) (Join (P \<bind> f) Empty)"
   10.77 +| "apply f (Join P xq) = Join (P \<bind> f) (apply f xq)"
   10.78  
   10.79  lemma apply_bind:
   10.80 -  "pred_of_seq (apply f xq) = pred_of_seq xq \<guillemotright>= f"
   10.81 +  "pred_of_seq (apply f xq) = pred_of_seq xq \<bind> f"
   10.82  proof (induct xq)
   10.83    case Empty show ?case
   10.84      by (simp add: bottom_bind)
   10.85 @@ -472,7 +472,7 @@
   10.86  qed
   10.87    
   10.88  lemma bind_code [code]:
   10.89 -  "Seq g \<guillemotright>= f = Seq (\<lambda>u. apply f (g ()))"
   10.90 +  "Seq g \<bind> f = Seq (\<lambda>u. apply f (g ()))"
   10.91    unfolding Seq_def by (rule sym, rule apply_bind)
   10.92  
   10.93  lemma bot_set_code [code]:
   10.94 @@ -727,7 +727,7 @@
   10.95    by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
   10.96  
   10.97  no_notation
   10.98 -  bind (infixl "\<guillemotright>=" 70)
   10.99 +  bind (infixl "\<bind>" 70)
  10.100  
  10.101  hide_type (open) pred seq
  10.102  hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
    11.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri Jan 01 11:27:29 2016 +0100
    11.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jan 01 14:44:52 2016 +0100
    11.3 @@ -1107,13 +1107,13 @@
    11.4  
    11.5  lemma emeasure_bind:
    11.6      "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>
    11.7 -      \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
    11.8 +      \<Longrightarrow> emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
    11.9    by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
   11.10  
   11.11  lemma nn_integral_bind:
   11.12    assumes f: "f \<in> borel_measurable B"
   11.13    assumes N: "N \<in> measurable M (subprob_algebra B)"
   11.14 -  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   11.15 +  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   11.16  proof cases
   11.17    assume M: "space M \<noteq> {}" show ?thesis
   11.18      unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
   11.19 @@ -1123,17 +1123,17 @@
   11.20  lemma AE_bind:
   11.21    assumes P[measurable]: "Measurable.pred B P"
   11.22    assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
   11.23 -  shows "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
   11.24 +  shows "(AE x in M \<bind> N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)"
   11.25  proof cases
   11.26    assume M: "space M = {}" show ?thesis
   11.27      unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
   11.28  next
   11.29    assume M: "space M \<noteq> {}"
   11.30    note sets_kernel[OF N, simp]
   11.31 -  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
   11.32 +  have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<bind> N))"
   11.33      by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
   11.34  
   11.35 -  have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
   11.36 +  have "(AE x in M \<bind> N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
   11.37      by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
   11.38               del: nn_integral_indicator)
   11.39    also have "\<dots> = (AE x in M. AE y in N x. P y)"
   11.40 @@ -1180,9 +1180,9 @@
   11.41  
   11.42  lemma subprob_space_bind:
   11.43    assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
   11.44 -  shows "subprob_space (M \<guillemotright>= f)"
   11.45 -proof (rule subprob_space_kernel[of "\<lambda>x. x \<guillemotright>= f"])
   11.46 -  show "(\<lambda>x. x \<guillemotright>= f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
   11.47 +  shows "subprob_space (M \<bind> f)"
   11.48 +proof (rule subprob_space_kernel[of "\<lambda>x. x \<bind> f"])
   11.49 +  show "(\<lambda>x. x \<bind> f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
   11.50      by (rule measurable_bind, rule measurable_ident_sets, rule refl, 
   11.51          rule measurable_compose[OF measurable_snd assms(2)])
   11.52    from assms(1) show "M \<in> space (subprob_algebra M)"
   11.53 @@ -1218,27 +1218,27 @@
   11.54  lemma (in prob_space) prob_space_bind: 
   11.55    assumes ae: "AE x in M. prob_space (N x)"
   11.56      and N[measurable]: "N \<in> measurable M (subprob_algebra S)"
   11.57 -  shows "prob_space (M \<guillemotright>= N)"
   11.58 +  shows "prob_space (M \<bind> N)"
   11.59  proof
   11.60 -  have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
   11.61 +  have "emeasure (M \<bind> N) (space (M \<bind> N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
   11.62      by (subst emeasure_bind[where N=S])
   11.63         (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
   11.64    also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
   11.65      using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
   11.66 -  finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
   11.67 +  finally show "emeasure (M \<bind> N) (space (M \<bind> N)) = 1"
   11.68      by (simp add: emeasure_space_1)
   11.69  qed
   11.70  
   11.71  lemma (in subprob_space) bind_in_space:
   11.72 -  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
   11.73 +  "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<bind> A) \<in> space (subprob_algebra N)"
   11.74    by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
   11.75       unfold_locales
   11.76  
   11.77  lemma (in subprob_space) measure_bind:
   11.78    assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N"
   11.79 -  shows "measure (M \<guillemotright>= f) X = \<integral>x. measure (f x) X \<partial>M"
   11.80 +  shows "measure (M \<bind> f) X = \<integral>x. measure (f x) X \<partial>M"
   11.81  proof -
   11.82 -  interpret Mf: subprob_space "M \<guillemotright>= f"
   11.83 +  interpret Mf: subprob_space "M \<bind> f"
   11.84      by (rule subprob_space_bind[OF _ f]) unfold_locales
   11.85  
   11.86    { fix x assume "x \<in> space M"
   11.87 @@ -1248,7 +1248,7 @@
   11.88        by (auto simp: emeasure_eq_measure subprob_measure_le_1) }
   11.89    note this[simp]
   11.90  
   11.91 -  have "emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   11.92 +  have "emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   11.93      using subprob_not_empty f X by (rule emeasure_bind)
   11.94    also have "\<dots> = \<integral>\<^sup>+x. ereal (measure (f x) X) \<partial>M"
   11.95      by (intro nn_integral_cong) simp
   11.96 @@ -1262,29 +1262,29 @@
   11.97  
   11.98  lemma emeasure_bind_const: 
   11.99      "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 
  11.100 -         emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.101 +         emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.102    by (simp add: bind_nonempty emeasure_join nn_integral_distr 
  11.103                  space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg)
  11.104  
  11.105  lemma emeasure_bind_const':
  11.106    assumes "subprob_space M" "subprob_space N"
  11.107 -  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.108 +  shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.109  using assms
  11.110  proof (case_tac "X \<in> sets N")
  11.111    fix X assume "X \<in> sets N"
  11.112 -  thus "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
  11.113 +  thus "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms
  11.114        by (subst emeasure_bind_const) 
  11.115           (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1)
  11.116  next
  11.117    fix X assume "X \<notin> sets N"
  11.118 -  with assms show "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.119 +  with assms show "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)"
  11.120        by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty
  11.121                      space_subprob_algebra emeasure_notin_sets)
  11.122  qed
  11.123  
  11.124  lemma emeasure_bind_const_prob_space:
  11.125    assumes "prob_space M" "subprob_space N"
  11.126 -  shows "emeasure (M \<guillemotright>= (\<lambda>x. N)) X = emeasure N X"
  11.127 +  shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X"
  11.128    using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 
  11.129                              prob_space.emeasure_space_1)
  11.130  
  11.131 @@ -1304,7 +1304,7 @@
  11.132  lemma distr_bind:
  11.133    assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}"
  11.134    assumes f: "f \<in> measurable K R"
  11.135 -  shows "distr (M \<guillemotright>= N) R f = (M \<guillemotright>= (\<lambda>x. distr (N x) R f))"
  11.136 +  shows "distr (M \<bind> N) R f = (M \<bind> (\<lambda>x. distr (N x) R f))"
  11.137    unfolding bind_nonempty''[OF N]
  11.138    apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)])
  11.139    apply (rule f)
  11.140 @@ -1316,7 +1316,7 @@
  11.141  lemma bind_distr:
  11.142    assumes f[measurable]: "f \<in> measurable M X"
  11.143    assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}"
  11.144 -  shows "(distr M X f \<guillemotright>= N) = (M \<guillemotright>= (\<lambda>x. N (f x)))"
  11.145 +  shows "(distr M X f \<bind> N) = (M \<bind> (\<lambda>x. N (f x)))"
  11.146  proof -
  11.147    have "space X \<noteq> {}" "space M \<noteq> {}"
  11.148      using \<open>space M \<noteq> {}\<close> f[THEN measurable_space] by auto
  11.149 @@ -1326,12 +1326,12 @@
  11.150  
  11.151  lemma bind_count_space_singleton:
  11.152    assumes "subprob_space (f x)"
  11.153 -  shows "count_space {x} \<guillemotright>= f = f x"
  11.154 +  shows "count_space {x} \<bind> f = f x"
  11.155  proof-
  11.156    have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto
  11.157    have "count_space {x} = return (count_space {x}) x"
  11.158      by (intro measure_eqI) (auto dest: A)
  11.159 -  also have "... \<guillemotright>= f = f x"
  11.160 +  also have "... \<bind> f = f x"
  11.161      by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms)
  11.162    finally show ?thesis .
  11.163  qed
  11.164 @@ -1346,10 +1346,10 @@
  11.165    note N_space = sets_eq_imp_space_eq[OF N_sets, simp]
  11.166    show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))"
  11.167      by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]])
  11.168 -  fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
  11.169 +  fix A assume "A \<in> sets (restrict_space (M \<bind> N) X)"
  11.170    with X have "A \<in> sets K" "A \<subseteq> X"
  11.171      by (auto simp: sets_restrict_space)
  11.172 -  then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
  11.173 +  then show "emeasure (restrict_space (M \<bind> N) X) A = emeasure (M \<bind> (\<lambda>x. restrict_space (N x) X)) A"
  11.174      using assms
  11.175      apply (subst emeasure_restrict_space)
  11.176      apply (simp_all add: emeasure_bind[OF assms(2,1)])
  11.177 @@ -1362,8 +1362,8 @@
  11.178  lemma bind_restrict_space:
  11.179    assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M"
  11.180    and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)"
  11.181 -  shows "restrict_space M A \<guillemotright>= f = M \<guillemotright>= (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
  11.182 -  (is "?lhs = ?rhs" is "_ = M \<guillemotright>= ?f")
  11.183 +  shows "restrict_space M A \<bind> f = M \<bind> (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))"
  11.184 +  (is "?lhs = ?rhs" is "_ = M \<bind> ?f")
  11.185  proof -
  11.186    let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M"
  11.187    let ?x = "Eps ?P"
  11.188 @@ -1391,7 +1391,7 @@
  11.189    finally show ?thesis .
  11.190  qed
  11.191  
  11.192 -lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
  11.193 +lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<bind> (\<lambda>x. N) = N"
  11.194    by (intro measure_eqI) 
  11.195       (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space)
  11.196  
  11.197 @@ -1445,15 +1445,15 @@
  11.198    assumes Mg: "g \<in> measurable N (subprob_algebra N')"
  11.199    assumes Mf: "f \<in> measurable M (subprob_algebra M')"
  11.200    assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N"
  11.201 -  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g"
  11.202 +  shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g"
  11.203  proof-
  11.204 -  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g = 
  11.205 -            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g}"
  11.206 +  have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g = 
  11.207 +            do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g}"
  11.208      using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg
  11.209                        measurable_compose[OF _ return_measurable] simp: measurable_split_conv)
  11.210    also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable
  11.211 -  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<guillemotright>= g} = 
  11.212 -            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g}"
  11.213 +  hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g} = 
  11.214 +            do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g}"
  11.215      apply (intro ballI bind_cong bind_assoc)
  11.216      apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp)
  11.217      apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg)
  11.218 @@ -1461,7 +1461,7 @@
  11.219    also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'"
  11.220      by (intro sets_eq_imp_space_eq sets_kernel[OF Mf])
  11.221    with measurable_space[OF Mh] 
  11.222 -    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<guillemotright>= g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
  11.223 +    have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}"
  11.224      by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure)
  11.225    finally show ?thesis ..
  11.226  qed
  11.227 @@ -1470,36 +1470,36 @@
  11.228    by (simp add: space_subprob_algebra) unfold_locales
  11.229  
  11.230  lemma (in pair_prob_space) pair_measure_eq_bind:
  11.231 -  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
  11.232 +  "(M1 \<Otimes>\<^sub>M M2) = (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
  11.233  proof (rule measure_eqI)
  11.234    have ps_M2: "prob_space M2" by unfold_locales
  11.235    note return_measurable[measurable]
  11.236 -  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
  11.237 +  show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
  11.238      by (simp_all add: M1.not_empty M2.not_empty)
  11.239    fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
  11.240 -  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
  11.241 +  show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
  11.242      by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"]
  11.243               intro!: nn_integral_cong)
  11.244  qed
  11.245  
  11.246  lemma (in pair_prob_space) bind_rotate:
  11.247    assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)"
  11.248 -  shows "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
  11.249 +  shows "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))"
  11.250  proof - 
  11.251    interpret swap: pair_prob_space M2 M1 by unfold_locales
  11.252    note measurable_bind[where N="M2", measurable]
  11.253    note measurable_bind[where N="M1", measurable]
  11.254    have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)"
  11.255      by (auto simp: space_subprob_algebra) unfold_locales
  11.256 -  have "(M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. C x y))) = 
  11.257 -    (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<guillemotright>= (\<lambda>(x, y). C x y)"
  11.258 +  have "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = 
  11.259 +    (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<bind> (\<lambda>(x, y). C x y)"
  11.260      by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N])
  11.261 -  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<guillemotright>= (\<lambda>(x, y). C x y)"
  11.262 +  also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<bind> (\<lambda>(x, y). C x y)"
  11.263      unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] ..
  11.264 -  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>x. M1 \<guillemotright>= (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<guillemotright>= (\<lambda>(y, x). C x y)"
  11.265 +  also have "\<dots> = (M2 \<bind> (\<lambda>x. M1 \<bind> (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<bind> (\<lambda>(y, x). C x y)"
  11.266      unfolding swap.pair_measure_eq_bind[symmetric]
  11.267      by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong)
  11.268 -  also have "\<dots> = (M2 \<guillemotright>= (\<lambda>y. M1 \<guillemotright>= (\<lambda>x. C x y)))"
  11.269 +  also have "\<dots> = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))"
  11.270      by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N])
  11.271    finally show ?thesis .
  11.272  qed
  11.273 @@ -1552,7 +1552,7 @@
  11.274      by (simp add: emeasure_notin_sets)
  11.275  qed
  11.276  
  11.277 -lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<guillemotright>= return N = M"
  11.278 +lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<bind> return N = M"
  11.279     by (cases "space M = {}")
  11.280        (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'
  11.281                  cong: subprob_algebra_cong)
    12.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 11:27:29 2016 +0100
    12.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jan 01 14:44:52 2016 +0100
    12.3 @@ -334,13 +334,13 @@
    12.4    assumes "\<And>i. i \<in> set_pmf x \<Longrightarrow> A i = B i"
    12.5    shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
    12.6  proof (rule measure_eqI)
    12.7 -  show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
    12.8 +  show "sets (measure_pmf x \<bind> A) = sets (measure_pmf x \<bind> B)"
    12.9      using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
   12.10  next
   12.11 -  fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
   12.12 +  fix X assume "X \<in> sets (measure_pmf x \<bind> A)"
   12.13    then have X: "X \<in> sets N"
   12.14      using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
   12.15 -  show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
   12.16 +  show "emeasure (measure_pmf x \<bind> A) X = emeasure (measure_pmf x \<bind> B) X"
   12.17      using assms
   12.18      by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
   12.19         (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
   12.20 @@ -362,13 +362,13 @@
   12.21    have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
   12.22      by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
   12.23  
   12.24 -  show "prob_space (f \<guillemotright>= g)"
   12.25 +  show "prob_space (f \<bind> g)"
   12.26      using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
   12.27 -  then interpret fg: prob_space "f \<guillemotright>= g" .
   12.28 -  show [simp]: "sets (f \<guillemotright>= g) = UNIV"
   12.29 +  then interpret fg: prob_space "f \<bind> g" .
   12.30 +  show [simp]: "sets (f \<bind> g) = UNIV"
   12.31      using sets_eq_imp_space_eq[OF s_f]
   12.32      by (subst sets_bind[where N="count_space UNIV"]) auto
   12.33 -  show "AE x in f \<guillemotright>= g. measure (f \<guillemotright>= g) {x} \<noteq> 0"
   12.34 +  show "AE x in f \<bind> g. measure (f \<bind> g) {x} \<noteq> 0"
   12.35      apply (simp add: fg.prob_eq_0 AE_bind[where B="count_space UNIV"])
   12.36      using ae_f
   12.37      apply eventually_elim
   12.38 @@ -408,7 +408,7 @@
   12.39    "p = q \<Longrightarrow> (\<And>x. x \<in> set_pmf q =simp=> f x = g x) \<Longrightarrow> bind_pmf p f = bind_pmf q g"
   12.40    by (simp add: simp_implies_def cong: bind_pmf_cong)
   12.41  
   12.42 -lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
   12.43 +lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<bind> (\<lambda>x. measure_pmf (f x)))"
   12.44    by transfer simp
   12.45  
   12.46  lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   12.47 @@ -437,7 +437,7 @@
   12.48  
   12.49  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
   12.50  proof (transfer, clarify)
   12.51 -  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
   12.52 +  fix N :: "'a measure" assume "sets N = UNIV" then show "N \<bind> return (count_space UNIV) = N"
   12.53      by (subst return_sets_cong[where N=N]) (simp_all add: bind_return')
   12.54  qed
   12.55  
   12.56 @@ -458,7 +458,7 @@
   12.57    "rel_fun op = (rel_fun cr_pmf cr_pmf) (\<lambda>f M. distr M (count_space UNIV) f) map_pmf"
   12.58  proof -
   12.59    have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
   12.60 -     (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
   12.61 +     (\<lambda>f M. M \<bind> (return (count_space UNIV) o f)) map_pmf"
   12.62      unfolding map_pmf_def[abs_def] comp_def by transfer_prover
   12.63    then show ?thesis
   12.64      by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
   12.65 @@ -584,7 +584,7 @@
   12.66  
   12.67  lemma bind_pair_pmf:
   12.68    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
   12.69 -  shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
   12.70 +  shows "measure_pmf (pair_pmf A B) \<bind> M = (measure_pmf A \<bind> (\<lambda>x. measure_pmf B \<bind> (\<lambda>y. M (x, y))))"
   12.71      (is "?L = ?R")
   12.72  proof (rule measure_eqI)
   12.73    have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
    13.1 --- a/src/HOL/Probability/Projective_Family.thy	Fri Jan 01 11:27:29 2016 +0100
    13.2 +++ b/src/HOL/Probability/Projective_Family.thy	Fri Jan 01 14:44:52 2016 +0100
    13.3 @@ -316,7 +316,7 @@
    13.4  
    13.5  primrec C :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) measure" where
    13.6    "C n 0 \<omega> = return (PiM {0..<n} M) \<omega>"
    13.7 -| "C n (Suc m) \<omega> = C n m \<omega> \<guillemotright>= eP (n + m)"
    13.8 +| "C n (Suc m) \<omega> = C n m \<omega> \<bind> eP (n + m)"
    13.9  
   13.10  lemma measurable_C[measurable]:
   13.11    "C n m \<in> measurable (PiM {0..<n} M) (subprob_algebra (PiM {0..<n + m} M))"
   13.12 @@ -338,7 +338,7 @@
   13.13  qed (auto intro!: prob_space_return simp: space_PiM)
   13.14  
   13.15  lemma split_C:
   13.16 -  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<guillemotright>= C (n + m) l) = C n (m + l) \<omega>"
   13.17 +  assumes \<omega>: "\<omega> \<in> space (PiM {0..<n} M)" shows "(C n m \<omega> \<bind> C (n + m) l) = C n (m + l) \<omega>"
   13.18  proof (induction l)
   13.19    case 0
   13.20    with \<omega> show ?case