src/HOL/Quickcheck_Exhaustive.thy
changeset 45724 1f5fc44254d7
parent 45722 63b42a7db003
child 45732 ac5775bbc748
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  subsection {* exhaustive generator type classes *}
     1.5  
     1.6  class exhaustive = term_of +
     1.7 -  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
     1.9    
    1.10  class full_exhaustive = term_of +
    1.11    fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
    1.12 @@ -42,7 +42,7 @@
    1.13  instantiation code_numeral :: exhaustive
    1.14  begin
    1.15  
    1.16 -function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    1.17 +function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.18    where "exhaustive_code_numeral' f d i =
    1.19      (if d < i then None
    1.20      else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    1.21 @@ -78,7 +78,7 @@
    1.22  instantiation int :: exhaustive
    1.23  begin
    1.24  
    1.25 -function exhaustive' :: "(int => term list option) => int => int => term list option"
    1.26 +function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
    1.27    where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    1.28  by pat_completeness auto
    1.29  
    1.30 @@ -136,14 +136,14 @@
    1.31  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.32  begin
    1.33  
    1.34 -fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
    1.35 +fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.36  where
    1.37    "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
    1.38     orelse (if i > 1 then
    1.39       exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
    1.40         f (g(a := b))) d) d) (i - 1) d else None)"
    1.41  
    1.42 -definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
    1.43 +definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.44  where
    1.45    "exhaustive_fun f d = exhaustive_fun' f d d" 
    1.46