moved Random.thy to Library
authorhaftmann
Thu Feb 05 14:14:02 2009 +0100 (2009-02-05)
changeset 29806bebe5a254ba6
parent 29802 d201a838d0f7
child 29807 4159caa18f85
moved Random.thy to Library
src/HOL/Extraction/Higman.thy
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Random.thy
src/HOL/ex/Random.thy
     1.1 --- a/src/HOL/Extraction/Higman.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/Extraction/Higman.thy	Thu Feb 05 14:14:02 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Extraction/Higman.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer, TU Muenchen
     1.7                  Monika Seisenberger, LMU Muenchen
     1.8  *)
     1.9 @@ -7,7 +6,7 @@
    1.10  header {* Higman's lemma *}
    1.11  
    1.12  theory Higman
    1.13 -imports Main "~~/src/HOL/ex/Random"
    1.14 +imports Main State_Monad Random
    1.15  begin
    1.16  
    1.17  text {*
     2.1 --- a/src/HOL/IsaMakefile	Wed Feb 04 18:10:07 2009 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Thu Feb 05 14:14:02 2009 +0100
     2.3 @@ -311,6 +311,7 @@
     2.4  
     2.5  HOL-Library: HOL $(LOG)/HOL-Library.gz
     2.6  
     2.7 +
     2.8  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
     2.9    Library/Abstract_Rat.thy \
    2.10    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
    2.11 @@ -335,6 +336,7 @@
    2.12    Library/Mapping.thy	Library/Numeral_Type.thy	Library/Reflection.thy		\
    2.13    Library/Boolean_Algebra.thy Library/Countable.thy	\
    2.14    Library/RBT.thy	Library/Univ_Poly.thy	\
    2.15 +  Library/Random.thy	Library/Quickcheck.thy	\
    2.16    Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
    2.17    Library/reify_data.ML Library/reflection.ML
    2.18  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    2.19 @@ -814,7 +816,7 @@
    2.20    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
    2.21    ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
    2.22    ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
    2.23 -  ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
    2.24 +  ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy		\
    2.25    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
    2.26    ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy						\
    2.27    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
     3.1 --- a/src/HOL/Library/Library.thy	Wed Feb 04 18:10:07 2009 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Thu Feb 05 14:14:02 2009 +0100
     3.3 @@ -34,9 +34,11 @@
     3.4    Permutation
     3.5    Pocklington
     3.6    Primes
     3.7 +  Quickcheck
     3.8    Quicksort
     3.9    Quotient
    3.10    Ramsey
    3.11 +  Random
    3.12    Reflection
    3.13    RBT
    3.14    State_Monad
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Random.thy	Thu Feb 05 14:14:02 2009 +0100
     4.3 @@ -0,0 +1,182 @@
     4.4 +(*  Author:     Florian Haftmann, TU Muenchen
     4.5 +*)
     4.6 +
     4.7 +header {* A HOL random engine *}
     4.8 +
     4.9 +theory Random
    4.10 +imports State_Monad Code_Index
    4.11 +begin
    4.12 +
    4.13 +subsection {* Auxiliary functions *}
    4.14 +
    4.15 +definition
    4.16 +  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
    4.17 +where
    4.18 +  "inc_shift v k = (if v = k then 1 else k + 1)"
    4.19 +
    4.20 +definition
    4.21 +  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
    4.22 +where
    4.23 +  "minus_shift r k l = (if k < l then r + k - l else k - l)"
    4.24 +
    4.25 +fun
    4.26 +  log :: "index \<Rightarrow> index \<Rightarrow> index"
    4.27 +where
    4.28 +  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    4.29 +
    4.30 +subsection {* Random seeds *}
    4.31 +
    4.32 +types seed = "index \<times> index"
    4.33 +
    4.34 +primrec
    4.35 +  "next" :: "seed \<Rightarrow> index \<times> seed"
    4.36 +where
    4.37 +  "next (v, w) = (let
    4.38 +     k =  v div 53668;
    4.39 +     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    4.40 +     l =  w div 52774;
    4.41 +     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    4.42 +     z =  minus_shift 2147483562 v' (w' + 1) + 1
    4.43 +   in (z, (v', w')))"
    4.44 +
    4.45 +lemma next_not_0:
    4.46 +  "fst (next s) \<noteq> 0"
    4.47 +apply (cases s)
    4.48 +apply (auto simp add: minus_shift_def Let_def)
    4.49 +done
    4.50 +
    4.51 +primrec
    4.52 +  seed_invariant :: "seed \<Rightarrow> bool"
    4.53 +where
    4.54 +  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    4.55 +
    4.56 +lemma if_same:
    4.57 +  "(if b then f x else f y) = f (if b then x else y)"
    4.58 +  by (cases b) simp_all
    4.59 +
    4.60 +definition
    4.61 +  split_seed :: "seed \<Rightarrow> seed \<times> seed"
    4.62 +where
    4.63 +  "split_seed s = (let
    4.64 +     (v, w) = s;
    4.65 +     (v', w') = snd (next s);
    4.66 +     v'' = inc_shift 2147483562 v;
    4.67 +     s'' = (v'', w');
    4.68 +     w'' = inc_shift 2147483398 w;
    4.69 +     s''' = (v', w'')
    4.70 +   in (s'', s'''))"
    4.71 +
    4.72 +
    4.73 +subsection {* Base selectors *}
    4.74 +
    4.75 +function
    4.76 +  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
    4.77 +where
    4.78 +  "range_aux k l s = (if k = 0 then (l, s) else
    4.79 +    let (v, s') = next s
    4.80 +  in range_aux (k - 1) (v + l * 2147483561) s')"
    4.81 +by pat_completeness auto
    4.82 +termination
    4.83 +  by (relation "measure (nat_of_index o fst)")
    4.84 +    (auto simp add: index)
    4.85 +
    4.86 +definition
    4.87 +  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
    4.88 +where
    4.89 +  "range k = (do
    4.90 +     v \<leftarrow> range_aux (log 2147483561 k) 1;
    4.91 +     return (v mod k)
    4.92 +   done)"
    4.93 +
    4.94 +lemma range:
    4.95 +  assumes "k > 0"
    4.96 +  shows "fst (range k s) < k"
    4.97 +proof -
    4.98 +  obtain v w where range_aux:
    4.99 +    "range_aux (log 2147483561 k) 1 s = (v, w)"
   4.100 +    by (cases "range_aux (log 2147483561 k) 1 s")
   4.101 +  with assms show ?thesis
   4.102 +    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
   4.103 +qed
   4.104 +
   4.105 +definition
   4.106 +  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.107 +where
   4.108 +  "select xs = (do
   4.109 +     k \<leftarrow> range (index_of_nat (length xs));
   4.110 +     return (nth xs (nat_of_index k))
   4.111 +   done)"
   4.112 +
   4.113 +lemma select:
   4.114 +  assumes "xs \<noteq> []"
   4.115 +  shows "fst (select xs s) \<in> set xs"
   4.116 +proof -
   4.117 +  from assms have "index_of_nat (length xs) > 0" by simp
   4.118 +  with range have
   4.119 +    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
   4.120 +  then have
   4.121 +    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
   4.122 +  then show ?thesis
   4.123 +    by (auto simp add: monad_collapse select_def)
   4.124 +qed
   4.125 +
   4.126 +definition
   4.127 +  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.128 +where
   4.129 +  [code del]: "select_default k x y = (do
   4.130 +     l \<leftarrow> range k;
   4.131 +     return (if l + 1 < k then x else y)
   4.132 +   done)"
   4.133 +
   4.134 +lemma select_default_zero:
   4.135 +  "fst (select_default 0 x y s) = y"
   4.136 +  by (simp add: monad_collapse select_default_def)
   4.137 +
   4.138 +lemma select_default_code [code]:
   4.139 +  "select_default k x y = (if k = 0 then do
   4.140 +     _ \<leftarrow> range 1;
   4.141 +     return y
   4.142 +   done else do
   4.143 +     l \<leftarrow> range k;
   4.144 +     return (if l + 1 < k then x else y)
   4.145 +   done)"
   4.146 +proof (cases "k = 0")
   4.147 +  case False then show ?thesis by (simp add: select_default_def)
   4.148 +next
   4.149 +  case True then show ?thesis
   4.150 +    by (simp add: monad_collapse select_default_def range_def)
   4.151 +qed
   4.152 +
   4.153 +
   4.154 +subsection {* @{text ML} interface *}
   4.155 +
   4.156 +ML {*
   4.157 +structure Random_Engine =
   4.158 +struct
   4.159 +
   4.160 +type seed = int * int;
   4.161 +
   4.162 +local
   4.163 +
   4.164 +val seed = ref 
   4.165 +  (let
   4.166 +    val now = Time.toMilliseconds (Time.now ());
   4.167 +    val (q, s1) = IntInf.divMod (now, 2147483562);
   4.168 +    val s2 = q mod 2147483398;
   4.169 +  in (s1 + 1, s2 + 1) end);
   4.170 +
   4.171 +in
   4.172 +
   4.173 +fun run f =
   4.174 +  let
   4.175 +    val (x, seed') = f (! seed);
   4.176 +    val _ = seed := seed'
   4.177 +  in x end;
   4.178 +
   4.179 +end;
   4.180 +
   4.181 +end;
   4.182 +*}
   4.183 +
   4.184 +end
   4.185 +
     5.1 --- a/src/HOL/ex/Random.thy	Wed Feb 04 18:10:07 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,183 +0,0 @@
     5.4 -(*  ID:         $Id$
     5.5 -    Author:     Florian Haftmann, TU Muenchen
     5.6 -*)
     5.7 -
     5.8 -header {* A HOL random engine *}
     5.9 -
    5.10 -theory Random
    5.11 -imports State_Monad Code_Index
    5.12 -begin
    5.13 -
    5.14 -subsection {* Auxiliary functions *}
    5.15 -
    5.16 -definition
    5.17 -  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
    5.18 -where
    5.19 -  "inc_shift v k = (if v = k then 1 else k + 1)"
    5.20 -
    5.21 -definition
    5.22 -  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
    5.23 -where
    5.24 -  "minus_shift r k l = (if k < l then r + k - l else k - l)"
    5.25 -
    5.26 -fun
    5.27 -  log :: "index \<Rightarrow> index \<Rightarrow> index"
    5.28 -where
    5.29 -  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    5.30 -
    5.31 -subsection {* Random seeds *}
    5.32 -
    5.33 -types seed = "index \<times> index"
    5.34 -
    5.35 -primrec
    5.36 -  "next" :: "seed \<Rightarrow> index \<times> seed"
    5.37 -where
    5.38 -  "next (v, w) = (let
    5.39 -     k =  v div 53668;
    5.40 -     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    5.41 -     l =  w div 52774;
    5.42 -     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    5.43 -     z =  minus_shift 2147483562 v' (w' + 1) + 1
    5.44 -   in (z, (v', w')))"
    5.45 -
    5.46 -lemma next_not_0:
    5.47 -  "fst (next s) \<noteq> 0"
    5.48 -apply (cases s)
    5.49 -apply (auto simp add: minus_shift_def Let_def)
    5.50 -done
    5.51 -
    5.52 -primrec
    5.53 -  seed_invariant :: "seed \<Rightarrow> bool"
    5.54 -where
    5.55 -  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    5.56 -
    5.57 -lemma if_same:
    5.58 -  "(if b then f x else f y) = f (if b then x else y)"
    5.59 -  by (cases b) simp_all
    5.60 -
    5.61 -definition
    5.62 -  split_seed :: "seed \<Rightarrow> seed \<times> seed"
    5.63 -where
    5.64 -  "split_seed s = (let
    5.65 -     (v, w) = s;
    5.66 -     (v', w') = snd (next s);
    5.67 -     v'' = inc_shift 2147483562 v;
    5.68 -     s'' = (v'', w');
    5.69 -     w'' = inc_shift 2147483398 w;
    5.70 -     s''' = (v', w'')
    5.71 -   in (s'', s'''))"
    5.72 -
    5.73 -
    5.74 -subsection {* Base selectors *}
    5.75 -
    5.76 -function
    5.77 -  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
    5.78 -where
    5.79 -  "range_aux k l s = (if k = 0 then (l, s) else
    5.80 -    let (v, s') = next s
    5.81 -  in range_aux (k - 1) (v + l * 2147483561) s')"
    5.82 -by pat_completeness auto
    5.83 -termination
    5.84 -  by (relation "measure (nat_of_index o fst)")
    5.85 -    (auto simp add: index)
    5.86 -
    5.87 -definition
    5.88 -  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
    5.89 -where
    5.90 -  "range k = (do
    5.91 -     v \<leftarrow> range_aux (log 2147483561 k) 1;
    5.92 -     return (v mod k)
    5.93 -   done)"
    5.94 -
    5.95 -lemma range:
    5.96 -  assumes "k > 0"
    5.97 -  shows "fst (range k s) < k"
    5.98 -proof -
    5.99 -  obtain v w where range_aux:
   5.100 -    "range_aux (log 2147483561 k) 1 s = (v, w)"
   5.101 -    by (cases "range_aux (log 2147483561 k) 1 s")
   5.102 -  with assms show ?thesis
   5.103 -    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
   5.104 -qed
   5.105 -
   5.106 -definition
   5.107 -  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   5.108 -where
   5.109 -  "select xs = (do
   5.110 -     k \<leftarrow> range (index_of_nat (length xs));
   5.111 -     return (nth xs (nat_of_index k))
   5.112 -   done)"
   5.113 -
   5.114 -lemma select:
   5.115 -  assumes "xs \<noteq> []"
   5.116 -  shows "fst (select xs s) \<in> set xs"
   5.117 -proof -
   5.118 -  from assms have "index_of_nat (length xs) > 0" by simp
   5.119 -  with range have
   5.120 -    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
   5.121 -  then have
   5.122 -    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
   5.123 -  then show ?thesis
   5.124 -    by (auto simp add: monad_collapse select_def)
   5.125 -qed
   5.126 -
   5.127 -definition
   5.128 -  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   5.129 -where
   5.130 -  [code del]: "select_default k x y = (do
   5.131 -     l \<leftarrow> range k;
   5.132 -     return (if l + 1 < k then x else y)
   5.133 -   done)"
   5.134 -
   5.135 -lemma select_default_zero:
   5.136 -  "fst (select_default 0 x y s) = y"
   5.137 -  by (simp add: monad_collapse select_default_def)
   5.138 -
   5.139 -lemma select_default_code [code]:
   5.140 -  "select_default k x y = (if k = 0 then do
   5.141 -     _ \<leftarrow> range 1;
   5.142 -     return y
   5.143 -   done else do
   5.144 -     l \<leftarrow> range k;
   5.145 -     return (if l + 1 < k then x else y)
   5.146 -   done)"
   5.147 -proof (cases "k = 0")
   5.148 -  case False then show ?thesis by (simp add: select_default_def)
   5.149 -next
   5.150 -  case True then show ?thesis
   5.151 -    by (simp add: monad_collapse select_default_def range_def)
   5.152 -qed
   5.153 -
   5.154 -
   5.155 -subsection {* @{text ML} interface *}
   5.156 -
   5.157 -ML {*
   5.158 -structure Random_Engine =
   5.159 -struct
   5.160 -
   5.161 -type seed = int * int;
   5.162 -
   5.163 -local
   5.164 -
   5.165 -val seed = ref 
   5.166 -  (let
   5.167 -    val now = Time.toMilliseconds (Time.now ());
   5.168 -    val (q, s1) = IntInf.divMod (now, 2147483562);
   5.169 -    val s2 = q mod 2147483398;
   5.170 -  in (s1 + 1, s2 + 1) end);
   5.171 -
   5.172 -in
   5.173 -
   5.174 -fun run f =
   5.175 -  let
   5.176 -    val (x, seed') = f (! seed);
   5.177 -    val _ = seed := seed'
   5.178 -  in x end;
   5.179 -
   5.180 -end;
   5.181 -
   5.182 -end;
   5.183 -*}
   5.184 -
   5.185 -end
   5.186 -