src/HOL/Quickcheck_Exhaustive.thy
changeset 46305 8ea02e499d53
parent 46193 55a4769d0abe
child 46307 ec8f975c059b
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 08:24:51 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Jan 20 09:28:50 2012 +0100
     1.3 @@ -146,8 +146,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 -definition (in term_syntax) "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
     1.8 -definition (in term_syntax) "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
     1.9 +definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
    1.10 +definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
    1.11  
    1.12  instantiation set :: (full_exhaustive) full_exhaustive
    1.13  begin
    1.14 @@ -160,8 +160,6 @@
    1.15  
    1.16  end
    1.17  
    1.18 -hide_const valterm_emptyset valtermify_insert
    1.19 -
    1.20  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.21  begin
    1.22  
    1.23 @@ -252,6 +250,33 @@
    1.24  
    1.25  end
    1.26  
    1.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"
    1.28 +where
    1.29 +  "check_all_subsets f [] = f valterm_emptyset"
    1.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"
    1.31 +
    1.32 +
    1.33 +definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
    1.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"
    1.35 +
    1.36 +definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
    1.37 +where
    1.38 +  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
    1.39 +
    1.40 +instantiation set :: (check_all) check_all
    1.41 +begin
    1.42 +
    1.43 +definition
    1.44 +  "check_all_set f =
    1.45 +     check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
    1.46 +
    1.47 +definition enum_term_of_set :: "'a set itself => unit => term list"
    1.48 +where
    1.49 +  "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
    1.50 +
    1.51 +instance ..
    1.52 +
    1.53 +end
    1.54  
    1.55  instantiation unit :: check_all
    1.56  begin
    1.57 @@ -573,11 +598,13 @@
    1.58    exhaustive'_def
    1.59    exhaustive_code_numeral'_def
    1.60  
    1.61 +hide_const valterm_emptyset valtermify_insert term_emptyset termify_insert setify
    1.62 +
    1.63  hide_const (open)
    1.64    exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
    1.65    throw_Counterexample catch_Counterexample
    1.66    check_all enum_term_of
    1.67 -  orelse unknown mk_map_term check_all_n_lists
    1.68 +  orelse unknown mk_map_term check_all_n_lists check_all_subsets
    1.69  
    1.70  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    1.71  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not