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