merged
authorhaftmann
Sat, 16 May 2009 20:18:05 +0200
changeset 31187 7893975cc527
parent 31184 6dc73ea0dbc0 (diff)
parent 31168 138eae508556 (current diff)
child 31188 e5d01f8a916d
merged
--- a/src/HOL/Code_Eval.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Sat May 16 20:18:05 2009 +0200
@@ -28,6 +28,14 @@
 lemma term_of_anything: "term_of x \<equiv> t"
   by (rule eq_reflection) (cases "term_of x", cases t, simp)
 
+definition app :: "('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)
+  \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
+  "app f x = (fst f (fst x), \<lambda>u. Code_Eval.App (snd f ()) (snd x ()))"
+
+lemma app_code [code, code inline]:
+  "app (f, tf) (x, tx) = (f x, \<lambda>u. Code_Eval.App (tf ()) (tx ()))"
+  by (simp only: app_def fst_conv snd_conv)
+
 
 subsubsection {* @{text term_of} instances *}
 
@@ -135,6 +143,68 @@
 code_reserved Eval HOLogic
 
 
+subsubsection {* Syntax *}
+
+definition termify :: "'a \<Rightarrow> 'a \<times> (unit \<Rightarrow> term)" where
+  [code del]: "termify x = (x, \<lambda>u. dummy_term)"
+
+setup {*
+let
+  fun map_default f xs =
+    let val ys = map f xs
+    in if exists is_some ys
+      then SOME (map2 the_default xs ys)
+      else NONE
+    end;
+  fun subst_termify_app (Const (@{const_name termify}, T), [t]) =
+        if not (Term.has_abs t)
+        then if fold_aterms (fn Const _ => I | _ => K false) t true
+          then SOME (HOLogic.mk_prod
+            (t, Abs ("u", HOLogic.unitT, HOLogic.reflect_term t)))
+          else error "Cannot termify expression containing variables"
+        else error "Cannot termify expression containing abstraction"
+    | subst_termify_app (t, ts) = case map_default subst_termify ts
+       of SOME ts' => SOME (list_comb (t, ts'))
+        | NONE => NONE
+  and subst_termify (Abs (v, T, t)) = (case subst_termify t
+       of SOME t' => SOME (Abs (v, T, t'))
+        | NONE => NONE)
+    | subst_termify t = subst_termify_app (strip_comb t) 
+  fun check_termify ts ctxt = map_default subst_termify ts
+    |> Option.map (rpair ctxt)
+in
+  Context.theory_map (Syntax.add_term_check 0 "termify" check_termify)
+end;
+*}
+
+locale term_syntax
+begin
+
+notation app (infixl "<\<cdot>>" 70) and termify ("termify")
+
+end
+
+interpretation term_syntax .
+
+no_notation app (infixl "<\<cdot>>" 70) and termify ("termify")
+
+print_translation {*
+let
+  val term = Const ("<TERM>", dummyT);
+  fun tr1' [_, _] = term;
+  fun tr2' [] = term;
+in
+  [(@{const_syntax Const}, tr1'),
+    (@{const_syntax App}, tr1'),
+    (@{const_syntax dummy_term}, tr2')]
+end
+*}
+
+hide const dummy_term termify app
+hide (open) const Const App term_of
+
+
+
 subsection {* Evaluation setup *}
 
 ML {*
@@ -159,23 +229,4 @@
   Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
 *}
 
-
-subsubsection {* Syntax *}
-
-print_translation {*
-let
-  val term = Const ("<TERM>", dummyT);
-  fun tr1' [_, _] = term;
-  fun tr2' [] = term;
-in
-  [(@{const_syntax Const}, tr1'),
-    (@{const_syntax App}, tr1'),
-    (@{const_syntax dummy_term}, tr2')]
 end
-*}
-
-hide const dummy_term
-hide (open) const Const App
-hide (open) const term_of
-
-end
--- a/src/HOL/Complex_Main.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Complex_Main.thy	Sat May 16 20:18:05 2009 +0200
@@ -9,6 +9,7 @@
   Ln
   Taylor
   Integration
+  "Library/Quickcheck"
 begin
 
 end
--- a/src/HOL/Extraction/Higman.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Extraction/Higman.thy	Sat May 16 20:18:05 2009 +0200
@@ -349,9 +349,9 @@
 
 end
 
-function mk_word_aux :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word_aux k = (do
-     i \<leftarrow> range 10;
+     i \<leftarrow> Random.range 10;
      (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
      else do
        let l = (if i mod 2 = 0 then A else B);
@@ -362,10 +362,10 @@
 by pat_completeness auto
 termination by (relation "measure ((op -) 1001)") auto
 
-definition mk_word :: "seed \<Rightarrow> letter list \<times> seed" where
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word = mk_word_aux 0"
 
-primrec mk_word_s :: "nat \<Rightarrow> seed \<Rightarrow> letter list \<times> seed" where
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word_s 0 = mk_word"
   | "mk_word_s (Suc n) = (do
        _ \<leftarrow> mk_word;
--- a/src/HOL/IsaMakefile	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/IsaMakefile	Sat May 16 20:18:05 2009 +0200
@@ -851,7 +851,7 @@
   ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
-  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy	\
+  ex/Sudoku.thy ex/Tarski.thy \
   ex/Termination.thy ex/Unification.thy ex/document/root.bib		\
   ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \
   ex/Predicate_Compile.thy ex/predicate_compile.ML ex/Predicate_Compile_ex.thy
--- a/src/HOL/Library/Quickcheck.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Library/Quickcheck.thy	Sat May 16 20:18:05 2009 +0200
@@ -3,43 +3,22 @@
 header {* A simple counterexample generator *}
 
 theory Quickcheck
-imports Random Code_Eval Map
+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> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
-
-text {* Type @{typ "'a itself"} *}
-
-instantiation itself :: ("{type, typerep}") random
-begin
-
-definition
-  "random _ = Pair (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
-
-instance ..
-
-end
+  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
 
 
 subsection {* Quickcheck generator *}
 
 ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name Pair}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
-  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-end;
-
 structure Quickcheck =
 struct
 
@@ -58,24 +37,26 @@
     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> seed \<Rightarrow> term list option \<times> seed"};
+    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"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
+      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
     fun mk_scomp_split ty t t' =
-      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
+      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)
-    val t = fold_rev mk_bindclause bounds (return $ check);
-  in Abs ("n", @{typ index}, t) end;
+      (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 + 1) #>> (Option.map o map) proc) thy t' [];
+      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
   in f #> Random_Engine.run end;
 
 end
@@ -87,7 +68,35 @@
 *}
 
 
-subsection {* Type @{typ "'a \<Rightarrow> 'b"} *}
+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 =
@@ -123,10 +132,9 @@
 end
 *}
 
-axiomatization
-  random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
-    \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
-    \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
+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};
@@ -136,8 +144,8 @@
 instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
 begin
 
-definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
-  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
+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 ..
 
@@ -145,4 +153,80 @@
 
 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
--- a/src/HOL/Library/Random.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Library/Random.thy	Sat May 16 20:18:05 2009 +0200
@@ -87,6 +87,32 @@
     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))"
@@ -140,6 +166,10 @@
 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)
 
--- a/src/HOL/Nat_Numeral.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Sat May 16 20:18:05 2009 +0200
@@ -316,13 +316,13 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
-lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)
 
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
 by (simp add: nat_1 nat_number_of_def)
 
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
 by (simp add: nat_numeral_1_eq_1)
 
 
--- a/src/HOL/Tools/hologic.ML	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/Tools/hologic.ML	Sat May 16 20:18:05 2009 +0200
@@ -122,6 +122,8 @@
   val mk_typerep: typ -> term
   val mk_term_of: typ -> term -> term
   val reflect_term: term -> term
+  val mk_return: typ -> typ -> term -> term
+  val mk_ST: ((term * typ) * (string * typ) option)  list -> term -> typ -> typ option * typ -> term
 end;
 
 structure HOLogic: HOLOGIC =
@@ -612,8 +614,23 @@
   | reflect_term (t1 $ t2) =
       Const ("Code_Eval.App", termT --> termT --> termT)
         $ reflect_term t1 $ reflect_term t2
-  | reflect_term (t as Free _) = t
-  | reflect_term (t as Bound _) = t
-  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t);
+  | reflect_term (Abs (v, _, t)) = Abs (v, termT, reflect_term t)
+  | reflect_term t = t;
+
+
+(* open state monads *)
+
+fun mk_return T U x = pair_const T U $ x;
+
+fun mk_ST clauses t U (someT, V) =
+  let
+    val R = case someT of SOME T => mk_prodT (T, V) | NONE => V
+    fun mk_clause ((t, U), SOME (v, T)) (t', U') =
+          (Const ("Product_Type.scomp", (U --> mk_prodT (T, U')) --> (T --> U' --> R) --> U --> R)
+            $ t $ lambda (Free (v, T)) t', U)
+      | mk_clause ((t, U), NONE) (t', U') =
+          (Const ("Product_Type.fcomp", (U --> U') --> (U' --> R) --> U --> R)
+            $ t $ t', U)
+  in fold_rev mk_clause clauses (t, U) |> fst end;
 
 end;
--- a/src/HOL/ex/Quickcheck_Generators.thy	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy	Sat May 16 20:18:05 2009 +0200
@@ -8,27 +8,11 @@
 
 subsection {* Datatypes *}
 
-definition
-  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   "collapse f = (do g \<leftarrow> f; g done)"
 
-ML {*
-structure StateMonad =
-struct
-
-fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
-fun liftT' sT = sT --> sT;
-
-fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
-
-fun scomp T1 T2 sT f g = Const (@{const_name scomp},
-  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
-
-end;
-*}
-
 lemma random'_if:
-  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
+  fixes random' :: "index \<Rightarrow> index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   assumes "random' 0 j = (\<lambda>s. undefined)"
     and "\<And>i. random' (Suc_index i) j = rhs2 i"
   shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
@@ -36,15 +20,18 @@
 
 setup {*
 let
+  fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
+  fun scomp T1 T2 sT f g = Const (@{const_name scomp},
+    liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   exception REC of string;
   exception TYP of string;
   fun mk_collapse thy ty = Sign.mk_const thy
-    (@{const_name collapse}, [@{typ seed}, ty]);
+    (@{const_name collapse}, [@{typ Random.seed}, ty]);
   fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   fun mk_split thy ty ty' = Sign.mk_const thy
-    (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
+    (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT (term_ty ty') @{typ Random.seed}]);
   fun mk_scomp_split thy ty ty' t t' =
-    StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
+    scomp (term_ty ty) (term_ty ty') @{typ Random.seed} t
       (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
   fun mk_cons thy this_ty (c, args) =
     let
@@ -57,7 +44,7 @@
       val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term
         (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
         |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
-      val return = StateMonad.return (term_ty this_ty) @{typ seed}
+      val return = HOLogic.mk_return (term_ty this_ty) @{typ Random.seed}
         (HOLogic.mk_prod (c_t, t_t));
       val t = fold_rev (fn ((ty, _), random) =>
         mk_scomp_split thy ty this_ty random)
@@ -67,21 +54,21 @@
   fun mk_conss thy ty [] = NONE
     | mk_conss thy ty [(_, t)] = SOME t
     | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
-          (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
-            HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
+          (Sign.mk_const thy (@{const_name Random.select}, [liftT (term_ty ty) @{typ Random.seed}]) $
+            HOLogic.mk_list (liftT (term_ty ty) @{typ Random.seed}) (map snd ts)));
   fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
     let
       val SOME t_atom = mk_conss thy ty ts_atom;
     in case mk_conss thy ty ts_rec
      of SOME t_rec => mk_collapse thy (term_ty ty) $
-          (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
+          (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $
              @{term "i\<Colon>index"} $ t_rec $ t_atom)
       | NONE => t_atom
     end;
   fun mk_random_eqs thy vs tycos =
     let
       val this_ty = Type (hd tycos, map TFree vs);
-      val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
+      val this_ty' = liftT (term_ty this_ty) @{typ Random.seed};
       val random_name = Long_Name.base_name @{const_name random};
       val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
       fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
@@ -100,8 +87,8 @@
         |> (map o apsnd) (List.partition fst)
         |> map (mk_clauses thy this_ty)
       val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
-          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
-            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
+          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ Random.seed},
+            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))),
           (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
         ]))) rhss;
     in eqss end;
@@ -113,7 +100,7 @@
           val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
           val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
             (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
-               random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
+               random' $ @{term "max (i\<Colon>index) 1"} $ @{term "i\<Colon>index"})
           val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
             (fn thm => Context.mapping (Code.del_eqn thm) I));
           fun add_code simps lthy =
@@ -146,32 +133,15 @@
         end
     | random_inst tycos thy = raise REC
         ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
-  fun add_random_inst tycos thy = random_inst tycos thy
-     handle REC msg => (warning msg; thy)
-          | TYP msg => (warning msg; thy)
+  fun add_random_inst [@{type_name bool}] thy = thy
+    | add_random_inst [@{type_name nat}] thy = thy
+    | add_random_inst tycos thy = random_inst tycos thy
+        handle REC msg => (warning msg; thy)
+             | TYP msg => (warning msg; thy)
 in DatatypePackage.interpretation add_random_inst end
 *}
 
 
-subsection {* Type @{typ int} *}
-
-instantiation int :: random
-begin
-
-definition
-  "random n = (do
-     (b, _) \<leftarrow> random n;
-     (m, t) \<leftarrow> random n;
-     return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
-       else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
-         (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
-   done)"
-
-instance ..
-
-end
-
-
 subsection {* Examples *}
 
 theorem "map g (map f xs) = map (g o f) xs"
@@ -294,4 +264,8 @@
   quickcheck [generator = code]
   oops
 
+lemma "int (nat k) = k"
+  quickcheck [generator = code]
+  oops
+
 end
--- a/src/HOL/ex/ROOT.ML	Sat May 16 17:44:11 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Sat May 16 20:18:05 2009 +0200
@@ -11,7 +11,6 @@
   "Word",
   "Eval_Examples",
   "Quickcheck_Generators",
-  "Term_Of_Syntax",
   "Codegenerator",
   "Codegenerator_Pretty",
   "NormalForm",
--- a/src/HOL/ex/Term_Of_Syntax.thy	Sat May 16 17:44:11 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      HOL/ex/Term_Of_Syntax.thy
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-*)
-
-header {* Input syntax for term_of functions *}
-
-theory Term_Of_Syntax
-imports Code_Eval
-begin
-
-setup {*
-  Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
-  #> snd
-*}
-
-notation (output)
-  rterm_of ("\<guillemotleft>_\<guillemotright>")
-
-locale rterm_syntax =
-  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
-
-parse_translation {*
-let
-  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
-    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
-in
-  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
-end
-*}
-
-setup {*
-let
-  val subst_rterm_of = map_aterms
-    (fn Free (v, _) => error ("illegal free variable in term quotation: " ^ quote v) | t => t)
-      o HOLogic.reflect_term;
-  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
-    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
-        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
-    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
-  fun subst_rterm_of'' t = 
-    let
-      val t' = subst_rterm_of' (strip_comb t);
-    in if t aconv t'
-      then NONE
-      else SOME t'
-    end;
-  fun check_rterm_of ts ctxt =
-    let
-      val ts' = map subst_rterm_of'' ts;
-    in if exists is_some ts'
-      then SOME (map2 the_default ts ts', ctxt)
-      else NONE
-    end;
-in
-  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
-end;
-*}
-
-end