author bulwahn Fri Mar 11 15:21:13 2011 +0100 (2011-03-11) changeset 41916 80060d5f864a parent 41915 fba21941bdc5 child 41917 caa650526f98
renaming constants in Quickcheck_Exhaustive theory
```     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"
```