--- 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 ..
--- 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
--- 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 ..