src/HOL/Quickcheck_Exhaustive.thy
changeset 42304 34366f39d32d
parent 42274 50850486f8dc
child 42305 494c31fdec95
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 07 21:49:24 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -16,22 +16,35 @@
     1.4  subsection {* exhaustive generator type classes *}
     1.5  
     1.6  class exhaustive = term_of +
     1.7 -fixes exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.8 +  fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.9 +  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.10  
    1.11  instantiation code_numeral :: exhaustive
    1.12  begin
    1.13  
    1.14 -function exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.15 +function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.16 +  where "full_exhaustive_code_numeral' f d i =
    1.17 +    (if d < i then None
    1.18 +    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    1.19 +by pat_completeness auto
    1.20 +
    1.21 +termination
    1.22 +  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.23 +
    1.24 +definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    1.25 +
    1.26 +function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    1.27    where "exhaustive_code_numeral' f d i =
    1.28      (if d < i then None
    1.29 -    else (f (i, %_. Code_Evaluation.term_of i)) orelse (exhaustive_code_numeral' f d (i + 1)))"
    1.30 +    else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    1.31  by pat_completeness auto
    1.32  
    1.33 -termination 
    1.34 +termination
    1.35    by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.36  
    1.37  definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    1.38  
    1.39 +
    1.40  instance ..
    1.41  
    1.42  end
    1.43 @@ -39,7 +52,9 @@
    1.44  instantiation nat :: exhaustive
    1.45  begin
    1.46  
    1.47 -definition "exhaustive f d = exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.48 +definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
    1.49 +
    1.50 +definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.51  
    1.52  instance ..
    1.53  
    1.54 @@ -48,8 +63,8 @@
    1.55  instantiation int :: exhaustive
    1.56  begin
    1.57  
    1.58 -function exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.59 -  where "exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => exhaustive' f d (i + 1)))"
    1.60 +function exhaustive' :: "(int => term list option) => int => int => term list option"
    1.61 +  where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
    1.62  by pat_completeness auto
    1.63  
    1.64  termination 
    1.65 @@ -57,6 +72,15 @@
    1.66  
    1.67  definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.68  
    1.69 +function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.70 +  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.71 +by pat_completeness auto
    1.72 +
    1.73 +termination 
    1.74 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
    1.75 +
    1.76 +definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.77 +
    1.78  instance ..
    1.79  
    1.80  end
    1.81 @@ -65,7 +89,10 @@
    1.82  begin
    1.83  
    1.84  definition
    1.85 -  "exhaustive f d = exhaustive (%(x, t1). exhaustive (%(y, t2). f ((x, y),
    1.86 +  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
    1.87 +
    1.88 +definition
    1.89 +  "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
    1.90      %u. let T1 = (Typerep.typerep (TYPE('a)));
    1.91              T2 = (Typerep.typerep (TYPE('b)))
    1.92      in Code_Evaluation.App (Code_Evaluation.App (
    1.93 @@ -80,11 +107,23 @@
    1.94  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
    1.95  begin
    1.96  
    1.97 -fun exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.98 +fun exhaustive_fun' :: "(('a => 'b) => term list option) => code_numeral => code_numeral => term list option"
    1.99 +where
   1.100 +  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   1.101 +   orelse (if i > 1 then
   1.102 +     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   1.103 +       f (g(a := b))) d) d) (i - 1) d else None)"
   1.104 +
   1.105 +definition exhaustive_fun :: "(('a => 'b) => term list option) => code_numeral => term list option"
   1.106  where
   1.107 -  "exhaustive_fun' f i d = (exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   1.108 +  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.109 +
   1.110 +
   1.111 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   1.112 +where
   1.113 +  "full_exhaustive_fun' f i d = (full_exhaustive (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d)
   1.114     orelse (if i > 1 then
   1.115 -     exhaustive_fun' (%(g, gt). exhaustive (%(a, at). exhaustive (%(b, bt).
   1.116 +     full_exhaustive_fun' (%(g, gt). full_exhaustive (%(a, at). full_exhaustive (%(b, bt).
   1.117         f (g(a := b),
   1.118           (%_. let A = (Typerep.typerep (TYPE('a)));
   1.119                    B = (Typerep.typerep (TYPE('b)));
   1.120 @@ -94,9 +133,9 @@
   1.121                    (Code_Evaluation.Const (STR ''Fun.fun_upd'') (fun (fun A B) (fun A (fun B (fun A B)))))
   1.122                  (gt ())) (at ())) (bt ())))) d) d) (i - 1) d else None)"
   1.123  
   1.124 -definition exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.125 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   1.126  where
   1.127 -  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.128 +  "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   1.129  
   1.130  instance ..
   1.131