# HG changeset patch
# User haftmann
# Date 1242398359 -7200
# Node ID 6dc73ea0dbc02f22b564cf81fe8ac390f288921b
# Parent  13effe47174cfd636d2664cc6c4b1def4cfdf5a4
adjusted to changes in theory Quickcheck

diff -r 13effe47174c -r 6dc73ea0dbc0 src/HOL/ex/Quickcheck_Generators.thy
--- a/src/HOL/ex/Quickcheck_Generators.thy	Fri May 15 16:39:18 2009 +0200
+++ b/src/HOL/ex/Quickcheck_Generators.thy	Fri May 15 16:39:19 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