src/HOL/Quickcheck_Exhaustive.thy
changeset 42195 1e7b62c93f5d
parent 42117 306713ec55c3
child 42230 594480d25aaa
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:36 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 01 13:49:38 2011 +0200
     1.3 @@ -355,7 +355,22 @@
     1.4  
     1.5  end
     1.6  
     1.7 +subsection {* Bounded universal quantifiers *}
     1.8  
     1.9 +class bounded_forall =
    1.10 +  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
    1.11 +
    1.12 +
    1.13 +instantiation nat :: bounded_forall
    1.14 +begin
    1.15 +
    1.16 +fun bounded_forall_nat :: "(nat => bool) => code_numeral => bool"
    1.17 +where
    1.18 +  "bounded_forall P d = ((P 0) \<and> (if d > 0 then bounded_forall (%n. P (Suc n)) (d - 1) else True))"
    1.19 +
    1.20 +instance ..
    1.21 +
    1.22 +end
    1.23  
    1.24  subsection {* Defining combinators for any first-order data type *}
    1.25