src/HOL/Quickcheck.thy
changeset 31186 b458b4ac570f
parent 31179 ced817160283
child 31194 1d6926f96440
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quickcheck.thy	Sat May 16 20:16:49 2009 +0200
     1.3 @@ -0,0 +1,232 @@
     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 Main Real Random
    1.10 +begin
    1.11 +
    1.12 +notation fcomp (infixl "o>" 60)
    1.13 +notation scomp (infixl "o\<rightarrow>" 60)
    1.14 +
    1.15 +
    1.16 +subsection {* The @{text random} class *}
    1.17 +
    1.18 +class random = typerep +
    1.19 +  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    1.20 +
    1.21 +
    1.22 +subsection {* Quickcheck generator *}
    1.23 +
    1.24 +ML {*
    1.25 +structure Quickcheck =
    1.26 +struct
    1.27 +
    1.28 +open Quickcheck;
    1.29 +
    1.30 +val eval_ref : (unit -> int -> int * int -> term list option * (int * int)) option ref = ref NONE;
    1.31 +
    1.32 +val target = "Quickcheck";
    1.33 +
    1.34 +fun mk_generator_expr thy prop tys =
    1.35 +  let
    1.36 +    val bound_max = length tys - 1;
    1.37 +    val bounds = map_index (fn (i, ty) =>
    1.38 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) tys;
    1.39 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
    1.40 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    1.41 +    val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    1.42 +      $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    1.43 +    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
    1.44 +    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    1.45 +    fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    1.46 +    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    1.47 +      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    1.48 +    fun mk_split ty = Sign.mk_const thy
    1.49 +      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    1.50 +    fun mk_scomp_split ty t t' =
    1.51 +      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    1.52 +        (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    1.53 +    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    1.54 +      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    1.55 +  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
    1.56 +
    1.57 +fun compile_generator_expr thy t =
    1.58 +  let
    1.59 +    val tys = (map snd o fst o strip_abs) t;
    1.60 +    val t' = mk_generator_expr thy t tys;
    1.61 +    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    1.62 +      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    1.63 +  in f #> Random_Engine.run end;
    1.64 +
    1.65 +end
    1.66 +*}
    1.67 +
    1.68 +setup {*
    1.69 +  Code_Target.extend_target (Quickcheck.target, (Code_ML.target_Eval, K I))
    1.70 +  #> Quickcheck.add_generator ("code", Quickcheck.compile_generator_expr o ProofContext.theory_of)
    1.71 +*}
    1.72 +
    1.73 +
    1.74 +subsection {* Fundamental types*}
    1.75 +
    1.76 +definition (in term_syntax)
    1.77 +  "termify_bool b = (if b then termify True else termify False)"
    1.78 +
    1.79 +instantiation bool :: random
    1.80 +begin
    1.81 +
    1.82 +definition
    1.83 +  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
    1.84 +
    1.85 +instance ..
    1.86 +
    1.87 +end
    1.88 +
    1.89 +definition (in term_syntax)
    1.90 +  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
    1.91 +
    1.92 +instantiation itself :: (typerep) random
    1.93 +begin
    1.94 +
    1.95 +definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    1.96 +  "random_itself _ = Pair (termify_itself TYPE('a))"
    1.97 +
    1.98 +instance ..
    1.99 +
   1.100 +end
   1.101 +
   1.102 +text {* Type @{typ "'a \<Rightarrow> 'b"} *}
   1.103 +
   1.104 +ML {*
   1.105 +structure Random_Engine =
   1.106 +struct
   1.107 +
   1.108 +open Random_Engine;
   1.109 +
   1.110 +fun random_fun (T1 : typ) (T2 : typ) (eq : 'a -> 'a -> bool) (term_of : 'a -> term)
   1.111 +    (random : Random_Engine.seed -> ('b * (unit -> term)) * Random_Engine.seed)
   1.112 +    (random_split : Random_Engine.seed -> Random_Engine.seed * Random_Engine.seed)
   1.113 +    (seed : Random_Engine.seed) =
   1.114 +  let
   1.115 +    val (seed', seed'') = random_split seed;
   1.116 +    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
   1.117 +    val fun_upd = Const (@{const_name fun_upd},
   1.118 +      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
   1.119 +    fun random_fun' x =
   1.120 +      let
   1.121 +        val (seed, fun_map, f_t) = ! state;
   1.122 +      in case AList.lookup (uncurry eq) fun_map x
   1.123 +       of SOME y => y
   1.124 +        | NONE => let
   1.125 +              val t1 = term_of x;
   1.126 +              val ((y, t2), seed') = random seed;
   1.127 +              val fun_map' = (x, y) :: fun_map;
   1.128 +              val f_t' = fun_upd $ f_t $ t1 $ t2 ();
   1.129 +              val _ = state := (seed', fun_map', f_t');
   1.130 +            in y end
   1.131 +      end;
   1.132 +    fun term_fun' () = #3 (! state);
   1.133 +  in ((random_fun', term_fun'), seed'') end;
   1.134 +
   1.135 +end
   1.136 +*}
   1.137 +
   1.138 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   1.139 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   1.140 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   1.141 +
   1.142 +code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
   1.143 +  -- {* With enough criminal energy this can be abused to derive @{prop False};
   1.144 +  for this reason we use a distinguished target @{text Quickcheck}
   1.145 +  not spoiling the regular trusted code generation *}
   1.146 +
   1.147 +instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   1.148 +begin
   1.149 +
   1.150 +definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   1.151 +  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   1.152 +
   1.153 +instance ..
   1.154 +
   1.155 +end
   1.156 +
   1.157 +code_reserved Quickcheck Random_Engine
   1.158 +
   1.159 +
   1.160 +subsection {* Numeric types *}
   1.161 +
   1.162 +function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   1.163 +  "termify_numeral k = (if k = 0 then termify Int.Pls
   1.164 +    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
   1.165 +  by pat_completeness auto
   1.166 +
   1.167 +declare (in term_syntax) termify_numeral.psimps [simp del]
   1.168 +
   1.169 +termination termify_numeral by (relation "measure Code_Index.nat_of")
   1.170 +  (simp_all add: index)
   1.171 +
   1.172 +definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   1.173 +  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
   1.174 +
   1.175 +definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
   1.176 +  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
   1.177 +
   1.178 +declare termify_nat_number_def [simplified snd_conv, code]
   1.179 +
   1.180 +instantiation nat :: random
   1.181 +begin
   1.182 +
   1.183 +definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   1.184 +  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
   1.185 +
   1.186 +instance ..
   1.187 +
   1.188 +end
   1.189 +
   1.190 +definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   1.191 +  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
   1.192 +
   1.193 +instantiation int :: random
   1.194 +begin
   1.195 +
   1.196 +definition
   1.197 +  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
   1.198 +     then let j = k - i in termify_int_number j
   1.199 +     else let j = i - k in term_uminus (termify_int_number j)))"
   1.200 +
   1.201 +instance ..
   1.202 +
   1.203 +end
   1.204 +
   1.205 +definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
   1.206 +  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
   1.207 +
   1.208 +instantiation rat :: random
   1.209 +begin
   1.210 +
   1.211 +definition
   1.212 +  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
   1.213 +
   1.214 +instance ..
   1.215 +
   1.216 +end
   1.217 +
   1.218 +definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
   1.219 +  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
   1.220 +
   1.221 +instantiation real :: random
   1.222 +begin
   1.223 +
   1.224 +definition
   1.225 +  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
   1.226 +
   1.227 +instance ..
   1.228 +
   1.229 +end
   1.230 +
   1.231 +
   1.232 +no_notation fcomp (infixl "o>" 60)
   1.233 +no_notation scomp (infixl "o\<rightarrow>" 60)
   1.234 +
   1.235 +end