src/HOL/Quickcheck_Exhaustive.thy

 
 subsection {* exhaustive generator type classes *}
 
 class exhaustive = term_of +
   fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+  
+class full_exhaustive = term_of +
   fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
 
-instantiation code_numeral :: exhaustive
+instantiation code_numeral :: full_exhaustive
 begin
 
 function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   where "full_exhaustive_code_numeral' f d i =
     (if d < i then None

 termination
   by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
 
 definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
 
+instance ..
+
+end
+
+instantiation code_numeral :: exhaustive
+begin
+
 function exhaustive_code_numeral' :: "(code_numeral => 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 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 "exhaustive f d = exhaustive_code_numeral' f d 0"
 
-
 instance ..
 
 end
 
 instantiation nat :: exhaustive
 begin
 
 definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
+
+instance ..
+
+end
+
+instantiation nat :: full_exhaustive
+begin
 
 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"
 
 instance ..
 

 termination 
   by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
 
 definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
 
+instance ..
+
+end
+
+instantiation int :: full_exhaustive
+begin
+
 function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
   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)))"
 by pat_completeness auto
 
 termination 

 instantiation prod :: (exhaustive, exhaustive) exhaustive
 begin
 
 definition
   "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
+
+instance ..
+
+end
+
+instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
+begin
 
 definition
   "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
     %u. let T1 = (Typerep.typerep (TYPE('a)));
             T2 = (Typerep.typerep (TYPE('b)))

 
 definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
 where
   "exhaustive_fun f d = exhaustive_fun' f d d" 
 
+instance ..
+
+end
+
+instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
+begin
 
 fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
 where
   "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
    orelse (if i > 1 then