first running version of qc generators for datatypes
authorhaftmann
Tue Jun 09 22:59:54 2009 +0200 (2009-06-09)
changeset 31595bd2f7211a420
parent 31594 a94aa5f045fb
child 31596 c96d7e5df659
first running version of qc generators for datatypes
src/HOL/IsaMakefile
src/HOL/Tools/quickcheck_generators.ML
src/HOL/ex/Quickcheck_Generators.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jun 09 22:59:53 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jun 09 22:59:54 2009 +0200
     1.3 @@ -854,7 +854,7 @@
     1.4    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
     1.5    ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
     1.6    ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
     1.7 -  ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML	\
     1.8 +  ex/Quickcheck_Examples.thy ex/ROOT.ML	\
     1.9    ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy			\
    1.10    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    1.11    ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
     2.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 09 22:59:53 2009 +0200
     2.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 09 22:59:54 2009 +0200
     2.3 @@ -12,6 +12,10 @@
     2.4      -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
     2.5    val ensure_random_typecopy: string -> theory -> theory
     2.6    val random_aux_specification: string -> term list -> local_theory -> local_theory
     2.7 +  val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
     2.8 +    -> typ list -> typ list -> string list -> string list
     2.9 +    -> string * (term list * (term * term) list)
    2.10 +  val ensure_random_datatype: string list -> theory -> theory
    2.11    val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref
    2.12    val setup: theory -> theory
    2.13  end;
    2.14 @@ -208,19 +212,19 @@
    2.15  
    2.16  fun random_aux_specification prefix eqs lthy =
    2.17    let
    2.18 -    val _ $ Free (v, _) $ Free (w, _) =
    2.19 -      (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o hd) eqs;
    2.20 +    val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
    2.21 +      o HOLogic.dest_Trueprop o hd) eqs) [];
    2.22      fun mk_proto_eq eq =
    2.23        let
    2.24 -        val (head $ arg, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    2.25 -      in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda arg rhs)) end;
    2.26 +        val (head $ t $ u, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    2.27 +      in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda t (lambda u rhs))) end;
    2.28      val proto_eqs = map mk_proto_eq eqs;
    2.29      fun prove_simps proto_simps lthy =
    2.30        let
    2.31 -        val ext_simps = map (fn thm => fun_cong OF [thm]) proto_simps;
    2.32 +        val ext_simps = map (fn thm => fun_cong OF [fun_cong OF  [thm]]) proto_simps;
    2.33          val tac = ALLGOALS Goal.conjunction_tac
    2.34            THEN ALLGOALS (ProofContext.fact_tac ext_simps);
    2.35 -      in (Goal.prove_multi lthy [v, w] [] eqs (K tac), lthy) end;
    2.36 +      in (Goal.prove_multi lthy vs [] eqs (K tac), lthy) end;
    2.37      val b = Binding.qualify true prefix (Binding.name "simps");
    2.38    in
    2.39      lthy
    2.40 @@ -236,13 +240,141 @@
    2.41  
    2.42  (* constructing random instances on datatypes *)
    2.43  
    2.44 -(*still under construction*)
    2.45 +fun mk_random_aux_eqs thy descr vs Ts rtyps tycos names =
    2.46 +  let
    2.47 +    val mk_const = curry (Sign.mk_const thy);
    2.48 +    val i = @{term "i\<Colon>code_numeral"};
    2.49 +    val i1 = @{term "(i\<Colon>code_numeral) - 1"};
    2.50 +    val j = @{term "j\<Colon>code_numeral"};
    2.51 +    val seed = @{term "s\<Colon>Random.seed"};
    2.52 +    val random_auxN = "random_aux";
    2.53 +    val random_auxsN = map (prefix (random_auxN ^ "_"))
    2.54 +      (map Long_Name.base_name names @ map DatatypeAux.name_of_typ rtyps);
    2.55 +    fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
    2.56 +    val rTs = Ts @ rtyps;
    2.57 +    fun random_resultT T = @{typ Random.seed}
    2.58 +      --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed});
    2.59 +    val pTs = map random_resultT rTs;
    2.60 +    fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T;
    2.61 +    val random_auxT = sizeT o random_resultT;
    2.62 +    val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
    2.63 +      random_auxsN rTs;
    2.64 +    fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
    2.65 +    fun mk_random_aux_call T =
    2.66 +      let
    2.67 +        val k = find_index (fn T' => T = T') rTs;
    2.68 +        val random = nth random_auxs k;
    2.69 +        val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
    2.70 +          |> the_default 0;
    2.71 +      in (SOME size, (random $ i1 $ j, T)) end;
    2.72 +    fun atom T = mk_random_call T;
    2.73 +    fun dtyp tyco = mk_random_aux_call (Type (tyco, map TFree vs));
    2.74 +    fun rtyp (tyco, Ts) _ = mk_random_aux_call (Type (tyco, Ts));
    2.75 +    val (tss1, tss2) = DatatypePackage.construction_interpretation thy
    2.76 +      {atom = atom, dtyp = dtyp, rtyp = rtyp} vs tycos;
    2.77 +    fun mk_consexpr simpleT (c, xs) =
    2.78 +      let
    2.79 +        val (ks, simple_tTs) = split_list xs;
    2.80 +        val T = termifyT simpleT;
    2.81 +        val tTs = (map o apsnd) termifyT simple_tTs;
    2.82 +        val is_rec = exists is_some ks;
    2.83 +        val k = fold (fn NONE => I | SOME k => curry Int.max k) ks 0;
    2.84 +        val vs = Name.names Name.context "x" (map snd simple_tTs);
    2.85 +        val vs' = (map o apsnd) termifyT vs;
    2.86 +        val tc = HOLogic.mk_return T @{typ Random.seed}
    2.87 +          (HOLogic.mk_valtermify_app c vs simpleT);
    2.88 +        val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs')
    2.89 +          tc @{typ Random.seed} (SOME T, @{typ Random.seed});
    2.90 +        val tk = if is_rec
    2.91 +          then if k = 0 then i
    2.92 +            else @{term "Quickcheck.beyond :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
    2.93 +             $ HOLogic.mk_number @{typ code_numeral} k $ i
    2.94 +          else @{term "1::code_numeral"}
    2.95 +      in (is_rec, HOLogic.mk_prod (tk, t)) end;
    2.96 +    fun sort_rec xs =
    2.97 +      map_filter (fn (true, t) => SOME t | _ =>  NONE) xs
    2.98 +      @ map_filter (fn (false, t) => SOME t | _ =>  NONE) xs;
    2.99 +    val gen_exprss = (map o apfst) (fn tyco => Type (tyco, map TFree vs)) tss1
   2.100 +      @ (map o apfst) Type tss2
   2.101 +      |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs));
   2.102 +    fun mk_select (rT, xs) =
   2.103 +      mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT]
   2.104 +      $ (mk_const @{const_name Random.select_weight} [random_resultT rT]
   2.105 +        $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs)
   2.106 +          $ seed;
   2.107 +    val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
   2.108 +    val auxs_rhss = map mk_select gen_exprss;
   2.109 +    val prefix = space_implode "_" (random_auxN :: names);
   2.110 +  in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
   2.111 +
   2.112 +fun mk_random_datatype descr vs rtyps tycos names thy =
   2.113 +  let
   2.114 +    val i = @{term "i\<Colon>code_numeral"};
   2.115 +    val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   2.116 +    val Ts = map (fn tyco => Type (tyco, map TFree vs)) tycos;
   2.117 +    fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
   2.118 +     of SOME (_, l) => if l = 0 then i
   2.119 +          else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
   2.120 +            $ HOLogic.mk_number @{typ code_numeral} l $ i
   2.121 +      | NONE => i;
   2.122 +    val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
   2.123 +      (mk_random_aux_eqs thy descr vs Ts rtyps tycos names);
   2.124 +    val random_defs = map_index (fn (k, T) => mk_prop_eq
   2.125 +      (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
   2.126 +  in
   2.127 +    thy
   2.128 +    |> TheoryTarget.instantiation (tycos, vs, @{sort random})
   2.129 +    |> random_aux_specification prefix auxs_eqs
   2.130 +    |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
   2.131 +    |-> (fn random_defs' => fold_map (fn random_def =>
   2.132 +          Specification.definition (NONE, (Attrib.empty_binding,
   2.133 +            random_def))) random_defs')
   2.134 +    |> snd
   2.135 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   2.136 +  end;
   2.137 +
   2.138 +fun ensure_random_datatype (raw_tycos as tyco :: _) thy =
   2.139 +  let
   2.140 +    val pp = Syntax.pp_global thy;
   2.141 +    val algebra = Sign.classes_of thy;
   2.142 +    val info = DatatypePackage.the_datatype thy tyco;
   2.143 +    val descr = #descr info;
   2.144 +    val tycos = Library.take (length raw_tycos, descr)
   2.145 +      |> map (fn (_, (tyco, dTs, _)) => tyco);
   2.146 +    val names = map Long_Name.base_name (the_default tycos (#alt_names info));
   2.147 +    val (raw_vs :: _, raw_coss) = (split_list
   2.148 +      o map (DatatypePackage.the_datatype_spec thy)) tycos;
   2.149 +    val raw_Ts = maps (maps snd) raw_coss;
   2.150 +    val vs' = (fold o fold_atyps) (fn TFree (v, _) => insert (op =) v) raw_Ts [];
   2.151 +    val vs = map (fn (v, sort) => (v, if member (op =) vs' v
   2.152 +      then Sorts.inter_sort algebra (sort, @{sort random}) else sort)) raw_vs;
   2.153 +    val rtyps = Library.drop (length tycos, descr)
   2.154 +      |> map (fn (_, (tyco, dTs, _)) =>
   2.155 +          Type (tyco, map (DatatypeAux.typ_of_dtyp descr vs) dTs));
   2.156 +    val sorts = map snd vs;
   2.157 +    val constrain = map_atyps
   2.158 +      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v));
   2.159 +    val Ts = map constrain raw_Ts;
   2.160 +    val algebra' = algebra
   2.161 +      |> fold (fn tyco => Sorts.add_arities pp
   2.162 +           (tyco, map (rpair sorts) @{sort random})) tycos;
   2.163 +    val can_inst = forall (fn T =>
   2.164 +      Sorts.of_sort algebra' (T, @{sort random})) Ts;
   2.165 +    val hast_inst = exists (fn tyco =>
   2.166 +      can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   2.167 +  in if can_inst andalso not hast_inst then (mk_random_datatype descr vs rtyps tycos names thy
   2.168 +    (*FIXME ephemeral handles*)
   2.169 +    handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
   2.170 +         | e as TYPE (msg, _, _) =>  (tracing msg; raise e)
   2.171 +         | e as ERROR msg =>  (tracing msg; raise e))
   2.172 +  else thy end;
   2.173  
   2.174  
   2.175  (** setup **)
   2.176  
   2.177  val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I))
   2.178    #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of)
   2.179 -  #> TypecopyPackage.interpretation ensure_random_typecopy;
   2.180 +  #> TypecopyPackage.interpretation ensure_random_typecopy
   2.181 +  #> DatatypePackage.interpretation ensure_random_datatype;
   2.182  
   2.183  end;
     3.1 --- a/src/HOL/ex/Quickcheck_Generators.thy	Tue Jun 09 22:59:53 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,274 +0,0 @@
     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 {* Datatypes *}
    3.13 -
    3.14 -definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
    3.15 -  "collapse f = (do g \<leftarrow> f; g done)"
    3.16 -
    3.17 -lemma random'_if:
    3.18 -  fixes random' :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    3.19 -  assumes "random' 0 j = (\<lambda>s. undefined)"
    3.20 -    and "\<And>i. random' (Suc_code_numeral i) j = rhs2 i"
    3.21 -  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
    3.22 -  by (cases i rule: code_numeral.exhaust) (insert assms, simp_all)
    3.23 -
    3.24 -setup {*
    3.25 -let
    3.26 -  fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    3.27 -  fun scomp T1 T2 sT f g = Const (@{const_name scomp},
    3.28 -    liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    3.29 -  exception REC of string;
    3.30 -  exception TYP of string;
    3.31 -  fun mk_collapse thy ty = Sign.mk_const thy
    3.32 -    (@{const_name collapse}, [@{typ Random.seed}, ty]);
    3.33 -  fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    3.34 -  fun mk_split thy ty ty' = Sign.mk_const thy
    3.35 -    (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT (term_ty ty') @{typ Random.seed}]);
    3.36 -  fun mk_scomp_split thy ty ty' t t' =
    3.37 -    scomp (term_ty ty) (term_ty ty') @{typ Random.seed} t
    3.38 -      (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
    3.39 -  fun mk_cons thy this_ty (c, args) =
    3.40 -    let
    3.41 -      val tys = map (fst o fst) args;
    3.42 -      val c_ty = tys ---> this_ty;
    3.43 -      val c = Const (c, tys ---> this_ty);
    3.44 -      val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0);
    3.45 -      val c_indices = map (curry ( op + ) 1) t_indices;
    3.46 -      val c_t = list_comb (c, map Bound c_indices);
    3.47 -      val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term
    3.48 -        (list_comb (c, map (fn k => Bound (k + 1)) t_indices))
    3.49 -        |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t));
    3.50 -      val return = HOLogic.mk_return (term_ty this_ty) @{typ Random.seed}
    3.51 -        (HOLogic.mk_prod (c_t, t_t));
    3.52 -      val t = fold_rev (fn ((ty, _), random) =>
    3.53 -        mk_scomp_split thy ty this_ty random)
    3.54 -          args return;
    3.55 -      val is_rec = exists (snd o fst) args;
    3.56 -    in (is_rec, t) end;
    3.57 -  fun mk_conss thy ty [] = NONE
    3.58 -    | mk_conss thy ty [(_, t)] = SOME t
    3.59 -    | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $
    3.60 -          (Sign.mk_const thy (@{const_name Random.select}, [liftT (term_ty ty) @{typ Random.seed}]) $
    3.61 -            HOLogic.mk_list (liftT (term_ty ty) @{typ Random.seed}) (map snd ts)));
    3.62 -  fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = 
    3.63 -    let
    3.64 -      val SOME t_atom = mk_conss thy ty ts_atom;
    3.65 -    in case mk_conss thy ty ts_rec
    3.66 -     of SOME t_rec => mk_collapse thy (term_ty ty) $
    3.67 -          (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $
    3.68 -             @{term "i\<Colon>code_numeral"} $ t_rec $ t_atom)
    3.69 -      | NONE => t_atom
    3.70 -    end;
    3.71 -  fun mk_random_eqs thy vs tycos =
    3.72 -    let
    3.73 -      val this_ty = Type (hd tycos, map TFree vs);
    3.74 -      val this_ty' = liftT (term_ty this_ty) @{typ Random.seed};
    3.75 -      val random_name = Long_Name.base_name @{const_name random};
    3.76 -      val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
    3.77 -      fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
    3.78 -      val random' = Free (random'_name,
    3.79 -        @{typ code_numeral} --> @{typ code_numeral} --> this_ty');
    3.80 -      fun atom ty = if Sign.of_sort thy (ty, @{sort random})
    3.81 -        then ((ty, false), random ty $ @{term "j\<Colon>code_numeral"})
    3.82 -        else raise TYP
    3.83 -          ("Will not generate random elements for type(s) " ^ quote (hd tycos));
    3.84 -      fun dtyp tyco = ((this_ty, true), random' $ @{term "i\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"});
    3.85 -      fun rtyp (tyco, Ts) _ = raise REC
    3.86 -        ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos));
    3.87 -      val rhss = DatatypePackage.construction_interpretation thy
    3.88 -            { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos
    3.89 -        |> fst
    3.90 -        |> (map o apsnd o map) (mk_cons thy this_ty) 
    3.91 -        |> (map o apsnd) (List.partition fst)
    3.92 -        |> map (mk_clauses thy this_ty)
    3.93 -      val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
    3.94 -          (random' $ @{term "0\<Colon>code_numeral"} $ @{term "j\<Colon>code_numeral"}, Abs ("s", @{typ Random.seed},
    3.95 -            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))),
    3.96 -          (random' $ @{term "Suc_code_numeral i"} $ @{term "j\<Colon>code_numeral"}, rhs)
    3.97 -        ]))) rhss;
    3.98 -    in eqss end;
    3.99 -  fun random_inst [tyco] thy =
   3.100 -        let
   3.101 -          val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
   3.102 -          val vs = (map o apsnd)
   3.103 -            (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
   3.104 -          val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco;
   3.105 -          val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   3.106 -            (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\<Colon>code_numeral"},
   3.107 -               random' $ @{term "max (i\<Colon>code_numeral) 1"} $ @{term "i\<Colon>code_numeral"})
   3.108 -          val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
   3.109 -            (fn thm => Context.mapping (Code.del_eqn thm) I));
   3.110 -          fun add_code simps lthy =
   3.111 -            let
   3.112 -              val thy = ProofContext.theory_of lthy;
   3.113 -              val thm = @{thm random'_if}
   3.114 -                |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')]
   3.115 -                |> (fn thm => thm OF simps)
   3.116 -                |> singleton (ProofContext.export lthy (ProofContext.init thy));
   3.117 -              val c = (fst o dest_Const o fst o strip_comb o fst
   3.118 -                o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
   3.119 -            in
   3.120 -              lthy
   3.121 -              |> LocalTheory.theory (Code.del_eqns c
   3.122 -                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
   3.123 -                   #-> Code.add_eqn)
   3.124 -            end;
   3.125 -        in
   3.126 -          thy
   3.127 -          |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   3.128 -          |> PrimrecPackage.add_primrec
   3.129 -               [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
   3.130 -                 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
   3.131 -          |-> add_code
   3.132 -          |> `(fn lthy => Syntax.check_term lthy eq)
   3.133 -          |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   3.134 -          |> snd
   3.135 -          |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   3.136 -          |> LocalTheory.exit_global
   3.137 -        end
   3.138 -    | random_inst tycos thy = raise REC
   3.139 -        ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos));
   3.140 -  fun add_random_inst [@{type_name bool}] thy = thy
   3.141 -    | add_random_inst [@{type_name nat}] thy = thy
   3.142 -    | add_random_inst [@{type_name char}] thy = thy
   3.143 -    | add_random_inst [@{type_name String.literal}] thy = thy
   3.144 -    | add_random_inst tycos thy = random_inst tycos thy
   3.145 -        handle REC msg => (warning msg; thy)
   3.146 -             | TYP msg => (warning msg; thy)
   3.147 -in DatatypePackage.interpretation add_random_inst end
   3.148 -*}
   3.149 -
   3.150 -
   3.151 -subsection {* Examples *}
   3.152 -
   3.153 -theorem "map g (map f xs) = map (g o f) xs"
   3.154 -  quickcheck [generator = code]
   3.155 -  by (induct xs) simp_all
   3.156 -
   3.157 -theorem "map g (map f xs) = map (f o g) xs"
   3.158 -  quickcheck [generator = code]
   3.159 -  oops
   3.160 -
   3.161 -theorem "rev (xs @ ys) = rev ys @ rev xs"
   3.162 -  quickcheck [generator = code]
   3.163 -  by simp
   3.164 -
   3.165 -theorem "rev (xs @ ys) = rev xs @ rev ys"
   3.166 -  quickcheck [generator = code]
   3.167 -  oops
   3.168 -
   3.169 -theorem "rev (rev xs) = xs"
   3.170 -  quickcheck [generator = code]
   3.171 -  by simp
   3.172 -
   3.173 -theorem "rev xs = xs"
   3.174 -  quickcheck [generator = code]
   3.175 -  oops
   3.176 -
   3.177 -primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
   3.178 -  "app [] x = x"
   3.179 -  | "app (f # fs) x = app fs (f x)"
   3.180 -
   3.181 -lemma "app (fs @ gs) x = app gs (app fs x)"
   3.182 -  quickcheck [generator = code]
   3.183 -  by (induct fs arbitrary: x) simp_all
   3.184 -
   3.185 -lemma "app (fs @ gs) x = app fs (app gs x)"
   3.186 -  quickcheck [generator = code]
   3.187 -  oops
   3.188 -
   3.189 -primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
   3.190 -  "occurs a [] = 0"
   3.191 -  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
   3.192 -
   3.193 -primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   3.194 -  "del1 a [] = []"
   3.195 -  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
   3.196 -
   3.197 -lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   3.198 -  -- {* Wrong. Precondition needed.*}
   3.199 -  quickcheck [generator = code]
   3.200 -  oops
   3.201 -
   3.202 -lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   3.203 -  quickcheck [generator = code]
   3.204 -    -- {* Also wrong.*}
   3.205 -  oops
   3.206 -
   3.207 -lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   3.208 -  quickcheck [generator = code]
   3.209 -  by (induct xs) auto
   3.210 -
   3.211 -primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   3.212 -  "replace a b [] = []"
   3.213 -  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
   3.214 -                            else (x#(replace a b xs)))"
   3.215 -
   3.216 -lemma "occurs a xs = occurs b (replace a b xs)"
   3.217 -  quickcheck [generator = code]
   3.218 -  -- {* Wrong. Precondition needed.*}
   3.219 -  oops
   3.220 -
   3.221 -lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
   3.222 -  quickcheck [generator = code]
   3.223 -  by (induct xs) simp_all
   3.224 -
   3.225 -
   3.226 -subsection {* Trees *}
   3.227 -
   3.228 -datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   3.229 -
   3.230 -primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   3.231 -  "leaves Twig = []"
   3.232 -  | "leaves (Leaf a) = [a]"
   3.233 -  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
   3.234 -
   3.235 -primrec plant :: "'a list \<Rightarrow> 'a tree" where
   3.236 -  "plant [] = Twig "
   3.237 -  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
   3.238 -
   3.239 -primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   3.240 -  "mirror (Twig) = Twig "
   3.241 -  | "mirror (Leaf a) = Leaf a "
   3.242 -  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   3.243 -
   3.244 -theorem "plant (rev (leaves xt)) = mirror xt"
   3.245 -  quickcheck [generator = code]
   3.246 -    --{* Wrong! *} 
   3.247 -  oops
   3.248 -
   3.249 -theorem "plant (leaves xt @ leaves yt) = Branch xt yt"
   3.250 -  quickcheck [generator = code]
   3.251 -    --{* Wrong! *} 
   3.252 -  oops
   3.253 -
   3.254 -datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   3.255 -
   3.256 -primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   3.257 -  "inOrder (Tip a)= [a]"
   3.258 -  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   3.259 -
   3.260 -primrec root :: "'a ntree \<Rightarrow> 'a" where
   3.261 -  "root (Tip a) = a"
   3.262 -  | "root (Node f x y) = f"
   3.263 -
   3.264 -theorem "hd (inOrder xt) = root xt"
   3.265 -  quickcheck [generator = code]
   3.266 -    --{* Wrong! *} 
   3.267 -  oops
   3.268 -
   3.269 -lemma "int (f k) = k"
   3.270 -  quickcheck [generator = code]
   3.271 -  oops
   3.272 -
   3.273 -lemma "int (nat k) = k"
   3.274 -  quickcheck [generator = code]
   3.275 -  oops
   3.276 -
   3.277 -end
     4.1 --- a/src/HOL/ex/ROOT.ML	Tue Jun 09 22:59:53 2009 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Tue Jun 09 22:59:54 2009 +0200
     4.3 @@ -9,7 +9,6 @@
     4.4    "FuncSet",
     4.5    "Word",
     4.6    "Eval_Examples",
     4.7 -  "Quickcheck_Generators",
     4.8    "Codegenerator_Test",
     4.9    "Codegenerator_Pretty_Test",
    4.10    "NormalForm",