src/HOL/Quickcheck_Exhaustive.thy
changeset 45722 63b42a7db003
parent 45718 8979b2463fc8
child 45724 1f5fc44254d7
     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 @@ -19,12 +19,12 @@
     1.4    fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.5    
     1.6  class full_exhaustive = term_of +
     1.7 -  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
     1.9  
    1.10  instantiation code_numeral :: full_exhaustive
    1.11  begin
    1.12  
    1.13 -function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.14 +function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.15    where "full_exhaustive_code_numeral' f d i =
    1.16      (if d < i then None
    1.17      else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    1.18 @@ -94,7 +94,7 @@
    1.19  instantiation int :: full_exhaustive
    1.20  begin
    1.21  
    1.22 -function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.23 +function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
    1.24    where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
    1.25  by pat_completeness auto
    1.26  
    1.27 @@ -154,7 +154,7 @@
    1.28  instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
    1.29  begin
    1.30  
    1.31 -fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.32 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.33  where
    1.34    "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
    1.35     orelse (if i > 1 then
    1.36 @@ -168,7 +168,7 @@
    1.37                    (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
    1.38                  (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
    1.39  
    1.40 -definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
    1.41 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
    1.42  where
    1.43    "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
    1.44  
    1.45 @@ -179,10 +179,10 @@
    1.46  subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
    1.47  
    1.48  class check_all = enum + term_of +
    1.49 -  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
    1.50 +  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
    1.51    fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
    1.52    
    1.53 -fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.54 +fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
    1.55  where
    1.56    "check_all_n_lists f n =
    1.57       (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"