separated Random.thy from Quickcheck.thy
authorhaftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 262654b63b9e9b10d
parent 26264 89e25cc8da7a
child 26266 35ae83ca190a
separated Random.thy from Quickcheck.thy
src/HOL/IsaMakefile
src/HOL/ex/Quickcheck.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/Random.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 12 19:38:13 2008 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 12 19:38:14 2008 +0100
     1.3 @@ -674,7 +674,7 @@
     1.4    ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
     1.5    ex/BT.thy ex/BinEx.thy ex/CTL.thy \
     1.6    ex/Chinese.thy ex/Classical.thy ex/Dense_Linear_Order_Ex.thy \
     1.7 -  ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
     1.8 +  ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy \
     1.9    ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
    1.10    ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy ex/Hex_Bin_Examples.thy \
    1.11    ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Quickcheck.thy	Wed Mar 12 19:38:14 2008 +0100
     2.3 @@ -0,0 +1,383 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Florian Haftmann, TU Muenchen
     2.6 +*)
     2.7 +
     2.8 +header {* A simple counterexample generator *}
     2.9 +
    2.10 +theory Quickcheck
    2.11 +imports Random Eval
    2.12 +begin
    2.13 +
    2.14 +subsection {* The @{text random} class *}
    2.15 +
    2.16 +class random = type +
    2.17 +  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
    2.18 +
    2.19 +print_classes
    2.20 +
    2.21 +instantiation itself :: (type) random
    2.22 +begin
    2.23 +
    2.24 +definition
    2.25 +  "random _ = return TYPE('a)"
    2.26 +
    2.27 +instance ..
    2.28 +
    2.29 +end
    2.30 +
    2.31 +lemma random_aux_if:
    2.32 +  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
    2.33 +  assumes "random' 0 j = undefined"
    2.34 +    and "\<And>i. random' (Suc_index i) j = rhs2 i"
    2.35 +  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
    2.36 +  by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun)
    2.37 +
    2.38 +setup {*
    2.39 +let
    2.40 +  exception REC;
    2.41 +  fun random_inst tyco thy =
    2.42 +    let
    2.43 +      val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
    2.44 +      val _ = if length descr > 1 then raise REC else ();
    2.45 +      val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
    2.46 +      val vs = (map o apsnd)
    2.47 +        (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
    2.48 +      val ty = Type (tyco, map TFree vs);
    2.49 +      val typ_of = DatatypeAux.typ_of_dtyp descr vs;
    2.50 +      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
    2.51 +      val randomN = NameSpace.base @{const_name random};
    2.52 +      val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";
    2.53 +      fun lift_ty ty = StateMonad.liftT ty @{typ seed};
    2.54 +      val ty_aux = @{typ index} --> @{typ index} --> lift_ty ty;
    2.55 +      fun random ty =
    2.56 +        Const (@{const_name random}, @{typ index} --> lift_ty ty);
    2.57 +      val random_aux = Free (random_aux_name, ty_aux);
    2.58 +      fun add_cons_arg dty (is_rec, t) =
    2.59 +        let
    2.60 +          val ty' = typ_of dty;
    2.61 +          val rec_call = case try DatatypeAux.dest_DtRec dty
    2.62 +           of SOME index' => index = index'
    2.63 +            | NONE => false
    2.64 +          val random' = if rec_call
    2.65 +            then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}
    2.66 +            else random ty' $ @{term "j\<Colon>index"}
    2.67 +          val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;
    2.68 +          val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))
    2.69 +        in (is_rec', t') end;
    2.70 +      fun mk_cons_t (c, dtys) =
    2.71 +        let
    2.72 +          val ty' = map typ_of dtys ---> ty;
    2.73 +          val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),
    2.74 +            map Bound (length dtys - 1 downto 0)));
    2.75 +          val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);
    2.76 +        in (is_rec, StateMonad.run ty @{typ seed} t') end;
    2.77 +      fun check_empty [] = NONE
    2.78 +        | check_empty xs = SOME xs;
    2.79 +      fun bundle_cons_ts cons_ts =
    2.80 +        let
    2.81 +          val ts = map snd cons_ts;
    2.82 +          val t = HOLogic.mk_list (lift_ty ty) ts;
    2.83 +          val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) --> lift_ty (lift_ty ty)) $ t;
    2.84 +          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
    2.85 +        in t'' end;
    2.86 +      fun bundle_conss (some_rec_t, nonrec_t) =
    2.87 +        let
    2.88 +          val t = case some_rec_t
    2.89 +           of SOME rec_t => Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty)
    2.90 +               $ (Const (@{const_name select_default},
    2.91 +                   @{typ index} --> lift_ty ty --> lift_ty ty --> lift_ty (lift_ty ty))
    2.92 +                  $ @{term "i\<Colon>index"} $ rec_t $ nonrec_t)
    2.93 +            | NONE => nonrec_t
    2.94 +        in t end;
    2.95 +      val random_rhs = constrs
    2.96 +        |> map mk_cons_t 
    2.97 +        |> List.partition fst
    2.98 +        |> apfst (Option.map bundle_cons_ts o check_empty)
    2.99 +        |> apsnd bundle_cons_ts
   2.100 +        |> bundle_conss;
   2.101 +      val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   2.102 +        (random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))
   2.103 +      val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   2.104 +        (random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);
   2.105 +      val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},
   2.106 +        @{typ index} --> lift_ty ty) $ @{term "i\<Colon>index"},
   2.107 +          random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});
   2.108 +      val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
   2.109 +        (fn thm => Context.mapping (Code.del_func thm) I));
   2.110 +      fun add_code simps lthy =
   2.111 +        let
   2.112 +          val thy = ProofContext.theory_of lthy;
   2.113 +          val thm = @{thm random_aux_if}
   2.114 +            |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]
   2.115 +            |> (fn thm => thm OF simps)
   2.116 +            |> singleton (ProofContext.export lthy (ProofContext.init thy))
   2.117 +        in
   2.118 +          lthy
   2.119 +          |> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)
   2.120 +               #-> Code.add_func)
   2.121 +        end;
   2.122 +    in
   2.123 +      thy
   2.124 +      |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   2.125 +      |> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]
   2.126 +           [(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]
   2.127 +      |-> add_code
   2.128 +      |> `(fn lthy => Syntax.check_term lthy random_eq)
   2.129 +      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
   2.130 +      |> snd
   2.131 +      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   2.132 +      |> LocalTheory.exit
   2.133 +      |> ProofContext.theory_of
   2.134 +    end;
   2.135 +  fun add_random_inst [tyco] = (fn thy => random_inst tyco thy handle REC =>
   2.136 +        (warning ("Will not generated random elements for mutual recursive type " ^ quote tyco); thy))
   2.137 +    | add_random_inst tycos = tap (fn _ => warning
   2.138 +        ("Will not generated random elements for mutual recursive type(s) " ^ commas (map quote tycos)));
   2.139 +in DatatypePackage.interpretation add_random_inst end
   2.140 +*}
   2.141 +
   2.142 +instantiation int :: random
   2.143 +begin
   2.144 +
   2.145 +definition
   2.146 +  "random n = (do
   2.147 +     (b, m) \<leftarrow> random n;
   2.148 +     return (if b then int m else - int m)
   2.149 +   done)"
   2.150 +
   2.151 +instance ..
   2.152 +
   2.153 +end
   2.154 +
   2.155 +instantiation set :: (random) random
   2.156 +begin
   2.157 +
   2.158 +primrec random_set' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a set \<times> seed" where
   2.159 +  "random_set' 0 j = undefined"
   2.160 +  | "random_set' (Suc_index i) j = collapse (select_default i
   2.161 +       (do x \<leftarrow> random i; xs \<leftarrow> random_set' i j; return (insert x xs) done)
   2.162 +       (return {}))"
   2.163 +
   2.164 +lemma random_set'_code [code func]:
   2.165 +  "random_set' i j s = (if i = 0 then undefined else collapse (select_default (i - 1)
   2.166 +       (do x \<leftarrow> random (i - 1); xs \<leftarrow> random_set' (i - 1) j; return (insert x xs) done)
   2.167 +       (return {})) s)"
   2.168 +  by (rule random_aux_if random_set'.simps)+
   2.169 +
   2.170 +definition
   2.171 +  "random i = random_set' i i"
   2.172 +
   2.173 +instance ..
   2.174 +
   2.175 +end
   2.176 +
   2.177 +code_reserved SML Quickcheck
   2.178 +
   2.179 +
   2.180 +subsection {* Quickcheck generator *}
   2.181 +
   2.182 +ML {*
   2.183 +structure Quickcheck =
   2.184 +struct
   2.185 +
   2.186 +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   2.187 +
   2.188 +fun mk_generator_expr prop tys =
   2.189 +  let
   2.190 +    val bounds = map_index (fn (i, ty) => (i, ty)) tys;
   2.191 +    val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
   2.192 +    val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds;
   2.193 +    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
   2.194 +      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);
   2.195 +    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
   2.196 +    fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
   2.197 +    fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
   2.198 +      --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
   2.199 +      $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
   2.200 +        $ Bound i) $ Abs ("a", ty, t);
   2.201 +    val t = fold_rev mk_bindclause bounds (return $ check);
   2.202 +  in Abs ("n", @{typ index}, t) end;
   2.203 +
   2.204 +fun compile_generator_expr thy prop tys =
   2.205 +  let
   2.206 +    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
   2.207 +      (mk_generator_expr prop tys) [];
   2.208 +  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
   2.209 +
   2.210 +fun VALUE prop tys thy =
   2.211 +  let
   2.212 +    val t = mk_generator_expr prop tys;
   2.213 +    val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t)
   2.214 +  in
   2.215 +    thy
   2.216 +    |> TheoryTarget.init NONE
   2.217 +    |> Specification.definition (NONE, (("", []), eq))
   2.218 +    |> snd
   2.219 +    |> LocalTheory.exit
   2.220 +    |> ProofContext.theory_of
   2.221 +  end;
   2.222 +
   2.223 +end
   2.224 +*}
   2.225 +
   2.226 +(*setup {* Quickcheck.VALUE @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
   2.227 +export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
   2.228 +use "~~/../../gen_code/quickcheck.ML"
   2.229 +ML {* Random_Engine.run (QuickcheckExample.range 1) *}*)
   2.230 +
   2.231 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.232 +  @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
   2.233 +
   2.234 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.235 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.236 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.237 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.238 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.239 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.240 +ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.241 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.242 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.243 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.244 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.245 +
   2.246 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.247 +  @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
   2.248 +
   2.249 +(*definition "FOO = (True, Suc 0)"
   2.250 +
   2.251 +code_module (test) QuickcheckExample
   2.252 +  file "~~/../../gen_code/quickcheck'.ML"
   2.253 +  contains FOO*)
   2.254 +
   2.255 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.256 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.257 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.258 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.259 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.260 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.261 +ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.262 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.263 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.264 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.265 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.266 +ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.267 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.268 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.269 +
   2.270 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.271 +  @{term "\<lambda>(xs\<Colon>int list) ys. rev (xs @ ys) = rev xs @ rev ys"}
   2.272 +  [@{typ "int list"}, @{typ "int list"}] *}
   2.273 +
   2.274 +ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.275 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.276 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.277 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.278 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.279 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.280 +ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.281 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.282 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.283 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.284 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.285 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.286 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.287 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.288 +ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.289 +ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.290 +ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.291 +ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.292 +
   2.293 +subsection {* Incremental function generator *}
   2.294 +
   2.295 +ML {*
   2.296 +structure Quickcheck =
   2.297 +struct
   2.298 +
   2.299 +open Quickcheck;
   2.300 +
   2.301 +fun random_fun (eq : 'a -> 'a -> bool)
   2.302 +    (random : Random_Engine.seed -> 'b * Random_Engine.seed)
   2.303 +    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
   2.304 +    (seed : Random_Engine.seed) =
   2.305 +  let
   2.306 +    val (seed', seed'') = random_split seed;
   2.307 +    val state = ref (seed', []);
   2.308 +    fun random_fun' x =
   2.309 +      let
   2.310 +        val (seed, fun_map) = ! state;
   2.311 +      in case AList.lookup (uncurry eq) fun_map x
   2.312 +       of SOME y => y
   2.313 +        | NONE => let
   2.314 +              val (y, seed') = random seed;
   2.315 +              val _ = state := (seed', (x, y) :: fun_map);
   2.316 +            in y end
   2.317 +      end;
   2.318 +  in (random_fun', seed'') end;
   2.319 +
   2.320 +end
   2.321 +*}
   2.322 +
   2.323 +axiomatization
   2.324 +  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
   2.325 +    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
   2.326 +
   2.327 +code_const random_fun_aux (SML "Quickcheck.random'_fun")
   2.328 +
   2.329 +instantiation "fun" :: (term_of, term_of) term_of
   2.330 +begin
   2.331 +
   2.332 +instance ..
   2.333 +
   2.334 +end
   2.335 +
   2.336 +code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
   2.337 +  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
   2.338 +
   2.339 +instantiation "fun" :: (eq, "{type, random}") random
   2.340 +begin
   2.341 +
   2.342 +definition
   2.343 +  "random n = random_fun_aux (op =) (random n) split_seed"
   2.344 +
   2.345 +instance ..
   2.346 +
   2.347 +end
   2.348 +
   2.349 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.350 +  @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
   2.351 +
   2.352 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.353 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.354 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.355 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.356 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.357 +ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.358 +
   2.359 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.360 +  @{term "\<lambda>(A \<Colon> nat set) B. card (A \<union> B) = card A + card B"} [@{typ "nat set"}, @{typ "nat set"}] *}
   2.361 +
   2.362 +ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.363 +ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.364 +ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.365 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.366 +ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.367 +ML {* f 6 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.368 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.369 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.370 +
   2.371 +ML {* val f = Quickcheck.compile_generator_expr @{theory}
   2.372 +  @{term "\<lambda>(s \<Colon> string). s \<noteq> rev s"} [@{typ string}] *}
   2.373 +
   2.374 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.375 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.376 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.377 +ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.378 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.379 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.380 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.381 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.382 +ML {* f 10 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.383 +ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.384 +ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   2.385 +
   2.386 +end
     3.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 12 19:38:13 2008 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 12 19:38:14 2008 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4    "FuncSet",
     3.5    "Word",
     3.6    "Eval_Examples",
     3.7 -  "Random"
     3.8 +  "Quickcheck"
     3.9  ];
    3.10  
    3.11  no_document use_thy "Codegenerator";
     4.1 --- a/src/HOL/ex/Random.thy	Wed Mar 12 19:38:13 2008 +0100
     4.2 +++ b/src/HOL/ex/Random.thy	Wed Mar 12 19:38:14 2008 +0100
     4.3 @@ -2,30 +2,75 @@
     4.4      Author:     Florian Haftmann, TU Muenchen
     4.5  *)
     4.6  
     4.7 -header {* A simple term generator *}
     4.8 +header {* A HOL random engine *}
     4.9  
    4.10  theory Random
    4.11 -imports State_Monad Code_Index List Eval
    4.12 +imports State_Monad Code_Index
    4.13  begin
    4.14  
    4.15 -subsection {* The random engine *}
    4.16 +subsection {* Auxiliary functions *}
    4.17 +
    4.18 +definition
    4.19 +  inc_shift :: "index \<Rightarrow> index \<Rightarrow> index"
    4.20 +where
    4.21 +  "inc_shift v k = (if v = k then 1 else k + 1)"
    4.22 +
    4.23 +definition
    4.24 +  minus_shift :: "index \<Rightarrow> index \<Rightarrow> index \<Rightarrow> index"
    4.25 +where
    4.26 +  "minus_shift r k l = (if k < l then r + k - l else k - l)"
    4.27 +
    4.28 +function
    4.29 +  log :: "index \<Rightarrow> index \<Rightarrow> index"
    4.30 +where
    4.31 +  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"
    4.32 +by pat_completeness auto
    4.33 +termination
    4.34 +  by (relation "measure (nat_of_index o snd)")
    4.35 +    (auto simp add: index)
    4.36 +
    4.37 +
    4.38 +subsection {* Random seeds *}
    4.39  
    4.40  types seed = "index \<times> index"
    4.41  
    4.42 -definition
    4.43 +primrec
    4.44    "next" :: "seed \<Rightarrow> index \<times> seed"
    4.45  where
    4.46 -  "next s = (let
    4.47 -     (v, w) = s;
    4.48 -     k = v div 53668;
    4.49 -     v' = 40014 * (v - k * 53668) - k * 12211;
    4.50 -     v'' = (if v' < 0 then v' + 2147483563 else v');
    4.51 -     l = w div 52774;
    4.52 -     w' = 40692 * (w - l * 52774) - l * 3791;
    4.53 -     w'' = (if w' < 0 then w' + 2147483399 else w');
    4.54 -     z = v'' - w'';
    4.55 -     z' = (if z < 1 then z + 2147483562 else z)
    4.56 -   in (z',  (v'', w'')))"
    4.57 +  "next (v, w) = (let
    4.58 +     k =  v div 53668;
    4.59 +     v' = minus_shift 2147483563 (40014 * (v mod 53668)) (k * 12211);
    4.60 +     l =  w div 52774;
    4.61 +     w' = minus_shift 2147483399 (40692 * (w mod 52774)) (l * 3791);
    4.62 +     z =  minus_shift 2147483562 v' (w' + 1) + 1
    4.63 +   in (z, (v', w')))"
    4.64 +
    4.65 +lemma next_not_0:
    4.66 +  "fst (next s) \<noteq> 0"
    4.67 +apply (cases s)
    4.68 +apply (auto simp add: minus_shift_def Let_def)
    4.69 +done
    4.70 +
    4.71 +primrec
    4.72 +  seed_invariant :: "seed \<Rightarrow> bool"
    4.73 +where
    4.74 +  "seed_invariant (v, w) \<longleftrightarrow> 0 < v \<and> v < 9438322952 \<and> 0 < w \<and> True"
    4.75 +
    4.76 +lemma if_same:
    4.77 +  "(if b then f x else f y) = f (if b then x else y)"
    4.78 +  by (cases b) simp_all
    4.79 +
    4.80 +(*lemma seed_invariant:
    4.81 +  assumes "seed_invariant (index_of_nat v, index_of_nat w)"
    4.82 +    and "(index_of_nat z, (index_of_nat v', index_of_nat w')) = next (index_of_nat v, index_of_nat w)"
    4.83 +  shows "seed_invariant (index_of_nat v', index_of_nat w')"
    4.84 +using assms
    4.85 +apply (auto simp add: seed_invariant_def)
    4.86 +apply (auto simp add: minus_shift_def Let_def)
    4.87 +apply (simp_all add: if_same cong del: if_cong)
    4.88 +apply safe
    4.89 +unfolding not_less
    4.90 +oops*)
    4.91  
    4.92  definition
    4.93    split_seed :: "seed \<Rightarrow> seed \<times> seed"
    4.94 @@ -33,27 +78,14 @@
    4.95    "split_seed s = (let
    4.96       (v, w) = s;
    4.97       (v', w') = snd (next s);
    4.98 -     v'' = (if v = 2147483562 then 1 else v + 1);
    4.99 +     v'' = inc_shift 2147483562 v;
   4.100       s'' = (v'', w');
   4.101 -     w'' = (if w = 2147483398 then 1 else w + 1);
   4.102 +     w'' = inc_shift 2147483398 w;
   4.103       s''' = (v', w'')
   4.104     in (s'', s'''))"
   4.105  
   4.106 -text {* Base selectors *}
   4.107  
   4.108 -primrec
   4.109 -  pick :: "(index \<times> 'a) list \<Rightarrow> index \<Rightarrow> 'a"
   4.110 -where
   4.111 -  "pick (x#xs) n = (if n < fst x then snd x else pick xs (n - fst x))"
   4.112 -
   4.113 -function
   4.114 -  iLogBase :: "index \<Rightarrow> index \<Rightarrow> index"
   4.115 -where
   4.116 -  "iLogBase b i = (if b \<le> 1 \<or> i < b then 1 else 1 + iLogBase b (i div b))"
   4.117 -by pat_completeness auto
   4.118 -termination
   4.119 -  by (relation "measure (nat_of_index o snd)")
   4.120 -    (auto simp add: index)
   4.121 +subsection {* Base selectors *}
   4.122  
   4.123  function
   4.124    range_aux :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
   4.125 @@ -69,122 +101,94 @@
   4.126  definition
   4.127    range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed"
   4.128  where
   4.129 -  "range k s = (let
   4.130 -    b = 2147483561;
   4.131 -    n = iLogBase b k;
   4.132 -    (v, s') = range_aux n 1 s
   4.133 -  in (v mod k, s'))"
   4.134 +  "range k = (do
   4.135 +     v \<leftarrow> range_aux (log 2147483561 k) 1;
   4.136 +     return (v mod k)
   4.137 +   done)"
   4.138 +
   4.139 +lemma range:
   4.140 +  assumes "k > 0"
   4.141 +  shows "fst (range k s) < k"
   4.142 +proof -
   4.143 +  obtain v w where range_aux:
   4.144 +    "range_aux (log 2147483561 k) 1 s = (v, w)"
   4.145 +    by (cases "range_aux (log 2147483561 k) 1 s")
   4.146 +  with assms show ?thesis
   4.147 +    by (simp add: range_def run_def mbind_def split_def del: range_aux.simps log.simps)
   4.148 +qed
   4.149  
   4.150  definition
   4.151    select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.152  where
   4.153 -  [simp]: "select xs s = (let
   4.154 -    (k, s') = range (index_of_nat (length xs)) s
   4.155 -  in (nth xs (nat_of_index k), s'))"
   4.156 +  "select xs = (do
   4.157 +     k \<leftarrow> range (index_of_nat (length xs));
   4.158 +     return (nth xs (nat_of_index k))
   4.159 +   done)"
   4.160 +
   4.161 +lemma select:
   4.162 +  assumes "xs \<noteq> []"
   4.163 +  shows "fst (select xs s) \<in> set xs"
   4.164 +proof -
   4.165 +  from assms have "index_of_nat (length xs) > 0" by simp
   4.166 +  with range have
   4.167 +    "fst (range (index_of_nat (length xs)) s) < index_of_nat (length xs)" by best
   4.168 +  then have
   4.169 +    "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
   4.170 +  then show ?thesis
   4.171 +    by (auto simp add: select_def run_def mbind_def split_def)
   4.172 +qed
   4.173  
   4.174  definition
   4.175 -  select_weight :: "(index \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.176 +  select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.177  where
   4.178 -  [simp]: "select_weight xs s = (let
   4.179 -    (k, s') = range (foldr (op + \<circ> fst) xs 0) s
   4.180 -  in (pick xs k, s'))"
   4.181 +  [code func del]: "select_default k x y = (do
   4.182 +     l \<leftarrow> range k;
   4.183 +     return (if l + 1 < k then x else y)
   4.184 +   done)"
   4.185 +
   4.186 +lemma select_default_zero:
   4.187 +  "fst (select_default 0 x y s) = y"
   4.188 +  by (simp add: run_def mbind_def split_def select_default_def)
   4.189  
   4.190 -(*lemma
   4.191 -  "select (x#xs) s = select_weight (map (Pair 1) (x#xs)) s"
   4.192 -proof (induct xs)
   4.193 -  case Nil show ?case apply (auto simp add: Let_def split_def) 
   4.194 +lemma select_default_code [code]:
   4.195 +  "select_default k x y = (if k = 0 then do
   4.196 +     _ \<leftarrow> range 1;
   4.197 +     return y
   4.198 +   done else do
   4.199 +     l \<leftarrow> range k;
   4.200 +     return (if l + 1 < k then x else y)
   4.201 +   done)"
   4.202 +proof (cases "k = 0")
   4.203 +  case False then show ?thesis by (simp add: select_default_def)
   4.204  next
   4.205 -  have map_fst_Pair: "!!xs y. map fst (map (Pair y) xs) = replicate (length xs) y"
   4.206 -  proof -
   4.207 -    fix xs
   4.208 -    fix y
   4.209 -    show "map fst (map (Pair y) xs) = replicate (length xs) y"
   4.210 -      by (induct xs) simp_all
   4.211 -  qed
   4.212 -  have pick_nth: "!!xs n. n < length xs \<Longrightarrow> pick (map (Pair 1) xs) n = nth xs n"
   4.213 -  proof -
   4.214 -    fix xs
   4.215 -    fix n
   4.216 -    assume "n < length xs"
   4.217 -    then show "pick (map (Pair 1) xs) n = nth xs n"
   4.218 -    proof (induct xs arbitrary: n)
   4.219 -      case Nil then show ?case by simp
   4.220 -    next
   4.221 -      case (Cons x xs) show ?case
   4.222 -      proof (cases n)
   4.223 -        case 0 then show ?thesis by simp
   4.224 -      next
   4.225 -        case (Suc _)
   4.226 -    from Cons have "n < length (x # xs)" by auto
   4.227 -        then have "n < Suc (length xs)" by simp
   4.228 -        with Suc have "n - 1 < Suc (length xs) - 1" by auto
   4.229 -        with Cons have "pick (map (Pair (1\<Colon>nat)) xs) (n - 1) = xs ! (n - 1)" by auto
   4.230 -        with Suc show ?thesis by auto
   4.231 -      qed
   4.232 -    qed
   4.233 -  qed
   4.234 -  have sum_length: "!!xs. foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
   4.235 -  proof -
   4.236 -    have replicate_append:
   4.237 -      "!!x xs y. replicate (length (x # xs)) y = replicate (length xs) y @ [y]"
   4.238 -      by (simp add: replicate_app_Cons_same)
   4.239 -    fix xs
   4.240 -    show "foldl (op +) 0 (map fst (map (Pair 1) xs)) = length xs"
   4.241 -    unfolding map_fst_Pair proof (induct xs)
   4.242 -      case Nil show ?case by simp
   4.243 -    next
   4.244 -      case (Cons x xs) then show ?case unfolding replicate_append by simp
   4.245 -    qed
   4.246 -  qed
   4.247 -  have pick_nth_random:
   4.248 -    "!!x xs s. pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))"
   4.249 -  proof -
   4.250 -    fix s
   4.251 -    fix x
   4.252 -    fix xs
   4.253 -    have bound: "fst (random (length (x#xs)) s) < length (x#xs)" by (rule random_bound) simp
   4.254 -    from pick_nth [OF bound] show
   4.255 -      "pick (map (Pair 1) (x#xs)) (fst (random (length (x#xs)) s)) = nth (x#xs) (fst (random (length (x#xs)) s))" .
   4.256 -  qed
   4.257 -  have pick_nth_random_do:
   4.258 -    "!!x xs s. (do n \<leftarrow> random (length (x#xs)); return (pick (map (Pair 1) (x#xs)) n) done) s =
   4.259 -      (do n \<leftarrow> random (length (x#xs)); return (nth (x#xs) n) done) s"
   4.260 -  unfolding monad_collapse split_def unfolding pick_nth_random ..
   4.261 -  case (Cons x xs) then show ?case
   4.262 -    unfolding select_weight_def sum_length pick_nth_random_do
   4.263 -    by simp
   4.264 -qed*)
   4.265 +  case True then show ?thesis
   4.266 +    by (simp add: run_def mbind_def split_def select_default_def expand_fun_eq range_def)
   4.267 +qed
   4.268  
   4.269 -text {* The @{text ML} interface *}
   4.270 +
   4.271 +subsection {* @{text ML} interface *}
   4.272  
   4.273  ML {*
   4.274 -structure Quickcheck =
   4.275 +structure Random_Engine =
   4.276  struct
   4.277  
   4.278  type seed = int * int;
   4.279  
   4.280  local
   4.281  
   4.282 -val seed = ref (0, 0);
   4.283 -
   4.284 -fun init () =
   4.285 -  let
   4.286 -    val now = Time.toNanoseconds (Time.now ());
   4.287 +val seed = ref 
   4.288 +  (let
   4.289 +    val now = Time.toMilliseconds (Time.now ());
   4.290      val (q, s1) = IntInf.divMod (now, 2147483562);
   4.291      val s2 = q mod 2147483398;
   4.292 -  in seed := (s1 + 1, s2 + 1) end;
   4.293 -  
   4.294 +  in (s1 + 1, s2 + 1) end);
   4.295 +
   4.296  in
   4.297  
   4.298 -val seed = seed; (* FIXME *)
   4.299 -
   4.300  fun run f =
   4.301    let
   4.302 -    val (x, seed') = f (!seed);
   4.303 +    val (x, seed') = f (! seed);
   4.304      val _ = seed := seed'
   4.305 -    val _ = if fst (! seed) = 0 orelse snd (! seed) = 0 then
   4.306 -      (warning "broken random seed"; init ())
   4.307 -      else ()
   4.308    in x end;
   4.309  
   4.310  end;
   4.311 @@ -192,325 +196,4 @@
   4.312  end;
   4.313  *}
   4.314  
   4.315 -
   4.316 -subsection {* The @{text random} class *}
   4.317 -
   4.318 -class random =
   4.319 -  fixes random :: "index \<Rightarrow> seed \<Rightarrow> 'a\<Colon>{} \<times> seed"
   4.320 -
   4.321 -instantiation itself :: (type) random
   4.322 -begin
   4.323 -
   4.324 -definition
   4.325 -  "random _ = return TYPE('a)"
   4.326 -
   4.327 -instance ..
   4.328 -
   4.329  end
   4.330 -
   4.331 -lemma random_aux_if:
   4.332 -  fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
   4.333 -  assumes "random' 0 j = undefined"
   4.334 -    and "\<And>i. random' (Suc_index i) j = rhs2 i"
   4.335 -  shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
   4.336 -  by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun)
   4.337 -
   4.338 -setup {*
   4.339 -let
   4.340 -  fun random_inst tyco thy =
   4.341 -    let
   4.342 -      val { descr, index, ... } = DatatypePackage.the_datatype thy tyco;
   4.343 -      val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco;
   4.344 -      val vs = (map o apsnd)
   4.345 -        (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs;
   4.346 -      val ty = Type (tyco, map TFree vs);
   4.347 -      val typ_of = DatatypeAux.typ_of_dtyp descr vs;
   4.348 -      val SOME (_, _, constrs) = AList.lookup (op =) descr index;
   4.349 -      val randomN = NameSpace.base @{const_name random};
   4.350 -      val random_aux_name = randomN ^ "_" ^ Class.type_name tyco ^ "'";
   4.351 -      fun lift_ty ty = StateMonad.liftT ty @{typ seed};
   4.352 -      val ty_aux = @{typ index} --> @{typ index} --> lift_ty ty;
   4.353 -      fun random ty =
   4.354 -        Const (@{const_name random}, @{typ index} --> lift_ty ty);
   4.355 -      val random_aux = Free (random_aux_name, ty_aux);
   4.356 -      fun add_cons_arg dty (is_rec, t) =
   4.357 -        let
   4.358 -          val ty' = typ_of dty;
   4.359 -          val random' = if can DatatypeAux.dest_DtRec dty
   4.360 -            then random_aux $ @{term "i\<Colon>index"} $ @{term "j\<Colon>index"}
   4.361 -            else random ty' $ @{term "j\<Colon>index"}
   4.362 -          val is_rec' = is_rec orelse DatatypeAux.is_rec_type dty;
   4.363 -          val t' = StateMonad.mbind ty' ty @{typ seed} random' (Abs ("", ty', t))
   4.364 -        in (is_rec', t') end;
   4.365 -      fun mk_cons_t (c, dtys) =
   4.366 -        let
   4.367 -          val ty' = map typ_of dtys ---> ty;
   4.368 -          val t = StateMonad.return ty @{typ seed} (list_comb (Const (c, ty'),
   4.369 -            map Bound (length dtys - 1 downto 0)));
   4.370 -          val (is_rec, t') = fold_rev add_cons_arg dtys (false, t);
   4.371 -        in (is_rec, StateMonad.run ty @{typ seed} t') end;
   4.372 -      fun check_empty [] = NONE
   4.373 -        | check_empty xs = SOME xs;
   4.374 -      fun bundle_cons_ts cons_ts =
   4.375 -        let
   4.376 -          val ts = map snd cons_ts;
   4.377 -          val t = HOLogic.mk_list (lift_ty ty) ts;
   4.378 -          val t' = Const (@{const_name select}, HOLogic.listT (lift_ty ty) --> lift_ty (lift_ty ty)) $ t;
   4.379 -          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
   4.380 -        in t'' end;
   4.381 -      fun bundle_conss (some_rec_t, nonrec_t) =
   4.382 -        let
   4.383 -          val rec' = case some_rec_t
   4.384 -           of SOME rec_t => SOME (HOLogic.mk_prod (@{term "i\<Colon>index"}, rec_t))
   4.385 -            | NONE => NONE;
   4.386 -          val nonrec' = HOLogic.mk_prod (@{term "1\<Colon>index"}, nonrec_t);
   4.387 -          val i_ty = HOLogic.mk_prodT (@{typ index}, lift_ty ty);
   4.388 -          val t = HOLogic.mk_list i_ty (the_list rec' @ single nonrec');
   4.389 -          val t' = Const (@{const_name select_weight}, HOLogic.listT i_ty --> lift_ty (lift_ty ty)) $ t;
   4.390 -          val t'' = Const (@{const_name collapse}, lift_ty (lift_ty ty) --> lift_ty ty) $ t';
   4.391 -        in t'' end;
   4.392 -      val random_rhs = constrs
   4.393 -        |> map mk_cons_t 
   4.394 -        |> List.partition fst
   4.395 -        |> apfst (Option.map bundle_cons_ts o check_empty)
   4.396 -        |> apsnd bundle_cons_ts
   4.397 -        |> bundle_conss;
   4.398 -      val random_aux_undef = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   4.399 -        (random_aux $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, lift_ty ty))
   4.400 -      val random_aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
   4.401 -        (random_aux $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, random_rhs);
   4.402 -      val random_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (Const (@{const_name random},
   4.403 -        @{typ index} --> lift_ty ty) $ @{term "i\<Colon>index"},
   4.404 -          random_aux $ @{term "i\<Colon>index"} $ @{term "i\<Colon>index"});
   4.405 -      val del_func = Attrib.internal (fn _ => Thm.declaration_attribute
   4.406 -        (fn thm => Context.mapping (Code.del_func thm) I));
   4.407 -      fun add_code simps lthy =
   4.408 -        let
   4.409 -          val thy = ProofContext.theory_of lthy;
   4.410 -          val thm = @{thm random_aux_if}
   4.411 -            |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] [SOME (Thm.cterm_of thy random_aux)]
   4.412 -            |> (fn thm => thm OF simps)
   4.413 -            |> singleton (ProofContext.export lthy (ProofContext.init thy))
   4.414 -        in
   4.415 -          lthy
   4.416 -          |> LocalTheory.theory (PureThy.note Thm.internalK (random_aux_name ^ "_code", thm)
   4.417 -               #-> Code.add_func)
   4.418 -        end;
   4.419 -    in
   4.420 -      thy
   4.421 -      |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
   4.422 -      |> PrimrecPackage.add_primrec [(random_aux_name, SOME ty_aux, NoSyn)]
   4.423 -           [(("", [del_func]), random_aux_undef), (("", [del_func]), random_aux_eq)]
   4.424 -      |-> add_code
   4.425 -      |> `(fn lthy => Syntax.check_term lthy random_eq)
   4.426 -      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
   4.427 -      |> snd
   4.428 -      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   4.429 -      |> LocalTheory.exit
   4.430 -      |> ProofContext.theory_of
   4.431 -    end;
   4.432 -  fun add_random_inst [tyco] = (fn thy => case try (random_inst tyco) thy
   4.433 -       of SOME thy => thy
   4.434 -        | NONE => (warning ("Failed to generate random elements for type" ^ tyco); thy))
   4.435 -    | add_random_inst tycos = tap (fn _ => warning
   4.436 -        ("Will not generated random elements for mutual recursive types " ^ commas (map quote tycos)));
   4.437 -in DatatypePackage.interpretation add_random_inst end
   4.438 -*}
   4.439 -
   4.440 -instantiation int :: random
   4.441 -begin
   4.442 -
   4.443 -definition
   4.444 -  "random n = (do
   4.445 -     (b, m) \<leftarrow> random n;
   4.446 -     return (if b then int m else - int m)
   4.447 -   done)"
   4.448 -
   4.449 -instance ..
   4.450 -
   4.451 -end
   4.452 -
   4.453 -code_reserved SML Quickcheck
   4.454 -
   4.455 -
   4.456 -subsection {* Quickcheck generator *}
   4.457 -
   4.458 -ML {*
   4.459 -structure Quickcheck =
   4.460 -struct
   4.461 -
   4.462 -open Quickcheck;
   4.463 -
   4.464 -val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
   4.465 -
   4.466 -fun mk_generator_expr prop tys =
   4.467 -  let
   4.468 -    val bounds = map_index (fn (i, ty) => (i, ty)) tys;
   4.469 -    val result = list_comb (prop, map (fn (i, _) => Bound (length tys - i - 1)) bounds);
   4.470 -    val terms = map (fn (i, ty) => Const (@{const_name Eval.term_of}, ty --> @{typ term}) $ Bound (length tys - i - 1)) bounds;
   4.471 -    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
   4.472 -      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ HOLogic.mk_list @{typ term} terms);
   4.473 -    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
   4.474 -    fun mk_bindtyp ty = @{typ seed} --> HOLogic.mk_prodT (ty, @{typ seed});
   4.475 -    fun mk_bindclause (i, ty) t = Const (@{const_name mbind}, mk_bindtyp ty
   4.476 -      --> (ty --> mk_bindtyp @{typ "term list option"}) --> mk_bindtyp @{typ "term list option"})
   4.477 -      $ (Const (@{const_name random}, @{typ index} --> mk_bindtyp ty)
   4.478 -        $ Bound i) $ Abs ("a", ty, t);
   4.479 -    val t = fold_rev mk_bindclause bounds (return $ check);
   4.480 -  in Abs ("n", @{typ index}, t) end;
   4.481 -
   4.482 -fun compile_generator_expr thy prop tys =
   4.483 -  let
   4.484 -    val f = CodePackage.eval_term ("Quickcheck.eval_ref", eval_ref) thy
   4.485 -      (mk_generator_expr prop tys) [];
   4.486 -  in f #> run #> (Option.map o map) (Code.postprocess_term thy) end;
   4.487 -
   4.488 -fun VALUE prop tys thy =
   4.489 -  let
   4.490 -    val t = mk_generator_expr prop tys;
   4.491 -    val eq = Logic.mk_equals (Free ("VALUE", fastype_of t), t)
   4.492 -  in
   4.493 -    thy
   4.494 -    |> TheoryTarget.init NONE
   4.495 -    |> Specification.definition (NONE, (("", []), eq))
   4.496 -    |> snd
   4.497 -    |> LocalTheory.exit
   4.498 -    |> ProofContext.theory_of
   4.499 -  end;
   4.500 -
   4.501 -end
   4.502 -*}
   4.503 -
   4.504 -ML {* val f = Quickcheck.compile_generator_expr @{theory}
   4.505 -  @{term "\<lambda>(n::nat) (m::nat) (q::nat). n = m + q + 1"} [@{typ nat}, @{typ nat}, @{typ nat}] *}
   4.506 -
   4.507 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.508 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.509 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.510 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.511 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.512 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.513 -ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.514 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.515 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.516 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.517 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.518 -
   4.519 -ML {* val f = Quickcheck.compile_generator_expr @{theory}
   4.520 -  @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
   4.521 -
   4.522 -(*setup {* Quickcheck.VALUE @{term "\<lambda>(n::int) (m::int) (q::int). n = m + q + 1"} [@{typ int}, @{typ int}, @{typ int}] *}
   4.523 -
   4.524 -export_code VALUE in SML module_name QuickcheckExample file "~~/../../gen_code/quickcheck.ML"
   4.525 -
   4.526 -definition "FOO = (True, Suc 0)"
   4.527 -
   4.528 -code_module (test) QuickcheckExample
   4.529 -  file "~~/../../gen_code/quickcheck'.ML"
   4.530 -  contains FOO*)
   4.531 -
   4.532 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.533 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.534 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.535 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.536 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.537 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.538 -ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.539 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.540 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.541 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.542 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.543 -ML {* f 3 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.544 -ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.545 -ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.546 -
   4.547 -ML {* val f = Quickcheck.compile_generator_expr @{theory}
   4.548 -  @{term "\<lambda>(xs\<Colon>nat list) ys. rev (xs @ ys) = rev xs @ rev ys"}
   4.549 -  [@{typ "nat list"}, @{typ "nat list"}] *}
   4.550 -
   4.551 -ML {* f 15 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.552 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.553 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.554 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.555 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.556 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.557 -ML {* f 25 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.558 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.559 -ML {* f 1 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.560 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.561 -ML {* f 2 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.562 -ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.563 -ML {* f 4 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.564 -ML {* f 5 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.565 -ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.566 -ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.567 -ML {* f 8 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.568 -ML {* f 88 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.569 -
   4.570 -subsection {* Incremental function generator *}
   4.571 -
   4.572 -ML {*
   4.573 -structure Quickcheck =
   4.574 -struct
   4.575 -
   4.576 -open Quickcheck;
   4.577 -
   4.578 -fun random_fun (eq : 'a -> 'a -> bool)
   4.579 -    (random : seed -> 'b * seed)
   4.580 -    (random_split : seed -> seed * seed)
   4.581 -    (seed : seed) =
   4.582 -  let
   4.583 -    val (seed', seed'') = random_split seed;
   4.584 -    val state = ref (seed', []);
   4.585 -    fun random_fun' x =
   4.586 -      let
   4.587 -        val (seed, fun_map) = ! state;
   4.588 -      in case AList.lookup (uncurry eq) fun_map x
   4.589 -       of SOME y => y
   4.590 -        | NONE => let
   4.591 -              val (y, seed') = random seed;
   4.592 -              val _ = state := (seed', (x, y) :: fun_map);
   4.593 -            in y end
   4.594 -      end;
   4.595 -  in (random_fun', seed'') end;
   4.596 -
   4.597 -end
   4.598 -*}
   4.599 -
   4.600 -axiomatization
   4.601 -  random_fun_aux :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> (seed \<Rightarrow> 'b \<times> seed)
   4.602 -    \<Rightarrow> (seed \<Rightarrow> seed \<times> seed) \<Rightarrow> seed \<Rightarrow> ('a \<Rightarrow> 'b) \<times> seed"
   4.603 -
   4.604 -code_const random_fun_aux (SML "Quickcheck.random'_fun")
   4.605 -
   4.606 -instantiation "fun" :: (term_of, term_of) term_of
   4.607 -begin
   4.608 -
   4.609 -instance ..
   4.610 -
   4.611 -end
   4.612 -
   4.613 -code_const "Eval.term_of :: ('a\<Colon>term_of \<Rightarrow> 'b\<Colon>term_of) \<Rightarrow> _"
   4.614 -  (SML "(fn '_ => Const (\"arbitrary\", dummyT))")
   4.615 -
   4.616 -instantiation "fun" :: (eq, "{type, random}") random
   4.617 -begin
   4.618 -
   4.619 -definition
   4.620 -  "random n = random_fun_aux (op =) (random n) split_seed"
   4.621 -
   4.622 -instance ..
   4.623 -
   4.624 -end
   4.625 -
   4.626 -ML {* val f = Quickcheck.compile_generator_expr @{theory}
   4.627 -  @{term "\<lambda>f k. int (f k) = k"} [@{typ "int \<Rightarrow> nat"}, @{typ int}] *}
   4.628 -
   4.629 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.630 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.631 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.632 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.633 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.634 -ML {* f 20 |> (Option.map o map) (Sign.string_of_term @{theory}) *}
   4.635 -
   4.636 -end