# HG changeset patch
# User haftmann
# Date 1233839642 -3600
# Node ID bebe5a254ba6e727be46f31a7f57e31db0d51530
# Parent  d201a838d0f7e16e7570899c97b0594483f3067f
moved Random.thy to Library

diff -r d201a838d0f7 -r bebe5a254ba6 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Extraction/Higman.thy	Thu Feb 05 14:14:02 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Extraction/Higman.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
                 Monika Seisenberger, LMU Muenchen
 *)
@@ -7,7 +6,7 @@
 header {* Higman's lemma *}
 
 theory Higman
-imports Main "~~/src/HOL/ex/Random"
+imports Main State_Monad Random
 begin
 
 text {*
diff -r d201a838d0f7 -r bebe5a254ba6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 05 14:14:02 2009 +0100
@@ -311,6 +311,7 @@
 
 HOL-Library: HOL $(LOG)/HOL-Library.gz
 
+
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/SetsAndFunctions.thy		\
   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
@@ -335,6 +336,7 @@
   Library/Mapping.thy	Library/Numeral_Type.thy	Library/Reflection.thy		\
   Library/Boolean_Algebra.thy Library/Countable.thy	\
   Library/RBT.thy	Library/Univ_Poly.thy	\
+  Library/Random.thy	Library/Quickcheck.thy	\
   Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
   Library/reify_data.ML Library/reflection.ML
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
@@ -814,7 +816,7 @@
   ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy ex/BT.thy	\
   ex/BinEx.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
   ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
-  ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
+  ex/Groebner_Examples.thy ex/Quickcheck_Generators.thy		\
   ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
   ex/CodegenSML_Test.thy ex/Formal_Power_Series_Examples.thy						\
   ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
diff -r d201a838d0f7 -r bebe5a254ba6 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Feb 04 18:10:07 2009 +0100
+++ b/src/HOL/Library/Library.thy	Thu Feb 05 14:14:02 2009 +0100
@@ -34,9 +34,11 @@
   Permutation
   Pocklington
   Primes
+  Quickcheck
   Quicksort
   Quotient
   Ramsey
+  Random
   Reflection
   RBT
   State_Monad
diff -r d201a838d0f7 -r bebe5a254ba6 src/HOL/Library/Random.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Random.thy	Thu Feb 05 14:14:02 2009 +0100
@@ -0,0 +1,182 @@
+(*  Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* A HOL random engine *}
+
+theory Random
+imports State_Monad Code_Index
+begin
+
+subsection {* Auxiliary functions *}
+
+definition
+  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
+where
+  "inc_shift v k = (if v = k then 1 else k + 1)"
+
+definition
+  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
+where
+  "minus_shift r k l = (if k < l then r + k - l else k - l)"
+
+fun
+  log :: "index \<Rightarrow> index \<Rightarrow> index"
+where
+  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
+
+subsection {* Random seeds *}
+
+types seed = "index \<times> index"
+
+primrec
+  "next" :: "seed \<Rightarrow> index \<times> seed"
+where
+  "next (v, w) = (let
+     k =  v div 53668;
+     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
+     l =  w div 52774;
+     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
+     z =  minus_shift 2147483562 v' (w' + 1) + 1
+   in (z, (v', w')))"
+
+lemma next_not_0:
+  "fst (next s) \<noteq> 0"
+apply (cases s)
+apply (auto simp add: minus_shift_def Let_def)
+done
+
+primrec
+  seed_invariant :: "seed \<Rightarrow> bool"
+where
+  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
+
+lemma if_same:
+  "(if b then f x else f y) = f (if b then x else y)"
+  by (cases b) simp_all
+
+definition
+  split_seed :: "seed \<Rightarrow> seed \<times> seed"
+where
+  "split_seed s = (let
+     (v, w) = s;
+     (v', w') = snd (next s);
+     v'' = inc_shift 2147483562 v;
+     s'' = (v'', w');
+     w'' = inc_shift 2147483398 w;
+     s''' = (v', w'')
+   in (s'', s'''))"
+
+
+subsection {* Base selectors *}
+
+function
+  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
+where
+  "range_aux k l s = (if k = 0 then (l, s) else
+    let (v, s') = next s
+  in range_aux (k - 1) (v + l * 2147483561) s')"
+by pat_completeness auto
+termination
+  by (relation "measure (nat_of_index o fst)")
+    (auto simp add: index)
+
+definition
+  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
+where
+  "range k = (do
+     v \<leftarrow> range_aux (log 2147483561 k) 1;
+     return (v mod k)
+   done)"
+
+lemma range:
+  assumes "k > 0"
+  shows "fst (range k s) < k"
+proof -
+  obtain v w where range_aux:
+    "range_aux (log 2147483561 k) 1 s = (v, w)"
+    by (cases "range_aux (log 2147483561 k) 1 s")
+  with assms show ?thesis
+    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
+qed
+
+definition
+  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+where
+  "select xs = (do
+     k \<leftarrow> range (index_of_nat (length xs));
+     return (nth xs (nat_of_index k))
+   done)"
+
+lemma select:
+  assumes "xs \<noteq> []"
+  shows "fst (select xs s) \<in> set xs"
+proof -
+  from assms have "index_of_nat (length xs) > 0" by simp
+  with range have
+    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
+  then have
+    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
+  then show ?thesis
+    by (auto simp add: monad_collapse select_def)
+qed
+
+definition
+  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
+where
+  [code del]: "select_default k x y = (do
+     l \<leftarrow> range k;
+     return (if l + 1 < k then x else y)
+   done)"
+
+lemma select_default_zero:
+  "fst (select_default 0 x y s) = y"
+  by (simp add: monad_collapse select_default_def)
+
+lemma select_default_code [code]:
+  "select_default k x y = (if k = 0 then do
+     _ \<leftarrow> range 1;
+     return y
+   done else do
+     l \<leftarrow> range k;
+     return (if l + 1 < k then x else y)
+   done)"
+proof (cases "k = 0")
+  case False then show ?thesis by (simp add: select_default_def)
+next
+  case True then show ?thesis
+    by (simp add: monad_collapse select_default_def range_def)
+qed
+
+
+subsection {* @{text ML} interface *}
+
+ML {*
+structure Random_Engine =
+struct
+
+type seed = int * int;
+
+local
+
+val seed = ref 
+  (let
+    val now = Time.toMilliseconds (Time.now ());
+    val (q, s1) = IntInf.divMod (now, 2147483562);
+    val s2 = q mod 2147483398;
+  in (s1 + 1, s2 + 1) end);
+
+in
+
+fun run f =
+  let
+    val (x, seed') = f (! seed);
+    val _ = seed := seed'
+  in x end;
+
+end;
+
+end;
+*}
+
+end
+
diff -r d201a838d0f7 -r bebe5a254ba6 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Wed Feb 04 18:10:07 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(*  ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* A HOL random engine *}
-
-theory Random
-imports State_Monad Code_Index
-begin
-
-subsection {* Auxiliary functions *}
-
-definition
-  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
-where
-  "inc_shift v k = (if v = k then 1 else k + 1)"
-
-definition
-  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
-where
-  "minus_shift r k l = (if k < l then r + k - l else k - l)"
-
-fun
-  log :: "index \<Rightarrow> index \<Rightarrow> index"
-where
-  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
-
-subsection {* Random seeds *}
-
-types seed = "index \<times> index"
-
-primrec
-  "next" :: "seed \<Rightarrow> index \<times> seed"
-where
-  "next (v, w) = (let
-     k =  v div 53668;
-     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
-     l =  w div 52774;
-     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
-     z =  minus_shift 2147483562 v' (w' + 1) + 1
-   in (z, (v', w')))"
-
-lemma next_not_0:
-  "fst (next s) \<noteq> 0"
-apply (cases s)
-apply (auto simp add: minus_shift_def Let_def)
-done
-
-primrec
-  seed_invariant :: "seed \<Rightarrow> bool"
-where
-  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
-
-lemma if_same:
-  "(if b then f x else f y) = f (if b then x else y)"
-  by (cases b) simp_all
-
-definition
-  split_seed :: "seed \<Rightarrow> seed \<times> seed"
-where
-  "split_seed s = (let
-     (v, w) = s;
-     (v', w') = snd (next s);
-     v'' = inc_shift 2147483562 v;
-     s'' = (v'', w');
-     w'' = inc_shift 2147483398 w;
-     s''' = (v', w'')
-   in (s'', s'''))"
-
-
-subsection {* Base selectors *}
-
-function
-  range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
-where
-  "range_aux k l s = (if k = 0 then (l, s) else
-    let (v, s') = next s
-  in range_aux (k - 1) (v + l * 2147483561) s')"
-by pat_completeness auto
-termination
-  by (relation "measure (nat_of_index o fst)")
-    (auto simp add: index)
-
-definition
-  range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
-where
-  "range k = (do
-     v \<leftarrow> range_aux (log 2147483561 k) 1;
-     return (v mod k)
-   done)"
-
-lemma range:
-  assumes "k > 0"
-  shows "fst (range k s) < k"
-proof -
-  obtain v w where range_aux:
-    "range_aux (log 2147483561 k) 1 s = (v, w)"
-    by (cases "range_aux (log 2147483561 k) 1 s")
-  with assms show ?thesis
-    by (simp add: monad_collapse range_def del: range_aux.simps log.simps)
-qed
-
-definition
-  select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
-where
-  "select xs = (do
-     k \<leftarrow> range (index_of_nat (length xs));
-     return (nth xs (nat_of_index k))
-   done)"
-
-lemma select:
-  assumes "xs \<noteq> []"
-  shows "fst (select xs s) \<in> set xs"
-proof -
-  from assms have "index_of_nat (length xs) > 0" by simp
-  with range have
-    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
-  then have
-    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
-  then show ?thesis
-    by (auto simp add: monad_collapse select_def)
-qed
-
-definition
-  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
-where
-  [code del]: "select_default k x y = (do
-     l \<leftarrow> range k;
-     return (if l + 1 < k then x else y)
-   done)"
-
-lemma select_default_zero:
-  "fst (select_default 0 x y s) = y"
-  by (simp add: monad_collapse select_default_def)
-
-lemma select_default_code [code]:
-  "select_default k x y = (if k = 0 then do
-     _ \<leftarrow> range 1;
-     return y
-   done else do
-     l \<leftarrow> range k;
-     return (if l + 1 < k then x else y)
-   done)"
-proof (cases "k = 0")
-  case False then show ?thesis by (simp add: select_default_def)
-next
-  case True then show ?thesis
-    by (simp add: monad_collapse select_default_def range_def)
-qed
-
-
-subsection {* @{text ML} interface *}
-
-ML {*
-structure Random_Engine =
-struct
-
-type seed = int * int;
-
-local
-
-val seed = ref 
-  (let
-    val now = Time.toMilliseconds (Time.now ());
-    val (q, s1) = IntInf.divMod (now, 2147483562);
-    val s2 = q mod 2147483398;
-  in (s1 + 1, s2 + 1) end);
-
-in
-
-fun run f =
-  let
-    val (x, seed') = f (! seed);
-    val _ = seed := seed'
-  in x end;
-
-end;
-
-end;
-*}
-
-end
-