src/HOL/Quickcheck_Exhaustive.thy
changeset 62979 1e527c40ae40
parent 62597 b3f2b8c906a6
child 64670 f77b946d18aa
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 14 15:33:23 2016 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Apr 14 15:33:51 2016 +0200
     1.3 @@ -1,4 +1,6 @@
     1.4 -(* Author: Lukas Bulwahn, TU Muenchen *)
     1.5 +(*  Title:      HOL/Quickcheck_Exhaustive.thy
     1.6 +    Author:     Lukas Bulwahn, TU Muenchen
     1.7 +*)
     1.8  
     1.9  section \<open>A simple counterexample generator performing exhaustive testing\<close>
    1.10  
    1.11 @@ -7,32 +9,34 @@
    1.12  keywords "quickcheck_generator" :: thy_decl
    1.13  begin
    1.14  
    1.15 -subsection \<open>basic operations for exhaustive generators\<close>
    1.16 +subsection \<open>Basic operations for exhaustive generators\<close>
    1.17  
    1.18 -definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55)
    1.19 -where
    1.20 -  [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)"
    1.21 +definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option"  (infixr "orelse" 55)
    1.22 +  where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)"
    1.23  
    1.24 -subsection \<open>exhaustive generator type classes\<close>
    1.25 +
    1.26 +subsection \<open>Exhaustive generator type classes\<close>
    1.27  
    1.28  class exhaustive = term_of +
    1.29 -  fixes exhaustive :: "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    1.30 -  
    1.31 +  fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    1.32 +
    1.33  class full_exhaustive = term_of +
    1.34 -  fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
    1.35 +  fixes full_exhaustive ::
    1.36 +    "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    1.37  
    1.38  instantiation natural :: full_exhaustive
    1.39  begin
    1.40  
    1.41 -function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
    1.42 +function full_exhaustive_natural' ::
    1.43 +    "(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
    1.44 +      natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    1.45    where "full_exhaustive_natural' f d i =
    1.46      (if d < i then None
    1.47 -    else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
    1.48 +     else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))"
    1.49  by pat_completeness auto
    1.50  
    1.51  termination
    1.52 -  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    1.53 -    (auto simp add: less_natural_def)
    1.54 +  by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
    1.55  
    1.56  definition "full_exhaustive f d = full_exhaustive_natural' f d 0"
    1.57  
    1.58 @@ -43,15 +47,15 @@
    1.59  instantiation natural :: exhaustive
    1.60  begin
    1.61  
    1.62 -function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option"
    1.63 +function exhaustive_natural' ::
    1.64 +    "(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
    1.65    where "exhaustive_natural' f d i =
    1.66      (if d < i then None
    1.67 -    else (f i orelse exhaustive_natural' f d (i + 1)))"
    1.68 +     else (f i orelse exhaustive_natural' f d (i + 1)))"
    1.69  by pat_completeness auto
    1.70  
    1.71  termination
    1.72 -  by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))")
    1.73 -    (auto simp add: less_natural_def)
    1.74 +  by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def)
    1.75  
    1.76  definition "exhaustive f d = exhaustive_natural' f d 0"
    1.77  
    1.78 @@ -62,12 +66,14 @@
    1.79  instantiation integer :: exhaustive
    1.80  begin
    1.81  
    1.82 -function exhaustive_integer' :: "(integer => (bool * term list) option) => integer => integer => (bool * term list) option"
    1.83 -  where "exhaustive_integer' f d i = (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
    1.84 +function exhaustive_integer' ::
    1.85 +    "(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
    1.86 +  where "exhaustive_integer' f d i =
    1.87 +    (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))"
    1.88  by pat_completeness auto
    1.89  
    1.90 -termination 
    1.91 -  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
    1.92 +termination
    1.93 +  by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
    1.94      (auto simp add: less_integer_def nat_of_integer_def)
    1.95  
    1.96  definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
    1.97 @@ -79,15 +85,23 @@
    1.98  instantiation integer :: full_exhaustive
    1.99  begin
   1.100  
   1.101 -function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option"
   1.102 -  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.103 +function full_exhaustive_integer' ::
   1.104 +    "(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   1.105 +      integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option"
   1.106 +  where "full_exhaustive_integer' f d i =
   1.107 +    (if d < i then None
   1.108 +     else
   1.109 +      (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
   1.110 +        Some t \<Rightarrow> Some t
   1.111 +      | None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))"
   1.112  by pat_completeness auto
   1.113  
   1.114 -termination 
   1.115 -  by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))")
   1.116 +termination
   1.117 +  by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))")
   1.118      (auto simp add: less_integer_def nat_of_integer_def)
   1.119  
   1.120 -definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
   1.121 +definition "full_exhaustive f d =
   1.122 +  full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))"
   1.123  
   1.124  instance ..
   1.125  
   1.126 @@ -96,7 +110,7 @@
   1.127  instantiation nat :: exhaustive
   1.128  begin
   1.129  
   1.130 -definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d"
   1.131 +definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d"
   1.132  
   1.133  instance ..
   1.134  
   1.135 @@ -105,7 +119,8 @@
   1.136  instantiation nat :: full_exhaustive
   1.137  begin
   1.138  
   1.139 -definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d"
   1.140 +definition "full_exhaustive f d =
   1.141 +  full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. Code_Evaluation.term_of (nat_of_natural x))) d"
   1.142  
   1.143  instance ..
   1.144  
   1.145 @@ -114,15 +129,18 @@
   1.146  instantiation int :: exhaustive
   1.147  begin
   1.148  
   1.149 -function exhaustive_int' :: "(int => (bool * term list) option) => int => int => (bool * term list) option"
   1.150 -  where "exhaustive_int' f d i = (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
   1.151 +function exhaustive_int' ::
   1.152 +    "(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
   1.153 +  where "exhaustive_int' f d i =
   1.154 +    (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))"
   1.155  by pat_completeness auto
   1.156  
   1.157 -termination 
   1.158 -  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.159 +termination
   1.160 +  by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
   1.161  
   1.162 -definition "exhaustive f d = exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.163 -  (- (int_of_integer (integer_of_natural d)))"
   1.164 +definition "exhaustive f d =
   1.165 +  exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.166 +    (- (int_of_integer (integer_of_natural d)))"
   1.167  
   1.168  instance ..
   1.169  
   1.170 @@ -131,15 +149,23 @@
   1.171  instantiation int :: full_exhaustive
   1.172  begin
   1.173  
   1.174 -function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option"
   1.175 -  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.176 +function full_exhaustive_int' ::
   1.177 +    "(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   1.178 +      int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option"
   1.179 +  where "full_exhaustive_int' f d i =
   1.180 +    (if d < i then None
   1.181 +     else
   1.182 +      (case f (i, \<lambda>_. Code_Evaluation.term_of i) of
   1.183 +        Some t \<Rightarrow> Some t
   1.184 +       | None \<Rightarrow> full_exhaustive_int' f d (i + 1)))"
   1.185  by pat_completeness auto
   1.186  
   1.187 -termination 
   1.188 -  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   1.189 +termination
   1.190 +  by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto
   1.191  
   1.192 -definition "full_exhaustive f d = full_exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.193 -  (- (int_of_integer (integer_of_natural d)))"
   1.194 +definition "full_exhaustive f d =
   1.195 +  full_exhaustive_int' f (int_of_integer (integer_of_natural d))
   1.196 +    (- (int_of_integer (integer_of_natural d)))"
   1.197  
   1.198  instance ..
   1.199  
   1.200 @@ -148,20 +174,21 @@
   1.201  instantiation prod :: (exhaustive, exhaustive) exhaustive
   1.202  begin
   1.203  
   1.204 -definition
   1.205 -  "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
   1.206 +definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d"
   1.207  
   1.208  instance ..
   1.209  
   1.210  end
   1.211  
   1.212 -definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\<cdot>} x {\<cdot>} y"
   1.213 +definition (in term_syntax)
   1.214 +  [code_unfold]: "valtermify_pair x y =
   1.215 +    Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y"
   1.216  
   1.217  instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
   1.218  begin
   1.219  
   1.220 -definition
   1.221 -  "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d"
   1.222 +definition "full_exhaustive f d =
   1.223 +  full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d"
   1.224  
   1.225  instance ..
   1.226  
   1.227 @@ -172,7 +199,12 @@
   1.228  
   1.229  fun exhaustive_set
   1.230  where
   1.231 -  "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1)))"
   1.232 +  "exhaustive_set f i =
   1.233 +    (if i = 0 then None
   1.234 +     else
   1.235 +      f {} orelse
   1.236 +      exhaustive_set
   1.237 +        (\<lambda>A. f A orelse exhaustive (\<lambda>x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1))"
   1.238  
   1.239  instance ..
   1.240  
   1.241 @@ -181,49 +213,70 @@
   1.242  instantiation set :: (full_exhaustive) full_exhaustive
   1.243  begin
   1.244  
   1.245 -fun full_exhaustive_set 
   1.246 +fun full_exhaustive_set
   1.247  where
   1.248 -  "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))"
   1.249 +  "full_exhaustive_set f i =
   1.250 +    (if i = 0 then None
   1.251 +     else
   1.252 +      f valterm_emptyset orelse
   1.253 +      full_exhaustive_set
   1.254 +        (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive
   1.255 +          (\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))"
   1.256  
   1.257  instance ..
   1.258  
   1.259  end
   1.260  
   1.261 -instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive
   1.262 +instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive
   1.263  begin
   1.264  
   1.265 -fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option"
   1.266 +fun exhaustive_fun' ::
   1.267 +  "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   1.268  where
   1.269 -  "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d)
   1.270 -   orelse (if i > 1 then
   1.271 -     exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b.
   1.272 -       f (g(a := b))) d) d) (i - 1) d else None)"
   1.273 +  "exhaustive_fun' f i d =
   1.274 +    (exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse
   1.275 +      (if i > 1 then
   1.276 +        exhaustive_fun'
   1.277 +          (\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)"
   1.278  
   1.279 -definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => natural => (bool * term list) option"
   1.280 -where
   1.281 -  "exhaustive_fun f d = exhaustive_fun' f d d" 
   1.282 +definition exhaustive_fun ::
   1.283 +  "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   1.284 +  where "exhaustive_fun f d = exhaustive_fun' f d d"
   1.285  
   1.286  instance ..
   1.287  
   1.288  end
   1.289  
   1.290 -definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
   1.291 +definition [code_unfold]:
   1.292 +  "valtermify_absdummy =
   1.293 +    (\<lambda>(v, t).
   1.294 +      (\<lambda>_::'a. v,
   1.295 +        \<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))"
   1.296  
   1.297 -definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
   1.298 +definition (in term_syntax)
   1.299 +  [code_unfold]: "valtermify_fun_upd g a b =
   1.300 +    Code_Evaluation.valtermify
   1.301 +      (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b"
   1.302  
   1.303 -instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
   1.304 +instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive
   1.305  begin
   1.306  
   1.307 -fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option"
   1.308 +fun full_exhaustive_fun' ::
   1.309 +  "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   1.310 +    natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   1.311  where
   1.312 -  "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d)
   1.313 -   orelse (if i > 1 then
   1.314 -     full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b.
   1.315 -       f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)"
   1.316 +  "full_exhaustive_fun' f i d =
   1.317 +    full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse
   1.318 +    (if i > 1 then
   1.319 +      full_exhaustive_fun'
   1.320 +        (\<lambda>g. full_exhaustive
   1.321 +          (\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d
   1.322 +     else None)"
   1.323  
   1.324 -definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
   1.325 -where
   1.326 -  "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 
   1.327 +definition full_exhaustive_fun ::
   1.328 +  "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   1.329 +    natural \<Rightarrow> (bool \<times> term list) option"
   1.330 +  where "full_exhaustive_fun f d = full_exhaustive_fun' f d d"
   1.331  
   1.332  instance ..
   1.333  
   1.334 @@ -232,75 +285,110 @@
   1.335  subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close>
   1.336  
   1.337  class check_all = enum + term_of +
   1.338 -  fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> (bool * term list) option) \<Rightarrow> (bool * term list) option"
   1.339 +  fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option"
   1.340    fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list"
   1.341 -  
   1.342 -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.343 +
   1.344 +fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow>
   1.345 +  (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   1.346  where
   1.347    "check_all_n_lists f n =
   1.348 -     (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
   1.349 +    (if n = 0 then f ([], (\<lambda>_. []))
   1.350 +     else check_all (\<lambda>(x, xt).
   1.351 +      check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))"
   1.352  
   1.353 -definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
   1.354 +definition (in term_syntax)
   1.355 +  [code_unfold]: "termify_fun_upd g a b =
   1.356 +    (Code_Evaluation.termify
   1.357 +      (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)"
   1.358  
   1.359 -definition mk_map_term :: " (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
   1.360 -where
   1.361 -  "mk_map_term T1 T2 domm rng =
   1.362 -     (%_. let T1 = T1 ();
   1.363 -              T2 = T2 ();
   1.364 -              update_term = (%g (a, b).
   1.365 -                Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   1.366 -                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   1.367 -                   (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   1.368 -                      Typerep.Typerep (STR ''fun'') [T1,
   1.369 -                        Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   1.370 -                        g) a) b)
   1.371 -          in
   1.372 -             List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   1.373 +definition mk_map_term ::
   1.374 +  "(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow>
   1.375 +    (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term"
   1.376 +  where "mk_map_term T1 T2 domm rng =
   1.377 +    (\<lambda>_.
   1.378 +      let
   1.379 +        T1 = T1 ();
   1.380 +        T2 = T2 ();
   1.381 +        update_term =
   1.382 +          (\<lambda>g (a, b).
   1.383 +            Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   1.384 +             (Code_Evaluation.Const (STR ''Fun.fun_upd'')
   1.385 +               (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
   1.386 +                  Typerep.Typerep (STR ''fun'') [T1,
   1.387 +                    Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   1.388 +                    g) a) b)
   1.389 +      in
   1.390 +        List.foldl update_term
   1.391 +          (Code_Evaluation.Abs (STR ''x'') T1
   1.392 +            (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))"
   1.393  
   1.394 -instantiation "fun" :: ("{equal, check_all}", check_all) check_all
   1.395 +instantiation "fun" :: ("{equal,check_all}", check_all) check_all
   1.396  begin
   1.397  
   1.398  definition
   1.399    "check_all f =
   1.400      (let
   1.401 -      mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a)));
   1.402 +      mk_term =
   1.403 +        mk_map_term
   1.404 +          (\<lambda>_. Typerep.typerep (TYPE('a)))
   1.405 +          (\<lambda>_. Typerep.typerep (TYPE('b)))
   1.406 +          (enum_term_of (TYPE('a)));
   1.407        enum = (Enum.enum :: 'a list)
   1.408 -    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.409 +    in
   1.410 +      check_all_n_lists
   1.411 +        (\<lambda>(ys, yst). f (the o map_of (zip enum ys), mk_term yst))
   1.412 +        (natural_of_nat (length enum)))"
   1.413  
   1.414 -definition enum_term_of_fun :: "('a => 'b) itself => unit => term list"
   1.415 -where
   1.416 -  "enum_term_of_fun = (%_ _. let
   1.417 -    enum_term_of_a = enum_term_of (TYPE('a));
   1.418 -    mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a
   1.419 -  in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   1.420 - 
   1.421 +definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   1.422 +  where "enum_term_of_fun =
   1.423 +    (\<lambda>_ _.
   1.424 +      let
   1.425 +        enum_term_of_a = enum_term_of (TYPE('a));
   1.426 +        mk_term =
   1.427 +          mk_map_term
   1.428 +            (\<lambda>_. Typerep.typerep (TYPE('a)))
   1.429 +            (\<lambda>_. Typerep.typerep (TYPE('b)))
   1.430 +            enum_term_of_a
   1.431 +      in
   1.432 +        map (\<lambda>ys. mk_term (\<lambda>_. ys) ())
   1.433 +          (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))"
   1.434 +
   1.435  instance ..
   1.436  
   1.437  end
   1.438  
   1.439 -fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option"
   1.440 +fun (in term_syntax) check_all_subsets ::
   1.441 +  "(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow>
   1.442 +    ('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option"
   1.443  where
   1.444    "check_all_subsets f [] = f valterm_emptyset"
   1.445 -| "check_all_subsets f (x # xs) = check_all_subsets (%s. case f s of Some ts => Some ts | None => f (valtermify_insert x s)) xs"
   1.446 +| "check_all_subsets f (x # xs) =
   1.447 +    check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs"
   1.448  
   1.449  
   1.450 -definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)"
   1.451 -definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set)  <\<cdot>> x <\<cdot>> s"
   1.452 +definition (in term_syntax)
   1.453 +  [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)"
   1.454  
   1.455 -definition (in term_syntax) setify :: "('a::typerep) itself => term list => term"
   1.456 +definition (in term_syntax)
   1.457 +  [code_unfold]: "termify_insert x s =
   1.458 +    Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set)  <\<cdot>> x <\<cdot>> s"
   1.459 +
   1.460 +definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term"
   1.461  where
   1.462 -  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 
   1.463 +  "setify T ts = foldr (termify_insert T) ts (term_emptyset T)"
   1.464  
   1.465  instantiation set :: (check_all) check_all
   1.466  begin
   1.467  
   1.468  definition
   1.469    "check_all_set f =
   1.470 -     check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
   1.471 +     check_all_subsets f
   1.472 +      (zip (Enum.enum :: 'a list)
   1.473 +        (map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))"
   1.474  
   1.475 -definition enum_term_of_set :: "'a set itself => unit => term list"
   1.476 -where
   1.477 -  "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
   1.478 +definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list"
   1.479 +  where "enum_term_of_set _ _ =
   1.480 +    map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))"
   1.481  
   1.482  instance ..
   1.483  
   1.484 @@ -309,12 +397,10 @@
   1.485  instantiation unit :: check_all
   1.486  begin
   1.487  
   1.488 -definition
   1.489 -  "check_all f = f (Code_Evaluation.valtermify ())"
   1.490 +definition "check_all f = f (Code_Evaluation.valtermify ())"
   1.491  
   1.492 -definition enum_term_of_unit :: "unit itself => unit => term list"
   1.493 -where
   1.494 -  "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])"
   1.495 +definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list"
   1.496 +  where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])"
   1.497  
   1.498  instance ..
   1.499  
   1.500 @@ -325,55 +411,66 @@
   1.501  begin
   1.502  
   1.503  definition
   1.504 -  "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   1.505 +  "check_all f =
   1.506 +    (case f (Code_Evaluation.valtermify False) of
   1.507 +      Some x' \<Rightarrow> Some x'
   1.508 +    | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
   1.509  
   1.510 -definition enum_term_of_bool :: "bool itself => unit => term list"
   1.511 -where
   1.512 -  "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   1.513 +definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list"
   1.514 +  where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))"
   1.515  
   1.516  instance ..
   1.517  
   1.518  end
   1.519  
   1.520 -definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\<cdot>> x <\<cdot>> y"
   1.521 +definition (in term_syntax) [code_unfold]:
   1.522 +  "termify_pair x y =
   1.523 +    Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y"
   1.524  
   1.525  instantiation prod :: (check_all, check_all) check_all
   1.526  begin
   1.527  
   1.528 -definition
   1.529 -  "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))"
   1.530 +definition "check_all f = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))"
   1.531  
   1.532 -definition enum_term_of_prod :: "('a * 'b) itself => unit => term list"
   1.533 -where
   1.534 -  "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y)
   1.535 -     (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   1.536 +definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   1.537 +  where "enum_term_of_prod =
   1.538 +    (\<lambda>_ _.
   1.539 +      map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y)
   1.540 +        (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))"
   1.541  
   1.542  instance ..
   1.543  
   1.544  end
   1.545  
   1.546 -definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\<cdot>} x"
   1.547 -definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\<cdot>} x"
   1.548 +definition (in term_syntax)
   1.549 +  [code_unfold]: "valtermify_Inl x =
   1.550 +    Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x"
   1.551 +
   1.552 +definition (in term_syntax)
   1.553 +  [code_unfold]: "valtermify_Inr x =
   1.554 +    Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x"
   1.555  
   1.556  instantiation sum :: (check_all, check_all) check_all
   1.557  begin
   1.558  
   1.559  definition
   1.560 -  "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))"
   1.561 +  "check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))"
   1.562  
   1.563 -definition enum_term_of_sum :: "('a + 'b) itself => unit => term list"
   1.564 -where
   1.565 -  "enum_term_of_sum = (%_ _.
   1.566 -     let
   1.567 -       T1 = (Typerep.typerep (TYPE('a)));
   1.568 -       T2 = (Typerep.typerep (TYPE('b)))
   1.569 -     in
   1.570 -       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 
   1.571 -             (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.572 -             (enum_term_of (TYPE('a)) ()) @
   1.573 -       map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 
   1.574 -             (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.575 -             (enum_term_of (TYPE('b)) ()))"
   1.576 +definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list"
   1.577 +  where "enum_term_of_sum =
   1.578 +    (\<lambda>_ _.
   1.579 +      let
   1.580 +        T1 = Typerep.typerep (TYPE('a));
   1.581 +        T2 = Typerep.typerep (TYPE('b))
   1.582 +      in
   1.583 +        map
   1.584 +          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'')
   1.585 +            (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.586 +          (enum_term_of (TYPE('a)) ()) @
   1.587 +        map
   1.588 +          (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'')
   1.589 +            (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]])))
   1.590 +          (enum_term_of (TYPE('b)) ()))"
   1.591  
   1.592  instance ..
   1.593  
   1.594 @@ -383,13 +480,13 @@
   1.595  begin
   1.596  
   1.597  definition
   1.598 -  "check_all f = check_all (%(x, t1). check_all (%(y, t2).
   1.599 -     f (Char x y, %_. Code_Evaluation.App
   1.600 +  "check_all f = check_all (\<lambda>(x, t1). check_all (\<lambda>(y, t2).
   1.601 +     f (Char x y, \<lambda>_. Code_Evaluation.App
   1.602         (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))"
   1.603  
   1.604 -definition enum_term_of_char :: "char itself => unit => term list"
   1.605 +definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list"
   1.606  where
   1.607 -  "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   1.608 +  "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))"
   1.609  
   1.610  instance ..
   1.611  
   1.612 @@ -399,14 +496,29 @@
   1.613  begin
   1.614  
   1.615  definition
   1.616 -  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
   1.617 -    (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.618 -      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   1.619 +  "check_all f =
   1.620 +    f (Code_Evaluation.valtermify (None :: 'a option)) orelse
   1.621 +    check_all
   1.622 +      (\<lambda>(x, t).
   1.623 +        f
   1.624 +          (Some x,
   1.625 +            \<lambda>_. Code_Evaluation.App
   1.626 +              (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.627 +                (Typerep.Typerep (STR ''fun'')
   1.628 +                [Typerep.typerep TYPE('a),
   1.629 +                 Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
   1.630  
   1.631 -definition enum_term_of_option :: "'a option itself => unit => term list"
   1.632 -where
   1.633 -  "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.634 -      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))"
   1.635 +definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list"
   1.636 +  where "enum_term_of_option =
   1.637 +    (\<lambda> _ _.
   1.638 +      Code_Evaluation.term_of (None :: 'a option) #
   1.639 +      (map
   1.640 +        (Code_Evaluation.App
   1.641 +          (Code_Evaluation.Const (STR ''Option.option.Some'')
   1.642 +            (Typerep.Typerep (STR ''fun'')
   1.643 +              [Typerep.typerep TYPE('a),
   1.644 +               Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])))
   1.645 +        (enum_term_of (TYPE('a)) ())))"
   1.646  
   1.647  instance ..
   1.648  
   1.649 @@ -416,12 +528,10 @@
   1.650  instantiation Enum.finite_1 :: check_all
   1.651  begin
   1.652  
   1.653 -definition
   1.654 -  "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
   1.655 +definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)"
   1.656  
   1.657 -definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list"
   1.658 -where
   1.659 -  "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
   1.660 +definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list"
   1.661 +  where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])"
   1.662  
   1.663  instance ..
   1.664  
   1.665 @@ -431,12 +541,13 @@
   1.666  begin
   1.667  
   1.668  definition
   1.669 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1)
   1.670 -    orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
   1.671 +  "check_all f =
   1.672 +    (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse
   1.673 +     f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))"
   1.674  
   1.675 -definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list"
   1.676 -where
   1.677 -  "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   1.678 +definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list"
   1.679 +  where "enum_term_of_finite_2 =
   1.680 +    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))"
   1.681  
   1.682  instance ..
   1.683  
   1.684 @@ -446,13 +557,14 @@
   1.685  begin
   1.686  
   1.687  definition
   1.688 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1)
   1.689 -    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2)
   1.690 -    orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
   1.691 +  "check_all f =
   1.692 +    (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse
   1.693 +     f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse
   1.694 +     f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))"
   1.695  
   1.696 -definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list"
   1.697 -where
   1.698 -  "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   1.699 +definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list"
   1.700 +  where "enum_term_of_finite_3 =
   1.701 +    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))"
   1.702  
   1.703  instance ..
   1.704  
   1.705 @@ -462,14 +574,15 @@
   1.706  begin
   1.707  
   1.708  definition
   1.709 -  "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1)
   1.710 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2)
   1.711 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3)
   1.712 -    orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))"
   1.713 +  "check_all f =
   1.714 +    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse
   1.715 +    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse
   1.716 +    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse
   1.717 +    f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)"
   1.718  
   1.719 -definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list"
   1.720 -where
   1.721 -  "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
   1.722 +definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list"
   1.723 +  where "enum_term_of_finite_4 =
   1.724 +    (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))"
   1.725  
   1.726  instance ..
   1.727  
   1.728 @@ -480,69 +593,61 @@
   1.729  class bounded_forall =
   1.730    fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool"
   1.731  
   1.732 +
   1.733  subsection \<open>Fast exhaustive combinators\<close>
   1.734  
   1.735  class fast_exhaustive = term_of +
   1.736    fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit"
   1.737  
   1.738 -axiomatization throw_Counterexample :: "term list => unit"
   1.739 -axiomatization catch_Counterexample :: "unit => term list option"
   1.740 +axiomatization throw_Counterexample :: "term list \<Rightarrow> unit"
   1.741 +axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option"
   1.742  
   1.743  code_printing
   1.744    constant throw_Counterexample \<rightharpoonup>
   1.745      (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
   1.746  | constant catch_Counterexample \<rightharpoonup>
   1.747 -    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
   1.748 +    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)"
   1.749 +
   1.750  
   1.751  subsection \<open>Continuation passing style functions as plus monad\<close>
   1.752 -  
   1.753 -type_synonym 'a cps = "('a => term list option) => term list option"
   1.754 +
   1.755 +type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option"
   1.756  
   1.757  definition cps_empty :: "'a cps"
   1.758 -where
   1.759 -  "cps_empty = (%cont. None)"
   1.760 +  where "cps_empty = (\<lambda>cont. None)"
   1.761  
   1.762 -definition cps_single :: "'a => 'a cps"
   1.763 -where
   1.764 -  "cps_single v = (%cont. cont v)"
   1.765 +definition cps_single :: "'a \<Rightarrow> 'a cps"
   1.766 +  where "cps_single v = (\<lambda>cont. cont v)"
   1.767  
   1.768 -definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" 
   1.769 -where
   1.770 -  "cps_bind m f = (%cont. m (%a. (f a) cont))"
   1.771 +definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps"
   1.772 +  where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))"
   1.773  
   1.774 -definition cps_plus :: "'a cps => 'a cps => 'a cps"
   1.775 -where
   1.776 -  "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)"
   1.777 +definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps"
   1.778 +  where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)"
   1.779 +
   1.780 +definition cps_if :: "bool \<Rightarrow> unit cps"
   1.781 +  where "cps_if b = (if b then cps_single () else cps_empty)"
   1.782  
   1.783 -definition cps_if :: "bool => unit cps"
   1.784 -where
   1.785 -  "cps_if b = (if b then cps_single () else cps_empty)"
   1.786 +definition cps_not :: "unit cps \<Rightarrow> unit cps"
   1.787 +  where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)"
   1.788  
   1.789 -definition cps_not :: "unit cps => unit cps"
   1.790 -where
   1.791 -  "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
   1.792 -
   1.793 -type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => natural => (bool * term list) option"
   1.794 +type_synonym 'a pos_bound_cps =
   1.795 +  "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option"
   1.796  
   1.797  definition pos_bound_cps_empty :: "'a pos_bound_cps"
   1.798 -where
   1.799 -  "pos_bound_cps_empty = (%cont i. None)"
   1.800 +  where "pos_bound_cps_empty = (\<lambda>cont i. None)"
   1.801  
   1.802 -definition pos_bound_cps_single :: "'a => 'a pos_bound_cps"
   1.803 -where
   1.804 -  "pos_bound_cps_single v = (%cont i. cont v)"
   1.805 +definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps"
   1.806 +  where "pos_bound_cps_single v = (\<lambda>cont i. cont v)"
   1.807  
   1.808 -definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" 
   1.809 -where
   1.810 -  "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))"
   1.811 +definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps"
   1.812 +  where "pos_bound_cps_bind m f = (\<lambda>cont i. if i = 0 then None else (m (\<lambda>a. (f a) cont i) (i - 1)))"
   1.813  
   1.814 -definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps"
   1.815 -where
   1.816 -  "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)"
   1.817 +definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps"
   1.818 +  where "pos_bound_cps_plus a b = (\<lambda>c i. case a c i of None \<Rightarrow> b c i | Some x \<Rightarrow> Some x)"
   1.819  
   1.820 -definition pos_bound_cps_if :: "bool => unit pos_bound_cps"
   1.821 -where
   1.822 -  "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   1.823 +definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps"
   1.824 +  where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)"
   1.825  
   1.826  datatype (plugins only: code extraction) (dead 'a) unknown =
   1.827    Unknown | Known 'a
   1.828 @@ -550,35 +655,44 @@
   1.829  datatype (plugins only: code extraction) (dead 'a) three_valued =
   1.830    Unknown_value | Value 'a | No_value
   1.831  
   1.832 -type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued"
   1.833 +type_synonym 'a neg_bound_cps =
   1.834 +  "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued"
   1.835  
   1.836  definition neg_bound_cps_empty :: "'a neg_bound_cps"
   1.837 -where
   1.838 -  "neg_bound_cps_empty = (%cont i. No_value)"
   1.839 +  where "neg_bound_cps_empty = (\<lambda>cont i. No_value)"
   1.840 +
   1.841 +definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps"
   1.842 +  where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))"
   1.843  
   1.844 -definition neg_bound_cps_single :: "'a => 'a neg_bound_cps"
   1.845 -where
   1.846 -  "neg_bound_cps_single v = (%cont i. cont (Known v))"
   1.847 -
   1.848 -definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" 
   1.849 -where
   1.850 -  "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))"
   1.851 +definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps"
   1.852 +  where "neg_bound_cps_bind m f =
   1.853 +    (\<lambda>cont i.
   1.854 +      if i = 0 then cont Unknown
   1.855 +      else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))"
   1.856  
   1.857 -definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps"
   1.858 -where
   1.859 -  "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))"
   1.860 -
   1.861 -definition neg_bound_cps_if :: "bool => unit neg_bound_cps"
   1.862 -where
   1.863 -  "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   1.864 +definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps"
   1.865 +  where "neg_bound_cps_plus a b =
   1.866 +    (\<lambda>c i.
   1.867 +      case a c i of
   1.868 +        No_value \<Rightarrow> b c i
   1.869 +      | Value x \<Rightarrow> Value x
   1.870 +      | Unknown_value \<Rightarrow>
   1.871 +          (case b c i of
   1.872 +            No_value \<Rightarrow> Unknown_value
   1.873 +          | Value x \<Rightarrow> Value x
   1.874 +          | Unknown_value \<Rightarrow> Unknown_value))"
   1.875  
   1.876 -definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
   1.877 -where
   1.878 -  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
   1.879 +definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps"
   1.880 +  where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)"
   1.881  
   1.882 -definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
   1.883 -where
   1.884 -  "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)"
   1.885 +definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps"
   1.886 +  where "neg_bound_cps_not n =
   1.887 +    (\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)"
   1.888 +
   1.889 +definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps"
   1.890 +  where "pos_bound_cps_not n =
   1.891 +    (\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)"
   1.892 +
   1.893  
   1.894  subsection \<open>Defining generators for any first-order data type\<close>
   1.895  
   1.896 @@ -590,6 +704,7 @@
   1.897  
   1.898  declare [[quickcheck_batch_tester = exhaustive]]
   1.899  
   1.900 +
   1.901  subsection \<open>Defining generators for abstract types\<close>
   1.902  
   1.903  ML_file "Tools/Quickcheck/abstract_generators.ML"
   1.904 @@ -615,10 +730,11 @@
   1.905  end *)
   1.906  
   1.907  hide_fact (open) orelse_def
   1.908 -no_notation orelse (infixr "orelse" 55)
   1.909 +no_notation orelse  (infixr "orelse" 55)
   1.910  
   1.911 -hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
   1.912 -  valtermify_Inl valtermify_Inr
   1.913 +hide_const valtermify_absdummy valtermify_fun_upd
   1.914 +  valterm_emptyset valtermify_insert
   1.915 +  valtermify_pair valtermify_Inl valtermify_Inr
   1.916    termify_fun_upd term_emptyset termify_insert termify_pair setify
   1.917  
   1.918  hide_const (open)
   1.919 @@ -631,9 +747,12 @@
   1.920    orelse unknown mk_map_term check_all_n_lists check_all_subsets
   1.921  
   1.922  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
   1.923 +
   1.924  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not
   1.925 -  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   1.926 -  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   1.927 +  pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind
   1.928 +  pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not
   1.929 +  neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind
   1.930 +  neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not
   1.931    Unknown Known Unknown_value Value No_value
   1.932  
   1.933  end