split of already properly working part of Quickcheck infrastructure
authorhaftmann
Thu Feb 05 14:14:03 2009 +0100 (2009-02-05)
changeset 29808b8b9d529663b
parent 29807 4159caa18f85
child 29809 df25a6b1a475
split of already properly working part of Quickcheck infrastructure
src/HOL/Library/Quickcheck.thy
src/HOL/ex/Quickcheck.thy
src/HOL/ex/Quickcheck_Generators.thy
src/HOL/ex/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Quickcheck.thy	Thu Feb 05 14:14:03 2009 +0100
     1.3 @@ -0,0 +1,85 @@
     1.4 +(* Author: Florian Haftmann, TU Muenchen *)
     1.5 +
     1.6 +header {* A simple counterexample generator *}
     1.7 +
     1.8 +theory Quickcheck
     1.9 +imports Random Code_Eval Map
    1.10 +begin
    1.11 +
    1.12 +subsection {* The @{text random} class *}
    1.13 +
    1.14 +class random = typerep +
    1.15 +  fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    1.16 +
    1.17 +text {* Type @{typ "'a itself"} *}
    1.18 +
    1.19 +instantiation itself :: ("{type, typerep}") random
    1.20 +begin
    1.21 +
    1.22 +definition
    1.23 +  "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
    1.24 +
    1.25 +instance ..
    1.26 +
    1.27 +end
    1.28 +
    1.29 +
    1.30 +subsection {* Quickcheck generator *}
    1.31 +
    1.32 +ML {*
    1.33 +structure StateMonad =
    1.34 +struct
    1.35 +
    1.36 +fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    1.37 +fun liftT' sT = sT --> sT;
    1.38 +
    1.39 +fun return T sT x = Const (@{const_name Pair}, T --> liftT T sT) $ x;
    1.40 +
    1.41 +fun scomp T1 T2 sT f g = Const (@{const_name scomp},
    1.42 +  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    1.43 +
    1.44 +end;
    1.45 +
    1.46 +structure Quickcheck =
    1.47 +struct
    1.48 +
    1.49 +open Quickcheck;
    1.50 +
    1.51 +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    1.52 +
    1.53 +fun mk_generator_expr thy prop tys =
    1.54 +  let
    1.55 +    val bound_max = length tys - 1;
    1.56 +    val bounds = map_index (fn (i, ty) =>
    1.57 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    1.58 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    1.59 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    1.60 +    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    1.61 +      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    1.62 +    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
    1.63 +    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    1.64 +    fun mk_split ty = Sign.mk_const thy
    1.65 +      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
    1.66 +    fun mk_scomp_split ty t t' =
    1.67 +      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
    1.68 +        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    1.69 +    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    1.70 +      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
    1.71 +    val t = fold_rev mk_bindclause bounds (return $ check);
    1.72 +  in Abs ("n", @{typ index}, t) end;
    1.73 +
    1.74 +fun compile_generator_expr thy t =
    1.75 +  let
    1.76 +    val tys = (map snd o fst o strip_abs) t;
    1.77 +    val t' = mk_generator_expr thy t tys;
    1.78 +    val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' [];
    1.79 +  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
    1.80 +
    1.81 +end
    1.82 +*}
    1.83 +
    1.84 +setup {*
    1.85 +  Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
    1.86 +*}
    1.87 +
    1.88 +end
     2.1 --- a/src/HOL/ex/Quickcheck.thy	Thu Feb 05 14:14:03 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,413 +0,0 @@
     2.4 -(* Author: Florian Haftmann, TU Muenchen *)
     2.5 -
     2.6 -header {* A simple counterexample generator *}
     2.7 -
     2.8 -theory Quickcheck
     2.9 -imports Random Code_Eval Map
    2.10 -begin
    2.11 -
    2.12 -subsection {* The @{text random} class *}
    2.13 -
    2.14 -class random = typerep +
    2.15 -  fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    2.16 -
    2.17 -text {* Type @{typ "'a itself"} *}
    2.18 -
    2.19 -instantiation itself :: ("{type, typerep}") random
    2.20 -begin
    2.21 -
    2.22 -definition
    2.23 -  "random _ = return (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
    2.24 -
    2.25 -instance ..
    2.26 -
    2.27 -end
    2.28 -
    2.29 -text {* Type @{typ "'a \<Rightarrow> 'b"} *}
    2.30 -
    2.31 -ML {*
    2.32 -structure Random_Engine =
    2.33 -struct
    2.34 -
    2.35 -open Random_Engine;
    2.36 -
    2.37 -fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
    2.38 -    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
    2.39 -    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
    2.40 -    (seed : Random_Engine.seed) =
    2.41 -  let
    2.42 -    val (seed', seed'') = random_split seed;
    2.43 -    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
    2.44 -    val fun_upd = Const (@{const_name fun_upd},
    2.45 -      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    2.46 -    fun random_fun' x =
    2.47 -      let
    2.48 -        val (seed, fun_map, f_t) = ! state;
    2.49 -      in case AList.lookup (uncurry eq) fun_map x
    2.50 -       of SOME y => y
    2.51 -        | NONE => let
    2.52 -              val t1 = term_of x;
    2.53 -              val ((y, t2), seed') = random seed;
    2.54 -              val fun_map' = (x, y) :: fun_map;
    2.55 -              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
    2.56 -              val _ = state := (seed', fun_map', f_t');
    2.57 -            in y end
    2.58 -      end;
    2.59 -    fun term_fun' () = #3 (! state);
    2.60 -  in ((random_fun', term_fun'), seed'') end;
    2.61 -
    2.62 -end
    2.63 -*}
    2.64 -
    2.65 -axiomatization
    2.66 -  random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
    2.67 -    \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
    2.68 -    \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
    2.69 -
    2.70 -code_const random_fun_aux (SML "Random'_Engine.random'_fun")
    2.71 -
    2.72 -instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
    2.73 -begin
    2.74 -
    2.75 -definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
    2.76 -  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
    2.77 -
    2.78 -instance ..
    2.79 -
    2.80 -end
    2.81 -
    2.82 -code_reserved SML Random_Engine
    2.83 -
    2.84 -text {* Datatypes *}
    2.85 -
    2.86 -definition
    2.87 -  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    2.88 -  "collapse f = (do g \<leftarrow> f; g done)"
    2.89 -
    2.90 -ML {*
    2.91 -structure StateMonad =
    2.92 -struct
    2.93 -
    2.94 -fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    2.95 -fun liftT' sT = sT --> sT;
    2.96 -
    2.97 -fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    2.98 -
    2.99 -fun scomp T1 T2 sT f g = Const (@{const_name scomp},
   2.100 -  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
   2.101 -
   2.102 -end;
   2.103 -*}
   2.104 -
   2.105 -lemma random'_if:
   2.106 -  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
   2.107 -  assumes "random' 0 j = (\<lambda>s. undefined)"
   2.108 -    and "\<And>i. random' (Suc_index i) j = rhs2 i"
   2.109 -  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
   2.110 -  by (cases i rule: index.exhaust) (insert assms, simp_all)
   2.111 -
   2.112 -setup {*
   2.113 -let
   2.114 -  exception REC of string;
   2.115 -  exception TYP of string;
   2.116 -  fun mk_collapse thy ty = Sign.mk_const thy
   2.117 -    (@{const_name collapse}, [@{typ seed}, ty]);
   2.118 -  fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   2.119 -  fun mk_split thy ty ty' = Sign.mk_const thy
   2.120 -    (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
   2.121 -  fun mk_scomp_split thy ty ty' t t' =
   2.122 -    StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
   2.123 -      (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
   2.124 -  fun mk_cons thy this_ty (c, args) =
   2.125 -    let
   2.126 -      val tys = map (fst o fst) args;
   2.127 -      val c_ty = tys ---> this_ty;
   2.128 -      val c = Const (c, tys ---> this_ty);
   2.129 -      val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
   2.130 -      val c_indices = map (curry ( op + ) 1) t_indices;
   2.131 -      val c_t = list_comb (c, map Bound c_indices);
   2.132 -      val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
   2.133 -        (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
   2.134 -        |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
   2.135 -      val return = StateMonad.return (term_ty this_ty) @{typ seed}
   2.136 -        (HOLogic.mk_prod (c_t, t_t));
   2.137 -      val t = fold_rev (fn ((ty, _), random) =>
   2.138 -        mk_scomp_split thy ty this_ty random)
   2.139 -          args return;
   2.140 -      val is_rec = exists (snd o fst) args;
   2.141 -    in (is_rec, t) end;
   2.142 -  fun mk_conss thy ty [] = NONE
   2.143 -    | mk_conss thy ty [(_, t)] = SOME t
   2.144 -    | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
   2.145 -          (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
   2.146 -            HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
   2.147 -  fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
   2.148 -    let
   2.149 -      val SOME t_atom = mk_conss thy ty ts_atom;
   2.150 -    in case mk_conss thy ty ts_rec
   2.151 -     of SOME t_rec => mk_collapse thy (term_ty ty) $
   2.152 -          (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
   2.153 -             @{term "i\<Colon>index"} $ t_rec $ t_atom)
   2.154 -      | NONE => t_atom
   2.155 -    end;
   2.156 -  fun mk_random_eqs thy vs tycos =
   2.157 -    let
   2.158 -      val this_ty = Type (hd tycos, map TFree vs);
   2.159 -      val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
   2.160 -      val random_name = NameSpace.base @{const_name random};
   2.161 -      val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
   2.162 -      fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
   2.163 -      val random' = Free (random'_name,
   2.164 -        @{typ index} --> @{typ index} --> this_ty');
   2.165 -      fun atom ty = if Sign.of_sort thy (ty, @{sort random})
   2.166 -        then ((ty, false), random ty $ @{term "j\<Colon>index"})
   2.167 -        else raise TYP
   2.168 -          ("Will not generate random elements for type(s) " ^ quote (hd tycos));
   2.169 -      fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
   2.170 -      fun rtyp tyco tys = raise REC
   2.171 -        ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
   2.172 -      val rhss = DatatypePackage.construction_interpretation thy
   2.173 -            { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
   2.174 -        |> (map o apsnd o map) (mk_cons thy this_ty) 
   2.175 -        |> (map o apsnd) (List.partition fst)
   2.176 -        |> map (mk_clauses thy this_ty)
   2.177 -      val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
   2.178 -          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
   2.179 -            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
   2.180 -          (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
   2.181 -        ]))) rhss;
   2.182 -    in eqss end;
   2.183 -  fun random_inst [tyco] thy =
   2.184 -        let
   2.185 -          val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
   2.186 -          val vs = (map o apsnd)
   2.187 -            (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
   2.188 -          val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
   2.189 -          val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   2.190 -            (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
   2.191 -               random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
   2.192 -          val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
   2.193 -            (fn thm => Context.mapping (Code.del_eqn thm) I));
   2.194 -          fun add_code simps lthy =
   2.195 -            let
   2.196 -              val thy = ProofContext.theory_of lthy;
   2.197 -              val thm = @{thm random'_if}
   2.198 -                |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
   2.199 -                |> (fn thm => thm OF simps)
   2.200 -                |> singleton (ProofContext.export lthy (ProofContext.init thy));
   2.201 -              val c = (fst o dest_Const o fst o strip_comb o fst
   2.202 -                o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
   2.203 -            in
   2.204 -              lthy
   2.205 -              |> LocalTheory.theory (Code.del_eqns c
   2.206 -                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
   2.207 -                   #-> Code.add_eqn)
   2.208 -            end;
   2.209 -        in
   2.210 -          thy
   2.211 -          |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   2.212 -          |> PrimrecPackage.add_primrec
   2.213 -               [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
   2.214 -                 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
   2.215 -          |-> add_code
   2.216 -          |> `(fn lthy => Syntax.check_term lthy eq)
   2.217 -          |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   2.218 -          |> snd
   2.219 -          |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   2.220 -          |> LocalTheory.exit_global
   2.221 -        end
   2.222 -    | random_inst tycos thy = raise REC
   2.223 -        ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
   2.224 -  fun add_random_inst tycos thy = random_inst tycos thy
   2.225 -     handle REC msg => (warning msg; thy)
   2.226 -          | TYP msg => (warning msg; thy)
   2.227 -in DatatypePackage.interpretation add_random_inst end
   2.228 -*}
   2.229 -
   2.230 -text {* Type @{typ int} *}
   2.231 -
   2.232 -instantiation int :: random
   2.233 -begin
   2.234 -
   2.235 -definition
   2.236 -  "random n = (do
   2.237 -     (b, _) \<leftarrow> random n;
   2.238 -     (m, t) \<leftarrow> random n;
   2.239 -     return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
   2.240 -       else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
   2.241 -         (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
   2.242 -   done)"
   2.243 -
   2.244 -instance ..
   2.245 -
   2.246 -end
   2.247 -
   2.248 -
   2.249 -subsection {* Quickcheck generator *}
   2.250 -
   2.251 -ML {*
   2.252 -structure Quickcheck =
   2.253 -struct
   2.254 -
   2.255 -open Quickcheck;
   2.256 -
   2.257 -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   2.258 -
   2.259 -fun mk_generator_expr thy prop tys =
   2.260 -  let
   2.261 -    val bound_max = length tys - 1;
   2.262 -    val bounds = map_index (fn (i, ty) =>
   2.263 -      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
   2.264 -    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
   2.265 -    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   2.266 -    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
   2.267 -      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
   2.268 -    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
   2.269 -    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   2.270 -    fun mk_split ty = Sign.mk_const thy
   2.271 -      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
   2.272 -    fun mk_scomp_split ty t t' =
   2.273 -      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
   2.274 -        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
   2.275 -    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
   2.276 -      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
   2.277 -    val t = fold_rev mk_bindclause bounds (return $ check);
   2.278 -  in Abs ("n", @{typ index}, t) end;
   2.279 -
   2.280 -fun compile_generator_expr thy t =
   2.281 -  let
   2.282 -    val tys = (map snd o fst o strip_abs) t;
   2.283 -    val t' = mk_generator_expr thy t tys;
   2.284 -    val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy t' [];
   2.285 -  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
   2.286 -
   2.287 -end
   2.288 -*}
   2.289 -
   2.290 -setup {*
   2.291 -  Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
   2.292 -*}
   2.293 -
   2.294 -subsection {* Examples *}
   2.295 -
   2.296 -theorem "map g (map f xs) = map (g o f) xs"
   2.297 -  quickcheck [generator = code]
   2.298 -  by (induct xs) simp_all
   2.299 -
   2.300 -theorem "map g (map f xs) = map (f o g) xs"
   2.301 -  quickcheck [generator = code]
   2.302 -  oops
   2.303 -
   2.304 -theorem "rev (xs @ ys) = rev ys @ rev xs"
   2.305 -  quickcheck [generator = code]
   2.306 -  by simp
   2.307 -
   2.308 -theorem "rev (xs @ ys) = rev xs @ rev ys"
   2.309 -  quickcheck [generator = code]
   2.310 -  oops
   2.311 -
   2.312 -theorem "rev (rev xs) = xs"
   2.313 -  quickcheck [generator = code]
   2.314 -  by simp
   2.315 -
   2.316 -theorem "rev xs = xs"
   2.317 -  quickcheck [generator = code]
   2.318 -  oops
   2.319 -
   2.320 -primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
   2.321 -  "app [] x = x"
   2.322 -  | "app (f # fs) x = app fs (f x)"
   2.323 -
   2.324 -lemma "app (fs @ gs) x = app gs (app fs x)"
   2.325 -  quickcheck [generator = code]
   2.326 -  by (induct fs arbitrary: x) simp_all
   2.327 -
   2.328 -lemma "app (fs @ gs) x = app fs (app gs x)"
   2.329 -  quickcheck [generator = code]
   2.330 -  oops
   2.331 -
   2.332 -primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
   2.333 -  "occurs a [] = 0"
   2.334 -  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
   2.335 -
   2.336 -primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   2.337 -  "del1 a [] = []"
   2.338 -  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
   2.339 -
   2.340 -lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   2.341 -  -- {* Wrong. Precondition needed.*}
   2.342 -  quickcheck [generator = code]
   2.343 -  oops
   2.344 -
   2.345 -lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   2.346 -  quickcheck [generator = code]
   2.347 -    -- {* Also wrong.*}
   2.348 -  oops
   2.349 -
   2.350 -lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   2.351 -  quickcheck [generator = code]
   2.352 -  by (induct xs) auto
   2.353 -
   2.354 -primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   2.355 -  "replace a b [] = []"
   2.356 -  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
   2.357 -                            else (x#(replace a b xs)))"
   2.358 -
   2.359 -lemma "occurs a xs = occurs b (replace a b xs)"
   2.360 -  quickcheck [generator = code]
   2.361 -  -- {* Wrong. Precondition needed.*}
   2.362 -  oops
   2.363 -
   2.364 -lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
   2.365 -  quickcheck [generator = code]
   2.366 -  by (induct xs) simp_all
   2.367 -
   2.368 -
   2.369 -subsection {* Trees *}
   2.370 -
   2.371 -datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   2.372 -
   2.373 -primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   2.374 -  "leaves Twig = []"
   2.375 -  | "leaves (Leaf a) = [a]"
   2.376 -  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
   2.377 -
   2.378 -primrec plant :: "'a list \<Rightarrow> 'a tree" where
   2.379 -  "plant [] = Twig "
   2.380 -  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
   2.381 -
   2.382 -primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   2.383 -  "mirror (Twig) = Twig "
   2.384 -  | "mirror (Leaf a) = Leaf a "
   2.385 -  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   2.386 -
   2.387 -theorem "plant (rev (leaves xt)) = mirror xt"
   2.388 -  quickcheck [generator = code]
   2.389 -    --{* Wrong! *} 
   2.390 -  oops
   2.391 -
   2.392 -theorem "plant (leaves xt @ leaves yt) = Branch xt yt"
   2.393 -  quickcheck [generator = code]
   2.394 -    --{* Wrong! *} 
   2.395 -  oops
   2.396 -
   2.397 -datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   2.398 -
   2.399 -primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   2.400 -  "inOrder (Tip a)= [a]"
   2.401 -  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   2.402 -
   2.403 -primrec root :: "'a ntree \<Rightarrow> 'a" where
   2.404 -  "root (Tip a) = a"
   2.405 -  | "root (Node f x y) = f"
   2.406 -
   2.407 -theorem "hd (inOrder xt) = root xt"
   2.408 -  quickcheck [generator = code]
   2.409 -    --{* Wrong! *} 
   2.410 -  oops
   2.411 -
   2.412 -lemma "int (f k) = k"
   2.413 -  quickcheck [generator = code]
   2.414 -  oops
   2.415 -
   2.416 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Quickcheck_Generators.thy	Thu Feb 05 14:14:03 2009 +0100
     3.3 @@ -0,0 +1,353 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Experimental counterexample generators *}
     3.7 +
     3.8 +theory Quickcheck_Generators
     3.9 +imports Quickcheck State_Monad
    3.10 +begin
    3.11 +
    3.12 +subsection {* Type @{typ "'a \<Rightarrow> 'b"} *}
    3.13 +
    3.14 +ML {*
    3.15 +structure Random_Engine =
    3.16 +struct
    3.17 +
    3.18 +open Random_Engine;
    3.19 +
    3.20 +fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
    3.21 +    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
    3.22 +    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
    3.23 +    (seed : Random_Engine.seed) =
    3.24 +  let
    3.25 +    val (seed', seed'') = random_split seed;
    3.26 +    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
    3.27 +    val fun_upd = Const (@{const_name fun_upd},
    3.28 +      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    3.29 +    fun random_fun' x =
    3.30 +      let
    3.31 +        val (seed, fun_map, f_t) = ! state;
    3.32 +      in case AList.lookup (uncurry eq) fun_map x
    3.33 +       of SOME y => y
    3.34 +        | NONE => let
    3.35 +              val t1 = term_of x;
    3.36 +              val ((y, t2), seed') = random seed;
    3.37 +              val fun_map' = (x, y) :: fun_map;
    3.38 +              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
    3.39 +              val _ = state := (seed', fun_map', f_t');
    3.40 +            in y end
    3.41 +      end;
    3.42 +    fun term_fun' () = #3 (! state);
    3.43 +  in ((random_fun', term_fun'), seed'') end;
    3.44 +
    3.45 +end
    3.46 +*}
    3.47 +
    3.48 +axiomatization
    3.49 +  random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
    3.50 +    \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
    3.51 +    \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
    3.52 +
    3.53 +code_const random_fun_aux (SML "Random'_Engine.random'_fun")
    3.54 +
    3.55 +instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
    3.56 +begin
    3.57 +
    3.58 +definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
    3.59 +  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
    3.60 +
    3.61 +instance ..
    3.62 +
    3.63 +end
    3.64 +
    3.65 +code_reserved SML Random_Engine
    3.66 +
    3.67 +
    3.68 +subsection {* Datatypes *}
    3.69 +
    3.70 +definition
    3.71 +  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    3.72 +  "collapse f = (do g \<leftarrow> f; g done)"
    3.73 +
    3.74 +ML {*
    3.75 +structure StateMonad =
    3.76 +struct
    3.77 +
    3.78 +fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    3.79 +fun liftT' sT = sT --> sT;
    3.80 +
    3.81 +fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x;
    3.82 +
    3.83 +fun scomp T1 T2 sT f g = Const (@{const_name scomp},
    3.84 +  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    3.85 +
    3.86 +end;
    3.87 +*}
    3.88 +
    3.89 +lemma random'_if:
    3.90 +  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    3.91 +  assumes "random' 0 j = (\<lambda>s. undefined)"
    3.92 +    and "\<And>i. random' (Suc_index i) j = rhs2 i"
    3.93 +  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
    3.94 +  by (cases i rule: index.exhaust) (insert assms, simp_all)
    3.95 +
    3.96 +setup {*
    3.97 +let
    3.98 +  exception REC of string;
    3.99 +  exception TYP of string;
   3.100 +  fun mk_collapse thy ty = Sign.mk_const thy
   3.101 +    (@{const_name collapse}, [@{typ seed}, ty]);
   3.102 +  fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   3.103 +  fun mk_split thy ty ty' = Sign.mk_const thy
   3.104 +    (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
   3.105 +  fun mk_scomp_split thy ty ty' t t' =
   3.106 +    StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
   3.107 +      (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
   3.108 +  fun mk_cons thy this_ty (c, args) =
   3.109 +    let
   3.110 +      val tys = map (fst o fst) args;
   3.111 +      val c_ty = tys ---> this_ty;
   3.112 +      val c = Const (c, tys ---> this_ty);
   3.113 +      val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
   3.114 +      val c_indices = map (curry ( op + ) 1) t_indices;
   3.115 +      val c_t = list_comb (c, map Bound c_indices);
   3.116 +      val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep
   3.117 +        (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
   3.118 +        |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
   3.119 +      val return = StateMonad.return (term_ty this_ty) @{typ seed}
   3.120 +        (HOLogic.mk_prod (c_t, t_t));
   3.121 +      val t = fold_rev (fn ((ty, _), random) =>
   3.122 +        mk_scomp_split thy ty this_ty random)
   3.123 +          args return;
   3.124 +      val is_rec = exists (snd o fst) args;
   3.125 +    in (is_rec, t) end;
   3.126 +  fun mk_conss thy ty [] = NONE
   3.127 +    | mk_conss thy ty [(_, t)] = SOME t
   3.128 +    | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
   3.129 +          (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
   3.130 +            HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts)));
   3.131 +  fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
   3.132 +    let
   3.133 +      val SOME t_atom = mk_conss thy ty ts_atom;
   3.134 +    in case mk_conss thy ty ts_rec
   3.135 +     of SOME t_rec => mk_collapse thy (term_ty ty) $
   3.136 +          (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $
   3.137 +             @{term "i\<Colon>index"} $ t_rec $ t_atom)
   3.138 +      | NONE => t_atom
   3.139 +    end;
   3.140 +  fun mk_random_eqs thy vs tycos =
   3.141 +    let
   3.142 +      val this_ty = Type (hd tycos, map TFree vs);
   3.143 +      val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
   3.144 +      val random_name = NameSpace.base @{const_name random};
   3.145 +      val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
   3.146 +      fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
   3.147 +      val random' = Free (random'_name,
   3.148 +        @{typ index} --> @{typ index} --> this_ty');
   3.149 +      fun atom ty = if Sign.of_sort thy (ty, @{sort random})
   3.150 +        then ((ty, false), random ty $ @{term "j\<Colon>index"})
   3.151 +        else raise TYP
   3.152 +          ("Will not generate random elements for type(s) " ^ quote (hd tycos));
   3.153 +      fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"});
   3.154 +      fun rtyp tyco tys = raise REC
   3.155 +        ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
   3.156 +      val rhss = DatatypePackage.construction_interpretation thy
   3.157 +            { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
   3.158 +        |> (map o apsnd o map) (mk_cons thy this_ty) 
   3.159 +        |> (map o apsnd) (List.partition fst)
   3.160 +        |> map (mk_clauses thy this_ty)
   3.161 +      val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
   3.162 +          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
   3.163 +            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
   3.164 +          (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
   3.165 +        ]))) rhss;
   3.166 +    in eqss end;
   3.167 +  fun random_inst [tyco] thy =
   3.168 +        let
   3.169 +          val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
   3.170 +          val vs = (map o apsnd)
   3.171 +            (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
   3.172 +          val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
   3.173 +          val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   3.174 +            (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>index"},
   3.175 +               random' $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"})
   3.176 +          val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
   3.177 +            (fn thm => Context.mapping (Code.del_eqn thm) I));
   3.178 +          fun add_code simps lthy =
   3.179 +            let
   3.180 +              val thy = ProofContext.theory_of lthy;
   3.181 +              val thm = @{thm random'_if}
   3.182 +                |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
   3.183 +                |> (fn thm => thm OF simps)
   3.184 +                |> singleton (ProofContext.export lthy (ProofContext.init thy));
   3.185 +              val c = (fst o dest_Const o fst o strip_comb o fst
   3.186 +                o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
   3.187 +            in
   3.188 +              lthy
   3.189 +              |> LocalTheory.theory (Code.del_eqns c
   3.190 +                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
   3.191 +                   #-> Code.add_eqn)
   3.192 +            end;
   3.193 +        in
   3.194 +          thy
   3.195 +          |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   3.196 +          |> PrimrecPackage.add_primrec
   3.197 +               [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
   3.198 +                 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
   3.199 +          |-> add_code
   3.200 +          |> `(fn lthy => Syntax.check_term lthy eq)
   3.201 +          |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   3.202 +          |> snd
   3.203 +          |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   3.204 +          |> LocalTheory.exit_global
   3.205 +        end
   3.206 +    | random_inst tycos thy = raise REC
   3.207 +        ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
   3.208 +  fun add_random_inst tycos thy = random_inst tycos thy
   3.209 +     handle REC msg => (warning msg; thy)
   3.210 +          | TYP msg => (warning msg; thy)
   3.211 +in DatatypePackage.interpretation add_random_inst end
   3.212 +*}
   3.213 +
   3.214 +
   3.215 +subsection {* Type @{typ int} *}
   3.216 +
   3.217 +instantiation int :: random
   3.218 +begin
   3.219 +
   3.220 +definition
   3.221 +  "random n = (do
   3.222 +     (b, _) \<leftarrow> random n;
   3.223 +     (m, t) \<leftarrow> random n;
   3.224 +     return (if b then (int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))
   3.225 +       else (- int m, \<lambda>u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \<Rightarrow> int))
   3.226 +         (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \<Rightarrow> int)) (t ()))))
   3.227 +   done)"
   3.228 +
   3.229 +instance ..
   3.230 +
   3.231 +end
   3.232 +
   3.233 +
   3.234 +subsection {* Examples *}
   3.235 +
   3.236 +theorem "map g (map f xs) = map (g o f) xs"
   3.237 +  quickcheck [generator = code]
   3.238 +  by (induct xs) simp_all
   3.239 +
   3.240 +theorem "map g (map f xs) = map (f o g) xs"
   3.241 +  quickcheck [generator = code]
   3.242 +  oops
   3.243 +
   3.244 +theorem "rev (xs @ ys) = rev ys @ rev xs"
   3.245 +  quickcheck [generator = code]
   3.246 +  by simp
   3.247 +
   3.248 +theorem "rev (xs @ ys) = rev xs @ rev ys"
   3.249 +  quickcheck [generator = code]
   3.250 +  oops
   3.251 +
   3.252 +theorem "rev (rev xs) = xs"
   3.253 +  quickcheck [generator = code]
   3.254 +  by simp
   3.255 +
   3.256 +theorem "rev xs = xs"
   3.257 +  quickcheck [generator = code]
   3.258 +  oops
   3.259 +
   3.260 +primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
   3.261 +  "app [] x = x"
   3.262 +  | "app (f # fs) x = app fs (f x)"
   3.263 +
   3.264 +lemma "app (fs @ gs) x = app gs (app fs x)"
   3.265 +  quickcheck [generator = code]
   3.266 +  by (induct fs arbitrary: x) simp_all
   3.267 +
   3.268 +lemma "app (fs @ gs) x = app fs (app gs x)"
   3.269 +  quickcheck [generator = code]
   3.270 +  oops
   3.271 +
   3.272 +primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
   3.273 +  "occurs a [] = 0"
   3.274 +  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
   3.275 +
   3.276 +primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   3.277 +  "del1 a [] = []"
   3.278 +  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
   3.279 +
   3.280 +lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   3.281 +  -- {* Wrong. Precondition needed.*}
   3.282 +  quickcheck [generator = code]
   3.283 +  oops
   3.284 +
   3.285 +lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   3.286 +  quickcheck [generator = code]
   3.287 +    -- {* Also wrong.*}
   3.288 +  oops
   3.289 +
   3.290 +lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   3.291 +  quickcheck [generator = code]
   3.292 +  by (induct xs) auto
   3.293 +
   3.294 +primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   3.295 +  "replace a b [] = []"
   3.296 +  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
   3.297 +                            else (x#(replace a b xs)))"
   3.298 +
   3.299 +lemma "occurs a xs = occurs b (replace a b xs)"
   3.300 +  quickcheck [generator = code]
   3.301 +  -- {* Wrong. Precondition needed.*}
   3.302 +  oops
   3.303 +
   3.304 +lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
   3.305 +  quickcheck [generator = code]
   3.306 +  by (induct xs) simp_all
   3.307 +
   3.308 +
   3.309 +subsection {* Trees *}
   3.310 +
   3.311 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   3.312 +
   3.313 +primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   3.314 +  "leaves Twig = []"
   3.315 +  | "leaves (Leaf a) = [a]"
   3.316 +  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
   3.317 +
   3.318 +primrec plant :: "'a list \<Rightarrow> 'a tree" where
   3.319 +  "plant [] = Twig "
   3.320 +  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
   3.321 +
   3.322 +primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   3.323 +  "mirror (Twig) = Twig "
   3.324 +  | "mirror (Leaf a) = Leaf a "
   3.325 +  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   3.326 +
   3.327 +theorem "plant (rev (leaves xt)) = mirror xt"
   3.328 +  quickcheck [generator = code]
   3.329 +    --{* Wrong! *} 
   3.330 +  oops
   3.331 +
   3.332 +theorem "plant (leaves xt @ leaves yt) = Branch xt yt"
   3.333 +  quickcheck [generator = code]
   3.334 +    --{* Wrong! *} 
   3.335 +  oops
   3.336 +
   3.337 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   3.338 +
   3.339 +primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   3.340 +  "inOrder (Tip a)= [a]"
   3.341 +  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   3.342 +
   3.343 +primrec root :: "'a ntree \<Rightarrow> 'a" where
   3.344 +  "root (Tip a) = a"
   3.345 +  | "root (Node f x y) = f"
   3.346 +
   3.347 +theorem "hd (inOrder xt) = root xt"
   3.348 +  quickcheck [generator = code]
   3.349 +    --{* Wrong! *} 
   3.350 +  oops
   3.351 +
   3.352 +lemma "int (f k) = k"
   3.353 +  quickcheck [generator = code]
   3.354 +  oops
   3.355 +
   3.356 +end
     4.1 --- a/src/HOL/ex/ROOT.ML	Thu Feb 05 14:14:03 2009 +0100
     4.2 +++ b/src/HOL/ex/ROOT.ML	Thu Feb 05 14:14:03 2009 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4    "FuncSet",
     4.5    "Word",
     4.6    "Eval_Examples",
     4.7 -  "Quickcheck",
     4.8 +  "Quickcheck_Generators",
     4.9    "Term_Of_Syntax",
    4.10    "Codegenerator",
    4.11    "Codegenerator_Pretty",