src/HOL/Smallcheck.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 41178 f4d3acf0c4cc
child 41231 2e901158675e
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Another simple counterexample generator *}
     4 
     5 theory Smallcheck
     6 imports Quickcheck
     7 uses ("Tools/smallvalue_generators.ML")
     8 begin
     9 
    10 subsection {* basic operations for generators *}
    11 
    12 definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    13 where
    14   [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    15 
    16 subsection {* small value generator type classes *}
    17 
    18 class small = term_of +
    19 fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    20 
    21 instantiation unit :: small
    22 begin
    23 
    24 definition "small f d = f ()"
    25 
    26 instance ..
    27 
    28 end
    29 
    30 instantiation int :: small
    31 begin
    32 
    33 function small' :: "(int => term list option) => int => int => term list option"
    34 where "small' f d i = (if d < i then None else (case f i of Some t => Some t | None => small' f d (i + 1)))"
    35 by pat_completeness auto
    36 
    37 termination 
    38   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    39 
    40 definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    41 
    42 instance ..
    43 
    44 end
    45 
    46 instantiation prod :: (small, small) small
    47 begin
    48 
    49 definition
    50   "small f d = small (%x. small (%y. f (x, y)) d) d"
    51 
    52 instance ..
    53 
    54 end
    55 
    56 subsection {* full small value generator type classes *}
    57 
    58 class full_small = term_of +
    59 fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    60 
    61 instantiation unit :: full_small
    62 begin
    63 
    64 definition "full_small f d = f (Code_Evaluation.valtermify ())"
    65 
    66 instance ..
    67 
    68 end
    69 
    70 instantiation int :: full_small
    71 begin
    72 
    73 function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
    74   where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
    75 by pat_completeness auto
    76 
    77 termination 
    78   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    79 
    80 definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    81 
    82 instance ..
    83 
    84 end
    85 
    86 instantiation prod :: (full_small, full_small) full_small
    87 begin
    88 
    89 definition
    90   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
    91     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
    92 
    93 instance ..
    94 
    95 end
    96 
    97 instantiation "fun" :: ("{equal, full_small}", full_small) full_small
    98 begin
    99 
   100 fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   101 where
   102   "full_small_fun' f i d = (if i > 1 then
   103     full_small (%(a, at). full_small (%(b, bt).
   104       full_small_fun' (%(g, gt). f (g(a := b),
   105         (%_. let T1 = (Typerep.typerep (TYPE('a)));
   106                  T2 = (Typerep.typerep (TYPE('b)))
   107              in
   108                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   109                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   110                     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   111                        Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   112                (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
   113   else (if i > 0 then
   114     full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   115 
   116 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   117 where
   118   "full_small_fun f d = full_small_fun' f d d" 
   119 
   120 instance ..
   121 
   122 end
   123 
   124 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   125 
   126 
   127 class check_all = enum + term_of +
   128   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   129   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   130   
   131 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
   132 where
   133   "check_all_n_lists f n =
   134      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   135 
   136 definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
   137 where
   138   "mk_map_term T1 T2 domm rng =
   139      (%_. let T1 = T1 ();
   140               T2 = T2 ();
   141               update_term = (%g (a, b).
   142                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   143                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   144                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   145                       Typerep.Typerep (STR ''fun'') [T1,
   146                         Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   147                         g) a) b)
   148           in
   149              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   150 
   151 instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   152 begin
   153 
   154 definition
   155   "check_all f =
   156     (let
   157       mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   158       enum = (Enum.enum :: 'a list)
   159     in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))"
   160 
   161 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   162 where
   163   "enum_term_of_fun = (%_ _. let
   164     enum_term_of_a = enum_term_of (TYPE('a));
   165     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   166   in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   167  
   168 instance ..
   169 
   170 end
   171 
   172 
   173 instantiation unit :: check_all
   174 begin
   175 
   176 definition
   177   "check_all f = f (Code_Evaluation.valtermify ())"
   178 
   179 definition enum_term_of_unit :: "unit itself => unit => term list"
   180 where
   181   "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   182 
   183 instance ..
   184 
   185 end
   186 
   187 
   188 instantiation bool :: check_all
   189 begin
   190 
   191 definition
   192   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   193 
   194 definition enum_term_of_bool :: "bool itself => unit => term list"
   195 where
   196   "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   197 
   198 instance ..
   199 
   200 end
   201 
   202 
   203 instantiation prod :: (check_all, check_all) check_all
   204 begin
   205 
   206 definition
   207   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
   208 
   209 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   210 where
   211   "enum_term_of_prod = (%_ _. map (%(x, y). Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) x) y) (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   212 
   213 instance ..
   214 
   215 end
   216 
   217 
   218 instantiation sum :: (check_all, check_all) check_all
   219 begin
   220 
   221 definition
   222   "check_all f = (case check_all (%(a, t). f (Inl a, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => 'a + 'b)) (t ()))) of Some x' => Some x'
   223              | None => check_all (%(b, t). f (Inr b, %_. Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => 'a + 'b)) (t ()))))"
   224 
   225 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   226 where
   227   "enum_term_of_sum = (%_ _. map (Code_Evaluation.App (Code_Evaluation.term_of (Inl :: 'a => ('a + 'b)))) (enum_term_of (TYPE('a)) ()) @
   228      map (Code_Evaluation.App (Code_Evaluation.term_of (Inr :: 'b => ('a + 'b)))) (enum_term_of (TYPE('b)) ()))"
   229 
   230 instance ..
   231 
   232 end
   233 
   234 instantiation nibble :: check_all
   235 begin
   236 
   237 definition
   238   "check_all f =
   239     f (Code_Evaluation.valtermify Nibble0) orelse
   240     f (Code_Evaluation.valtermify Nibble1) orelse
   241     f (Code_Evaluation.valtermify Nibble2) orelse
   242     f (Code_Evaluation.valtermify Nibble3) orelse
   243     f (Code_Evaluation.valtermify Nibble4) orelse
   244     f (Code_Evaluation.valtermify Nibble5) orelse
   245     f (Code_Evaluation.valtermify Nibble6) orelse
   246     f (Code_Evaluation.valtermify Nibble7) orelse
   247     f (Code_Evaluation.valtermify Nibble8) orelse
   248     f (Code_Evaluation.valtermify Nibble9) orelse
   249     f (Code_Evaluation.valtermify NibbleA) orelse
   250     f (Code_Evaluation.valtermify NibbleB) orelse
   251     f (Code_Evaluation.valtermify NibbleC) orelse
   252     f (Code_Evaluation.valtermify NibbleD) orelse
   253     f (Code_Evaluation.valtermify NibbleE) orelse
   254     f (Code_Evaluation.valtermify NibbleF)"
   255 
   256 definition enum_term_of_nibble :: "nibble itself => unit => term list"
   257 where
   258   "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"
   259 
   260 instance ..
   261 
   262 end
   263 
   264 
   265 instantiation char :: check_all
   266 begin
   267 
   268 definition
   269   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f (Char x y, %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   270 
   271 definition enum_term_of_char :: "char itself => unit => term list"
   272 where
   273   "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   274 
   275 instance ..
   276 
   277 end
   278 
   279 
   280 instantiation option :: (check_all) check_all
   281 begin
   282 
   283 definition
   284   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   285     (Code_Evaluation.Const (STR ''Option.option.Some'')
   286       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   287 
   288 definition enum_term_of_option :: "'a option itself => unit => term list"
   289 where
   290   "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option))) (enum_term_of (TYPE('a)) ())))"
   291 
   292 instance ..
   293 
   294 end
   295 
   296 
   297 instantiation Enum.finite_1 :: check_all
   298 begin
   299 
   300 definition
   301   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
   302 
   303 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   304 where
   305   "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"
   306 
   307 instance ..
   308 
   309 end
   310 
   311 instantiation Enum.finite_2 :: check_all
   312 begin
   313 
   314 definition
   315   "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
   316 
   317 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   318 where
   319   "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   320 
   321 instance ..
   322 
   323 end
   324 
   325 instantiation Enum.finite_3 :: check_all
   326 begin
   327 
   328 definition
   329   "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
   330 
   331 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   332 where
   333   "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   334 
   335 instance ..
   336 
   337 end
   338 
   339 
   340 
   341 subsection {* Defining combinators for any first-order data type *}
   342 
   343 definition catch_match :: "term list option => term list option => term list option"
   344 where
   345   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
   346 
   347 code_const catch_match 
   348   (SML "(_) handle Match => _")
   349 
   350 use "Tools/smallvalue_generators.ML"
   351 
   352 setup {* Smallvalue_Generators.setup *}
   353 
   354 declare [[quickcheck_tester = exhaustive]]
   355 
   356 hide_fact orelse_def catch_match_def
   357 no_notation orelse (infixr "orelse" 55)
   358 hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   359 
   360 end