src/HOL/Smallcheck.thy
author bulwahn
Mon Nov 22 10:41:58 2010 +0100 (2010-11-22)
changeset 40639 f1f0e6adca0a
parent 40620 7a9278de19ad
child 40899 ef6fde932f4c
permissions -rw-r--r--
adding function generation to SmallCheck; activating exhaustive search space testing
     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 
    11 subsection {* small value generator type classes *}
    12 
    13 class small = term_of +
    14 fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    15 
    16 instantiation unit :: small
    17 begin
    18 
    19 definition "small f d = f ()"
    20 
    21 instance ..
    22 
    23 end
    24 
    25 instantiation int :: small
    26 begin
    27 
    28 function small' :: "(int => term list option) => int => int => term list option"
    29 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)))"
    30 by pat_completeness auto
    31 
    32 termination 
    33   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    34 
    35 definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    36 
    37 instance ..
    38 
    39 end
    40 
    41 instantiation prod :: (small, small) small
    42 begin
    43 
    44 definition
    45   "small f d = small (%x. small (%y. f (x, y)) d) d"
    46 
    47 instance ..
    48 
    49 end
    50 
    51 section {* full small value generator type classes *}
    52 
    53 class full_small = term_of +
    54 fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    55 
    56 instantiation unit :: full_small
    57 begin
    58 
    59 definition "full_small f d = f (Code_Evaluation.valtermify ())"
    60 
    61 instance ..
    62 
    63 end
    64 
    65 instantiation int :: full_small
    66 begin
    67 
    68 function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
    69   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)))"
    70 by pat_completeness auto
    71 
    72 termination 
    73   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    74 
    75 definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    76 
    77 instance ..
    78 
    79 end
    80 
    81 instantiation prod :: (full_small, full_small) full_small
    82 begin
    83 ML {* @{const_name "Pair"} *}
    84 definition
    85   "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
    86     %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
    87 
    88 instance ..
    89 
    90 end
    91 
    92 instantiation "fun" :: ("{equal, full_small}", full_small) full_small
    93 begin
    94 
    95 fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    96 where
    97   "full_small_fun' f i d = (if i > 1 then
    98     full_small (%(a, at). full_small (%(b, bt).
    99       full_small_fun' (%(g, gt). f (g(a := b),
   100         (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   101          
   102 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   103 
   104 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   105 
   106  (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
   107   full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   108 
   109 definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   110 where
   111   "full_small_fun f d = full_small_fun' f d d" 
   112 
   113 
   114 instance ..
   115 
   116 end
   117 
   118 subsection {* Defining combinators for any first-order data type *}
   119 
   120 definition catch_match :: "term list option => term list option => term list option"
   121 where
   122   [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
   123 
   124 code_const catch_match 
   125   (SML "(_) handle Match => _")
   126 
   127 use "Tools/smallvalue_generators.ML"
   128 
   129 (* We do not activate smallcheck yet.
   130 setup {* Smallvalue_Generators.setup *}
   131 *)
   132 
   133 hide_fact catch_match_def
   134 hide_const (open) catch_match
   135 
   136 end