src/HOL/Random.thy
changeset 51143 0a2371e7ced3
parent 46311 56fae81902ce
child 57225 ff69e42ccf92
     1.1 --- a/src/HOL/Random.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Random.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -13,21 +13,21 @@
     1.4  
     1.5  subsection {* Auxiliary functions *}
     1.6  
     1.7 -fun log :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
     1.8 +fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
     1.9    "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    1.10  
    1.11 -definition inc_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.12 +definition inc_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
    1.13    "inc_shift v k = (if v = k then 1 else k + 1)"
    1.14  
    1.15 -definition minus_shift :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
    1.16 +definition minus_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> natural" where
    1.17    "minus_shift r k l = (if k < l then r + k - l else k - l)"
    1.18  
    1.19  
    1.20  subsection {* Random seeds *}
    1.21  
    1.22 -type_synonym seed = "code_numeral \<times> code_numeral"
    1.23 +type_synonym seed = "natural \<times> natural"
    1.24  
    1.25 -primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
    1.26 +primrec "next" :: "seed \<Rightarrow> natural \<times> seed" where
    1.27    "next (v, w) = (let
    1.28       k =  v div 53668;
    1.29       v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211);
    1.30 @@ -47,55 +47,55 @@
    1.31  
    1.32  subsection {* Base selectors *}
    1.33  
    1.34 -fun iterate :: "code_numeral \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    1.35 +fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    1.36    "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"
    1.37  
    1.38 -definition range :: "code_numeral \<Rightarrow> seed \<Rightarrow> code_numeral \<times> seed" where
    1.39 +definition range :: "natural \<Rightarrow> seed \<Rightarrow> natural \<times> seed" where
    1.40    "range k = iterate (log 2147483561 k)
    1.41        (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    1.42      \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"
    1.43  
    1.44  lemma range:
    1.45    "k > 0 \<Longrightarrow> fst (range k s) < k"
    1.46 -  by (simp add: range_def split_def del: log.simps iterate.simps)
    1.47 +  by (simp add: range_def split_def less_natural_def del: log.simps iterate.simps)
    1.48  
    1.49  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    1.50 -  "select xs = range (Code_Numeral.of_nat (length xs))
    1.51 -    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Numeral.nat_of k)))"
    1.52 +  "select xs = range (natural_of_nat (length xs))
    1.53 +    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (nat_of_natural k)))"
    1.54       
    1.55  lemma select:
    1.56    assumes "xs \<noteq> []"
    1.57    shows "fst (select xs s) \<in> set xs"
    1.58  proof -
    1.59 -  from assms have "Code_Numeral.of_nat (length xs) > 0" by simp
    1.60 +  from assms have "natural_of_nat (length xs) > 0" by (simp add: less_natural_def)
    1.61    with range have
    1.62 -    "fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)" by best
    1.63 +    "fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)" by best
    1.64    then have
    1.65 -    "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
    1.66 +    "nat_of_natural (fst (range (natural_of_nat (length xs)) s)) < length xs" by (simp add: less_natural_def)
    1.67    then show ?thesis
    1.68      by (simp add: split_beta select_def)
    1.69  qed
    1.70  
    1.71 -primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
    1.72 +primrec pick :: "(natural \<times> 'a) list \<Rightarrow> natural \<Rightarrow> 'a" where
    1.73    "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
    1.74  
    1.75  lemma pick_member:
    1.76    "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
    1.77 -  by (induct xs arbitrary: i) simp_all
    1.78 +  by (induct xs arbitrary: i) (simp_all add: less_natural_def)
    1.79  
    1.80  lemma pick_drop_zero:
    1.81    "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
    1.82 -  by (induct xs) (auto simp add: fun_eq_iff)
    1.83 +  by (induct xs) (auto simp add: fun_eq_iff less_natural_def minus_natural_def)
    1.84  
    1.85  lemma pick_same:
    1.86 -  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (Code_Numeral.of_nat l) = nth xs l"
    1.87 +  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l"
    1.88  proof (induct xs arbitrary: l)
    1.89    case Nil then show ?case by simp
    1.90  next
    1.91 -  case (Cons x xs) then show ?case by (cases l) simp_all
    1.92 +  case (Cons x xs) then show ?case by (cases l) (simp_all add: less_natural_def)
    1.93  qed
    1.94  
    1.95 -definition select_weight :: "(code_numeral \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    1.96 +definition select_weight :: "(natural \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
    1.97    "select_weight xs = range (listsum (map fst xs))
    1.98     \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"
    1.99  
   1.100 @@ -112,13 +112,13 @@
   1.101  
   1.102  lemma select_weight_cons_zero:
   1.103    "select_weight ((0, x) # xs) = select_weight xs"
   1.104 -  by (simp add: select_weight_def)
   1.105 +  by (simp add: select_weight_def less_natural_def)
   1.106  
   1.107  lemma select_weight_drop_zero:
   1.108    "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
   1.109  proof -
   1.110    have "listsum (map fst [(k, _)\<leftarrow>xs . 0 < k]) = listsum (map fst xs)"
   1.111 -    by (induct xs) auto
   1.112 +    by (induct xs) (auto simp add: less_natural_def, simp add: plus_natural_def)
   1.113    then show ?thesis by (simp only: select_weight_def pick_drop_zero)
   1.114  qed
   1.115  
   1.116 @@ -126,13 +126,13 @@
   1.117    assumes "xs \<noteq> []"
   1.118    shows "select_weight (map (Pair 1) xs) = select xs"
   1.119  proof -
   1.120 -  have less: "\<And>s. fst (range (Code_Numeral.of_nat (length xs)) s) < Code_Numeral.of_nat (length xs)"
   1.121 -    using assms by (intro range) simp
   1.122 -  moreover have "listsum (map fst (map (Pair 1) xs)) = Code_Numeral.of_nat (length xs)"
   1.123 +  have less: "\<And>s. fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)"
   1.124 +    using assms by (intro range) (simp add: less_natural_def)
   1.125 +  moreover have "listsum (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
   1.126      by (induct xs) simp_all
   1.127    ultimately show ?thesis
   1.128      by (auto simp add: select_weight_def select_def scomp_def split_def
   1.129 -      fun_eq_iff pick_same [symmetric])
   1.130 +      fun_eq_iff pick_same [symmetric] less_natural_def)
   1.131  qed
   1.132  
   1.133  
   1.134 @@ -147,7 +147,7 @@
   1.135  
   1.136  open Random_Engine;
   1.137  
   1.138 -type seed = int * int;
   1.139 +type seed = Code_Numeral.natural * Code_Numeral.natural;
   1.140  
   1.141  local
   1.142  
   1.143 @@ -156,7 +156,7 @@
   1.144      val now = Time.toMilliseconds (Time.now ());
   1.145      val (q, s1) = IntInf.divMod (now, 2147483562);
   1.146      val s2 = q mod 2147483398;
   1.147 -  in (s1 + 1, s2 + 1) end);
   1.148 +  in pairself Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end);
   1.149  
   1.150  in
   1.151  
   1.152 @@ -188,3 +188,4 @@
   1.153  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.154  
   1.155  end
   1.156 +