src/HOL/Quickcheck_Random.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 62979 1e527c40ae40
child 67399 eab6ce8368fa
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 (*  Title:      HOL/Quickcheck_Random.thy
     2     Author:     Florian Haftmann & Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 section \<open>A simple counterexample generator performing random testing\<close>
     6 
     7 theory Quickcheck_Random
     8 imports Random Code_Evaluation Enum
     9 begin
    10 
    11 notation fcomp (infixl "\<circ>>" 60)
    12 notation scomp (infixl "\<circ>\<rightarrow>" 60)
    13 
    14 setup \<open>Code_Target.add_derived_target ("Quickcheck", [(Code_Runtime.target, I)])\<close>
    15 
    16 subsection \<open>Catching Match exceptions\<close>
    17 
    18 axiomatization catch_match :: "'a => 'a => 'a"
    19 
    20 code_printing
    21   constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
    22 
    23 subsection \<open>The \<open>random\<close> class\<close>
    24 
    25 class random = typerep +
    26   fixes random :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    27 
    28 
    29 subsection \<open>Fundamental and numeric types\<close>
    30 
    31 instantiation bool :: random
    32 begin
    33 
    34 definition
    35   "random i = Random.range 2 \<circ>\<rightarrow>
    36     (\<lambda>k. Pair (if k = 0 then Code_Evaluation.valtermify False else Code_Evaluation.valtermify True))"
    37 
    38 instance ..
    39 
    40 end
    41 
    42 instantiation itself :: (typerep) random
    43 begin
    44 
    45 definition
    46   random_itself :: "natural \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
    47 where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
    48 
    49 instance ..
    50 
    51 end
    52 
    53 instantiation char :: random
    54 begin
    55 
    56 definition
    57   "random _ = Random.select (Enum.enum :: char list) \<circ>\<rightarrow> (\<lambda>c. Pair (c, \<lambda>u. Code_Evaluation.term_of c))"
    58 
    59 instance ..
    60 
    61 end
    62 
    63 instantiation String.literal :: random
    64 begin
    65 
    66 definition 
    67   "random _ = Pair (STR '''', \<lambda>u. Code_Evaluation.term_of (STR ''''))"
    68 
    69 instance ..
    70 
    71 end
    72 
    73 instantiation nat :: random
    74 begin
    75 
    76 definition random_nat :: "natural \<Rightarrow> Random.seed
    77   \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
    78 where
    79   "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    80      let n = nat_of_natural k
    81      in (n, \<lambda>_. Code_Evaluation.term_of n)))"
    82 
    83 instance ..
    84 
    85 end
    86 
    87 instantiation int :: random
    88 begin
    89 
    90 definition
    91   "random i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
    92      let j = (if k \<ge> i then int (nat_of_natural (k - i)) else - (int (nat_of_natural (i - k))))
    93      in (j, \<lambda>_. Code_Evaluation.term_of j)))"
    94 
    95 instance ..
    96 
    97 end
    98 
    99 instantiation natural :: random
   100 begin
   101 
   102 definition random_natural :: "natural \<Rightarrow> Random.seed
   103   \<Rightarrow> (natural \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
   104 where
   105   "random_natural i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>n. Pair (n, \<lambda>_. Code_Evaluation.term_of n))"
   106 
   107 instance ..
   108 
   109 end
   110 
   111 instantiation integer :: random
   112 begin
   113 
   114 definition random_integer :: "natural \<Rightarrow> Random.seed
   115   \<Rightarrow> (integer \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
   116 where
   117   "random_integer i = Random.range (2 * i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
   118      let j = (if k \<ge> i then integer_of_natural (k - i) else - (integer_of_natural (i - k)))
   119       in (j, \<lambda>_. Code_Evaluation.term_of j)))"
   120 
   121 instance ..
   122 
   123 end
   124 
   125 
   126 subsection \<open>Complex generators\<close>
   127 
   128 text \<open>Towards @{typ "'a \<Rightarrow> 'b"}\<close>
   129 
   130 axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
   131   \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   132   \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
   133   \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   134 
   135 definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
   136   \<Rightarrow> Random.seed \<Rightarrow> (('a::term_of \<Rightarrow> 'b::typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   137 where
   138   "random_fun_lift f =
   139     random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
   140 
   141 instantiation "fun" :: ("{equal, term_of}", random) random
   142 begin
   143 
   144 definition
   145   random_fun :: "natural \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
   146   where "random i = random_fun_lift (random i)"
   147 
   148 instance ..
   149 
   150 end
   151 
   152 text \<open>Towards type copies and datatypes\<close>
   153 
   154 definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
   155   where "collapse f = (f \<circ>\<rightarrow> id)"
   156 
   157 definition beyond :: "natural \<Rightarrow> natural \<Rightarrow> natural"
   158   where "beyond k l = (if l > k then l else 0)"
   159 
   160 lemma beyond_zero: "beyond k 0 = 0"
   161   by (simp add: beyond_def)
   162 
   163 
   164 definition (in term_syntax) [code_unfold]:
   165   "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
   166 
   167 definition (in term_syntax) [code_unfold]:
   168   "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
   169 
   170 instantiation set :: (random) random
   171 begin
   172 
   173 fun random_aux_set
   174 where
   175   "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
   176 | "random_aux_set (Code_Numeral.Suc i) j =
   177     collapse (Random.select_weight
   178       [(1, Pair valterm_emptyset),
   179        (Code_Numeral.Suc i,
   180         random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
   181 
   182 lemma [code]:
   183   "random_aux_set i j =
   184     collapse (Random.select_weight [(1, Pair valterm_emptyset),
   185       (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
   186 proof (induct i rule: natural.induct)
   187   case zero
   188   show ?case by (subst select_weight_drop_zero [symmetric])
   189     (simp add: random_aux_set.simps [simplified] less_natural_def)
   190 next
   191   case (Suc i)
   192   show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_natural_minus_one)
   193 qed
   194 
   195 definition "random_set i = random_aux_set i i"
   196 
   197 instance ..
   198 
   199 end
   200 
   201 lemma random_aux_rec:
   202   fixes random_aux :: "natural \<Rightarrow> 'a"
   203   assumes "random_aux 0 = rhs 0"
   204     and "\<And>k. random_aux (Code_Numeral.Suc k) = rhs (Code_Numeral.Suc k)"
   205   shows "random_aux k = rhs k"
   206   using assms by (rule natural.induct)
   207 
   208 subsection \<open>Deriving random generators for datatypes\<close>
   209 
   210 ML_file "Tools/Quickcheck/quickcheck_common.ML" 
   211 ML_file "Tools/Quickcheck/random_generators.ML"
   212 
   213 
   214 subsection \<open>Code setup\<close>
   215 
   216 code_printing
   217   constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
   218   \<comment> \<open>With enough criminal energy this can be abused to derive @{prop False};
   219   for this reason we use a distinguished target \<open>Quickcheck\<close>
   220   not spoiling the regular trusted code generation\<close>
   221 
   222 code_reserved Quickcheck Random_Generators
   223 
   224 no_notation fcomp (infixl "\<circ>>" 60)
   225 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   226     
   227 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
   228 
   229 hide_fact (open) collapse_def beyond_def random_fun_lift_def
   230 
   231 end