src/HOL/Random.thy

 
 (* Author: Florian Haftmann, TU Muenchen *)
 
-section {* A HOL random engine *}
+section \<open>A HOL random engine\<close>
 
 theory Random
 imports List Groups_List
 begin
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 
-subsection {* Auxiliary functions *}
+subsection \<open>Auxiliary functions\<close>
 
 fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
   "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
 
 definition inc_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural" where

 
 definition minus_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> natural" where
   "minus_shift r k l = (if k < l then r + k - l else k - l)"
 
 
-subsection {* Random seeds *}
+subsection \<open>Random seeds\<close>
 
 type_synonym seed = "natural \<times> natural"
 
 primrec "next" :: "seed \<Rightarrow> natural \<times> seed" where
   "next (v, w) = (let

      v'' = inc_shift 2147483562 v;
      w'' = inc_shift 2147483398 w
    in ((v'', w'), (v', w'')))"
 
 
-subsection {* Base selectors *}
+subsection \<open>Base selectors\<close>
 
 fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
 
 definition range :: "natural \<Rightarrow> seed \<Rightarrow> natural \<times> seed" where

     by (auto simp add: select_weight_def select_def scomp_def split_def
       fun_eq_iff pick_same [symmetric] less_natural_def)
 qed
 
 
-subsection {* @{text ML} interface *}
+subsection \<open>@{text ML} interface\<close>
 
 code_reflect Random_Engine
   functions range select select_weight
 
-ML {*
+ML \<open>
 structure Random_Engine =
 struct
 
 open Random_Engine;
 

   in x end;
 
 end;
 
 end;
-*}
+\<close>
 
 hide_type (open) seed
 hide_const (open) inc_shift minus_shift log "next" split_seed
   iterate range select pick select_weight
 hide_fact (open) range_def