# HG changeset patch
# User bulwahn
# Date 1299853273 -3600
# Node ID 80060d5f864a25c9d73ecbf632d1e56324053adf
# Parent  fba21941bdc576bb00786a7d0f78fd17ae790bb4
renaming constants in Quickcheck_Exhaustive theory

diff -r fba21941bdc5 -r 80060d5f864a src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:12 2011 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Mar 11 15:21:13 2011 +0100
@@ -1,118 +1,80 @@
 (* Author: Lukas Bulwahn, TU Muenchen *)
 
-header {* Another simple counterexample generator *}
+header {* A simple counterexample generator performing exhaustive testing *}
 
-theory Smallcheck
+theory Quickcheck_Exhautive
 imports Quickcheck
-uses ("Tools/smallvalue_generators.ML")
+uses ("Tools/exhaustive_generators.ML")
 begin
 
-subsection {* basic operations for generators *}
+subsection {* basic operations for exhaustive generators *}
 
 definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
 where
   [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
 
-subsection {* small value generator type classes *}
-
-class small = term_of +
-fixes small :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
-
-instantiation unit :: small
-begin
+subsection {* exhaustive generator type classes *}
 
-definition "small f d = f ()"
-
-instance ..
+class exhaustive = term_of +
+fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
 
-end
-
-instantiation int :: small
+instantiation unit :: exhaustive
 begin
 
-function small' :: "(int => term list option) => int => int => term list option"
-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)))"
-by pat_completeness auto
-
-termination 
-  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
-
-definition "small f d = small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
-
-instance ..
-
-end
-
-instantiation prod :: (small, small) small
-begin
-
-definition
-  "small f d = small (%x. small (%y. f (x, y)) d) d"
+definition "exhaustive f d = f (Code_Evaluation.valtermify ())"
 
 instance ..
 
 end
 
-subsection {* full small value generator type classes *}
-
-class full_small = term_of +
-fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
-
-instantiation unit :: full_small
+instantiation code_numeral :: exhaustive
 begin
 
-definition "full_small f d = f (Code_Evaluation.valtermify ())"
-
-instance ..
-
-end
-
-instantiation code_numeral :: full_small
-begin
-
-function full_small_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
-  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)))"
+function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+  where "exhaustive_code_numeral' f d i =
+    (if d < i then None
+    else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
 by pat_completeness auto
 
 termination 
   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
 
-definition "full_small f d = full_small_code_numeral' f d 0"
+definition "exhaustive f d = exhaustive_code_numeral' f d 0"
 
 instance ..
 
 end
 
-instantiation nat :: full_small
+instantiation nat :: exhaustive
 begin
 
-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"
+definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
 
 instance ..
 
 end
 
-instantiation int :: full_small
+instantiation int :: exhaustive
 begin
 
-function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
-  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)))"
+function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
+  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)))"
 by pat_completeness auto
 
 termination 
   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
 
-definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
+definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
 
 instance ..
 
 end
 
-instantiation prod :: (full_small, full_small) full_small
+instantiation prod :: (exhaustive, exhaustive) exhaustive
 begin
 
 definition
-  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
+  "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
     %u. let T1 = (Typerep.typerep (TYPE('a)));
             T2 = (Typerep.typerep (TYPE('b)))
     in Code_Evaluation.App (Code_Evaluation.App (
@@ -124,14 +86,14 @@
 
 end
 
-instantiation "fun" :: ("{equal, full_small}", full_small) full_small
+instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
 begin
 
-fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
+fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
 where
-  "full_small_fun' f i d = (if i > 1 then
-    full_small (%(a, at). full_small (%(b, bt).
-      full_small_fun' (%(g, gt). f (g(a := b),
+  "exhaustive_fun' f i d = (if i > 1 then
+    exhaustive (%(a, at). exhaustive (%(b, bt).
+      exhaustive_fun' (%(g, gt). f (g(a := b),
         (%_. let T1 = (Typerep.typerep (TYPE('a)));
                  T2 = (Typerep.typerep (TYPE('b)))
              in
@@ -141,11 +103,11 @@
                        Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
                (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
   else (if i > 0 then
-    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+    exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
 
-definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
+definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
 where
-  "full_small_fun f d = full_small_fun' f d d" 
+  "exhaustive_fun f d = exhaustive_fun' f d d" 
 
 instance ..
 
@@ -153,7 +115,6 @@
 
 subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
 
-
 class check_all = enum + term_of +
   fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
   fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"