src/HOL/Random.thy
 changeset 37751 89e16802b6cc parent 36538 4fe16d49283b child 39198 f967a16dfcdd
```     1.1 --- a/src/HOL/Random.thy	Thu Jul 08 17:23:05 2010 +0200
1.2 +++ b/src/HOL/Random.thy	Fri Jul 09 08:11:10 2010 +0200
1.3 @@ -7,8 +7,8 @@
1.4  imports Code_Numeral List
1.5  begin
1.6
1.7 -notation fcomp (infixl "o>" 60)
1.8 -notation scomp (infixl "o\<rightarrow>" 60)
1.9 +notation fcomp (infixl "\<circ>>" 60)
1.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.11
1.12
1.13  subsection {* Auxiliary functions *}
1.14 @@ -48,12 +48,12 @@
1.15  subsection {* Base selectors *}
1.16
1.17  fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
1.18 -  "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
1.19 +  "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
1.20
1.21  definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
1.22    "range k = iterate (log 2147483561 k)
1.23 -      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
1.24 -    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
1.25 +      (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
1.26 +    \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
1.27
1.28  lemma range:
1.29    "k > 0 \<Longrightarrow> fst (range k s) < k"
1.30 @@ -61,7 +61,7 @@
1.31
1.32  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
1.33    "select xs = range (Code_Numeral.of_nat (length xs))
1.34 -    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
1.35 +    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
1.36
1.37  lemma select:
1.38    assumes "xs \<noteq> []"
1.39 @@ -97,7 +97,7 @@
1.40
1.41  definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
1.42    "select_weight xs = range (listsum (map fst xs))
1.43 -   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
1.44 +   \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
1.45
1.46  lemma select_weight_member:
1.47    assumes "0 < listsum (map fst xs)"
1.48 @@ -184,8 +184,8 @@
1.49    iterate range select pick select_weight
1.50  hide_fact (open) range_def
1.51
1.52 -no_notation fcomp (infixl "o>" 60)
1.53 -no_notation scomp (infixl "o\<rightarrow>" 60)
1.54 +no_notation fcomp (infixl "\<circ>>" 60)
1.55 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
1.56
1.57  end
1.58
```