src/HOL/Quickcheck_Exhaustive.thy
changeset 42305 494c31fdec95
parent 42304 34366f39d32d
child 42310 c664cc5cc5e9
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -390,6 +390,20 @@
     1.4  class bounded_forall =
     1.5    fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
     1.6  
     1.7 +subsection {* Fast exhaustive combinators *}
     1.8 +
     1.9 +
    1.10 +class fast_exhaustive = term_of +
    1.11 +  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
    1.12 +
    1.13 +consts throw_Counterexample :: "term list => unit"
    1.14 +consts catch_Counterexample :: "unit => term list option"
    1.15 +
    1.16 +code_const throw_Counterexample
    1.17 +  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
    1.18 +code_const catch_Counterexample
    1.19 +  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
    1.20 +
    1.21  subsection {* Defining combinators for any first-order data type *}
    1.22  
    1.23  definition catch_match :: "term list option => term list option => term list option"