src/HOL/Quickcheck_Random.thy
changeset 51126 df86080de4cb
parent 50046 0051dc4f301f
child 51143 0a2371e7ced3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quickcheck_Random.thy	Thu Feb 14 15:27:10 2013 +0100
     1.3 @@ -0,0 +1,204 @@
     1.4 +(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
     1.5 +
     1.6 +header {* A simple counterexample generator performing random testing *}
     1.7 +
     1.8 +theory Quickcheck_Random
     1.9 +imports Random Code_Evaluation Enum
    1.10 +begin
    1.11 +
    1.12 +notation fcomp (infixl "\<circ>>" 60)
    1.13 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.14 +
    1.15 +setup {* Code_Target.extend_target ("Quickcheck", (Code_Runtime.target, K I)) *}
    1.16 +
    1.17 +subsection {* Catching Match exceptions *}
    1.18 +
    1.19 +axiomatization catch_match :: "'a => 'a => 'a"
    1.20 +
    1.21 +code_const catch_match 
    1.22 +  (Quickcheck "((_) handle Match => _)")
    1.23 +
    1.24 +subsection {* The @{text random} class *}
    1.25 +
    1.26 +class random = typerep +
    1.27 +  fixes random :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    1.28 +
    1.29 +
    1.30 +subsection {* Fundamental and numeric types*}
    1.31 +
    1.32 +instantiation bool :: random
    1.33 +begin
    1.34 +
    1.35 +definition
    1.36 +  "random i = Random.range 2 \<circ>\<rightarrow>
    1.37 +    (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
    1.38 +
    1.39 +instance ..
    1.40 +
    1.41 +end
    1.42 +
    1.43 +instantiation itself :: (typerep) random
    1.44 +begin
    1.45 +
    1.46 +definition
    1.47 +  random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    1.48 +where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
    1.49 +
    1.50 +instance ..
    1.51 +
    1.52 +end
    1.53 +
    1.54 +instantiation char :: random
    1.55 +begin
    1.56 +
    1.57 +definition
    1.58 +  "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    1.59 +
    1.60 +instance ..
    1.61 +
    1.62 +end
    1.63 +
    1.64 +instantiation String.literal :: random
    1.65 +begin
    1.66 +
    1.67 +definition 
    1.68 +  "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
    1.69 +
    1.70 +instance ..
    1.71 +
    1.72 +end
    1.73 +
    1.74 +instantiation nat :: random
    1.75 +begin
    1.76 +
    1.77 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed
    1.78 +  \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
    1.79 +where
    1.80 +  "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    1.81 +     let n = Code_Numeral.nat_of k
    1.82 +     in (n, \<lambda>_. Code_Evaluation.term_of n)))"
    1.83 +
    1.84 +instance ..
    1.85 +
    1.86 +end
    1.87 +
    1.88 +instantiation int :: random
    1.89 +begin
    1.90 +
    1.91 +definition
    1.92 +  "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    1.93 +     let j = (if k \<ge> i then Code_Numeral.int_of (k - i) else - Code_Numeral.int_of (i - k))
    1.94 +     in (j, \<lambda>_. Code_Evaluation.term_of j)))"
    1.95 +
    1.96 +instance ..
    1.97 +
    1.98 +end
    1.99 +
   1.100 +
   1.101 +subsection {* Complex generators *}
   1.102 +
   1.103 +text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
   1.104 +
   1.105 +axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   1.106 +  \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   1.107 +  \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   1.108 +  \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   1.109 +
   1.110 +definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   1.111 +  \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   1.112 +where
   1.113 +  "random_fun_lift f =
   1.114 +    random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
   1.115 +
   1.116 +instantiation "fun" :: ("{equal, term_of}", random) random
   1.117 +begin
   1.118 +
   1.119 +definition
   1.120 +  random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   1.121 +  where "random i = random_fun_lift (random i)"
   1.122 +
   1.123 +instance ..
   1.124 +
   1.125 +end
   1.126 +
   1.127 +text {* Towards type copies and datatypes *}
   1.128 +
   1.129 +definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
   1.130 +  where "collapse f = (f \<circ>\<rightarrow> id)"
   1.131 +
   1.132 +definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
   1.133 +  where "beyond k l = (if l > k then l else 0)"
   1.134 +
   1.135 +lemma beyond_zero: "beyond k 0 = 0"
   1.136 +  by (simp add: beyond_def)
   1.137 +
   1.138 +
   1.139 +definition (in term_syntax) [code_unfold]:
   1.140 +  "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
   1.141 +
   1.142 +definition (in term_syntax) [code_unfold]:
   1.143 +  "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
   1.144 +
   1.145 +instantiation set :: (random) random
   1.146 +begin
   1.147 +
   1.148 +primrec random_aux_set
   1.149 +where
   1.150 +  "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
   1.151 +| "random_aux_set (Code_Numeral.Suc i) j =
   1.152 +    collapse (Random.select_weight
   1.153 +      [(1, Pair valterm_emptyset),
   1.154 +       (Code_Numeral.Suc i,
   1.155 +        random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
   1.156 +
   1.157 +lemma [code]:
   1.158 +  "random_aux_set i j =
   1.159 +    collapse (Random.select_weight [(1, Pair valterm_emptyset),
   1.160 +      (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
   1.161 +proof (induct i rule: code_numeral.induct)
   1.162 +  case zero
   1.163 +  show ?case by (subst select_weight_drop_zero [symmetric])
   1.164 +    (simp add: random_aux_set.simps [simplified])
   1.165 +next
   1.166 +  case (Suc i)
   1.167 +  show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one)
   1.168 +qed
   1.169 +
   1.170 +definition "random_set i = random_aux_set i i"
   1.171 +
   1.172 +instance ..
   1.173 +
   1.174 +end
   1.175 +
   1.176 +lemma random_aux_rec:
   1.177 +  fixes random_aux :: "code_numeral \<Rightarrow> 'a"
   1.178 +  assumes "random_aux 0 = rhs 0"
   1.179 +    and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
   1.180 +  shows "random_aux k = rhs k"
   1.181 +  using assms by (rule code_numeral.induct)
   1.182 +
   1.183 +subsection {* Deriving random generators for datatypes *}
   1.184 +
   1.185 +ML_file "Tools/Quickcheck/quickcheck_common.ML" 
   1.186 +ML_file "Tools/Quickcheck/random_generators.ML"
   1.187 +setup Random_Generators.setup
   1.188 +
   1.189 +
   1.190 +subsection {* Code setup *}
   1.191 +
   1.192 +code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
   1.193 +  -- {* With enough criminal energy this can be abused to derive @{prop False};
   1.194 +  for this reason we use a distinguished target @{text Quickcheck}
   1.195 +  not spoiling the regular trusted code generation *}
   1.196 +
   1.197 +code_reserved Quickcheck Random_Generators
   1.198 +
   1.199 +no_notation fcomp (infixl "\<circ>>" 60)
   1.200 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.201 +    
   1.202 +hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
   1.203 +
   1.204 +hide_fact (open) collapse_def beyond_def random_fun_lift_def
   1.205 +
   1.206 +end
   1.207 +