1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Jan 12 00:14:20 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Jan 12 10:19:33 2012 +0100
     1.3 @@ -135,6 +135,33 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instantiation set :: (exhaustive) exhaustive
     1.8 +begin
     1.9 +
    1.10 +fun exhaustive_set
    1.11 +where
    1.12 +  "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
    1.13 +
    1.14 +instance ..
    1.15 +
    1.16 +end
    1.17 +
    1.18 +definition (in term_syntax) "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
    1.19 +definition (in term_syntax) "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
    1.20 +
    1.21 +instantiation set :: (full_exhaustive) full_exhaustive
    1.22 +begin
    1.23 +
    1.24 +fun full_exhaustive_set 
    1.25 +where
    1.26 +  "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))"
    1.27 +
    1.28 +instance ..
    1.29 +
    1.30 +end
    1.31 +
    1.32 +hide_const valterm_emptyset valtermify_insert
    1.33 +
    1.34  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.35  begin
    1.36