renaming constants in Quickcheck_Exhaustive theory
authorbulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 4191680060d5f864a
parent 41915 fba21941bdc5
child 41917 caa650526f98
renaming constants in Quickcheck_Exhaustive theory
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:12 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -1,118 +1,80 @@
     1.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.5  
     1.6 -header {* Another simple counterexample generator *}
     1.7 +header {* A simple counterexample generator performing exhaustive testing *}
     1.8  
     1.9 -theory Smallcheck
    1.10 +theory Quickcheck_Exhautive
    1.11  imports Quickcheck
    1.12 -uses ("Tools/smallvalue_generators.ML")
    1.13 +uses ("Tools/exhaustive_generators.ML")
    1.14  begin
    1.15  
    1.16 -subsection {* basic operations for generators *}
    1.17 +subsection {* basic operations for exhaustive generators *}
    1.18  
    1.19  definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    1.20  where
    1.21    [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    1.22  
    1.23 -subsection {* small value generator type classes *}
    1.24 -
    1.25 -class small = term_of +
    1.26 -fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.27 -
    1.28 -instantiation unit :: small
    1.29 -begin
    1.30 +subsection {* exhaustive generator type classes *}
    1.31  
    1.32 -definition "small f d = f ()"
    1.33 -
    1.34 -instance ..
    1.35 +class exhaustive = term_of +
    1.36 +fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.37  
    1.38 -end
    1.39 -
    1.40 -instantiation int :: small
    1.41 +instantiation unit :: exhaustive
    1.42  begin
    1.43  
    1.44 -function small' :: "(int => term list option) => int => int => term list option"
    1.45 -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)))"
    1.46 -by pat_completeness auto
    1.47 -
    1.48 -termination 
    1.49 -  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    1.50 -
    1.51 -definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.52 -
    1.53 -instance ..
    1.54 -
    1.55 -end
    1.56 -
    1.57 -instantiation prod :: (small, small) small
    1.58 -begin
    1.59 -
    1.60 -definition
    1.61 -  "small f d = small (%x. small (%y. f (x, y)) d) d"
    1.62 +definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
    1.63  
    1.64  instance ..
    1.65  
    1.66  end
    1.67  
    1.68 -subsection {* full small value generator type classes *}
    1.69 -
    1.70 -class full_small = term_of +
    1.71 -fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.72 -
    1.73 -instantiation unit :: full_small
    1.74 +instantiation code_numeral :: exhaustive
    1.75  begin
    1.76  
    1.77 -definition "full_small f d = f (Code_Evaluation.valtermify ())"
    1.78 -
    1.79 -instance ..
    1.80 -
    1.81 -end
    1.82 -
    1.83 -instantiation code_numeral :: full_small
    1.84 -begin
    1.85 -
    1.86 -function full_small_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.87 -  where "full_small_code_numeral' 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_code_numeral' f d (i + 1)))"
    1.88 +function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.89 +  where "exhaustive_code_numeral' f d i =
    1.90 +    (if d < i then None
    1.91 +    else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
    1.92  by pat_completeness auto
    1.93  
    1.94  termination 
    1.95    by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.96  
    1.97 -definition "full_small f d = full_small_code_numeral' f d 0"
    1.98 +definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    1.99  
   1.100  instance ..
   1.101  
   1.102  end
   1.103  
   1.104 -instantiation nat :: full_small
   1.105 +instantiation nat :: exhaustive
   1.106  begin
   1.107  
   1.108 -definition "full_small f d = full_small (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
   1.109 +definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
   1.110  
   1.111  instance ..
   1.112  
   1.113  end
   1.114  
   1.115 -instantiation int :: full_small
   1.116 +instantiation int :: exhaustive
   1.117  begin
   1.118  
   1.119 -function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
   1.120 -  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)))"
   1.121 +function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
   1.122 +  where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
   1.123  by pat_completeness auto
   1.124  
   1.125  termination 
   1.126    by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.127  
   1.128 -definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   1.129 +definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   1.130  
   1.131  instance ..
   1.132  
   1.133  end
   1.134  
   1.135 -instantiation prod :: (full_small, full_small) full_small
   1.136 +instantiation prod :: (exhaustive, exhaustive) exhaustive
   1.137  begin
   1.138  
   1.139  definition
   1.140 -  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
   1.141 +  "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
   1.142      %u. let T1 = (Typerep.typerep (TYPE('a)));
   1.143              T2 = (Typerep.typerep (TYPE('b)))
   1.144      in Code_Evaluation.App (Code_Evaluation.App (
   1.145 @@ -124,14 +86,14 @@
   1.146  
   1.147  end
   1.148  
   1.149 -instantiation "fun" :: ("{equal, full_small}", full_small) full_small
   1.150 +instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   1.151  begin
   1.152  
   1.153 -fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   1.154 +fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   1.155  where
   1.156 -  "full_small_fun' f i d = (if i > 1 then
   1.157 -    full_small (%(a, at). full_small (%(b, bt).
   1.158 -      full_small_fun' (%(g, gt). f (g(a := b),
   1.159 +  "exhaustive_fun' f i d = (if i > 1 then
   1.160 +    exhaustive (%(a, at). exhaustive (%(b, bt).
   1.161 +      exhaustive_fun' (%(g, gt). f (g(a := b),
   1.162          (%_. let T1 = (Typerep.typerep (TYPE('a)));
   1.163                   T2 = (Typerep.typerep (TYPE('b)))
   1.164               in
   1.165 @@ -141,11 +103,11 @@
   1.166                         Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   1.167                 (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
   1.168    else (if i > 0 then
   1.169 -    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   1.170 +    exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   1.171  
   1.172 -definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.173 +definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.174  where
   1.175 -  "full_small_fun f d = full_small_fun' f d d" 
   1.176 +  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.177  
   1.178  instance ..
   1.179  
   1.180 @@ -153,7 +115,6 @@
   1.181  
   1.182  subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
   1.183  
   1.184 -
   1.185  class check_all = enum + term_of +
   1.186    fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   1.187    fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"