src/HOL/Quickcheck_Exhaustive.thy
changeset 45450 dc2236b19a3d
parent 43882 05d5696f177f
child 45684 3d6ee9c7d7ef
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:44 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Nov 11 08:32:45 2011 +0100
     1.3 @@ -427,7 +427,6 @@
     1.4  
     1.5  subsection {* Fast exhaustive combinators *}
     1.6  
     1.7 -
     1.8  class fast_exhaustive = term_of +
     1.9    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
    1.10  
    1.11 @@ -439,6 +438,89 @@
    1.12  code_const catch_Counterexample
    1.13    (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
    1.14  
    1.15 +subsection {* Continuation passing style functions as plus monad *}
    1.16 +  
    1.17 +type_synonym 'a cps = "('a => term list option) => term list option"
    1.18 +
    1.19 +definition cps_empty :: "'a cps"
    1.20 +where
    1.21 +  "cps_empty = (%cont. None)"
    1.22 +
    1.23 +definition cps_single :: "'a => 'a cps"
    1.24 +where
    1.25 +  "cps_single v = (%cont. cont v)"
    1.26 +
    1.27 +definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
    1.28 +where
    1.29 +  "cps_bind m f = (%cont. m (%a. (f a) cont))"
    1.30 +
    1.31 +definition cps_plus :: "'a cps => 'a cps => 'a cps"
    1.32 +where
    1.33 +  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
    1.34 +
    1.35 +definition cps_if :: "bool => unit cps"
    1.36 +where
    1.37 +  "cps_if b = (if b then cps_single () else cps_empty)"
    1.38 +
    1.39 +definition cps_not :: "unit cps => unit cps"
    1.40 +where
    1.41 +  "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
    1.42 +
    1.43 +type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
    1.44 +
    1.45 +definition pos_bound_cps_empty :: "'a pos_bound_cps"
    1.46 +where
    1.47 +  "pos_bound_cps_empty = (%cont i. None)"
    1.48 +
    1.49 +definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
    1.50 +where
    1.51 +  "pos_bound_cps_single v = (%cont i. cont v)"
    1.52 +
    1.53 +definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
    1.54 +where
    1.55 +  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
    1.56 +
    1.57 +definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
    1.58 +where
    1.59 +  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
    1.60 +
    1.61 +definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
    1.62 +where
    1.63 +  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
    1.64 +
    1.65 +datatype 'a unknown = Unknown | Known 'a
    1.66 +datatype 'a three_valued = Unknown_value | Value 'a | No_value
    1.67 +
    1.68 +type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
    1.69 +
    1.70 +definition neg_bound_cps_empty :: "'a neg_bound_cps"
    1.71 +where
    1.72 +  "neg_bound_cps_empty = (%cont i. No_value)"
    1.73 +
    1.74 +definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
    1.75 +where
    1.76 +  "neg_bound_cps_single v = (%cont i. cont (Known v))"
    1.77 +
    1.78 +definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
    1.79 +where
    1.80 +  "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
    1.81 +
    1.82 +definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
    1.83 +where
    1.84 +  "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))"
    1.85 +
    1.86 +definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
    1.87 +where
    1.88 +  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
    1.89 +
    1.90 +definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
    1.91 +where
    1.92 +  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
    1.93 +
    1.94 +definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
    1.95 +where
    1.96 +  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
    1.97 +
    1.98  subsection {* Defining combinators for any first-order data type *}
    1.99  
   1.100  definition catch_match :: "term list option => term list option => term list option"
   1.101 @@ -456,6 +538,12 @@
   1.102  
   1.103  hide_fact orelse_def catch_match_def
   1.104  no_notation orelse (infixr "orelse" 55)
   1.105 -hide_const (open) orelse catch_match mk_map_term check_all_n_lists
   1.106 +hide_const (open) orelse catch_match mk_map_term check_all_n_lists 
   1.107  
   1.108 -end
   1.109 \ No newline at end of file
   1.110 +hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   1.111 +hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   1.112 +  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   1.113 +  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   1.114 +  Unknown Known Unknown_value Value No_value
   1.115 +
   1.116 +end