# HG changeset patch
# User bulwahn
# Date 1326359973 -3600
# Node ID 55a4769d0abe917a7be900098e1150d1d8b41544
# Parent  93eaaacc1955f738260f019f2f02e70579254a5b
adding exhaustive instances for type constructor set

diff -r 93eaaacc1955 -r 55a4769d0abe src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Jan 12 00:14:20 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Jan 12 10:19:33 2012 +0100
@@ -135,6 +135,33 @@
 
 end
 
+instantiation set :: (exhaustive) exhaustive
+begin
+
+fun exhaustive_set
+where
+  "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)))"
+
+instance ..
+
+end
+
+definition (in term_syntax) "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
+definition (in term_syntax) "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
+
+instantiation set :: (full_exhaustive) full_exhaustive
+begin
+
+fun full_exhaustive_set 
+where
+  "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)))"
+
+instance ..
+
+end
+
+hide_const valterm_emptyset valtermify_insert
+
 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
 begin