src/HOL/Quickcheck_Exhaustive.thy
changeset 51143 0a2371e7ced3
parent 51126 df86080de4cb
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -16,42 +16,78 @@
     1.4  subsection {* exhaustive generator type classes *}
     1.5  
     1.6  class exhaustive = term_of +
     1.7 -  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> code_numeral \<Rightarrow> (bool * term list) option"
     1.8 +  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<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 +  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    1.13  
    1.14 -instantiation code_numeral :: full_exhaustive
    1.15 +instantiation natural :: full_exhaustive
    1.16  begin
    1.17  
    1.18 -function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.19 -  where "full_exhaustive_code_numeral' f d i =
    1.20 +function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
    1.21 +  where "full_exhaustive_natural' f d i =
    1.22      (if d < i then None
    1.23 -    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_code_numeral' f d (i + 1)))"
    1.24 +    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
    1.25  by pat_completeness auto
    1.26  
    1.27  termination
    1.28 -  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.29 +  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    1.30 +    (auto simp add: less_natural_def)
    1.31  
    1.32 -definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    1.33 +definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
    1.34  
    1.35  instance ..
    1.36  
    1.37  end
    1.38  
    1.39 -instantiation code_numeral :: exhaustive
    1.40 +instantiation natural :: exhaustive
    1.41  begin
    1.42  
    1.43 -function exhaustive_code_numeral' :: "(code_numeral => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
    1.44 -  where "exhaustive_code_numeral' f d i =
    1.45 +function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option"
    1.46 +  where "exhaustive_natural' f d i =
    1.47      (if d < i then None
    1.48 -    else (f i orelse exhaustive_code_numeral' f d (i + 1)))"
    1.49 +    else (f i orelse exhaustive_natural' f d (i + 1)))"
    1.50  by pat_completeness auto
    1.51  
    1.52  termination
    1.53 -  by (relation "measure (%(_, d, i). Code_Numeral.nat_of (d + 1 - i))") auto
    1.54 +  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    1.55 +    (auto simp add: less_natural_def)
    1.56 +
    1.57 +definition "exhaustive f d = exhaustive_natural' f d 0"
    1.58 +
    1.59 +instance ..
    1.60 +
    1.61 +end
    1.62 +
    1.63 +instantiation integer :: exhaustive
    1.64 +begin
    1.65 +
    1.66 +function exhaustive_integer' :: "(integer => (bool * term list) option) => integer => integer => (bool * term list) option"
    1.67 +  where "exhaustive_integer' f d i = (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
    1.68 +by pat_completeness auto
    1.69  
    1.70 -definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    1.71 +termination 
    1.72 +  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
    1.73 +    (auto simp add: less_integer_def nat_of_integer_def)
    1.74 +
    1.75 +definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    1.76 +
    1.77 +instance ..
    1.78 +
    1.79 +end
    1.80 +
    1.81 +instantiation integer :: full_exhaustive
    1.82 +begin
    1.83 +
    1.84 +function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option"
    1.85 +  where "full_exhaustive_integer' 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_integer' f d (i + 1)))"
    1.86 +by pat_completeness auto
    1.87 +
    1.88 +termination 
    1.89 +  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
    1.90 +    (auto simp add: less_integer_def nat_of_integer_def)
    1.91 +
    1.92 +definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    1.93  
    1.94  instance ..
    1.95  
    1.96 @@ -60,7 +96,7 @@
    1.97  instantiation nat :: exhaustive
    1.98  begin
    1.99  
   1.100 -definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
   1.101 +definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d"
   1.102  
   1.103  instance ..
   1.104  
   1.105 @@ -69,7 +105,7 @@
   1.106  instantiation nat :: full_exhaustive
   1.107  begin
   1.108  
   1.109 -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.110 +definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d"
   1.111  
   1.112  instance ..
   1.113  
   1.114 @@ -78,14 +114,15 @@
   1.115  instantiation int :: exhaustive
   1.116  begin
   1.117  
   1.118 -function exhaustive' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
   1.119 -  where "exhaustive' f d i = (if d < i then None else (f i orelse exhaustive' f d (i + 1)))"
   1.120 +function exhaustive_int' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
   1.121 +  where "exhaustive_int' f d i = (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
   1.122  by pat_completeness auto
   1.123  
   1.124  termination 
   1.125    by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.126  
   1.127 -definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   1.128 +definition "exhaustive f d = exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.129 +  (- (int_of_integer (integer_of_natural d)))"
   1.130  
   1.131  instance ..
   1.132  
   1.133 @@ -94,14 +131,15 @@
   1.134  instantiation int :: full_exhaustive
   1.135  begin
   1.136  
   1.137 -function full_exhaustive' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
   1.138 -  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.139 +function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
   1.140 +  where "full_exhaustive_int' 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_int' f d (i + 1)))"
   1.141  by pat_completeness auto
   1.142  
   1.143  termination 
   1.144    by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.145  
   1.146 -definition "full_exhaustive f d = full_exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   1.147 +definition "full_exhaustive f d = full_exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.148 +  (- (int_of_integer (integer_of_natural d)))"
   1.149  
   1.150  instance ..
   1.151  
   1.152 @@ -154,14 +192,14 @@
   1.153  instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   1.154  begin
   1.155  
   1.156 -fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   1.157 +fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option"
   1.158  where
   1.159    "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   1.160     orelse (if i > 1 then
   1.161       exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   1.162         f (g(a := b))) d) d) (i - 1) d else None)"
   1.163  
   1.164 -definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.165 +definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => natural => (bool * term list) option"
   1.166  where
   1.167    "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.168  
   1.169 @@ -176,14 +214,14 @@
   1.170  instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
   1.171  begin
   1.172  
   1.173 -fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => code_numeral => (bool * term list) option"
   1.174 +fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
   1.175  where
   1.176    "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
   1.177     orelse (if i > 1 then
   1.178       full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
   1.179         f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
   1.180  
   1.181 -definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.182 +definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
   1.183  where
   1.184    "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   1.185  
   1.186 @@ -197,7 +235,7 @@
   1.187    fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
   1.188    fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   1.189    
   1.190 -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.191 +fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   1.192  where
   1.193    "check_all_n_lists f n =
   1.194       (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   1.195 @@ -227,7 +265,7 @@
   1.196      (let
   1.197        mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   1.198        enum = (Enum.enum :: 'a list)
   1.199 -    in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (Code_Numeral.of_nat (length enum)))"
   1.200 +    in check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (natural_of_nat (length enum)))"
   1.201  
   1.202  definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   1.203  where
   1.204 @@ -470,12 +508,12 @@
   1.205  subsection {* Bounded universal quantifiers *}
   1.206  
   1.207  class bounded_forall =
   1.208 -  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> code_numeral \<Rightarrow> bool"
   1.209 +  fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
   1.210  
   1.211  subsection {* Fast exhaustive combinators *}
   1.212  
   1.213  class fast_exhaustive = term_of +
   1.214 -  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> code_numeral \<Rightarrow> unit"
   1.215 +  fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
   1.216  
   1.217  axiomatization throw_Counterexample :: "term list => unit"
   1.218  axiomatization catch_Counterexample :: "unit => term list option"
   1.219 @@ -513,7 +551,7 @@
   1.220  where
   1.221    "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
   1.222  
   1.223 -type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
   1.224 +type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => natural => (bool * term list) option"
   1.225  
   1.226  definition pos_bound_cps_empty :: "'a pos_bound_cps"
   1.227  where
   1.228 @@ -538,7 +576,7 @@
   1.229  datatype 'a unknown = Unknown | Known 'a
   1.230  datatype 'a three_valued = Unknown_value | Value 'a | No_value
   1.231  
   1.232 -type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => code_numeral => term list three_valued"
   1.233 +type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
   1.234  
   1.235  definition neg_bound_cps_empty :: "'a neg_bound_cps"
   1.236  where
   1.237 @@ -573,7 +611,7 @@
   1.238  axiomatization unknown :: 'a
   1.239  
   1.240  notation (output) unknown  ("?")
   1.241 - 
   1.242 +
   1.243  ML_file "Tools/Quickcheck/exhaustive_generators.ML"
   1.244  
   1.245  setup {* Exhaustive_Generators.setup *}
   1.246 @@ -588,15 +626,19 @@
   1.247  no_notation orelse (infixr "orelse" 55)
   1.248  
   1.249  hide_fact
   1.250 -  exhaustive'_def
   1.251 -  exhaustive_code_numeral'_def
   1.252 +  exhaustive_int'_def
   1.253 +  exhaustive_integer'_def
   1.254 +  exhaustive_natural'_def
   1.255  
   1.256  hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
   1.257    valtermify_Inl valtermify_Inr
   1.258    termify_fun_upd term_emptyset termify_insert termify_pair setify
   1.259  
   1.260  hide_const (open)
   1.261 -  exhaustive full_exhaustive exhaustive' exhaustive_code_numeral' full_exhaustive_code_numeral'
   1.262 +  exhaustive full_exhaustive
   1.263 +  exhaustive_int' full_exhaustive_int'
   1.264 +  exhaustive_integer' full_exhaustive_integer'
   1.265 +  exhaustive_natural' full_exhaustive_natural'
   1.266    throw_Counterexample catch_Counterexample
   1.267    check_all enum_term_of
   1.268    orelse unknown mk_map_term check_all_n_lists check_all_subsets