# HG changeset patch
# User bulwahn
# Date 1327048130 -3600
# Node ID 8ea02e499d53fcef838737c0780f6d913de8ebb4
# Parent  ef5d8e94f66f4e3827ca3c544c4e1abc9c90110c
adding check_all instance for sets; tuned

diff -r ef5d8e94f66f -r 8ea02e499d53 src/HOL/Library/List_Cset.thy
--- a/src/HOL/Library/List_Cset.thy	Fri Jan 20 08:24:51 2012 +0100
+++ b/src/HOL/Library/List_Cset.thy	Fri Jan 20 09:28:50 2012 +0100
@@ -15,9 +15,9 @@
   by (simp_all add: fun_eq_iff List.member_def)
 
 definition (in term_syntax)
-  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+  csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
-  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
+  [code_unfold]: "csetify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
@@ -26,7 +26,7 @@
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
 
 instance ..
 
diff -r ef5d8e94f66f -r 8ea02e499d53 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 08:24:51 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 09:28:50 2012 +0100
@@ -146,8 +146,8 @@
 
 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"
+definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
+definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
 
 instantiation set :: (full_exhaustive) full_exhaustive
 begin
@@ -160,8 +160,6 @@
 
 end
 
-hide_const valterm_emptyset valtermify_insert
-
 instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
 begin
 
@@ -252,6 +250,33 @@
 
 end
 
+fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option"
+where
+  "check_all_subsets f [] = f valterm_emptyset"
+| "check_all_subsets f (x # xs) = check_all_subsets (%s. case f s of Some ts => Some ts | None => f (valtermify_insert x s)) xs"
+
+
+definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
+definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set)  <\<cdot>> x <\<cdot>> s"
+
+definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
+where
+  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
+
+instantiation set :: (check_all) check_all
+begin
+
+definition
+  "check_all_set f =
+     check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
+
+definition enum_term_of_set :: "'a set itself => unit => term list"
+where
+  "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
+
+instance ..
+
+end
 
 instantiation unit :: check_all
 begin
@@ -573,11 +598,13 @@
   exhaustive'_def
   exhaustive_code_numeral'_def
 
+hide_const valterm_emptyset valtermify_insert term_emptyset termify_insert setify
+
 hide_const (open)
   exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
   throw_Counterexample catch_Counterexample
   check_all enum_term_of
-  orelse unknown mk_map_term check_all_n_lists
+  orelse unknown mk_map_term check_all_n_lists check_all_subsets
 
 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
diff -r ef5d8e94f66f -r 8ea02e499d53 src/HOL/Quotient_Examples/List_Quotient_Cset.thy
--- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 20 08:24:51 2012 +0100
+++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 20 09:28:50 2012 +0100
@@ -33,9 +33,9 @@
 by descending (simp add: in_set_member)
 
 definition (in term_syntax)
-  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+  csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     \<Rightarrow> 'a Quotient_Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
-  [code_unfold]: "setify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
+  [code_unfold]: "csetify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
 
 notation fcomp (infixl "\<circ>>" 60)
 notation scomp (infixl "\<circ>\<rightarrow>" 60)
@@ -44,7 +44,7 @@
 begin
 
 definition
-  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
 
 instance ..