adding check_all instance for sets; tuned
authorbulwahn
Fri Jan 20 09:28:50 2012 +0100 (2012-01-20)
changeset 463058ea02e499d53
parent 46304 ef5d8e94f66f
child 46306 940ddb42c998
adding check_all instance for sets; tuned
src/HOL/Library/List_Cset.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quotient_Examples/List_Quotient_Cset.thy
     1.1 --- a/src/HOL/Library/List_Cset.thy	Fri Jan 20 08:24:51 2012 +0100
     1.2 +++ b/src/HOL/Library/List_Cset.thy	Fri Jan 20 09:28:50 2012 +0100
     1.3 @@ -15,9 +15,9 @@
     1.4    by (simp_all add: fun_eq_iff List.member_def)
     1.5  
     1.6  definition (in term_syntax)
     1.7 -  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     1.8 +  csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     1.9      \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    1.10 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    1.11 +  [code_unfold]: "csetify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    1.12  
    1.13  notation fcomp (infixl "\<circ>>" 60)
    1.14  notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.15 @@ -26,7 +26,7 @@
    1.16  begin
    1.17  
    1.18  definition
    1.19 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    1.20 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
    1.21  
    1.22  instance ..
    1.23  
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 08:24:51 2012 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 09:28:50 2012 +0100
     2.3 @@ -146,8 +146,8 @@
     2.4  
     2.5  end
     2.6  
     2.7 -definition (in term_syntax) "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
     2.8 -definition (in term_syntax) "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
     2.9 +definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
    2.10 +definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
    2.11  
    2.12  instantiation set :: (full_exhaustive) full_exhaustive
    2.13  begin
    2.14 @@ -160,8 +160,6 @@
    2.15  
    2.16  end
    2.17  
    2.18 -hide_const valterm_emptyset valtermify_insert
    2.19 -
    2.20  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    2.21  begin
    2.22  
    2.23 @@ -252,6 +250,33 @@
    2.24  
    2.25  end
    2.26  
    2.27 +fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option"
    2.28 +where
    2.29 +  "check_all_subsets f [] = f valterm_emptyset"
    2.30 +| "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"
    2.31 +
    2.32 +
    2.33 +definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
    2.34 +definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set)  <\<cdot>> x <\<cdot>> s"
    2.35 +
    2.36 +definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
    2.37 +where
    2.38 +  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
    2.39 +
    2.40 +instantiation set :: (check_all) check_all
    2.41 +begin
    2.42 +
    2.43 +definition
    2.44 +  "check_all_set f =
    2.45 +     check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
    2.46 +
    2.47 +definition enum_term_of_set :: "'a set itself => unit => term list"
    2.48 +where
    2.49 +  "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
    2.50 +
    2.51 +instance ..
    2.52 +
    2.53 +end
    2.54  
    2.55  instantiation unit :: check_all
    2.56  begin
    2.57 @@ -573,11 +598,13 @@
    2.58    exhaustive'_def
    2.59    exhaustive_code_numeral'_def
    2.60  
    2.61 +hide_const valterm_emptyset valtermify_insert term_emptyset termify_insert setify
    2.62 +
    2.63  hide_const (open)
    2.64    exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
    2.65    throw_Counterexample catch_Counterexample
    2.66    check_all enum_term_of
    2.67 -  orelse unknown mk_map_term check_all_n_lists
    2.68 +  orelse unknown mk_map_term check_all_n_lists check_all_subsets
    2.69  
    2.70  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    2.71  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
     3.1 --- a/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 20 08:24:51 2012 +0100
     3.2 +++ b/src/HOL/Quotient_Examples/List_Quotient_Cset.thy	Fri Jan 20 09:28:50 2012 +0100
     3.3 @@ -33,9 +33,9 @@
     3.4  by descending (simp add: in_set_member)
     3.5  
     3.6  definition (in term_syntax)
     3.7 -  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     3.8 +  csetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
     3.9      \<Rightarrow> 'a Quotient_Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    3.10 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
    3.11 +  [code_unfold]: "csetify xs = Code_Evaluation.valtermify Quotient_Cset.set {\<cdot>} xs"
    3.12  
    3.13  notation fcomp (infixl "\<circ>>" 60)
    3.14  notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.15 @@ -44,7 +44,7 @@
    3.16  begin
    3.17  
    3.18  definition
    3.19 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    3.20 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (csetify xs))"
    3.21  
    3.22  instance ..
    3.23