wneuper/isa: src/HOL/Quickcheck_Exhaustive.thy@91c4d7397f0e

     1 (* Author: Lukas Bulwahn, TU Muenchen *)

     3 header {* A simple counterexample generator performing exhaustive testing *}

     5 theory Quickcheck_Exhaustive

     6 imports Quickcheck

     7 uses ("Tools/Quickcheck/exhaustive_generators.ML")

     8 begin

    10 subsection {* basic operations for exhaustive generators *}

    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)"

    16 subsection {* exhaustive generator type classes *}

    18 class exhaustive = term_of +

    19   fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"

    21 class full_exhaustive = term_of +

    22   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"

    24 instantiation code_numeral :: full_exhaustive

    25 begin

    27 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"

    28   where "full_exhaustive_code_numeral' f d i =

    29     (if d < i then None

    30     else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"

    31 by pat_completeness auto

    33 termination

    34   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto

    36 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"

    38 instance ..

    40 end

    42 instantiation code_numeral :: exhaustive

    43 begin

    45 function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"

    46   where "exhaustive_code_numeral' f d i =

    47     (if d < i then None

    48     else (f i orelse exhaustive_code_numeral' f d (i + 1)))"

    49 by pat_completeness auto

    51 termination

    52   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto

    54 definition "exhaustive f d = exhaustive_code_numeral' f d 0"

    56 instance ..

    58 end

    60 instantiation nat :: exhaustive

    61 begin

    63 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"

    65 instance ..

    67 end

    69 instantiation nat :: full_exhaustive

    70 begin

    72 definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"

    74 instance ..

    76 end

    78 instantiation int :: exhaustive

    79 begin

    81 function exhaustive' :: "(int => term list option) => int => int => term list option"

    82   where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"

    83 by pat_completeness auto

    85 termination

    86   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto

    88 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"

    90 instance ..

    92 end

    94 instantiation int :: full_exhaustive

    95 begin

    97 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"

    98   where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"

    99 by pat_completeness auto

   101 termination

   102   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto

   104 definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"

   106 instance ..

   108 end

   110 instantiation prod :: (exhaustive, exhaustive) exhaustive

   111 begin

   113 definition

   114   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"

   116 instance ..

   118 end

   120 instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive

   121 begin

   123 definition

   124   "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),

   125     %u. let T1 = (Typerep.typerep (TYPE('a)));

   126             T2 = (Typerep.typerep (TYPE('b)))

   127     in Code_Evaluation.App (Code_Evaluation.App (

   128       Code_Evaluation.Const (STR ''Product_Type.Pair'')

   129       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))

   130       (t1 ())) (t2 ()))) d) d"

   132 instance ..

   134 end

   136 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive

   137 begin

   139 fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"

   140 where

   141   "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)

   142    orelse (if i > 1 then

   143      exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.

   144        f (g(a := b))) d) d) (i - 1) d else None)"

   146 definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"

   147 where

   148   "exhaustive_fun f d = exhaustive_fun' f d d"

   150 instance ..

   152 end

   154 instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive

   155 begin

   157 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"

   158 where

   159   "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)

   160    orelse (if i > 1 then

   161      full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).

   162        f (g(a := b),

   163          (%_. let A = (Typerep.typerep (TYPE('a)));

   164                   B = (Typerep.typerep (TYPE('b)));

   165                   fun = (%T U. Typerep.Typerep (STR ''fun'') [T, U])

   166               in

   167                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App

   168                   (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))

   169                 (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"

   171 definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"

   172 where

   173   "full_exhaustive_fun f d = full_exhaustive_fun' f d d"

   175 instance ..

   177 end

   179 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}

   181 class check_all = enum + term_of +

   182   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"

   183   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"

   185 fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"

   186 where

   187   "check_all_n_lists f n =

   188      (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"

   190 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"

   191 where

   192   "mk_map_term T1 T2 domm rng =

   193      (%_. let T1 = T1 ();

   194               T2 = T2 ();

   195               update_term = (%g (a, b).

   196                 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App

   197                  (Code_Evaluation.Const (STR ''Fun.fun_upd'')

   198                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],

   199                       Typerep.Typerep (STR ''fun'') [T1,

   200                         Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))

   201                         g) a) b)

   202           in

   203              List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"

   205 instantiation "fun" :: ("{equal, check_all}", check_all) check_all

   206 begin

   208 definition

   209   "check_all f =

   210     (let

   211       mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));

   212       enum = (Enum.enum :: 'a list)

   213     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)))"

   215 definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"

   216 where

   217   "enum_term_of_fun = (%_ _. let

   218     enum_term_of_a = enum_term_of (TYPE('a));

   219     mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a

   220   in map (%ys. mk_term (%_. ys) ()) (Enum.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"

   222 instance ..

   224 end

   227 instantiation unit :: check_all

   228 begin

   230 definition

   231   "check_all f = f (Code_Evaluation.valtermify ())"

   233 definition enum_term_of_unit :: "unit itself => unit => term list"

   234 where

   235   "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"

   237 instance ..

   239 end

   242 instantiation bool :: check_all

   243 begin

   245 definition

   246   "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"

   248 definition enum_term_of_bool :: "bool itself => unit => term list"

   249 where

   250   "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"

   252 instance ..

   254 end

   257 instantiation prod :: (check_all, check_all) check_all

   258 begin

   260 definition

   261   "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y),

   262     %u. let T1 = (Typerep.typerep (TYPE('a)));

   263             T2 = (Typerep.typerep (TYPE('b)))

   264     in Code_Evaluation.App (Code_Evaluation.App (

   265       Code_Evaluation.Const (STR ''Product_Type.Pair'')

   266       (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]]))

   267       (t1 ())) (t2 ()))))"

   269 definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"

   270 where

   271   "enum_term_of_prod = (%_ _. map (%(x, y).

   272        let T1 = (Typerep.typerep (TYPE('a)));

   273            T2 = (Typerep.typerep (TYPE('b)))

   274        in Code_Evaluation.App (Code_Evaluation.App (

   275          Code_Evaluation.Const (STR ''Product_Type.Pair'')

   276            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Product_Type.prod'') [T1, T2]]])) x) y)

   277      (Enum.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))  "

   279 instance ..

   281 end

   284 instantiation sum :: (check_all, check_all) check_all

   285 begin

   287 definition

   288   "check_all f = (case check_all (%(a, t). f (Inl a, %_.

   289      let T1 = (Typerep.typerep (TYPE('a)));

   290          T2 = (Typerep.typerep (TYPE('b)))

   291        in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')

   292            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))) of Some x' => Some x'

   293              | None => check_all (%(b, t). f (Inr b, %_. let

   294                  T1 = (Typerep.typerep (TYPE('a)));

   295                  T2 = (Typerep.typerep (TYPE('b)))

   296                in Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')

   297                  (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])) (t ()))))"

   299 definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"

   300 where

   301   "enum_term_of_sum = (%_ _.

   302      let

   303        T1 = (Typerep.typerep (TYPE('a)));

   304        T2 = (Typerep.typerep (TYPE('b)))

   305      in

   306        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')

   307              (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))

   308              (enum_term_of (TYPE('a)) ()) @

   309        map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')

   310              (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))

   311              (enum_term_of (TYPE('b)) ()))"

   313 instance ..

   315 end

   317 instantiation nibble :: check_all

   318 begin

   320 definition

   321   "check_all f =

   322     f (Code_Evaluation.valtermify Nibble0) orelse

   323     f (Code_Evaluation.valtermify Nibble1) orelse

   324     f (Code_Evaluation.valtermify Nibble2) orelse

   325     f (Code_Evaluation.valtermify Nibble3) orelse

   326     f (Code_Evaluation.valtermify Nibble4) orelse

   327     f (Code_Evaluation.valtermify Nibble5) orelse

   328     f (Code_Evaluation.valtermify Nibble6) orelse

   329     f (Code_Evaluation.valtermify Nibble7) orelse

   330     f (Code_Evaluation.valtermify Nibble8) orelse

   331     f (Code_Evaluation.valtermify Nibble9) orelse

   332     f (Code_Evaluation.valtermify NibbleA) orelse

   333     f (Code_Evaluation.valtermify NibbleB) orelse

   334     f (Code_Evaluation.valtermify NibbleC) orelse

   335     f (Code_Evaluation.valtermify NibbleD) orelse

   336     f (Code_Evaluation.valtermify NibbleE) orelse

   337     f (Code_Evaluation.valtermify NibbleF)"

   339 definition enum_term_of_nibble :: "nibble itself => unit => term list"

   340 where

   341   "enum_term_of_nibble = (%_ _. map Code_Evaluation.term_of (Enum.enum :: nibble list))"

   343 instance ..

   345 end

   348 instantiation char :: check_all

   349 begin

   351 definition

   352   "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 ()))))"

   354 definition enum_term_of_char :: "char itself => unit => term list"

   355 where

   356   "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"

   358 instance ..

   360 end

   363 instantiation option :: (check_all) check_all

   364 begin

   366 definition

   367   "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App

   368     (Code_Evaluation.Const (STR ''Option.option.Some'')

   369       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"

   371 definition enum_term_of_option :: "'a option itself => unit => term list"

   372 where

   373   "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')

   374       (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"

   376 instance ..

   378 end

   381 instantiation Enum.finite_1 :: check_all

   382 begin

   384 definition

   385   "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"

   387 definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"

   388 where

   389   "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^isub>1])"

   391 instance ..

   393 end

   395 instantiation Enum.finite_2 :: check_all

   396 begin

   398 definition

   399   "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))"

   401 definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"

   402 where

   403   "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"

   405 instance ..

   407 end

   409 instantiation Enum.finite_3 :: check_all

   410 begin

   412 definition

   413   "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)))"

   415 definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"

   416 where

   417   "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"

   419 instance ..

   421 end

   423 subsection {* Bounded universal quantifiers *}

   425 class bounded_forall =

   426   fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"

   428 subsection {* Fast exhaustive combinators *}

   431 class fast_exhaustive = term_of +

   432   fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"

   434 consts throw_Counterexample :: "term list => unit"

   435 consts catch_Counterexample :: "unit => term list option"

   437 code_const throw_Counterexample

   438   (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")

   439 code_const catch_Counterexample

   440   (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")

   442 subsection {* Defining combinators for any first-order data type *}

   444 definition catch_match :: "term list option => term list option => term list option"

   445 where

   446   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"

   448 code_const catch_match

   449   (Quickcheck "(_) handle Match => _")

   451 use "Tools/Quickcheck/exhaustive_generators.ML"

   453 setup {* Exhaustive_Generators.setup *}

   455 declare [[quickcheck_tester = exhaustive]]

   457 hide_fact orelse_def catch_match_def

   458 no_notation orelse (infixr "orelse" 55)

   459 hide_const (open) orelse catch_match mk_map_term check_all_n_lists

   461 end

author	wenzelm
	Thu, 07 Jul 2011 23:55:15 +0200
changeset 44572	91c4d7397f0e
parent 43170	c664cc5cc5e9
child 44753	05d5696f177f
permissions	-rw-r--r--