experimental addition of quickcheck
authorhaftmann
Fri May 15 16:39:16 2009 +0200 (2009-05-15)
changeset 31179ced817160283
parent 31178 27afaaa6547a
child 31180 dae7be64d614
experimental addition of quickcheck
src/HOL/Complex_Main.thy
src/HOL/Library/Quickcheck.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Fri May 15 16:39:15 2009 +0200
     1.2 +++ b/src/HOL/Complex_Main.thy	Fri May 15 16:39:16 2009 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    Ln
     1.5    Taylor
     1.6    Integration
     1.7 +  "Library/Quickcheck"
     1.8  begin
     1.9  
    1.10  end
     2.1 --- a/src/HOL/Library/Quickcheck.thy	Fri May 15 16:39:15 2009 +0200
     2.2 +++ b/src/HOL/Library/Quickcheck.thy	Fri May 15 16:39:16 2009 +0200
     2.3 @@ -3,43 +3,22 @@
     2.4  header {* A simple counterexample generator *}
     2.5  
     2.6  theory Quickcheck
     2.7 -imports Random Code_Eval Map
     2.8 +imports Main Real Random
     2.9  begin
    2.10  
    2.11 +notation fcomp (infixl "o>" 60)
    2.12 +notation scomp (infixl "o\<rightarrow>" 60)
    2.13 +
    2.14 +
    2.15  subsection {* The @{text random} class *}
    2.16  
    2.17  class random = typerep +
    2.18 -  fixes random :: "index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    2.19 -
    2.20 -text {* Type @{typ "'a itself"} *}
    2.21 -
    2.22 -instantiation itself :: ("{type, typerep}") random
    2.23 -begin
    2.24 -
    2.25 -definition
    2.26 -  "random _ = Pair (TYPE('a), \<lambda>u. Code_Eval.Const (STR ''TYPE'') TYPEREP('a))"
    2.27 -
    2.28 -instance ..
    2.29 -
    2.30 -end
    2.31 +  fixes random :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    2.32  
    2.33  
    2.34  subsection {* Quickcheck generator *}
    2.35  
    2.36  ML {*
    2.37 -structure StateMonad =
    2.38 -struct
    2.39 -
    2.40 -fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    2.41 -fun liftT' sT = sT --> sT;
    2.42 -
    2.43 -fun return T sT x = Const (@{const_name Pair}, T --> liftT T sT) $ x;
    2.44 -
    2.45 -fun scomp T1 T2 sT f g = Const (@{const_name scomp},
    2.46 -  liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    2.47 -
    2.48 -end;
    2.49 -
    2.50  structure Quickcheck =
    2.51  struct
    2.52  
    2.53 @@ -58,24 +37,26 @@
    2.54      val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
    2.55      val check = @{term "If \<Colon> bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"}
    2.56        $ result $ @{term "None \<Colon> term list option"} $ (@{term "Some \<Colon> term list \<Rightarrow> term list option "} $ terms);
    2.57 -    val return = @{term "Pair \<Colon> term list option \<Rightarrow> seed \<Rightarrow> term list option \<times> seed"};
    2.58 +    val return = @{term "Pair \<Colon> term list option \<Rightarrow> Random.seed \<Rightarrow> term list option \<times> Random.seed"};
    2.59 +    fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT);
    2.60      fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
    2.61 +    fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
    2.62 +      liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
    2.63      fun mk_split ty = Sign.mk_const thy
    2.64 -      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
    2.65 +      (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
    2.66      fun mk_scomp_split ty t t' =
    2.67 -      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
    2.68 +      mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t
    2.69          (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
    2.70      fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
    2.71 -      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
    2.72 -    val t = fold_rev mk_bindclause bounds (return $ check);
    2.73 -  in Abs ("n", @{typ index}, t) end;
    2.74 +      (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i);
    2.75 +  in Abs ("n", @{typ index}, fold_rev mk_bindclause bounds (return $ check)) end;
    2.76  
    2.77  fun compile_generator_expr thy t =
    2.78    let
    2.79      val tys = (map snd o fst o strip_abs) t;
    2.80      val t' = mk_generator_expr thy t tys;
    2.81      val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    2.82 -      (fn proc => fn g => fn s => g (s + 1) #>> (Option.map o map) proc) thy t' [];
    2.83 +      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    2.84    in f #> Random_Engine.run end;
    2.85  
    2.86  end
    2.87 @@ -87,7 +68,35 @@
    2.88  *}
    2.89  
    2.90  
    2.91 -subsection {* Type @{typ "'a \<Rightarrow> 'b"} *}
    2.92 +subsection {* Fundamental types*}
    2.93 +
    2.94 +definition (in term_syntax)
    2.95 +  "termify_bool b = (if b then termify True else termify False)"
    2.96 +
    2.97 +instantiation bool :: random
    2.98 +begin
    2.99 +
   2.100 +definition
   2.101 +  "random i = Random.range i o\<rightarrow> (\<lambda>k. Pair (termify_bool (k div 2 = 0)))"
   2.102 +
   2.103 +instance ..
   2.104 +
   2.105 +end
   2.106 +
   2.107 +definition (in term_syntax)
   2.108 +  "termify_itself TYPE('a\<Colon>typerep) = termify TYPE('a)"
   2.109 +
   2.110 +instantiation itself :: (typerep) random
   2.111 +begin
   2.112 +
   2.113 +definition random_itself :: "index \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   2.114 +  "random_itself _ = Pair (termify_itself TYPE('a))"
   2.115 +
   2.116 +instance ..
   2.117 +
   2.118 +end
   2.119 +
   2.120 +text {* Type @{typ "'a \<Rightarrow> 'b"} *}
   2.121  
   2.122  ML {*
   2.123  structure Random_Engine =
   2.124 @@ -123,10 +132,9 @@
   2.125  end
   2.126  *}
   2.127  
   2.128 -axiomatization
   2.129 -  random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   2.130 -    \<Rightarrow> (seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> seed) \<Rightarrow> (seed \<Rightarrow> seed \<times> seed)
   2.131 -    \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed"
   2.132 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   2.133 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   2.134 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   2.135  
   2.136  code_const random_fun_aux (Quickcheck "Random'_Engine.random'_fun")
   2.137    -- {* With enough criminal energy this can be abused to derive @{prop False};
   2.138 @@ -136,8 +144,8 @@
   2.139  instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
   2.140  begin
   2.141  
   2.142 -definition random_fun :: "index \<Rightarrow> seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> seed" where
   2.143 -  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) split_seed"
   2.144 +definition random_fun :: "index \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   2.145 +  "random n = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (random n) Random.split_seed"
   2.146  
   2.147  instance ..
   2.148  
   2.149 @@ -145,4 +153,80 @@
   2.150  
   2.151  code_reserved Quickcheck Random_Engine
   2.152  
   2.153 +
   2.154 +subsection {* Numeric types *}
   2.155 +
   2.156 +function (in term_syntax) termify_numeral :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   2.157 +  "termify_numeral k = (if k = 0 then termify Int.Pls
   2.158 +    else (if k mod 2 = 0 then termify Int.Bit0 else termify Int.Bit1) <\<cdot>> termify_numeral (k div 2))"
   2.159 +  by pat_completeness auto
   2.160 +
   2.161 +declare (in term_syntax) termify_numeral.psimps [simp del]
   2.162 +
   2.163 +termination termify_numeral by (relation "measure Code_Index.nat_of")
   2.164 +  (simp_all add: index)
   2.165 +
   2.166 +definition (in term_syntax) termify_int_number :: "index \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   2.167 +  "termify_int_number k = termify number_of <\<cdot>> termify_numeral k"
   2.168 +
   2.169 +definition (in term_syntax) termify_nat_number :: "index \<Rightarrow> nat \<times> (unit \<Rightarrow> term)" where
   2.170 +  "termify_nat_number k = (nat \<circ> number_of, snd (termify (number_of :: int \<Rightarrow> nat))) <\<cdot>> termify_numeral k"
   2.171 +
   2.172 +declare termify_nat_number_def [simplified snd_conv, code]
   2.173 +
   2.174 +instantiation nat :: random
   2.175 +begin
   2.176 +
   2.177 +definition random_nat :: "index \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
   2.178 +  "random_nat i = Random.range (i + 1) o\<rightarrow> (\<lambda>k. Pair (termify_nat_number k))"
   2.179 +
   2.180 +instance ..
   2.181 +
   2.182  end
   2.183 +
   2.184 +definition (in term_syntax) term_uminus :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term)" where
   2.185 +  [code inline]: "term_uminus k = termify uminus <\<cdot>> k"
   2.186 +
   2.187 +instantiation int :: random
   2.188 +begin
   2.189 +
   2.190 +definition
   2.191 +  "random i = Random.range (2 * i + 1) o\<rightarrow> (\<lambda>k. Pair (if k \<ge> i
   2.192 +     then let j = k - i in termify_int_number j
   2.193 +     else let j = i - k in term_uminus (termify_int_number j)))"
   2.194 +
   2.195 +instance ..
   2.196 +
   2.197 +end
   2.198 +
   2.199 +definition (in term_syntax) term_fract :: "int \<times> (unit \<Rightarrow> term) \<Rightarrow> int \<times> (unit \<Rightarrow> term) \<Rightarrow> rat \<times> (unit \<Rightarrow> term)" where
   2.200 +  [code inline]: "term_fract k l = termify Fract <\<cdot>> k <\<cdot>> l"
   2.201 +
   2.202 +instantiation rat :: random
   2.203 +begin
   2.204 +
   2.205 +definition
   2.206 +  "random i = random i o\<rightarrow> (\<lambda>num. Random.range (i + 1) o\<rightarrow> (\<lambda>denom. Pair (term_fract num (termify_int_number denom))))"
   2.207 +
   2.208 +instance ..
   2.209 +
   2.210 +end
   2.211 +
   2.212 +definition (in term_syntax) term_ratreal :: "rat \<times> (unit \<Rightarrow> term) \<Rightarrow> real \<times> (unit \<Rightarrow> term)" where
   2.213 +  [code inline]: "term_ratreal k = termify Ratreal <\<cdot>> k"
   2.214 +
   2.215 +instantiation real :: random
   2.216 +begin
   2.217 +
   2.218 +definition
   2.219 +  "random i = random i o\<rightarrow> (\<lambda>r. Pair (term_ratreal r))"
   2.220 +
   2.221 +instance ..
   2.222 +
   2.223 +end
   2.224 +
   2.225 +
   2.226 +no_notation fcomp (infixl "o>" 60)
   2.227 +no_notation scomp (infixl "o\<rightarrow>" 60)
   2.228 +
   2.229 +end