# HG changeset patch
# User haftmann
# Date 1242497909 -7200
# Node ID e5d01f8a916db1c71b905407a7409dd22bee0749
# Parent  7893975cc5273d9015ecfe4e1621da44f09290dc# Parent  b458b4ac570f979fa1993f093419b3bef8b0c2bb
merged

diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Code_Index.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Index.thy	Sat May 16 20:18:29 2009 +0200
@@ -0,0 +1,336 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Type of indices *}
+
+theory Code_Index
+imports Main
+begin
+
+text {*
+  Indices are isomorphic to HOL @{typ nat} but
+  mapped to target-language builtin integers.
+*}
+
+subsection {* Datatype of indices *}
+
+typedef (open) index = "UNIV \<Colon> nat set"
+  morphisms nat_of of_nat by rule
+
+lemma of_nat_nat_of [simp]:
+  "of_nat (nat_of k) = k"
+  by (rule nat_of_inverse)
+
+lemma nat_of_of_nat [simp]:
+  "nat_of (of_nat n) = n"
+  by (rule of_nat_inverse) (rule UNIV_I)
+
+lemma [measure_function]:
+  "is_measure nat_of" by (rule is_measure_trivial)
+
+lemma index:
+  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
+proof
+  fix n :: nat
+  assume "\<And>n\<Colon>index. PROP P n"
+  then show "PROP P (of_nat n)" .
+next
+  fix n :: index
+  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
+  then have "PROP P (of_nat (nat_of n))" .
+  then show "PROP P n" by simp
+qed
+
+lemma index_case:
+  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
+  shows P
+  by (rule assms [of "nat_of k"]) simp
+
+lemma index_induct_raw:
+  assumes "\<And>n. P (of_nat n)"
+  shows "P k"
+proof -
+  from assms have "P (of_nat (nat_of k))" .
+  then show ?thesis by simp
+qed
+
+lemma nat_of_inject [simp]:
+  "nat_of k = nat_of l \<longleftrightarrow> k = l"
+  by (rule nat_of_inject)
+
+lemma of_nat_inject [simp]:
+  "of_nat n = of_nat m \<longleftrightarrow> n = m"
+  by (rule of_nat_inject) (rule UNIV_I)+
+
+instantiation index :: zero
+begin
+
+definition [simp, code del]:
+  "0 = of_nat 0"
+
+instance ..
+
+end
+
+definition [simp]:
+  "Suc_index k = of_nat (Suc (nat_of k))"
+
+rep_datatype "0 \<Colon> index" Suc_index
+proof -
+  fix P :: "index \<Rightarrow> bool"
+  fix k :: index
+  assume "P 0" then have init: "P (of_nat 0)" by simp
+  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
+    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
+    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
+  from init step have "P (of_nat (nat_of k))"
+    by (induct "nat_of k") simp_all
+  then show "P k" by simp
+qed simp_all
+
+declare index_case [case_names nat, cases type: index]
+declare index.induct [case_names nat, induct type: index]
+
+lemma index_decr [termination_simp]:
+  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
+  by (cases k) simp
+
+lemma [simp, code]:
+  "index_size = nat_of"
+proof (rule ext)
+  fix k
+  have "index_size k = nat_size (nat_of k)"
+    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
+  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
+  finally show "index_size k = nat_of k" .
+qed
+
+lemma [simp, code]:
+  "size = nat_of"
+proof (rule ext)
+  fix k
+  show "size k = nat_of k"
+  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
+qed
+
+lemmas [code del] = index.recs index.cases
+
+lemma [code]:
+  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
+  by (cases k, cases l) (simp add: eq)
+
+lemma [code nbe]:
+  "eq_class.eq (k::index) k \<longleftrightarrow> True"
+  by (rule HOL.eq_refl)
+
+
+subsection {* Indices as datatype of ints *}
+
+instantiation index :: number
+begin
+
+definition
+  "number_of = of_nat o nat"
+
+instance ..
+
+end
+
+lemma nat_of_number [simp]:
+  "nat_of (number_of k) = number_of k"
+  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
+
+code_datatype "number_of \<Colon> int \<Rightarrow> index"
+
+
+subsection {* Basic arithmetic *}
+
+instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
+begin
+
+definition [simp, code del]:
+  "(1\<Colon>index) = of_nat 1"
+
+definition [simp, code del]:
+  "n + m = of_nat (nat_of n + nat_of m)"
+
+definition [simp, code del]:
+  "n - m = of_nat (nat_of n - nat_of m)"
+
+definition [simp, code del]:
+  "n * m = of_nat (nat_of n * nat_of m)"
+
+definition [simp, code del]:
+  "n div m = of_nat (nat_of n div nat_of m)"
+
+definition [simp, code del]:
+  "n mod m = of_nat (nat_of n mod nat_of m)"
+
+definition [simp, code del]:
+  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
+
+definition [simp, code del]:
+  "n < m \<longleftrightarrow> nat_of n < nat_of m"
+
+instance proof
+qed (auto simp add: index left_distrib div_mult_self1)
+
+end
+
+lemma zero_index_code [code inline, code]:
+  "(0\<Colon>index) = Numeral0"
+  by (simp add: number_of_index_def Pls_def)
+lemma [code post]: "Numeral0 = (0\<Colon>index)"
+  using zero_index_code ..
+
+lemma one_index_code [code inline, code]:
+  "(1\<Colon>index) = Numeral1"
+  by (simp add: number_of_index_def Pls_def Bit1_def)
+lemma [code post]: "Numeral1 = (1\<Colon>index)"
+  using one_index_code ..
+
+lemma plus_index_code [code nbe]:
+  "of_nat n + of_nat m = of_nat (n + m)"
+  by simp
+
+definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
+  [simp, code del]: "subtract_index = op -"
+
+lemma subtract_index_code [code nbe]:
+  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
+  by simp
+
+lemma minus_index_code [code]:
+  "n - m = subtract_index n m"
+  by simp
+
+lemma times_index_code [code nbe]:
+  "of_nat n * of_nat m = of_nat (n * m)"
+  by simp
+
+lemma less_eq_index_code [code nbe]:
+  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
+  by simp
+
+lemma less_index_code [code nbe]:
+  "of_nat n < of_nat m \<longleftrightarrow> n < m"
+  by simp
+
+lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
+
+lemma of_nat_code [code]:
+  "of_nat = Nat.of_nat"
+proof
+  fix n :: nat
+  have "Nat.of_nat n = of_nat n"
+    by (induct n) simp_all
+  then show "of_nat n = Nat.of_nat n"
+    by (rule sym)
+qed
+
+lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
+  by (cases i) auto
+
+definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
+  "nat_of_aux i n = nat_of i + n"
+
+lemma nat_of_aux_code [code]:
+  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
+  by (auto simp add: nat_of_aux_def index_not_eq_zero)
+
+lemma nat_of_code [code]:
+  "nat_of i = nat_of_aux i 0"
+  by (simp add: nat_of_aux_def)
+
+definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
+  [code del]: "div_mod_index n m = (n div m, n mod m)"
+
+lemma [code]:
+  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
+  unfolding div_mod_index_def by auto
+
+lemma [code]:
+  "n div m = fst (div_mod_index n m)"
+  unfolding div_mod_index_def by simp
+
+lemma [code]:
+  "n mod m = snd (div_mod_index n m)"
+  unfolding div_mod_index_def by simp
+
+hide (open) const of_nat nat_of
+
+subsection {* ML interface *}
+
+ML {*
+structure Index =
+struct
+
+fun mk k = HOLogic.mk_number @{typ index} k;
+
+end;
+*}
+
+
+subsection {* Code generator setup *}
+
+text {* Implementation of indices by bounded integers *}
+
+code_type index
+  (SML "int")
+  (OCaml "int")
+  (Haskell "Int")
+
+code_instance index :: eq
+  (Haskell -)
+
+setup {*
+  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
+    false false) ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML Int int
+code_reserved OCaml Pervasives int
+
+code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+  (SML "Int.+/ ((_),/ (_))")
+  (OCaml "Pervasives.( + )")
+  (Haskell infixl 6 "+")
+
+code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
+  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
+  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+
+code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
+  (SML "Int.*/ ((_),/ (_))")
+  (OCaml "Pervasives.( * )")
+  (Haskell infixl 7 "*")
+
+code_const div_mod_index
+  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
+  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
+  (Haskell "divMod")
+
+code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+  (SML "!((_ : Int.int) = _)")
+  (OCaml "!((_ : int) = _)")
+  (Haskell infixl 4 "==")
+
+code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+  (SML "Int.<=/ ((_),/ (_))")
+  (OCaml "!((_ : int) <= _)")
+  (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
+  (SML "Int.</ ((_),/ (_))")
+  (OCaml "!((_ : int) < _)")
+  (Haskell infix 4 "<")
+
+text {* Evaluation *}
+
+lemma [code, code del]:
+  "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
+
+code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
+  (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
+
+end
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Sat May 16 20:18:05 2009 +0200
+++ b/src/HOL/Complex_Main.thy	Sat May 16 20:18:29 2009 +0200
@@ -9,7 +9,7 @@
   Ln
   Taylor
   Integration
-  "Library/Quickcheck"
+  Quickcheck
 begin
 
 end
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat May 16 20:18:05 2009 +0200
+++ b/src/HOL/IsaMakefile	Sat May 16 20:18:29 2009 +0200
@@ -206,6 +206,7 @@
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   ATP_Linkup.thy \
   Code_Eval.thy \
+  Code_Index.thy \
   Equiv_Relations.thy \
   Groebner_Basis.thy \
   Hilbert_Choice.thy \
@@ -286,8 +287,10 @@
   Transcendental.thy \
   GCD.thy \
   Parity.thy \
+  Quickcheck.thy \
   Lubs.thy \
   PReal.thy \
+  Random.thy \
   Rational.thy \
   RComplete.thy \
   RealDef.thy \
@@ -333,12 +336,11 @@
   Library/comm_ring.ML Library/Coinductive_List.thy			\
   Library/AssocList.thy	Library/Formal_Power_Series.thy	\
   Library/Binomial.thy Library/Eval_Witness.thy				\
-  Library/Code_Index.thy Library/Code_Char.thy				\
+  Library/Code_Char.thy				\
   Library/Code_Char_chr.thy Library/Code_Integer.thy			\
   Library/Mapping.thy Library/Numeral_Type.thy Library/Reflection.thy	\
   Library/Boolean_Algebra.thy Library/Countable.thy			\
   Library/Diagonalize.thy Library/RBT.thy Library/Univ_Poly.thy		\
-  Library/Random.thy Library/Quickcheck.thy	\
   Library/Poly_Deriv.thy \
   Library/Polynomial.thy \
   Library/Preorder.thy \
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Sat May 16 20:18:05 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Type of indices *}
-
-theory Code_Index
-imports Main
-begin
-
-text {*
-  Indices are isomorphic to HOL @{typ nat} but
-  mapped to target-language builtin integers.
-*}
-
-subsection {* Datatype of indices *}
-
-typedef (open) index = "UNIV \<Colon> nat set"
-  morphisms nat_of of_nat by rule
-
-lemma of_nat_nat_of [simp]:
-  "of_nat (nat_of k) = k"
-  by (rule nat_of_inverse)
-
-lemma nat_of_of_nat [simp]:
-  "nat_of (of_nat n) = n"
-  by (rule of_nat_inverse) (rule UNIV_I)
-
-lemma [measure_function]:
-  "is_measure nat_of" by (rule is_measure_trivial)
-
-lemma index:
-  "(\<And>n\<Colon>index. PROP P n) \<equiv> (\<And>n\<Colon>nat. PROP P (of_nat n))"
-proof
-  fix n :: nat
-  assume "\<And>n\<Colon>index. PROP P n"
-  then show "PROP P (of_nat n)" .
-next
-  fix n :: index
-  assume "\<And>n\<Colon>nat. PROP P (of_nat n)"
-  then have "PROP P (of_nat (nat_of n))" .
-  then show "PROP P n" by simp
-qed
-
-lemma index_case:
-  assumes "\<And>n. k = of_nat n \<Longrightarrow> P"
-  shows P
-  by (rule assms [of "nat_of k"]) simp
-
-lemma index_induct_raw:
-  assumes "\<And>n. P (of_nat n)"
-  shows "P k"
-proof -
-  from assms have "P (of_nat (nat_of k))" .
-  then show ?thesis by simp
-qed
-
-lemma nat_of_inject [simp]:
-  "nat_of k = nat_of l \<longleftrightarrow> k = l"
-  by (rule nat_of_inject)
-
-lemma of_nat_inject [simp]:
-  "of_nat n = of_nat m \<longleftrightarrow> n = m"
-  by (rule of_nat_inject) (rule UNIV_I)+
-
-instantiation index :: zero
-begin
-
-definition [simp, code del]:
-  "0 = of_nat 0"
-
-instance ..
-
-end
-
-definition [simp]:
-  "Suc_index k = of_nat (Suc (nat_of k))"
-
-rep_datatype "0 \<Colon> index" Suc_index
-proof -
-  fix P :: "index \<Rightarrow> bool"
-  fix k :: index
-  assume "P 0" then have init: "P (of_nat 0)" by simp
-  assume "\<And>k. P k \<Longrightarrow> P (Suc_index k)"
-    then have "\<And>n. P (of_nat n) \<Longrightarrow> P (Suc_index (of_nat n))" .
-    then have step: "\<And>n. P (of_nat n) \<Longrightarrow> P (of_nat (Suc n))" by simp
-  from init step have "P (of_nat (nat_of k))"
-    by (induct "nat_of k") simp_all
-  then show "P k" by simp
-qed simp_all
-
-declare index_case [case_names nat, cases type: index]
-declare index.induct [case_names nat, induct type: index]
-
-lemma index_decr [termination_simp]:
-  "k \<noteq> Code_Index.of_nat 0 \<Longrightarrow> Code_Index.nat_of k - Suc 0 < Code_Index.nat_of k"
-  by (cases k) simp
-
-lemma [simp, code]:
-  "index_size = nat_of"
-proof (rule ext)
-  fix k
-  have "index_size k = nat_size (nat_of k)"
-    by (induct k rule: index.induct) (simp_all del: zero_index_def Suc_index_def, simp_all)
-  also have "nat_size (nat_of k) = nat_of k" by (induct "nat_of k") simp_all
-  finally show "index_size k = nat_of k" .
-qed
-
-lemma [simp, code]:
-  "size = nat_of"
-proof (rule ext)
-  fix k
-  show "size k = nat_of k"
-  by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
-qed
-
-lemmas [code del] = index.recs index.cases
-
-lemma [code]:
-  "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of k) (nat_of l)"
-  by (cases k, cases l) (simp add: eq)
-
-lemma [code nbe]:
-  "eq_class.eq (k::index) k \<longleftrightarrow> True"
-  by (rule HOL.eq_refl)
-
-
-subsection {* Indices as datatype of ints *}
-
-instantiation index :: number
-begin
-
-definition
-  "number_of = of_nat o nat"
-
-instance ..
-
-end
-
-lemma nat_of_number [simp]:
-  "nat_of (number_of k) = number_of k"
-  by (simp add: number_of_index_def nat_number_of_def number_of_is_id)
-
-code_datatype "number_of \<Colon> int \<Rightarrow> index"
-
-
-subsection {* Basic arithmetic *}
-
-instantiation index :: "{minus, ordered_semidom, semiring_div, linorder}"
-begin
-
-definition [simp, code del]:
-  "(1\<Colon>index) = of_nat 1"
-
-definition [simp, code del]:
-  "n + m = of_nat (nat_of n + nat_of m)"
-
-definition [simp, code del]:
-  "n - m = of_nat (nat_of n - nat_of m)"
-
-definition [simp, code del]:
-  "n * m = of_nat (nat_of n * nat_of m)"
-
-definition [simp, code del]:
-  "n div m = of_nat (nat_of n div nat_of m)"
-
-definition [simp, code del]:
-  "n mod m = of_nat (nat_of n mod nat_of m)"
-
-definition [simp, code del]:
-  "n \<le> m \<longleftrightarrow> nat_of n \<le> nat_of m"
-
-definition [simp, code del]:
-  "n < m \<longleftrightarrow> nat_of n < nat_of m"
-
-instance proof
-qed (auto simp add: index left_distrib div_mult_self1)
-
-end
-
-lemma zero_index_code [code inline, code]:
-  "(0\<Colon>index) = Numeral0"
-  by (simp add: number_of_index_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>index)"
-  using zero_index_code ..
-
-lemma one_index_code [code inline, code]:
-  "(1\<Colon>index) = Numeral1"
-  by (simp add: number_of_index_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>index)"
-  using one_index_code ..
-
-lemma plus_index_code [code nbe]:
-  "of_nat n + of_nat m = of_nat (n + m)"
-  by simp
-
-definition subtract_index :: "index \<Rightarrow> index \<Rightarrow> index" where
-  [simp, code del]: "subtract_index = op -"
-
-lemma subtract_index_code [code nbe]:
-  "subtract_index (of_nat n) (of_nat m) = of_nat (n - m)"
-  by simp
-
-lemma minus_index_code [code]:
-  "n - m = subtract_index n m"
-  by simp
-
-lemma times_index_code [code nbe]:
-  "of_nat n * of_nat m = of_nat (n * m)"
-  by simp
-
-lemma less_eq_index_code [code nbe]:
-  "of_nat n \<le> of_nat m \<longleftrightarrow> n \<le> m"
-  by simp
-
-lemma less_index_code [code nbe]:
-  "of_nat n < of_nat m \<longleftrightarrow> n < m"
-  by simp
-
-lemma Suc_index_minus_one: "Suc_index n - 1 = n" by simp
-
-lemma of_nat_code [code]:
-  "of_nat = Nat.of_nat"
-proof
-  fix n :: nat
-  have "Nat.of_nat n = of_nat n"
-    by (induct n) simp_all
-  then show "of_nat n = Nat.of_nat n"
-    by (rule sym)
-qed
-
-lemma index_not_eq_zero: "i \<noteq> of_nat 0 \<longleftrightarrow> i \<ge> 1"
-  by (cases i) auto
-
-definition nat_of_aux :: "index \<Rightarrow> nat \<Rightarrow> nat" where
-  "nat_of_aux i n = nat_of i + n"
-
-lemma nat_of_aux_code [code]:
-  "nat_of_aux i n = (if i = 0 then n else nat_of_aux (i - 1) (Suc n))"
-  by (auto simp add: nat_of_aux_def index_not_eq_zero)
-
-lemma nat_of_code [code]:
-  "nat_of i = nat_of_aux i 0"
-  by (simp add: nat_of_aux_def)
-
-definition div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index" where
-  [code del]: "div_mod_index n m = (n div m, n mod m)"
-
-lemma [code]:
-  "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
-  unfolding div_mod_index_def by auto
-
-lemma [code]:
-  "n div m = fst (div_mod_index n m)"
-  unfolding div_mod_index_def by simp
-
-lemma [code]:
-  "n mod m = snd (div_mod_index n m)"
-  unfolding div_mod_index_def by simp
-
-hide (open) const of_nat nat_of
-
-subsection {* ML interface *}
-
-ML {*
-structure Index =
-struct
-
-fun mk k = HOLogic.mk_number @{typ index} k;
-
-end;
-*}
-
-
-subsection {* Code generator setup *}
-
-text {* Implementation of indices by bounded integers *}
-
-code_type index
-  (SML "int")
-  (OCaml "int")
-  (Haskell "Int")
-
-code_instance index :: eq
-  (Haskell -)
-
-setup {*
-  fold (Numeral.add_code @{const_name number_index_inst.number_of_index}
-    false false) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML Int int
-code_reserved OCaml Pervasives int
-
-code_const "op + \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.+/ ((_),/ (_))")
-  (OCaml "Pervasives.( + )")
-  (Haskell infixl 6 "+")
-
-code_const "subtract_index \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.max/ (_/ -/ _,/ 0 : int)")
-  (OCaml "Pervasives.max/ (_/ -/ _)/ (0 : int) ")
-  (Haskell "max/ (_/ -/ _)/ (0 :: Int)")
-
-code_const "op * \<Colon> index \<Rightarrow> index \<Rightarrow> index"
-  (SML "Int.*/ ((_),/ (_))")
-  (OCaml "Pervasives.( * )")
-  (Haskell infixl 7 "*")
-
-code_const div_mod_index
-  (SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
-  (OCaml "(fun n -> fun m ->/ if m = 0/ then (0, n) else/ (n '/ m, n mod m))")
-  (Haskell "divMod")
-
-code_const "eq_class.eq \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "!((_ : Int.int) = _)")
-  (OCaml "!((_ : int) = _)")
-  (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.<=/ ((_),/ (_))")
-  (OCaml "!((_ : int) <= _)")
-  (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> index \<Rightarrow> index \<Rightarrow> bool"
-  (SML "Int.</ ((_),/ (_))")
-  (OCaml "!((_ : int) < _)")
-  (Haskell infix 4 "<")
-
-text {* Evaluation *}
-
-lemma [code, code del]:
-  "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
-
-code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
-  (SML "HOLogic.mk'_number/ HOLogic.indexT/ (IntInf.fromInt/ _)")
-
-end
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sat May 16 20:18:05 2009 +0200
+++ b/src/HOL/Library/Library.thy	Sat May 16 20:18:29 2009 +0200
@@ -9,7 +9,6 @@
   Boolean_Algebra
   Char_ord
   Code_Char_chr
-  Code_Index
   Code_Integer
   Coinductive_List
   Commutative_Ring
@@ -45,11 +44,9 @@
   Preorder
   Primes
   Product_Vector
-  Quickcheck
   Quicksort
   Quotient
   Ramsey
-  Random
   Reflection
   RBT
   State_Monad
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Library/Quickcheck.thy
--- a/src/HOL/Library/Quickcheck.thy	Sat May 16 20:18:05 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A simple counterexample generator *}
-
-theory Quickcheck
-imports Main Real Random
-begin
-
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
-
-
-subsection {* The @{text random} class *}
-
-class random = typerep +
-  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-
-subsection {* Quickcheck generator *}
-
-ML {*
-structure Quickcheck =
-struct
-
-open Quickcheck;
-
-val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
-
-val target = "Quickcheck";
-
-fun mk_generator_expr thy prop tys =
-  let
-    val bound_max = length tys - 1;
-    val bounds = map_index (fn (i, ty) =>
-      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
-    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
-    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
-    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
-      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
-    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
-    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
-    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
-      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-    fun mk_split ty = Sign.mk_const thy
-      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
-    fun mk_scomp_split ty t t' =
-      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
-        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
-    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
-      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
-  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
-
-fun compile_generator_expr thy t =
-  let
-    val tys = (map snd o fst o strip_abs) t;
-    val t' = mk_generator_expr thy t tys;
-    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
-      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
-  in f #> Random_Engine.run end;
-
-end
-*}
-
-setup {*
-  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
-  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
-*}
-
-
-subsection {* Fundamental types*}
-
-definition (in term_syntax)
-  "termify_bool b = (if b then termify True else termify False)"
-
-instantiation bool :: random
-begin
-
-definition
-  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
-
-instance ..
-
-end
-
-definition (in term_syntax)
-  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
-
-instantiation itself :: (typerep) random
-begin
-
-definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
-  "random_itself _ = Pair (termify_itself TYPE('a))"
-
-instance ..
-
-end
-
-text {* Type @{typ "'a \<Rightarrow> 'b"} *}
-
-ML {*
-structure Random_Engine =
-struct
-
-open Random_Engine;
-
-fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
-    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
-    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
-    (seed : Random_Engine.seed) =
-  let
-    val (seed', seed'') = random_split seed;
-    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
-    val fun_upd = Const (@{const_name fun_upd},
-      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
-    fun random_fun' x =
-      let
-        val (seed, fun_map, f_t) = ! state;
-      in case AList.lookup (uncurry eq) fun_map x
-       of SOME y => y
-        | NONE => let
-              val t1 = term_of x;
-              val ((y, t2), seed') = random seed;
-              val fun_map' = (x, y) :: fun_map;
-              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
-              val _ = state := (seed', fun_map', f_t');
-            in y end
-      end;
-    fun term_fun' () = #3 (! state);
-  in ((random_fun', term_fun'), seed'') end;
-
-end
-*}
-
-axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
-  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
-  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-
-code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
-  -- {* With enough criminal energy this can be abused to derive @{prop False};
-  for this reason we use a distinguished target @{text Quickcheck}
-  not spoiling the regular trusted code generation *}
-
-instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
-begin
-
-definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
-  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
-
-instance ..
-
-end
-
-code_reserved Quickcheck Random_Engine
-
-
-subsection {* Numeric types *}
-
-function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
-  "termify_numeral k = (if k = 0 then termify Int.Pls
-    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
-  by pat_completeness auto
-
-declare (in term_syntax) termify_numeral.psimps [simp del]
-
-termination termify_numeral by (relation "measure Code_Index.nat_of")
-  (simp_all add: index)
-
-definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
-  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
-
-definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
-  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
-
-declare termify_nat_number_def [simplified snd_conv, code]
-
-instantiation nat :: random
-begin
-
-definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
-  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
-
-instance ..
-
-end
-
-definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
-  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
-
-instantiation int :: random
-begin
-
-definition
-  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
-     then let j = k - i in termify_int_number j
-     else let j = i - k in term_uminus (termify_int_number j)))"
-
-instance ..
-
-end
-
-definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
-  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
-
-instantiation rat :: random
-begin
-
-definition
-  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
-
-instance ..
-
-end
-
-definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
-  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
-
-instantiation real :: random
-begin
-
-definition
-  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
-
-instance ..
-
-end
-
-
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
-
-end
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Library/Random.thy
--- a/src/HOL/Library/Random.thy	Sat May 16 20:18:05 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,177 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* A HOL random engine *}
-
-theory Random
-imports Code_Index
-begin
-
-notation fcomp (infixl "o>" 60)
-notation scomp (infixl "o\<rightarrow>" 60)
-
-
-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"
-  by (cases s) (auto simp add: minus_shift_def Let_def)
-
-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 *}
-
-fun iterate :: "index \<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 o\<rightarrow> iterate (k - 1) f)"
-
-definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
-  "range k = iterate (log 2147483561 k)
-      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
-    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
-
-lemma range:
-  "k > 0 \<Longrightarrow> fst (range k s) < k"
-  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
-
-definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  "select xs = range (Code_Index.of_nat (length xs))
-    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
-     
-lemma select:
-  assumes "xs \<noteq> []"
-  shows "fst (select xs s) \<in> set xs"
-proof -
-  from assms have "Code_Index.of_nat (length xs) > 0" by simp
-  with range have
-    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
-  then have
-    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
-  then show ?thesis
-    by (simp add: scomp_apply split_beta select_def)
-qed
-
-primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
-  "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
-
-lemma pick_member:
-  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
-  by (induct xs arbitrary: i) simp_all
-
-lemma pick_drop_zero:
-  "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
-  by (induct xs) (auto simp add: expand_fun_eq)
-
-definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  "select_weight xs = range (listsum (map fst xs))
-   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
-
-lemma select_weight_member:
-  assumes "0 < listsum (map fst xs)"
-  shows "fst (select_weight xs s) \<in> set (map snd xs)"
-proof -
-  from range assms
-    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
-  with pick_member
-    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
-  then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
-qed
-
-definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
-  [code del]: "select_default k x y = range k
-     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
-
-lemma select_default_zero:
-  "fst (select_default 0 x y s) = y"
-  by (simp add: scomp_apply split_beta select_default_def)
-
-lemma select_default_code [code]:
-  "select_default k x y = (if k = 0
-    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
-    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
-proof
-  fix s
-  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
-    by (simp add: range_def scomp_Pair scomp_apply split_beta)
-  then show "select_default k x y s = (if k = 0
-    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
-    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
-    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
-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;
-*}
-
-hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
-  iterate range select pick select_weight select_default
-
-no_notation fcomp (infixl "o>" 60)
-no_notation scomp (infixl "o\<rightarrow>" 60)
-
-end
-
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Quickcheck.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck.thy	Sat May 16 20:18:29 2009 +0200
@@ -0,0 +1,232 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A simple counterexample generator *}
+
+theory Quickcheck
+imports Main Real Random
+begin
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+
+subsection {* The @{text random} class *}
+
+class random = typerep +
+  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+
+subsection {* Quickcheck generator *}
+
+ML {*
+structure Quickcheck =
+struct
+
+open Quickcheck;
+
+val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
+
+val target = "Quickcheck";
+
+fun mk_generator_expr thy prop tys =
+  let
+    val bound_max = length tys - 1;
+    val bounds = map_index (fn (i, ty) =>
+      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
+    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
+    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
+      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
+    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
+    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
+    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
+      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
+    fun mk_split ty = Sign.mk_const thy
+      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+    fun mk_scomp_split ty t t' =
+      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
+        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
+    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
+      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
+  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
+
+fun compile_generator_expr thy t =
+  let
+    val tys = (map snd o fst o strip_abs) t;
+    val t' = mk_generator_expr thy t tys;
+    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
+      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+  in f #> Random_Engine.run end;
+
+end
+*}
+
+setup {*
+  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
+  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
+*}
+
+
+subsection {* Fundamental types*}
+
+definition (in term_syntax)
+  "termify_bool b = (if b then termify True else termify False)"
+
+instantiation bool :: random
+begin
+
+definition
+  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
+
+instance ..
+
+end
+
+definition (in term_syntax)
+  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
+
+instantiation itself :: (typerep) random
+begin
+
+definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+  "random_itself _ = Pair (termify_itself TYPE('a))"
+
+instance ..
+
+end
+
+text {* Type @{typ "'a \<Rightarrow> 'b"} *}
+
+ML {*
+structure Random_Engine =
+struct
+
+open Random_Engine;
+
+fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
+    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
+    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
+    (seed : Random_Engine.seed) =
+  let
+    val (seed', seed'') = random_split seed;
+    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
+    val fun_upd = Const (@{const_name fun_upd},
+      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
+    fun random_fun' x =
+      let
+        val (seed, fun_map, f_t) = ! state;
+      in case AList.lookup (uncurry eq) fun_map x
+       of SOME y => y
+        | NONE => let
+              val t1 = term_of x;
+              val ((y, t2), seed') = random seed;
+              val fun_map' = (x, y) :: fun_map;
+              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
+              val _ = state := (seed', fun_map', f_t');
+            in y end
+      end;
+    fun term_fun' () = #3 (! state);
+  in ((random_fun', term_fun'), seed'') end;
+
+end
+*}
+
+axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
+  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
+  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
+
+code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
+  -- {* With enough criminal energy this can be abused to derive @{prop False};
+  for this reason we use a distinguished target @{text Quickcheck}
+  not spoiling the regular trusted code generation *}
+
+instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
+begin
+
+definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
+
+instance ..
+
+end
+
+code_reserved Quickcheck Random_Engine
+
+
+subsection {* Numeric types *}
+
+function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
+  "termify_numeral k = (if k = 0 then termify Int.Pls
+    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
+  by pat_completeness auto
+
+declare (in term_syntax) termify_numeral.psimps [simp del]
+
+termination termify_numeral by (relation "measure Code_Index.nat_of")
+  (simp_all add: index)
+
+definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
+  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
+
+definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
+  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
+
+declare termify_nat_number_def [simplified snd_conv, code]
+
+instantiation nat :: random
+begin
+
+definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
+
+instance ..
+
+end
+
+definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
+  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
+
+instantiation int :: random
+begin
+
+definition
+  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
+     then let j = k - i in termify_int_number j
+     else let j = i - k in term_uminus (termify_int_number j)))"
+
+instance ..
+
+end
+
+definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
+  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
+
+instantiation rat :: random
+begin
+
+definition
+  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
+
+instance ..
+
+end
+
+definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
+  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
+
+instantiation real :: random
+begin
+
+definition
+  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
+
+instance ..
+
+end
+
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
+end
diff -r 7893975cc527 -r e5d01f8a916d src/HOL/Random.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Random.thy	Sat May 16 20:18:29 2009 +0200
@@ -0,0 +1,177 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* A HOL random engine *}
+
+theory Random
+imports Code_Index
+begin
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+
+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"
+  by (cases s) (auto simp add: minus_shift_def Let_def)
+
+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 *}
+
+fun iterate :: "index \<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 o\<rightarrow> iterate (k - 1) f)"
+
+definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+  "range k = iterate (log 2147483561 k)
+      (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
+    o\<rightarrow> (\<lambda>v. Pair (v mod k))"
+
+lemma range:
+  "k > 0 \<Longrightarrow> fst (range k s) < k"
+  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
+
+definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+  "select xs = range (Code_Index.of_nat (length xs))
+    o\<rightarrow> (\<lambda>k. Pair (nth xs (Code_Index.nat_of k)))"
+     
+lemma select:
+  assumes "xs \<noteq> []"
+  shows "fst (select xs s) \<in> set xs"
+proof -
+  from assms have "Code_Index.of_nat (length xs) > 0" by simp
+  with range have
+    "fst (range (Code_Index.of_nat (length xs)) s) < Code_Index.of_nat (length xs)" by best
+  then have
+    "Code_Index.nat_of (fst (range (Code_Index.of_nat (length xs)) s)) < length xs" by simp
+  then show ?thesis
+    by (simp add: scomp_apply split_beta select_def)
+qed
+
+primrec pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a" where
+  "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"
+
+lemma pick_member:
+  "i < listsum (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
+  by (induct xs arbitrary: i) simp_all
+
+lemma pick_drop_zero:
+  "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
+  by (induct xs) (auto simp add: expand_fun_eq)
+
+definition select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+  "select_weight xs = range (listsum (map fst xs))
+   o\<rightarrow> (\<lambda>k. Pair (pick xs k))"
+
+lemma select_weight_member:
+  assumes "0 < listsum (map fst xs)"
+  shows "fst (select_weight xs s) \<in> set (map snd xs)"
+proof -
+  from range assms
+    have "fst (range (listsum (map fst xs)) s) < listsum (map fst xs)" .
+  with pick_member
+    have "pick xs (fst (range (listsum (map fst xs)) s)) \<in> set (map snd xs)" .
+  then show ?thesis by (simp add: select_weight_def scomp_def split_def) 
+qed
+
+definition select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
+  [code del]: "select_default k x y = range k
+     o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))"
+
+lemma select_default_zero:
+  "fst (select_default 0 x y s) = y"
+  by (simp add: scomp_apply split_beta select_default_def)
+
+lemma select_default_code [code]:
+  "select_default k x y = (if k = 0
+    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
+    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y)))"
+proof
+  fix s
+  have "snd (range (Code_Index.of_nat 0) s) = snd (range (Code_Index.of_nat 1) s)"
+    by (simp add: range_def scomp_Pair scomp_apply split_beta)
+  then show "select_default k x y s = (if k = 0
+    then range 1 o\<rightarrow> (\<lambda>_. Pair y)
+    else range k o\<rightarrow> (\<lambda>l. Pair (if l + 1 < k then x else y))) s"
+    by (cases "k = 0") (simp_all add: select_default_def scomp_apply split_beta)
+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;
+*}
+
+hide (open) type seed
+hide (open) const inc_shift minus_shift log "next" seed_invariant split_seed
+  iterate range select pick select_weight select_default
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
+end
+