misc tuning and standardization;
authorwenzelm
Thu Apr 14 15:33:51 2016 +0200 (2016-04-14)
changeset 629791e527c40ae40
parent 62978 c04eead96cca
child 62980 fedbdfbaa07a
misc tuning and standardization;
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
     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
     2.1 --- a/src/HOL/Quickcheck_Random.thy	Thu Apr 14 15:33:23 2016 +0200
     2.2 +++ b/src/HOL/Quickcheck_Random.thy	Thu Apr 14 15:33:51 2016 +0200
     2.3 @@ -1,4 +1,6 @@
     2.4 -(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *)
     2.5 +(*  Title:      HOL/Quickcheck_Random.thy
     2.6 +    Author:     Florian Haftmann & Lukas Bulwahn, TU Muenchen
     2.7 +*)
     2.8  
     2.9  section \<open>A simple counterexample generator performing random testing\<close>
    2.10  
     3.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Apr 14 15:33:23 2016 +0200
     3.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Apr 14 15:33:51 2016 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature ABSTRACT_GENERATORS =
     3.5  sig
     3.6    val quickcheck_generator : string -> term option -> term list -> theory -> theory
     3.7 -end;
     3.8 +end
     3.9  
    3.10  structure Abstract_Generators : ABSTRACT_GENERATORS =
    3.11  struct
    3.12 @@ -15,19 +15,17 @@
    3.13  fun check_constrs ctxt tyco constrs =
    3.14    let
    3.15      fun check_type c =
    3.16 -      case try (dest_Type o body_type o fastype_of) c of
    3.17 +      (case try (dest_Type o body_type o fastype_of) c of
    3.18          NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
    3.19        | SOME (tyco', vs) => if not (tyco' = tyco) then
    3.20              error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^
    3.21                "Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".")
    3.22            else
    3.23 -            case try (map dest_TFree) vs of
    3.24 +            (case try (map dest_TFree) vs of
    3.25                NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.")
    3.26 -            | SOME _ => ()
    3.27 -  in
    3.28 -    map check_type constrs
    3.29 -  end
    3.30 -  
    3.31 +            | SOME _ => ()))
    3.32 +  in map check_type constrs end
    3.33 +
    3.34  fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy =
    3.35    let
    3.36      val ctxt = Proof_Context.init_global thy
    3.37 @@ -36,36 +34,36 @@
    3.38      val constrs = map (prep_term ctxt) constrs_raw
    3.39      val _ = check_constrs ctxt tyco constrs
    3.40      val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
    3.41 -    val name = Long_Name.base_name tyco 
    3.42 +    val name = Long_Name.base_name tyco
    3.43      fun mk_dconstrs (Const (s, T)) =
    3.44 -        (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
    3.45 -      | mk_dconstrs t = error (Syntax.string_of_term ctxt t ^
    3.46 -          " is not a valid constructor for quickcheck_generator, which expects a constant.")
    3.47 +          (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
    3.48 +      | mk_dconstrs t =
    3.49 +          error (Syntax.string_of_term ctxt t ^
    3.50 +            " is not a valid constructor for quickcheck_generator, which expects a constant.")
    3.51      fun the_descr _ _ =
    3.52 -      let
    3.53 -        val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
    3.54 -      in
    3.55 -        (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], []))
    3.56 -      end
    3.57 +      let val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))]
    3.58 +      in (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], [])) end
    3.59      fun ensure_sort (sort, instantiate) =
    3.60 -      Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
    3.61 -        (the_descr, instantiate))
    3.62 -      Old_Datatype_Aux.default_config [tyco]
    3.63 +      Quickcheck_Common.ensure_sort
    3.64 +        (((@{sort typerep}, @{sort term_of}), sort), (the_descr, instantiate))
    3.65 +        Old_Datatype_Aux.default_config [tyco]
    3.66    in
    3.67      thy
    3.68 -    |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
    3.69 +    |> ensure_sort
    3.70 +        (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype)
    3.71      |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype)
    3.72      |> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype)
    3.73 -    |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
    3.74 +    |> (case opt_pred of NONE => I
    3.75 +       | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco)))
    3.76    end
    3.77  
    3.78  val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
    3.79 -  
    3.80 +
    3.81  val quickcheck_generator_cmd =
    3.82    gen_quickcheck_generator
    3.83      ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
    3.84      Syntax.read_term
    3.85 -  
    3.86 +
    3.87  val _ =
    3.88    Outer_Syntax.command @{command_keyword quickcheck_generator}
    3.89      "define quickcheck generators for abstract types"
    3.90 @@ -75,4 +73,4 @@
    3.91        >> (fn ((tyco, opt_pred), constrs) =>
    3.92          Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs)))
    3.93  
    3.94 -end;
    3.95 +end
     4.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Apr 14 15:33:23 2016 +0200
     4.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Apr 14 15:33:51 2016 +0200
     4.3 @@ -6,28 +6,30 @@
     4.4  
     4.5  signature EXHAUSTIVE_GENERATORS =
     4.6  sig
     4.7 -  val compile_generator_expr:
     4.8 -    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
     4.9 +  val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list ->
    4.10 +    (bool * term list) option * Quickcheck.report option
    4.11    val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list
    4.12    val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list
    4.13 -  val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option)
    4.14 -    -> Proof.context -> Proof.context
    4.15 -  val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list)
    4.16 -    -> Proof.context -> Proof.context
    4.17 -  val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) -> Proof.context -> Proof.context
    4.18 +  val put_counterexample:
    4.19 +    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) ->
    4.20 +      Proof.context -> Proof.context
    4.21 +  val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list) ->
    4.22 +    Proof.context -> Proof.context
    4.23 +  val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) ->
    4.24 +    Proof.context -> Proof.context
    4.25    exception Counterexample of term list
    4.26    val smart_quantifier : bool Config.T
    4.27    val optimise_equality : bool Config.T
    4.28    val quickcheck_pretty : bool Config.T
    4.29    val setup_exhaustive_datatype_interpretation : theory -> theory
    4.30    val setup_bounded_forall_datatype_interpretation : theory -> theory
    4.31 -  
    4.32    val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
    4.33 -    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    4.34 +    (string * sort) list -> string list -> string -> string list * string list ->
    4.35 +    typ list * typ list -> theory -> theory
    4.36    val instantiate_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
    4.37 -    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    4.38 -
    4.39 -end;
    4.40 +    (string * sort) list -> string list -> string -> string list * string list ->
    4.41 +    typ list * typ list -> theory -> theory
    4.42 +end
    4.43  
    4.44  structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS =
    4.45  struct
    4.46 @@ -43,44 +45,40 @@
    4.47  val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false)
    4.48  val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true)
    4.49  val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true)
    4.50 - 
    4.51 +
    4.52  
    4.53  (** abstract syntax **)
    4.54  
    4.55 -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    4.56 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"})
    4.57  
    4.58  val size = @{term "i :: natural"}
    4.59  val size_pred = @{term "(i :: natural) - 1"}
    4.60  val size_ge_zero = @{term "(i :: natural) > 0"}
    4.61  
    4.62  fun mk_none_continuation (x, y) =
    4.63 -  let
    4.64 -    val (T as Type(@{type_name "option"}, _)) = fastype_of x
    4.65 -  in
    4.66 -    Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y
    4.67 -  end
    4.68 +  let val (T as Type (@{type_name option}, _)) = fastype_of x
    4.69 +  in Const (@{const_name Quickcheck_Exhaustive.orelse}, T --> T --> T) $ x $ y end
    4.70  
    4.71  fun mk_if (b, t, e) =
    4.72 -  let
    4.73 -    val T = fastype_of t
    4.74 -  in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
    4.75 +  let val T = fastype_of t
    4.76 +  in Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e end
    4.77 +
    4.78  
    4.79  (* handling inductive datatypes *)
    4.80  
    4.81  (** constructing generator instances **)
    4.82  
    4.83 -exception FUNCTION_TYPE;
    4.84 +exception FUNCTION_TYPE
    4.85  
    4.86  exception Counterexample of term list
    4.87  
    4.88 -val resultT =  @{typ "(bool * term list) option"};
    4.89 +val resultT =  @{typ "(bool * term list) option"}
    4.90  
    4.91 -val exhaustiveN = "exhaustive";
    4.92 -val full_exhaustiveN = "full_exhaustive";
    4.93 -val bounded_forallN = "bounded_forall";
    4.94 +val exhaustiveN = "exhaustive"
    4.95 +val full_exhaustiveN = "full_exhaustive"
    4.96 +val bounded_forallN = "bounded_forall"
    4.97  
    4.98 -fun fast_exhaustiveT T = (T --> @{typ unit})
    4.99 -  --> @{typ natural} --> @{typ unit}
   4.100 +fun fast_exhaustiveT T = (T --> @{typ unit}) --> @{typ natural} --> @{typ unit}
   4.101  
   4.102  fun exhaustiveT T = (T --> resultT) --> @{typ natural} --> resultT
   4.103  
   4.104 @@ -100,9 +98,7 @@
   4.105        |> map (fn (T, cs) => map (mk_consexpr T) cs)
   4.106        |> map mk_rhs
   4.107      val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts
   4.108 -  in
   4.109 -    map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   4.110 -  end
   4.111 +  in map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) end
   4.112  
   4.113  fun gen_mk_call c T =  (T, fn t => c T $ absdummy T t $ size_pred)
   4.114  
   4.115 @@ -110,9 +106,7 @@
   4.116    let
   4.117      val T = Type (tyco, Ts)
   4.118      val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   4.119 -  in
   4.120 -   (T, fn t => nth functerms k $ absdummy T t $ size_pred)
   4.121 -  end
   4.122 +  in (T, fn t => nth functerms k $ absdummy T t $ size_pred) end
   4.123  
   4.124  fun gen_mk_consexpr test_function simpleT (c, xs) =
   4.125    let
   4.126 @@ -126,49 +120,51 @@
   4.127    let
   4.128      fun test_function T = Free ("f", T --> resultT)
   4.129      val mk_call = gen_mk_call (fn T =>
   4.130 -      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T))
   4.131 +      Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T))
   4.132      val mk_aux_call = gen_mk_aux_call functerms
   4.133      val mk_consexpr = gen_mk_consexpr test_function
   4.134      fun mk_rhs exprs =
   4.135 -      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT))
   4.136 -  in
   4.137 -    mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   4.138 -  end
   4.139 +      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
   4.140 +  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
   4.141  
   4.142  fun mk_bounded_forall_equations functerms =
   4.143    let
   4.144      fun test_function T = Free ("P", T --> @{typ bool})
   4.145      val mk_call = gen_mk_call (fn T =>
   4.146 -      Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"},
   4.147 +      Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},
   4.148          bounded_forallT T))
   4.149      val mk_aux_call = gen_mk_aux_call functerms
   4.150      val mk_consexpr = gen_mk_consexpr test_function
   4.151 -    fun mk_rhs exprs =
   4.152 -      mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"})
   4.153 -  in
   4.154 -    mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   4.155 -  end
   4.156 -  
   4.157 +    fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True})
   4.158 +  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
   4.159 +
   4.160  fun mk_full_equations functerms =
   4.161    let
   4.162      fun test_function T = Free ("f", termifyT T --> resultT)
   4.163 -    fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT)
   4.164 +    fun case_prod_const T =
   4.165 +      HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> Code_Evaluation.term"}, resultT)
   4.166      fun mk_call T =
   4.167        let
   4.168          val full_exhaustive =
   4.169 -          Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
   4.170 +          Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},
   4.171              full_exhaustiveT T)
   4.172 -      in                                   
   4.173 -        (T, fn t => full_exhaustive $
   4.174 -          (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   4.175 +      in
   4.176 +        (T,
   4.177 +          fn t =>
   4.178 +            full_exhaustive $
   4.179 +              (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
   4.180 +              size_pred)
   4.181        end
   4.182      fun mk_aux_call fTs (k, _) (tyco, Ts) =
   4.183        let
   4.184          val T = Type (tyco, Ts)
   4.185          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   4.186        in
   4.187 -        (T, fn t => nth functerms k $
   4.188 -          (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred)
   4.189 +        (T,
   4.190 +          fn t =>
   4.191 +            nth functerms k $
   4.192 +              (case_prod_const T $ absdummy T (absdummy @{typ "unit \<Rightarrow> Code_Evaluation.term"} t)) $
   4.193 +              size_pred)
   4.194        end
   4.195      fun mk_consexpr simpleT (c, xs) =
   4.196        let
   4.197 @@ -176,29 +172,30 @@
   4.198          val constr = Const (c, Ts ---> simpleT)
   4.199          val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   4.200          val Eval_App =
   4.201 -          Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   4.202 +          Const (@{const_name Code_Evaluation.App},
   4.203 +            HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   4.204          val Eval_Const =
   4.205 -          Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   4.206 -        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   4.207 -          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   4.208 -        val start_term = test_function simpleT $ 
   4.209 -        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   4.210 -          $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
   4.211 +          Const (@{const_name Code_Evaluation.Const},
   4.212 +            HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   4.213 +        val term =
   4.214 +          fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   4.215 +            bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   4.216 +        val start_term =
   4.217 +          test_function simpleT $
   4.218 +            (HOLogic.pair_const simpleT @{typ "unit \<Rightarrow> Code_Evaluation.term"} $
   4.219 +              (list_comb (constr, bounds)) $ absdummy @{typ unit} term)
   4.220        in fold_rev (fn f => fn t => f t) fns start_term end
   4.221      fun mk_rhs exprs =
   4.222 -      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs,
   4.223 -        Const (@{const_name "None"}, resultT))
   4.224 -  in
   4.225 -    mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms)
   4.226 -  end
   4.227 -  
   4.228 +      mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT))
   4.229 +  in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end
   4.230 +
   4.231  
   4.232  (** instantiating generator classes **)
   4.233 -  
   4.234 +
   4.235  fun contains_recursive_type_under_function_types xs =
   4.236    exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
   4.237      (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
   4.238 -    
   4.239 +
   4.240  fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames)
   4.241      config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   4.242    if not (contains_recursive_type_under_function_types descr) then
   4.243 @@ -218,106 +215,111 @@
   4.244        ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type");
   4.245      thy)
   4.246  
   4.247 -val instantiate_bounded_forall_datatype = instantiate_datatype
   4.248 - ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
   4.249 -   mk_bounded_forall_equations, bounded_forallT, ["P", "i"]);
   4.250 +val instantiate_bounded_forall_datatype =
   4.251 +  instantiate_datatype
   4.252 +    ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall},
   4.253 +      mk_bounded_forall_equations, bounded_forallT, ["P", "i"])
   4.254  
   4.255 -val instantiate_exhaustive_datatype = instantiate_datatype  
   4.256 -  ("exhaustive generators", exhaustiveN, @{sort exhaustive},
   4.257 -    mk_equations, exhaustiveT, ["f", "i"])
   4.258 +val instantiate_exhaustive_datatype =
   4.259 +  instantiate_datatype
   4.260 +    ("exhaustive generators", exhaustiveN, @{sort exhaustive},
   4.261 +      mk_equations, exhaustiveT, ["f", "i"])
   4.262  
   4.263 -val instantiate_full_exhaustive_datatype = instantiate_datatype
   4.264 -  ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
   4.265 -    mk_full_equations, full_exhaustiveT, ["f", "i"])
   4.266 +val instantiate_full_exhaustive_datatype =
   4.267 +  instantiate_datatype
   4.268 +    ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive},
   4.269 +      mk_full_equations, full_exhaustiveT, ["f", "i"])
   4.270 +
   4.271  
   4.272  (* building and compiling generator expressions *)
   4.273  
   4.274  fun mk_let_expr (x, t, e) genuine =
   4.275 -  let
   4.276 -    val (T1, T2) = (fastype_of x, fastype_of (e genuine))
   4.277 -  in  
   4.278 -    Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)
   4.279 -  end
   4.280 +  let val (T1, T2) = (fastype_of x, fastype_of (e genuine))
   4.281 +  in Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) end
   4.282  
   4.283  fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine =
   4.284    let
   4.285      val (T1, T2) = (fastype_of x, fastype_of (e genuine))
   4.286 -    val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2)
   4.287 +    val if_t = Const (@{const_name If}, @{typ bool} --> T2 --> T2 --> T2)
   4.288    in
   4.289 -    Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $ 
   4.290 +    Const (@{const_name Quickcheck_Random.catch_match}, T2 --> T2 --> T2) $
   4.291        (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $
   4.292        (if_t $ genuine_only $ none $ safe false)
   4.293    end
   4.294  
   4.295  fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt =
   4.296    let
   4.297 -    val cnstrs = flat (maps
   4.298 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   4.299 -      (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt)
   4.300 -         Quickcheck_Common.compat_prefs)))
   4.301 -    fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
   4.302 -        (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
   4.303 -      | _ => false)
   4.304 +    val cnstrs =
   4.305 +      flat (maps
   4.306 +        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
   4.307 +        (Symtab.dest
   4.308 +          (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs)))
   4.309 +    fun is_constrt (Const (s, T), ts) =
   4.310 +          (case (AList.lookup (op =) cnstrs s, body_type T) of
   4.311 +            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
   4.312 +          | _ => false)
   4.313        | is_constrt _ = false
   4.314      fun mk_naive_test_term t =
   4.315 -      fold_rev mk_closure (map lookup (Term.add_free_names t []))
   4.316 -        (mk_if (t, none_t, return) true)
   4.317 +      fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true)
   4.318      fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check
   4.319      fun mk_smart_test_term' concl bound_vars assms genuine =
   4.320        let
   4.321          fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
   4.322          fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) =
   4.323 -          if member (op =) (Term.add_free_names lhs bound_vars) x then
   4.324 -            c (assm, assms)
   4.325 -          else
   4.326 -            (let
   4.327 -               val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms
   4.328 -               fun safe genuine =
   4.329 -                 the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine)
   4.330 -            in
   4.331 -              mk_test (remove (op =) x (vars_of assm),
   4.332 -                mk_let safe f (try lookup x) lhs 
   4.333 -                  (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
   4.334 -            
   4.335 -            end)
   4.336 +              if member (op =) (Term.add_free_names lhs bound_vars) x then
   4.337 +                c (assm, assms)
   4.338 +              else
   4.339 +                let
   4.340 +                   val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms
   4.341 +                   fun safe genuine =
   4.342 +                     the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine)
   4.343 +                in
   4.344 +                  mk_test (remove (op =) x (vars_of assm),
   4.345 +                    mk_let safe f (try lookup x) lhs
   4.346 +                      (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
   4.347 +    
   4.348 +                end
   4.349            | mk_equality_term (lhs, t) c (assm, assms) =
   4.350 -            if is_constrt (strip_comb t) then
   4.351 -              let
   4.352 -                val (constr, args) = strip_comb t
   4.353 -                val T = fastype_of t
   4.354 -                val vars = map Free (Variable.variant_frees ctxt (concl :: assms)
   4.355 -                  (map (fn t => ("x", fastype_of t)) args))
   4.356 -                val varnames = map (fst o dest_Free) vars
   4.357 -                val dummy_var = Free (singleton
   4.358 -                  (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
   4.359 -                val new_assms = map HOLogic.mk_eq (vars ~~ args)
   4.360 -                val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
   4.361 -                val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
   4.362 -              in
   4.363 -                mk_test (vars_of lhs,
   4.364 -                  Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
   4.365 -                    [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
   4.366 -              end
   4.367 -            else c (assm, assms)
   4.368 +              if is_constrt (strip_comb t) then
   4.369 +                let
   4.370 +                  val (constr, args) = strip_comb t
   4.371 +                  val T = fastype_of t
   4.372 +                  val vars =
   4.373 +                    map Free
   4.374 +                      (Variable.variant_frees ctxt (concl :: assms)
   4.375 +                        (map (fn t => ("x", fastype_of t)) args))
   4.376 +                  val varnames = map (fst o dest_Free) vars
   4.377 +                  val dummy_var =
   4.378 +                    Free (singleton
   4.379 +                      (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T))
   4.380 +                  val new_assms = map HOLogic.mk_eq (vars ~~ args)
   4.381 +                  val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars)
   4.382 +                  val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine
   4.383 +                in
   4.384 +                  mk_test (vars_of lhs,
   4.385 +                    Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs
   4.386 +                      [(list_comb (constr, vars), cont_t), (dummy_var, none_t)])
   4.387 +                end
   4.388 +              else c (assm, assms)
   4.389          fun default (assm, assms) =
   4.390 -          mk_test (vars_of assm,
   4.391 -            mk_if (HOLogic.mk_not assm, none_t, 
   4.392 -            mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
   4.393 +          mk_test
   4.394 +            (vars_of assm,
   4.395 +              mk_if (HOLogic.mk_not assm, none_t,
   4.396 +                mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine)
   4.397        in
   4.398 -        case assms of [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine)
   4.399 -          | assm :: assms =>
   4.400 +        (case assms of
   4.401 +          [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine)
   4.402 +        | assm :: assms =>
   4.403              if Config.get ctxt optimise_equality then
   4.404                (case try HOLogic.dest_eq assm of
   4.405                  SOME (lhs, rhs) =>
   4.406                    mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms)
   4.407                | NONE => default (assm, assms))
   4.408 -            else default (assm, assms)
   4.409 +            else default (assm, assms))
   4.410        end
   4.411      val mk_smart_test_term =
   4.412        Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true)
   4.413 -  in
   4.414 -    if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
   4.415 -  end
   4.416 +  in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end
   4.417  
   4.418  fun mk_fast_generator_expr ctxt (t, eval_terms) =
   4.419    let
   4.420 @@ -327,26 +329,31 @@
   4.421      fun lookup v = the (AList.lookup (op =) (names ~~ frees) v)
   4.422      val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
   4.423      val depth = Free (depth_name, @{typ natural})
   4.424 -    fun return _ = @{term "throw_Counterexample :: term list => unit"} $
   4.425 -      (HOLogic.mk_list @{typ "term"}
   4.426 -        (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
   4.427 +    fun return _ =
   4.428 +      @{term "throw_Counterexample :: term list \<Rightarrow> unit"} $
   4.429 +        (HOLogic.mk_list @{typ term}
   4.430 +          (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms)))
   4.431      fun mk_exhaustive_closure (free as Free (_, T)) t =
   4.432 -      Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"},
   4.433 -        fast_exhaustiveT T)
   4.434 -        $ lambda free t $ depth
   4.435 +      Const (@{const_name Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive},
   4.436 +        fast_exhaustiveT T) $ lambda free t $ depth
   4.437      val none_t = @{term "()"}
   4.438      fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
   4.439      fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   4.440 -    val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt 
   4.441 +    val mk_test_term =
   4.442 +      mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt
   4.443    in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end
   4.444  
   4.445 -fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
   4.446 +fun mk_unknown_term T =
   4.447 +  HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T))
   4.448  
   4.449 -fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"}
   4.450 -      $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)    
   4.451 +fun mk_safe_term t =
   4.452 +  @{term "Quickcheck_Random.catch_match :: term \<Rightarrow> term \<Rightarrow> term"} $
   4.453 +    (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t)
   4.454  
   4.455 -fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $
   4.456 -  (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t)
   4.457 +fun mk_return t genuine =
   4.458 +  @{term "Some :: bool \<times> term list \<Rightarrow> (bool \<times> term list) option"} $
   4.459 +    (HOLogic.pair_const @{typ bool} @{typ "term list"} $
   4.460 +      Quickcheck_Common.reflect_bool genuine $ t)
   4.461  
   4.462  fun mk_generator_expr ctxt (t, eval_terms) =
   4.463    let
   4.464 @@ -357,15 +364,17 @@
   4.465      val ([depth_name, genuine_only_name], _) =
   4.466        Variable.variant_fixes ["depth", "genuine_only"] ctxt'
   4.467      val depth = Free (depth_name, @{typ natural})
   4.468 -    val genuine_only = Free (genuine_only_name, @{typ bool}) 
   4.469 -    val return = mk_return (HOLogic.mk_list @{typ "term"}
   4.470 +    val genuine_only = Free (genuine_only_name, @{typ bool})
   4.471 +    val return =
   4.472 +      mk_return (HOLogic.mk_list @{typ term}
   4.473          (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms))
   4.474      fun mk_exhaustive_closure (free as Free (_, T)) t =
   4.475 -      Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
   4.476 -        $ lambda free t $ depth
   4.477 -    val none_t = Const (@{const_name "None"}, resultT)
   4.478 +      Const (@{const_name Quickcheck_Exhaustive.exhaustive_class.exhaustive}, exhaustiveT T) $
   4.479 +        lambda free t $ depth
   4.480 +    val none_t = Const (@{const_name None}, resultT)
   4.481      val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
   4.482 -    fun mk_let safe def v_opt t e = mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
   4.483 +    fun mk_let safe def v_opt t e =
   4.484 +      mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e)
   4.485      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
   4.486    in lambda genuine_only (lambda depth (mk_test_term t)) end
   4.487  
   4.488 @@ -379,33 +388,36 @@
   4.489        Variable.variant_fixes ["depth", "genuine_only"] ctxt'
   4.490      val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt''
   4.491      val depth = Free (depth_name, @{typ natural})
   4.492 -    val genuine_only = Free (genuine_only_name, @{typ bool})    
   4.493 -    val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
   4.494 +    val genuine_only = Free (genuine_only_name, @{typ bool})
   4.495 +    val term_vars = map (fn n => Free (n, @{typ "unit \<Rightarrow> term"})) term_names
   4.496      fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
   4.497 -    val return = mk_return (HOLogic.mk_list @{typ term}
   4.498 +    val return =
   4.499 +      mk_return
   4.500 +        (HOLogic.mk_list @{typ term}
   4.501            (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms))
   4.502      fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
   4.503        if Sign.of_sort thy (T, @{sort check_all}) then
   4.504 -        Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
   4.505 -          $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
   4.506 -            $ lambda free (lambda term_var t))
   4.507 +        Const (@{const_name Quickcheck_Exhaustive.check_all_class.check_all}, check_allT T) $
   4.508 +          (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
   4.509 +            lambda free (lambda term_var t))
   4.510        else
   4.511 -        Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T)
   4.512 -          $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT)
   4.513 -            $ lambda free (lambda term_var t)) $ depth
   4.514 -    val none_t = Const (@{const_name "None"}, resultT)
   4.515 +        Const (@{const_name Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive},
   4.516 +          full_exhaustiveT T) $
   4.517 +          (HOLogic.case_prod_const (T, @{typ "unit \<Rightarrow> term"}, resultT) $
   4.518 +            lambda free (lambda term_var t)) $ depth
   4.519 +    val none_t = Const (@{const_name None}, resultT)
   4.520      val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t
   4.521      fun mk_let safe _ (SOME (v, term_var)) t e =
   4.522 -        mk_safe_let_expr genuine_only none_t safe (v, t, 
   4.523 -          e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))])
   4.524 +          mk_safe_let_expr genuine_only none_t safe (v, t,
   4.525 +            e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))])
   4.526        | mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e)
   4.527      val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt
   4.528    in lambda genuine_only (lambda depth (mk_test_term t)) end
   4.529  
   4.530  fun mk_parametric_generator_expr mk_generator_expr =
   4.531 -  Quickcheck_Common.gen_mk_parametric_generator_expr 
   4.532 +  Quickcheck_Common.gen_mk_parametric_generator_expr
   4.533      ((mk_generator_expr,
   4.534 -      absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name "None"}, resultT)))),
   4.535 +      absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))),
   4.536        @{typ bool} --> @{typ natural} --> resultT)
   4.537  
   4.538  fun mk_validator_expr ctxt t =
   4.539 @@ -418,115 +430,117 @@
   4.540      val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt'
   4.541      val depth = Free (depth_name, @{typ natural})
   4.542      fun mk_bounded_forall (Free (s, T)) t =
   4.543 -      Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T)
   4.544 -        $ lambda (Free (s, T)) t $ depth
   4.545 +      Const (@{const_name Quickcheck_Exhaustive.bounded_forall_class.bounded_forall},
   4.546 +        bounded_forallT T) $ lambda (Free (s, T)) t $ depth
   4.547      fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine)
   4.548      fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e)
   4.549      val mk_test_term =
   4.550        mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt
   4.551    in lambda depth (mk_test_term t) end
   4.552  
   4.553 -
   4.554 -fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = 
   4.555 +fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) =
   4.556    let
   4.557      val frees = Term.add_free_names t []
   4.558 -    val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'')
   4.559 -      (Typerep.Typerep (STR ''dummy'') [])"}
   4.560 -    val return = @{term "Some :: term list => term list option"} $
   4.561 -      (HOLogic.mk_list @{typ "term"}
   4.562 -        (replicate (length frees + length eval_terms) dummy_term))
   4.563 +    val dummy_term =
   4.564 +      @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"}
   4.565 +    val return =
   4.566 +      @{term "Some :: term list => term list option"} $
   4.567 +        (HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term))
   4.568      val wrap = absdummy @{typ bool}
   4.569 -      (@{term "If :: bool => term list option => term list option => term list option"} $
   4.570 +      (@{term "If :: bool \<Rightarrow> term list option \<Rightarrow> term list option \<Rightarrow> term list option"} $
   4.571          Bound 0 $ @{term "None :: term list option"} $ return)
   4.572    in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   4.573 -  
   4.574 +
   4.575  
   4.576  (** generator compiliation **)
   4.577  
   4.578  structure Data = Proof_Data
   4.579  (
   4.580    type T =
   4.581 -    (unit -> Code_Numeral.natural -> bool ->
   4.582 -      Code_Numeral.natural -> (bool * term list) option) *
   4.583 +    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) *
   4.584      (unit -> (Code_Numeral.natural -> term list option) list) *
   4.585 -    (unit -> (Code_Numeral.natural -> bool) list);
   4.586 +    (unit -> (Code_Numeral.natural -> bool) list)
   4.587    val empty: T =
   4.588     (fn () => raise Fail "counterexample",
   4.589      fn () => raise Fail "counterexample_batch",
   4.590 -    fn () => raise Fail "validator_batch");
   4.591 -  fun init _ = empty;
   4.592 -);
   4.593 +    fn () => raise Fail "validator_batch")
   4.594 +  fun init _ = empty
   4.595 +)
   4.596  
   4.597 -val get_counterexample = #1 o Data.get;
   4.598 -val get_counterexample_batch = #2 o Data.get;
   4.599 -val get_validator_batch = #3 o Data.get;
   4.600 +val get_counterexample = #1 o Data.get
   4.601 +val get_counterexample_batch = #2 o Data.get
   4.602 +val get_validator_batch = #3 o Data.get
   4.603  
   4.604 -val put_counterexample = Data.map o @{apply 3(1)} o K;
   4.605 -val put_counterexample_batch = Data.map o @{apply 3(2)} o K;
   4.606 -val put_validator_batch = Data.map o @{apply 3(3)} o K;
   4.607 +val put_counterexample = Data.map o @{apply 3(1)} o K
   4.608 +val put_counterexample_batch = Data.map o @{apply 3(2)} o K
   4.609 +val put_validator_batch = Data.map o @{apply 3(3)} o K
   4.610  
   4.611 -val target = "Quickcheck";
   4.612 +val target = "Quickcheck"
   4.613  
   4.614  fun compile_generator_expr_raw ctxt ts =
   4.615    let
   4.616 -    val mk_generator_expr = 
   4.617 +    val mk_generator_expr =
   4.618        if Config.get ctxt fast then mk_fast_generator_expr
   4.619        else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr
   4.620        else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
   4.621 -    val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
   4.622 -    val compile = Code_Runtime.dynamic_value_strict
   4.623 -      (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
   4.624 -      ctxt (SOME target) (fn proc => fn g =>
   4.625 -        fn card => fn genuine_only => fn size => g card genuine_only size
   4.626 +    val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts
   4.627 +    val compile =
   4.628 +      Code_Runtime.dynamic_value_strict
   4.629 +        (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
   4.630 +        ctxt (SOME target)
   4.631 +        (fn proc => fn g => fn card => fn genuine_only => fn size =>
   4.632 +          g card genuine_only size
   4.633            |> (Option.map o apsnd o map) proc) t' []
   4.634    in
   4.635 -    fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |> 
   4.636 -      (if Config.get ctxt quickcheck_pretty then
   4.637 -        Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
   4.638 -  end;
   4.639 +    fn genuine_only => fn [card, size] =>
   4.640 +      rpair NONE (compile card genuine_only size
   4.641 +      |> (if Config.get ctxt quickcheck_pretty then
   4.642 +          Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I))
   4.643 +  end
   4.644  
   4.645  fun compile_generator_expr ctxt ts =
   4.646 -  let
   4.647 -    val compiled = compile_generator_expr_raw ctxt ts;
   4.648 -  in fn genuine_only => fn [card, size] =>
   4.649 -    compiled genuine_only [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
   4.650 -  end;
   4.651 +  let val compiled = compile_generator_expr_raw ctxt ts in
   4.652 +    fn genuine_only => fn [card, size] =>
   4.653 +      compiled genuine_only
   4.654 +        [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size]
   4.655 +  end
   4.656  
   4.657  fun compile_generator_exprs_raw ctxt ts =
   4.658    let
   4.659 -    val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
   4.660 -    val compiles = Code_Runtime.dynamic_value_strict
   4.661 -      (get_counterexample_batch, put_counterexample_batch,
   4.662 -        "Exhaustive_Generators.put_counterexample_batch")
   4.663 -      ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   4.664 -      (HOLogic.mk_list @{typ "natural => term list option"} ts') []
   4.665 +    val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts
   4.666 +    val compiles =
   4.667 +      Code_Runtime.dynamic_value_strict
   4.668 +        (get_counterexample_batch, put_counterexample_batch,
   4.669 +          "Exhaustive_Generators.put_counterexample_batch")
   4.670 +        ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
   4.671 +        (HOLogic.mk_list @{typ "natural => term list option"} ts') []
   4.672    in
   4.673 -    map (fn compile => fn size => compile size
   4.674 -      |> (Option.map o map) Quickcheck_Common.post_process_term) compiles
   4.675 -  end;
   4.676 +    map (fn compile => fn size =>
   4.677 +      compile size |> (Option.map o map) Quickcheck_Common.post_process_term) compiles
   4.678 +  end
   4.679  
   4.680  fun compile_generator_exprs ctxt ts =
   4.681    compile_generator_exprs_raw ctxt ts
   4.682 -  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size));
   4.683 +  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
   4.684  
   4.685  fun compile_validator_exprs_raw ctxt ts =
   4.686 -  let
   4.687 -    val ts' = map (mk_validator_expr ctxt) ts
   4.688 -  in
   4.689 +  let val ts' = map (mk_validator_expr ctxt) ts in
   4.690      Code_Runtime.dynamic_value_strict
   4.691        (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
   4.692 -      ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
   4.693 -  end;
   4.694 +      ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \<Rightarrow> bool"} ts') []
   4.695 +  end
   4.696  
   4.697  fun compile_validator_exprs ctxt ts =
   4.698    compile_validator_exprs_raw ctxt ts
   4.699 -  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size));
   4.700 +  |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size))
   4.701  
   4.702  fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T,  @{sort check_all})) Ts)
   4.703  
   4.704  val test_goals =
   4.705 -  Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr));
   4.706 -  
   4.707 +  Quickcheck_Common.generator_test_goal_terms
   4.708 +    ("exhaustive", (size_matters_for, compile_generator_expr))
   4.709 +
   4.710 +
   4.711  (* setup *)
   4.712  
   4.713  val setup_exhaustive_datatype_interpretation =
   4.714 @@ -540,7 +554,7 @@
   4.715         (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
   4.716          instantiate_bounded_forall_datatype)))
   4.717  
   4.718 -val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
   4.719 +val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true)
   4.720  
   4.721  val _ =
   4.722    Theory.setup
   4.723 @@ -548,6 +562,6 @@
   4.724        (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype)
   4.725      #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals)))
   4.726      #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs))
   4.727 -    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)));
   4.728 +    #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs)))
   4.729  
   4.730 -end;
   4.731 +end
     5.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 14 15:33:23 2016 +0200
     5.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 14 15:33:51 2016 +0200
     5.3 @@ -15,8 +15,9 @@
     5.4      | Existential_Counterexample of (term * counterexample) list
     5.5      | Empty_Assignment
     5.6    val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
     5.7 -  val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
     5.8 -end;
     5.9 +  val put_existential_counterexample : (unit -> counterexample option) ->
    5.10 +    Proof.context -> Proof.context
    5.11 +end
    5.12  
    5.13  structure Narrowing_Generators : NARROWING_GENERATORS =
    5.14  struct
    5.15 @@ -28,26 +29,29 @@
    5.16  val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
    5.17  val ghc_options = Attrib.setup_config_string @{binding quickcheck_narrowing_ghc_options} (K "")
    5.18  
    5.19 +
    5.20  (* partial_term_of instances *)
    5.21  
    5.22  fun mk_partial_term_of (x, T) =
    5.23    Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
    5.24 -    Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
    5.25 -      $ Logic.mk_type T $ x
    5.26 +    Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $ Logic.mk_type T $ x
    5.27 +
    5.28  
    5.29  (** formal definition **)
    5.30  
    5.31  fun add_partial_term_of tyco raw_vs thy =
    5.32    let
    5.33 -    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    5.34 -    val ty = Type (tyco, map TFree vs);
    5.35 -    val lhs = Const (@{const_name partial_term_of},
    5.36 -        Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
    5.37 -      $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term});
    5.38 -    val rhs = @{term "undefined :: Code_Evaluation.term"};
    5.39 -    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    5.40 -    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    5.41 -      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    5.42 +    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs
    5.43 +    val ty = Type (tyco, map TFree vs)
    5.44 +    val lhs =
    5.45 +      Const (@{const_name partial_term_of},
    5.46 +        Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $
    5.47 +      Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term})
    5.48 +    val rhs = @{term "undefined :: Code_Evaluation.term"}
    5.49 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
    5.50 +    fun triv_name_of t =
    5.51 +      (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^
    5.52 +        "_triv"
    5.53    in
    5.54      thy
    5.55      |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
    5.56 @@ -55,13 +59,13 @@
    5.57      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    5.58      |> snd
    5.59      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    5.60 -  end;
    5.61 +  end
    5.62  
    5.63  fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
    5.64    let
    5.65      val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of})
    5.66 -      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
    5.67 -  in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
    5.68 +      andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}
    5.69 +  in if need_inst then add_partial_term_of tyco raw_vs thy else thy end
    5.70  
    5.71  
    5.72  (** code equations for datatypes **)
    5.73 @@ -69,15 +73,17 @@
    5.74  fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
    5.75    let
    5.76      val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
    5.77 -    val narrowing_term = @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i
    5.78 -      $ HOLogic.mk_list @{typ narrowing_term} (rev frees)
    5.79 -    val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    5.80 +    val narrowing_term =
    5.81 +      @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i $
    5.82 +        HOLogic.mk_list @{typ narrowing_term} (rev frees)
    5.83 +    val rhs =
    5.84 +      fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    5.85          (map mk_partial_term_of (frees ~~ tys))
    5.86          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
    5.87      val insts =
    5.88        map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    5.89          [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
    5.90 -    val cty = Thm.global_ctyp_of thy ty;
    5.91 +    val cty = Thm.global_ctyp_of thy ty
    5.92    in
    5.93      @{thm partial_term_of_anything}
    5.94      |> Thm.instantiate' [SOME cty] insts
    5.95 @@ -86,44 +92,42 @@
    5.96  
    5.97  fun add_partial_term_of_code tyco raw_vs raw_cs thy =
    5.98    let
    5.99 -    val algebra = Sign.classes_of thy;
   5.100 -    val vs = map (fn (v, sort) =>
   5.101 -      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
   5.102 -    val ty = Type (tyco, map TFree vs);
   5.103 -    val cs = (map o apsnd o apsnd o map o map_atyps)
   5.104 -      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
   5.105 -    val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
   5.106 +    val algebra = Sign.classes_of thy
   5.107 +    val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs
   5.108 +    val ty = Type (tyco, map TFree vs)
   5.109 +    val cs =
   5.110 +      (map o apsnd o apsnd o map o map_atyps)
   5.111 +        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs
   5.112 +    val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco)
   5.113      val var_insts =
   5.114        map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
   5.115          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
   5.116 -          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
   5.117 +          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
   5.118      val var_eq =
   5.119        @{thm partial_term_of_anything}
   5.120        |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
   5.121        |> Thm.varifyT_global
   5.122 -    val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
   5.123 - in
   5.124 +    val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
   5.125 +  in
   5.126      thy
   5.127      |> Code.del_eqns const
   5.128      |> fold Code.add_eqn eqs
   5.129 -  end;
   5.130 +  end
   5.131  
   5.132  fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
   5.133 -  let
   5.134 -    val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of};
   5.135 -  in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
   5.136 +  let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}
   5.137 +  in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end
   5.138  
   5.139  
   5.140  (* narrowing generators *)
   5.141  
   5.142  (** narrowing specific names and types **)
   5.143  
   5.144 -exception FUNCTION_TYPE;
   5.145 +exception FUNCTION_TYPE
   5.146  
   5.147 -val narrowingN = "narrowing";
   5.148 +val narrowingN = "narrowing"
   5.149  
   5.150 -fun narrowingT T =
   5.151 -  @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
   5.152 +fun narrowingT T = @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
   5.153  
   5.154  fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
   5.155  
   5.156 @@ -136,11 +140,9 @@
   5.157    end
   5.158  
   5.159  fun mk_sum (t, u) =
   5.160 -  let
   5.161 -    val T = fastype_of t
   5.162 -  in
   5.163 -    Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
   5.164 -  end
   5.165 +  let val T = fastype_of t
   5.166 +  in Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u end
   5.167 +
   5.168  
   5.169  (** deriving narrowing instances **)
   5.170  
   5.171 @@ -156,8 +158,7 @@
   5.172          (T, nth narrowings k)
   5.173        end
   5.174      fun mk_consexpr simpleT (c, xs) =
   5.175 -      let
   5.176 -        val Ts = map fst xs
   5.177 +      let val Ts = map fst xs
   5.178        in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
   5.179      fun mk_rhs exprs = foldr1 mk_sum exprs
   5.180      val rhss =
   5.181 @@ -168,9 +169,7 @@
   5.182        |> map mk_rhs
   5.183      val lhss = narrowings
   5.184      val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   5.185 -  in
   5.186 -    eqs
   5.187 -  end
   5.188 +  in eqs end
   5.189  
   5.190  fun contains_recursive_type_under_function_types xs =
   5.191    exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
   5.192 @@ -178,8 +177,8 @@
   5.193  
   5.194  fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   5.195    let
   5.196 -    val _ = Old_Datatype_Aux.message config "Creating narrowing generators ...";
   5.197 -    val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
   5.198 +    val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..."
   5.199 +    val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames)
   5.200    in
   5.201      if not (contains_recursive_type_under_function_types descr) then
   5.202        thy
   5.203 @@ -188,14 +187,15 @@
   5.204          (fn narrowings => mk_equations descr vs narrowings, NONE)
   5.205          prfx [] narrowingsN (map narrowingT (Ts @ Us))
   5.206        |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   5.207 -    else
   5.208 -      thy
   5.209 -  end;
   5.210 +    else thy
   5.211 +  end
   5.212 +
   5.213  
   5.214  (* testing framework *)
   5.215  
   5.216  val target = "Haskell_Quickcheck"
   5.217  
   5.218 +
   5.219  (** invocation of Haskell interpreter **)
   5.220  
   5.221  val narrowing_engine =
   5.222 @@ -213,14 +213,15 @@
   5.223    let
   5.224      val path =
   5.225        Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   5.226 -    val _ = Isabelle_System.mkdirs path;
   5.227 -  in Exn.release (Exn.capture f path) end;
   5.228 +    val _ = Isabelle_System.mkdirs path
   5.229 +  in Exn.release (Exn.capture f path) end
   5.230  
   5.231  fun elapsed_time description e =
   5.232    let val ({elapsed, ...}, result) = Timing.timing e ()
   5.233    in (result, (description, Time.toMilliseconds elapsed)) end
   5.234  
   5.235 -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
   5.236 +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
   5.237 +    ctxt cookie (code_modules, _) =
   5.238    let
   5.239      val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
   5.240      fun message s = if quiet then () else writeln s
   5.241 @@ -235,26 +236,33 @@
   5.242        let
   5.243          fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
   5.244          val generatedN = Code_Target.generatedN
   5.245 -        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
   5.246 +        val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file
   5.247          val code = the (AList.lookup (op =) code_modules generatedN)
   5.248          val code_file = mk_code_file generatedN
   5.249          val narrowing_engine_file = mk_code_file "Narrowing_Engine"
   5.250          val main_file = mk_code_file "Main"
   5.251 -        val main = "module Main where {\n\n" ^
   5.252 +        val main =
   5.253 +          "module Main where {\n\n" ^
   5.254            "import System.IO;\n" ^
   5.255            "import System.Environment;\n" ^
   5.256            "import Narrowing_Engine;\n" ^
   5.257            "import " ^ generatedN ^ " ;\n\n" ^
   5.258            "main = getArgs >>= \\[potential, size] -> " ^
   5.259 -          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
   5.260 -          "}\n"
   5.261 -        val _ = map (uncurry File.write) (includes @
   5.262 -          [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
   5.263 -           (code_file, code), (main_file, main)])
   5.264 -        val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
   5.265 -        val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
   5.266 -          ghc_options ^ " " ^
   5.267 -          (space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
   5.268 +          "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^
   5.269 +          ".value ())\n\n}\n"
   5.270 +        val _ =
   5.271 +          map (uncurry File.write)
   5.272 +            (includes @
   5.273 +              [(narrowing_engine_file,
   5.274 +                if contains_existentials then pnf_narrowing_engine else narrowing_engine),
   5.275 +               (code_file, code), (main_file, main)])
   5.276 +        val executable =
   5.277 +          File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
   5.278 +        val cmd =
   5.279 +          "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
   5.280 +            (space_implode " "
   5.281 +              (map File.bash_path
   5.282 +                (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
   5.283            " -o " ^ executable ^ ";"
   5.284          val (_, compilation_time) =
   5.285            elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
   5.286 @@ -262,52 +270,49 @@
   5.287          fun haskell_string_of_bool v = if v then "True" else "False"
   5.288          val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
   5.289          fun with_size genuine_only k =
   5.290 -          if k > size then
   5.291 -            (NONE, !current_result)
   5.292 +          if k > size then (NONE, !current_result)
   5.293            else
   5.294              let
   5.295                val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
   5.296                val _ = current_size := k
   5.297 -              val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
   5.298 -                (fn () => Isabelle_System.bash_output
   5.299 -                  (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
   5.300 +              val ((response, _), timing) =
   5.301 +                elapsed_time ("execution of size " ^ string_of_int k)
   5.302 +                  (fn () => Isabelle_System.bash_output
   5.303 +                    (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k))
   5.304                val _ = Quickcheck.add_timing timing current_result
   5.305              in
   5.306 -              if response = "NONE\n" then
   5.307 -                with_size genuine_only (k + 1)
   5.308 +              if response = "NONE\n" then with_size genuine_only (k + 1)
   5.309                else
   5.310                  let
   5.311                    val output_value = the_default "NONE"
   5.312                      (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
   5.313                    val ml_code =
   5.314                      "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml
   5.315 -                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
   5.316 +                    ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"
   5.317                    val ctxt' = ctxt
   5.318                      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   5.319 -                    |> Context.proof_map (exec false ml_code);
   5.320 +                    |> Context.proof_map (exec false ml_code)
   5.321                    val counterexample = get ctxt' ()
   5.322                  in
   5.323                    if is_genuine counterexample then
   5.324                      (counterexample, !current_result)
   5.325                    else
   5.326                      let
   5.327 -                      val cex = Option.map (rpair []) (counterexample_of counterexample);
   5.328 -                      val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
   5.329 -                      val _ = message "Quickcheck continues to find a genuine counterexample...";
   5.330 +                      val cex = Option.map (rpair []) (counterexample_of counterexample)
   5.331 +                      val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex))
   5.332 +                      val _ = message "Quickcheck continues to find a genuine counterexample..."
   5.333                      in with_size true (k + 1) end
   5.334                 end
   5.335              end
   5.336        in with_size genuine_only 0 end
   5.337 -  in
   5.338 -    with_tmp_dir tmp_prefix run
   5.339 -  end;
   5.340 +  in with_tmp_dir tmp_prefix run end
   5.341  
   5.342  fun dynamic_value_strict opts cookie ctxt postproc t =
   5.343    let
   5.344      fun evaluator program _ vs_ty_t deps =
   5.345        Exn.interruptible_capture (value opts ctxt cookie)
   5.346 -        (Code_Target.evaluator ctxt target program deps true vs_ty_t);
   5.347 -  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end;
   5.348 +        (Code_Target.evaluator ctxt target program deps true vs_ty_t)
   5.349 +  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
   5.350  
   5.351  
   5.352  (** counterexample generator **)
   5.353 @@ -317,7 +322,7 @@
   5.354    | Existential_Counterexample of (term * counterexample) list
   5.355    | Empty_Assignment
   5.356  
   5.357 -fun map_counterexample f Empty_Assignment = Empty_Assignment
   5.358 +fun map_counterexample _ Empty_Assignment = Empty_Assignment
   5.359    | map_counterexample f (Universal_Counterexample (t, c)) =
   5.360        Universal_Counterexample (f t, map_counterexample f c)
   5.361    | map_counterexample f (Existential_Counterexample cs) =
   5.362 @@ -327,18 +332,18 @@
   5.363  (
   5.364    type T =
   5.365      (unit -> (bool * term list) option) *
   5.366 -    (unit -> counterexample option);
   5.367 +    (unit -> counterexample option)
   5.368    val empty: T =
   5.369     (fn () => raise Fail "counterexample",
   5.370 -    fn () => raise Fail "existential_counterexample");
   5.371 -  fun init _ = empty;
   5.372 -);
   5.373 +    fn () => raise Fail "existential_counterexample")
   5.374 +  fun init _ = empty
   5.375 +)
   5.376  
   5.377  val get_counterexample = #1 o Data.get;
   5.378  val get_existential_counterexample = #2 o Data.get;
   5.379  
   5.380 -val put_counterexample = Data.map o @{apply 2(1)} o K;
   5.381 -val put_existential_counterexample = Data.map o @{apply 2(2)} o K;
   5.382 +val put_counterexample = Data.map o @{apply 2(1)} o K
   5.383 +val put_existential_counterexample = Data.map o @{apply 2(2)} o K
   5.384  
   5.385  fun finitize_functions (xTs, t) =
   5.386    let
   5.387 @@ -350,27 +355,27 @@
   5.388        Const (@{const_name "Quickcheck_Narrowing.eval_cfun"},
   5.389          Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
   5.390      fun eval_function (Type (@{type_name fun}, [dT, rT])) =
   5.391 -      let
   5.392 -        val (rt', rT') = eval_function rT
   5.393 -      in
   5.394 -        case dT of
   5.395 -          Type (@{type_name fun}, _) =>
   5.396 -            (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   5.397 -              Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
   5.398 -        | _ =>
   5.399 -            (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   5.400 -              Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
   5.401 -      end
   5.402 +          let
   5.403 +            val (rt', rT') = eval_function rT
   5.404 +          in
   5.405 +            (case dT of
   5.406 +              Type (@{type_name fun}, _) =>
   5.407 +                (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   5.408 +                  Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
   5.409 +            | _ =>
   5.410 +                (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
   5.411 +                  Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])))
   5.412 +          end
   5.413        | eval_function (T as Type (@{type_name prod}, [fT, sT])) =
   5.414 -        let
   5.415 -          val (ft', fT') = eval_function fT
   5.416 -          val (st', sT') = eval_function sT
   5.417 -          val T' = Type (@{type_name prod}, [fT', sT'])
   5.418 -          val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
   5.419 -          fun apply_dummy T t = absdummy T (t (Bound 0))
   5.420 -        in
   5.421 -          (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
   5.422 -        end
   5.423 +          let
   5.424 +            val (ft', fT') = eval_function fT
   5.425 +            val (st', sT') = eval_function sT
   5.426 +            val T' = Type (@{type_name prod}, [fT', sT'])
   5.427 +            val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
   5.428 +            fun apply_dummy T t = absdummy T (t (Bound 0))
   5.429 +          in
   5.430 +            (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
   5.431 +          end
   5.432        | eval_function T = (I, T)
   5.433      val (tt, boundTs') = split_list (map eval_function boundTs)
   5.434      val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)
   5.435 @@ -381,63 +386,63 @@
   5.436  fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT)
   5.437  
   5.438  fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) =
   5.439 -    absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
   5.440 +      absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
   5.441    | eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) =
   5.442 -    let
   5.443 -      val (T1, T2) = dest_ffun (body_type T)
   5.444 -    in
   5.445 -      Quickcheck_Common.mk_fun_upd T1 T2
   5.446 -        (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
   5.447 -    end
   5.448 +      let
   5.449 +        val (T1, T2) = dest_ffun (body_type T)
   5.450 +      in
   5.451 +        Quickcheck_Common.mk_fun_upd T1 T2
   5.452 +          (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
   5.453 +      end
   5.454    | eval_finite_functions t = t
   5.455  
   5.456 +
   5.457  (** tester **)
   5.458  
   5.459  val rewrs =
   5.460 -    map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   5.461 -      (@{thms all_simps} @ @{thms ex_simps})
   5.462 -    @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   5.463 -        [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
   5.464 -         @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
   5.465 +  map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   5.466 +    (@{thms all_simps} @ @{thms ex_simps}) @
   5.467 +  map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
   5.468 +    [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
   5.469 +     @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
   5.470  
   5.471  fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
   5.472  
   5.473  fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   5.474 -    apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
   5.475 +      apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
   5.476    | strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) =
   5.477 -    apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
   5.478 +      apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
   5.479    | strip_quantifiers t = ([], t)
   5.480  
   5.481 -fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
   5.482 +fun contains_existentials t =
   5.483 +  exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
   5.484  
   5.485  fun mk_property qs t =
   5.486    let
   5.487      fun enclose (@{const_name Ex}, (x, T)) t =
   5.488 -        Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property})
   5.489 -          $ Abs (x, T, t)
   5.490 +          Const (@{const_name Quickcheck_Narrowing.exists},
   5.491 +            (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t)
   5.492        | enclose (@{const_name All}, (x, T)) t =
   5.493 -        Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
   5.494 -          $ Abs (x, T, t)
   5.495 -  in
   5.496 -    fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t)
   5.497 -  end
   5.498 +          Const (@{const_name Quickcheck_Narrowing.all},
   5.499 +            (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t)
   5.500 +  in fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) end
   5.501  
   5.502  fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
   5.503 -    Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
   5.504 -      (t, mk_case_term ctxt (p - 1) qs' c)) cs)
   5.505 +      Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
   5.506 +        (t, mk_case_term ctxt (p - 1) qs' c)) cs)
   5.507    | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) =
   5.508 -    if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
   5.509 +      if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
   5.510  
   5.511 -val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions
   5.512 +val post_process =
   5.513 +  perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions
   5.514  
   5.515  fun mk_terms ctxt qs result =
   5.516    let
   5.517 -    val
   5.518 -      ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
   5.519 -    in
   5.520 -      map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
   5.521 -      |> map (apsnd post_process)
   5.522 -    end
   5.523 +    val ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
   5.524 +  in
   5.525 +    map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
   5.526 +    |> map (apsnd post_process)
   5.527 +  end
   5.528  
   5.529  fun test_term ctxt catch_code_errors (t, _) =
   5.530    let
   5.531 @@ -453,8 +458,8 @@
   5.532      if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
   5.533        let
   5.534          fun wrap f (qs, t) =
   5.535 -          let val (qs1, qs2) = split_list qs in
   5.536 -          apfst (map2 pair qs1) (f (qs2, t)) end
   5.537 +          let val (qs1, qs2) = split_list qs
   5.538 +          in apfst (map2 pair qs1) (f (qs2, t)) end
   5.539          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   5.540          val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
   5.541          val act = if catch_code_errors then try else (fn f => SOME o f)
   5.542 @@ -465,14 +470,14 @@
   5.543                  "Narrowing_Generators.put_existential_counterexample"))
   5.544              ctxt (apfst o Option.map o map_counterexample)
   5.545        in
   5.546 -        case act execute (mk_property qs prop_t) of
   5.547 +        (case act execute (mk_property qs prop_t) of
   5.548            SOME (counterexample, result) => Quickcheck.Result
   5.549              {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
   5.550              evaluation_terms = Option.map (K []) counterexample,
   5.551              timings = #timings (dest_result result), reports = #reports (dest_result result)}
   5.552          | NONE =>
   5.553            (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
   5.554 -           Quickcheck.empty_result)
   5.555 +           Quickcheck.empty_result))
   5.556        end
   5.557      else
   5.558        let
   5.559 @@ -481,10 +486,12 @@
   5.560          fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
   5.561          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   5.562          fun ensure_testable t =
   5.563 -          Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   5.564 +          Const (@{const_name Quickcheck_Narrowing.ensure_testable},
   5.565 +            fastype_of t --> fastype_of t) $ t
   5.566          fun is_genuine (SOME (true, _)) = true
   5.567            | is_genuine _ = false
   5.568 -        val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
   5.569 +        val counterexample_of =
   5.570 +          Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
   5.571          val act = if catch_code_errors then try else (fn f => SOME o f)
   5.572          val execute =
   5.573            dynamic_value_strict (false, opts)
   5.574 @@ -493,7 +500,7 @@
   5.575                  "Narrowing_Generators.put_counterexample"))
   5.576              ctxt (apfst o Option.map o apsnd o map)
   5.577        in
   5.578 -        case act execute (ensure_testable (finitize t')) of
   5.579 +        (case act execute (ensure_testable (finitize t')) of
   5.580            SOME (counterexample, result) =>
   5.581              Quickcheck.Result
   5.582               {counterexample = counterexample_of counterexample,
   5.583 @@ -502,14 +509,14 @@
   5.584                reports = #reports (dest_result result)}
   5.585          | NONE =>
   5.586            (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
   5.587 -           Quickcheck.empty_result)
   5.588 +           Quickcheck.empty_result))
   5.589        end
   5.590 -  end;
   5.591 +  end
   5.592  
   5.593  fun test_goals ctxt catch_code_errors insts goals =
   5.594 -  if (not (getenv "ISABELLE_GHC" = "")) then
   5.595 +  if not (getenv "ISABELLE_GHC" = "") then
   5.596      let
   5.597 -      val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing...";
   5.598 +      val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..."
   5.599        val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
   5.600      in
   5.601        Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
   5.602 @@ -522,9 +529,10 @@
   5.603          ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
   5.604        [Quickcheck.empty_result])
   5.605  
   5.606 +
   5.607  (* setup *)
   5.608  
   5.609 -val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false);
   5.610 +val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false)
   5.611  
   5.612  val _ =
   5.613    Theory.setup
   5.614 @@ -532,6 +540,6 @@
   5.615      #> Code.datatype_interpretation ensure_partial_term_of_code
   5.616      #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
   5.617        (@{sort narrowing}, instantiate_narrowing_datatype)
   5.618 -    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
   5.619 +    #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))))
   5.620  
   5.621 -end;
   5.622 +end
     6.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 14 15:33:23 2016 +0200
     6.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 14 15:33:51 2016 +0200
     6.3 @@ -10,37 +10,39 @@
     6.4    val strip_imp : term -> (term list * term)
     6.5    val reflect_bool : bool -> term
     6.6    val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
     6.7 -    -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context 
     6.8 +    -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
     6.9    val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
    6.10      -> (string * sort -> string * sort) option
    6.11    val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
    6.12      -> (typ option * (term * term list)) list list
    6.13    val register_predicate : term * string -> Context.generic -> Context.generic
    6.14    val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
    6.15 -  val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
    6.16 +  val collect_results : ('a -> Quickcheck.result) -> 'a list ->
    6.17 +    Quickcheck.result list -> Quickcheck.result list
    6.18    type result = (bool * term list) option * Quickcheck.report option
    6.19 -  type generator = string * ((theory -> typ list -> bool) * 
    6.20 +  type generator = string * ((theory -> typ list -> bool) *
    6.21        (Proof.context -> (term * term list) list -> bool -> int list -> result))
    6.22    val generator_test_goal_terms :
    6.23      generator -> Proof.context -> bool -> (string * typ) list
    6.24        -> (term * term list) list -> Quickcheck.result list
    6.25 -  type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
    6.26 -     -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    6.27 +  type instantiation =
    6.28 +    Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
    6.29 +      string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    6.30    val ensure_sort :
    6.31      (((sort * sort) * sort) *
    6.32        ((theory -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list
    6.33 -        * string * (string list * string list) * (typ list * typ list)) * instantiation))
    6.34 -    -> Old_Datatype_Aux.config -> string list -> theory -> theory
    6.35 -  val ensure_common_sort_datatype :
    6.36 -    (sort * instantiation) -> Old_Datatype_Aux.config -> string list -> theory -> theory
    6.37 +        * string * (string list * string list) * (typ list * typ list)) * instantiation)) ->
    6.38 +    Old_Datatype_Aux.config -> string list -> theory -> theory
    6.39 +  val ensure_common_sort_datatype : (sort * instantiation) -> Old_Datatype_Aux.config ->
    6.40 +    string list -> theory -> theory
    6.41    val datatype_interpretation : string -> sort * instantiation -> theory -> theory
    6.42    val gen_mk_parametric_generator_expr :
    6.43 -   (((Proof.context -> term * term list -> term) * term) * typ)
    6.44 -     -> Proof.context -> (term * term list) list -> term
    6.45 +    (((Proof.context -> term * term list -> term) * term) * typ) ->
    6.46 +      Proof.context -> (term * term list) list -> term
    6.47    val mk_fun_upd : typ -> typ -> term * term -> term -> term
    6.48    val post_process_term : term -> term
    6.49    val test_term : generator -> Proof.context -> bool -> term * term list -> Quickcheck.result
    6.50 -end;
    6.51 +end
    6.52  
    6.53  structure Quickcheck_Common : QUICKCHECK_COMMON =
    6.54  struct
    6.55 @@ -51,27 +53,32 @@
    6.56  
    6.57  val define_foundationally = false
    6.58  
    6.59 +
    6.60  (* HOLogic's term functions *)
    6.61  
    6.62 -fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
    6.63 +fun strip_imp (Const(@{const_name HOL.implies}, _) $ A $ B) = apfst (cons A) (strip_imp B)
    6.64    | strip_imp A = ([], A)
    6.65  
    6.66 -fun reflect_bool b = if b then @{term "True"} else @{term "False"}
    6.67 +fun reflect_bool b = if b then @{term True} else @{term False}
    6.68  
    6.69 -fun mk_undefined T = Const(@{const_name undefined}, T)
    6.70 +fun mk_undefined T = Const (@{const_name undefined}, T)
    6.71 +
    6.72  
    6.73  (* testing functions: testing with increasing sizes (and cardinalities) *)
    6.74  
    6.75  type result = (bool * term list) option * Quickcheck.report option
    6.76 -type generator = string * ((theory -> typ list -> bool) * 
    6.77 -      (Proof.context -> (term * term list) list -> bool -> int list -> result))
    6.78 +type generator =
    6.79 +  string * ((theory -> typ list -> bool) *
    6.80 +    (Proof.context -> (term * term list) list -> bool -> int list -> result))
    6.81  
    6.82  fun check_test_term t =
    6.83    let
    6.84 -    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    6.85 -      error "Term to be tested contains type variables";
    6.86 -    val _ = null (Term.add_vars t []) orelse
    6.87 -      error "Term to be tested contains schematic variables";
    6.88 +    val _ =
    6.89 +      (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    6.90 +        error "Term to be tested contains type variables"
    6.91 +    val _ =
    6.92 +      null (Term.add_vars t []) orelse
    6.93 +        error "Term to be tested contains schematic variables"
    6.94    in () end
    6.95  
    6.96  fun cpu_time description e =
    6.97 @@ -85,55 +92,59 @@
    6.98      val _ = check_test_term t
    6.99      val names = Term.add_free_names t []
   6.100      val current_size = Unsynchronized.ref 0
   6.101 -    val current_result = Unsynchronized.ref Quickcheck.empty_result 
   6.102 -    val act = if catch_code_errors then try else (fn f => SOME o f) 
   6.103 -    val (test_fun, comp_time) = cpu_time "quickcheck compilation"
   6.104 -        (fn () => act (compile ctxt) [(t, eval_terms)]);
   6.105 +    val current_result = Unsynchronized.ref Quickcheck.empty_result
   6.106 +    val act = if catch_code_errors then try else (fn f => SOME o f)
   6.107 +    val (test_fun, comp_time) =
   6.108 +      cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)])
   6.109      val _ = Quickcheck.add_timing comp_time current_result
   6.110      fun with_size test_fun genuine_only k =
   6.111 -      if k > Config.get ctxt Quickcheck.size then
   6.112 -        NONE
   6.113 +      if k > Config.get ctxt Quickcheck.size then NONE
   6.114        else
   6.115          let
   6.116 -          val _ = Quickcheck.verbose_message ctxt
   6.117 -            ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
   6.118 +          val _ =
   6.119 +            Quickcheck.verbose_message ctxt
   6.120 +              ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
   6.121            val _ = current_size := k
   6.122            val ((result, report), time) =
   6.123              cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
   6.124 -          val _ = if Config.get ctxt Quickcheck.timing then
   6.125 -            Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
   6.126 +          val _ =
   6.127 +            if Config.get ctxt Quickcheck.timing then
   6.128 +              Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms")
   6.129 +            else ()
   6.130            val _ = Quickcheck.add_timing time current_result
   6.131            val _ = Quickcheck.add_report k report current_result
   6.132          in
   6.133 -          case result of
   6.134 +          (case result of
   6.135              NONE => with_size test_fun genuine_only (k + 1)
   6.136            | SOME (true, ts) => SOME (true, ts)
   6.137            | SOME (false, ts) =>
   6.138 -            if abort_potential then SOME (false, ts)
   6.139 -            else
   6.140 -              let
   6.141 -                val (ts1, ts2) = chop (length names) ts
   6.142 -                val (eval_terms', _) = chop (length ts2) eval_terms
   6.143 -                val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
   6.144 -              in
   6.145 -                (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
   6.146 -                Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
   6.147 -                with_size test_fun true k)
   6.148 -              end
   6.149 -        end;
   6.150 +              if abort_potential then SOME (false, ts)
   6.151 +              else
   6.152 +                let
   6.153 +                  val (ts1, ts2) = chop (length names) ts
   6.154 +                  val (eval_terms', _) = chop (length ts2) eval_terms
   6.155 +                  val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
   6.156 +                in
   6.157 +                  Quickcheck.message ctxt
   6.158 +                    (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
   6.159 +                  Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
   6.160 +                  with_size test_fun true k
   6.161 +                end)
   6.162 +        end
   6.163    in
   6.164      case test_fun of
   6.165 -      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
   6.166 -        !current_result)
   6.167 +      NONE =>
   6.168 +        (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
   6.169 +          !current_result)
   6.170      | SOME test_fun =>
   6.171 -      let
   6.172 -        val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
   6.173 -        val (response, exec_time) =
   6.174 -          cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
   6.175 -        val _ = Quickcheck.add_response names eval_terms response current_result
   6.176 -        val _ = Quickcheck.add_timing exec_time current_result
   6.177 -      in !current_result end
   6.178 -  end;
   6.179 +        let
   6.180 +          val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
   6.181 +          val (response, exec_time) =
   6.182 +            cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
   6.183 +          val _ = Quickcheck.add_response names eval_terms response current_result
   6.184 +          val _ = Quickcheck.add_timing exec_time current_result
   6.185 +        in !current_result end
   6.186 +  end
   6.187  
   6.188  fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
   6.189    let
   6.190 @@ -145,105 +156,104 @@
   6.191      val names = Term.add_free_names (hd ts') []
   6.192      val Ts = map snd (Term.add_frees (hd ts') [])
   6.193      val current_result = Unsynchronized.ref Quickcheck.empty_result
   6.194 -    fun test_card_size test_fun genuine_only (card, size) =
   6.195 -      (* FIXME: why decrement size by one? *)
   6.196 +    fun test_card_size test_fun genuine_only (card, size) = (* FIXME: why decrement size by one? *)
   6.197        let
   6.198          val _ =
   6.199            Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
   6.200              (if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^
   6.201 -            "cardinality: " ^ string_of_int card)          
   6.202 +            "cardinality: " ^ string_of_int card)
   6.203          val (ts, timing) =
   6.204            cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
   6.205              (fn () => fst (test_fun genuine_only [card, size + 1]))
   6.206          val _ = Quickcheck.add_timing timing current_result
   6.207 -      in
   6.208 -        Option.map (pair (card, size)) ts
   6.209 -      end
   6.210 +      in Option.map (pair (card, size)) ts end
   6.211      val enumeration_card_size =
   6.212        if size_matters_for thy Ts then
   6.213          map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
   6.214          |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
   6.215 -      else
   6.216 -        map (rpair 0) (1 upto (length ts))
   6.217 +      else map (rpair 0) (1 upto (length ts))
   6.218      val act = if catch_code_errors then try else (fn f => SOME o f)
   6.219      val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts)
   6.220      val _ = Quickcheck.add_timing comp_time current_result
   6.221    in
   6.222 -    case test_fun of
   6.223 -      NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
   6.224 -        !current_result)
   6.225 +    (case test_fun of
   6.226 +      NONE =>
   6.227 +        (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
   6.228 +          !current_result)
   6.229      | SOME test_fun =>
   6.230 -      let
   6.231 -        val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
   6.232 -        fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
   6.233 -          SOME ((card, _), (true, ts)) =>
   6.234 -            Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
   6.235 -        | SOME ((card, size), (false, ts)) =>
   6.236 -            if abort_potential then
   6.237 -              Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (false, ts)) current_result
   6.238 -            else
   6.239 -              let
   6.240 -                val (ts1, ts2) = chop (length names) ts
   6.241 -                val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
   6.242 -                val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
   6.243 -              in
   6.244 -                (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
   6.245 -                Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
   6.246 -                test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))              
   6.247 -            end
   6.248 -        | NONE => ()
   6.249 -      in (test genuine_only enumeration_card_size; !current_result) end
   6.250 +        let
   6.251 +          val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
   6.252 +          fun test genuine_only enum =
   6.253 +            (case get_first (test_card_size test_fun genuine_only) enum of
   6.254 +              SOME ((card, _), (true, ts)) =>
   6.255 +                Quickcheck.add_response names (nth eval_terms (card - 1))
   6.256 +                  (SOME (true, ts)) current_result
   6.257 +            | SOME ((card, size), (false, ts)) =>
   6.258 +                if abort_potential then
   6.259 +                  Quickcheck.add_response names (nth eval_terms (card - 1))
   6.260 +                    (SOME (false, ts)) current_result
   6.261 +                else
   6.262 +                  let
   6.263 +                    val (ts1, ts2) = chop (length names) ts
   6.264 +                    val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
   6.265 +                    val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
   6.266 +                  in
   6.267 +                    Quickcheck.message ctxt
   6.268 +                      (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
   6.269 +                    Quickcheck.message ctxt
   6.270 +                      "Quickcheck continues to find a genuine counterexample...";
   6.271 +                    test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
   6.272 +                end
   6.273 +            | NONE => ())
   6.274 +        in (test genuine_only enumeration_card_size; !current_result) end)
   6.275    end
   6.276  
   6.277  fun get_finite_types ctxt =
   6.278    fst (chop (Config.get ctxt Quickcheck.finite_type_size)
   6.279 -    [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"},
   6.280 -     @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}])
   6.281 +    [@{typ Enum.finite_1}, @{typ Enum.finite_2}, @{typ Enum.finite_3},
   6.282 +     @{typ Enum.finite_4}, @{typ Enum.finite_5}])
   6.283  
   6.284  exception WELLSORTED of string
   6.285  
   6.286  fun monomorphic_term thy insts default_T =
   6.287    let
   6.288      fun subst (T as TFree (v, S)) =
   6.289 -      let
   6.290 -        val T' = AList.lookup (op =) insts v
   6.291 -          |> the_default default_T
   6.292 -      in if Sign.of_sort thy (T', S) then T'
   6.293 -        else raise (WELLSORTED ("For instantiation with default_type " ^
   6.294 -          Syntax.string_of_typ_global thy default_T ^
   6.295 -          ":\n" ^ Syntax.string_of_typ_global thy T' ^
   6.296 -          " to be substituted for variable " ^
   6.297 -          Syntax.string_of_typ_global thy T ^ " does not have sort " ^
   6.298 -          Syntax.string_of_sort_global thy S))
   6.299 -      end
   6.300 -      | subst T = T;
   6.301 -  in (map_types o map_atyps) subst end;
   6.302 +          let val T' = AList.lookup (op =) insts v |> the_default default_T in
   6.303 +            if Sign.of_sort thy (T', S) then T'
   6.304 +            else raise (WELLSORTED ("For instantiation with default_type " ^
   6.305 +              Syntax.string_of_typ_global thy default_T ^
   6.306 +              ":\n" ^ Syntax.string_of_typ_global thy T' ^
   6.307 +              " to be substituted for variable " ^
   6.308 +              Syntax.string_of_typ_global thy T ^ " does not have sort " ^
   6.309 +              Syntax.string_of_sort_global thy S))
   6.310 +          end
   6.311 +      | subst T = T
   6.312 +  in (map_types o map_atyps) subst end
   6.313  
   6.314  datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
   6.315  
   6.316 +
   6.317  (* minimalistic preprocessing *)
   6.318  
   6.319 -fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = 
   6.320 -  let
   6.321 -    val (a', t') = strip_all t
   6.322 -  in ((a, T) :: a', t') end
   6.323 -  | strip_all t = ([], t);
   6.324 +fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) =
   6.325 +      let val (a', t') = strip_all t
   6.326 +      in ((a, T) :: a', t') end
   6.327 +  | strip_all t = ([], t)
   6.328  
   6.329  fun preprocess ctxt t =
   6.330    let
   6.331      val thy = Proof_Context.theory_of ctxt
   6.332      val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
   6.333 -    val rewrs = map (swap o dest) @{thms all_simps} @
   6.334 -      (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
   6.335 -        @{thm bot_fun_def}, @{thm less_bool_def}])
   6.336 +    val rewrs =
   6.337 +      map (swap o dest) @{thms all_simps} @
   6.338 +        (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
   6.339 +          @{thm bot_fun_def}, @{thm less_bool_def}])
   6.340      val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
   6.341      val (vs, body) = strip_all t'
   6.342      val vs' = Variable.variant_frees ctxt [t'] vs
   6.343 -  in
   6.344 -    subst_bounds (map Free (rev vs'), body)
   6.345 -  end
   6.346 +  in subst_bounds (map Free (rev vs'), body) end
   6.347  
   6.348 -  
   6.349 +
   6.350  structure Subtype_Predicates = Generic_Data
   6.351  (
   6.352    type T = (term * string) list
   6.353 @@ -257,31 +267,31 @@
   6.354  fun subtype_preprocess ctxt (T, (t, ts)) =
   6.355    let
   6.356      val preds = Subtype_Predicates.get (Context.Proof ctxt)
   6.357 -    fun matches (p $ _) = AList.defined Term.could_unify preds p  
   6.358 +    fun matches (p $ _) = AList.defined Term.could_unify preds p
   6.359      fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
   6.360      fun subst_of (tyco, v as Free (x, repT)) =
   6.361        let
   6.362          val [(info, _)] = Typedef.get_info ctxt tyco
   6.363          val repT' = Logic.varifyT_global (#rep_type info)
   6.364 -        val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty 
   6.365 +        val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
   6.366          val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
   6.367        in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
   6.368      val (prems, concl) = strip_imp t
   6.369      val subst = map subst_of (map_filter get_match prems)
   6.370      val t' = Term.subst_free subst
   6.371       (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
   6.372 -  in
   6.373 -    (T, (t', ts))
   6.374 -  end
   6.375 +  in (T, (t', ts)) end
   6.376 +
   6.377  
   6.378  (* instantiation of type variables with concrete types *)
   6.379 - 
   6.380 +
   6.381  fun instantiate_goals lthy insts goals =
   6.382    let
   6.383      fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
   6.384      val thy = Proof_Context.theory_of lthy
   6.385      val default_insts =
   6.386 -      if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type
   6.387 +      if Config.get lthy Quickcheck.finite_types
   6.388 +      then get_finite_types else Quickcheck.default_type
   6.389      val inst_goals =
   6.390        map (fn (check_goal, eval_terms) =>
   6.391          if not (null (Term.add_tfree_names check_goal [])) then
   6.392 @@ -289,67 +299,61 @@
   6.393              (pair (SOME T) o Term o apfst (preprocess lthy))
   6.394                (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
   6.395                handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
   6.396 -        else
   6.397 -          [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
   6.398 +        else [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
   6.399      val error_msg =
   6.400        cat_lines
   6.401          (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
   6.402      fun is_wellsorted_term (T, Term t) = SOME (T, t)
   6.403        | is_wellsorted_term (_, Wellsorted_Error _) = NONE
   6.404      val correct_inst_goals =
   6.405 -      case map (map_filter is_wellsorted_term) inst_goals of
   6.406 +      (case map (map_filter is_wellsorted_term) inst_goals of
   6.407          [[]] => error error_msg
   6.408 -      | xs => xs
   6.409 +      | xs => xs)
   6.410      val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
   6.411 -  in
   6.412 -    correct_inst_goals
   6.413 -  end
   6.414 +  in correct_inst_goals end
   6.415 +
   6.416  
   6.417  (* compilation of testing functions *)
   6.418  
   6.419  fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
   6.420    let
   6.421      val T = fastype_of then_t
   6.422 -    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
   6.423 +    val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
   6.424    in
   6.425 -    Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ 
   6.426 +    Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $
   6.427        (if_t $ cond $ then_t $ else_t genuine) $
   6.428        (if_t $ genuine_only $ none $ else_t false)
   6.429    end
   6.430  
   6.431  fun collect_results f [] results = results
   6.432    | collect_results f (t :: ts) results =
   6.433 -    let
   6.434 -      val result = f t
   6.435 -    in
   6.436 -      if Quickcheck.found_counterexample result then
   6.437 -        (result :: results)
   6.438 -      else
   6.439 -        collect_results f ts (result :: results)
   6.440 -    end  
   6.441 +      let val result = f t in
   6.442 +        if Quickcheck.found_counterexample result then result :: results
   6.443 +        else collect_results f ts (result :: results)
   6.444 +      end
   6.445  
   6.446  fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
   6.447    let
   6.448      val use_subtype = Config.get ctxt Quickcheck.use_subtype
   6.449      fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
   6.450      fun add_equation_eval_terms (t, eval_terms) =
   6.451 -      case try HOLogic.dest_eq (snd (strip_imp t)) of
   6.452 +      (case try HOLogic.dest_eq (snd (strip_imp t)) of
   6.453          SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms))
   6.454 -      | NONE => (t, eval_terms)
   6.455 +      | NONE => (t, eval_terms))
   6.456      fun test_term' goal =
   6.457 -      case goal of
   6.458 +      (case goal of
   6.459          [(NONE, t)] => test_term generator ctxt catch_code_errors t
   6.460 -      | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
   6.461 -    val goals' = instantiate_goals ctxt insts goals
   6.462 +      | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts))
   6.463 +    val goals' =
   6.464 +      instantiate_goals ctxt insts goals
   6.465        |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
   6.466        |> map (map (apsnd add_equation_eval_terms))
   6.467    in
   6.468      if Config.get ctxt Quickcheck.finite_types then
   6.469        collect_results test_term' goals' []
   6.470 -    else
   6.471 -      collect_results (test_term generator ctxt catch_code_errors)
   6.472 -        (maps (map snd) goals') []
   6.473 -  end;
   6.474 +    else collect_results (test_term generator ctxt catch_code_errors) (maps (map snd) goals') []
   6.475 +  end
   6.476 +
   6.477  
   6.478  (* defining functions *)
   6.479  
   6.480 @@ -388,38 +392,42 @@
   6.481            (names ~~ eqs) lthy
   6.482        end)
   6.483  
   6.484 +
   6.485  (** ensuring sort constraints **)
   6.486  
   6.487 -type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
   6.488 -  -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
   6.489 +type instantiation =
   6.490 +  Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
   6.491 +    string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
   6.492  
   6.493  fun perhaps_constrain thy insts raw_vs =
   6.494    let
   6.495 -    fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) 
   6.496 -      (Logic.varifyT_global T, sort);
   6.497 +    fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT_global T, sort)
   6.498      val vtab = Vartab.empty
   6.499        |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
   6.500 -      |> fold meet insts;
   6.501 -  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   6.502 -  end handle Sorts.CLASS_ERROR _ => NONE;
   6.503 +      |> fold meet insts
   6.504 +  in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end
   6.505 +  handle Sorts.CLASS_ERROR _ => NONE
   6.506  
   6.507  fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
   6.508    let
   6.509 -    val algebra = Sign.classes_of thy;
   6.510 +    val algebra = Sign.classes_of thy
   6.511      val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
   6.512      val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
   6.513      fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
   6.514        (Old_Datatype_Aux.interpret_construction descr vs constr)
   6.515      val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
   6.516        @ insts_of aux_sort { atyp = K [], dtyp = K o K }
   6.517 -    val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
   6.518 -  in if has_inst then thy
   6.519 -    else case perhaps_constrain thy insts vs
   6.520 -     of SOME constrain => instantiate config descr
   6.521 -          (map constrain vs) tycos prfx (names, auxnames)
   6.522 -            ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   6.523 -      | NONE => thy
   6.524 -  end;
   6.525 +    val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
   6.526 +  in
   6.527 +    if has_inst then thy
   6.528 +    else
   6.529 +      (case perhaps_constrain thy insts vs of
   6.530 +        SOME constrain =>
   6.531 +          instantiate config descr
   6.532 +            (map constrain vs) tycos prfx (names, auxnames)
   6.533 +              ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   6.534 +      | NONE => thy)
   6.535 +  end
   6.536  
   6.537  fun ensure_common_sort_datatype (sort, instantiate) =
   6.538    ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
   6.539 @@ -427,86 +435,89 @@
   6.540  
   6.541  fun datatype_interpretation name =
   6.542    BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype
   6.543 -  
   6.544 +
   6.545 +
   6.546  (** generic parametric compilation **)
   6.547  
   6.548  fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
   6.549    let
   6.550 -    val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
   6.551 -    fun mk_if (index, (t, eval_terms)) else_t = if_t $
   6.552 -        (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
   6.553 +    val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
   6.554 +    fun mk_if (index, (t, eval_terms)) else_t =
   6.555 +      if_t $ (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
   6.556          (mk_generator_expr ctxt (t, eval_terms)) $ else_t
   6.557 -  in
   6.558 -    absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
   6.559 -  end
   6.560 +  in absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) end
   6.561 +
   6.562  
   6.563  (** post-processing of function terms **)
   6.564  
   6.565  fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
   6.566    | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
   6.567  
   6.568 -fun mk_fun_upd T1 T2 (t1, t2) t = 
   6.569 +fun mk_fun_upd T1 T2 (t1, t2) t =
   6.570    Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
   6.571  
   6.572  fun dest_fun_upds t =
   6.573 -  case try dest_fun_upd t of
   6.574 +  (case try dest_fun_upd t of
   6.575      NONE =>
   6.576        (case t of
   6.577 -        Abs (_, _, _) => ([], t) 
   6.578 +        Abs (_, _, _) => ([], t)
   6.579        | _ => raise TERM ("dest_fun_upds", [t]))
   6.580 -  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
   6.581 +  | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0))
   6.582  
   6.583  fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
   6.584  
   6.585  fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
   6.586    | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
   6.587    | make_set T1 ((t1, @{const True}) :: tps) =
   6.588 -    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
   6.589 -      $ t1 $ (make_set T1 tps)
   6.590 +      Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $
   6.591 +        t1 $ (make_set T1 tps)
   6.592    | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
   6.593  
   6.594  fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
   6.595 -  | make_coset T tps = 
   6.596 +  | make_coset T tps =
   6.597      let
   6.598        val U = T --> @{typ bool}
   6.599        fun invert @{const False} = @{const True}
   6.600          | invert @{const True} = @{const False}
   6.601      in
   6.602 -      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
   6.603 -        $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   6.604 +      Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) $
   6.605 +        Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
   6.606      end
   6.607  
   6.608  fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
   6.609    | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   6.610    | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   6.611 -  
   6.612 +
   6.613  fun post_process_term t =
   6.614    let
   6.615      fun map_Abs f t =
   6.616 -      case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   6.617 -    fun process_args t = case strip_comb t of
   6.618 -      (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
   6.619 +      (case t of
   6.620 +        Abs (x, T, t') => Abs (x, T, f t')
   6.621 +      | _ => raise TERM ("map_Abs", [t]))
   6.622 +    fun process_args t =
   6.623 +      (case strip_comb t of
   6.624 +        (c as Const (_, _), ts) => list_comb (c, map post_process_term ts))
   6.625    in
   6.626 -    case fastype_of t of
   6.627 +    (case fastype_of t of
   6.628        Type (@{type_name fun}, [T1, T2]) =>
   6.629          (case try dest_fun_upds t of
   6.630            SOME (tps, t) =>
   6.631 -            (map (apply2 post_process_term) tps, map_Abs post_process_term t)
   6.632 -            |> (case T2 of
   6.633 -              @{typ bool} => 
   6.634 -                (case t of
   6.635 -                   Abs(_, _, @{const False}) => fst #> rev #> make_set T1
   6.636 -                 | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
   6.637 -                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   6.638 -                 | _ => raise TERM ("post_process_term", [t]))
   6.639 -            | Type (@{type_name option}, _) =>
   6.640 -                (case t of
   6.641 -                  Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
   6.642 -                | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   6.643 -                | _ => make_fun_upds T1 T2)
   6.644 -            | _ => make_fun_upds T1 T2)
   6.645 +            (map (apply2 post_process_term) tps, map_Abs post_process_term t) |>
   6.646 +              (case T2 of
   6.647 +                @{typ bool} =>
   6.648 +                  (case t of
   6.649 +                     Abs(_, _, @{const False}) => fst #> rev #> make_set T1
   6.650 +                   | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
   6.651 +                   | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
   6.652 +                   | _ => raise TERM ("post_process_term", [t]))
   6.653 +              | Type (@{type_name option}, _) =>
   6.654 +                  (case t of
   6.655 +                    Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
   6.656 +                  | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   6.657 +                  | _ => make_fun_upds T1 T2)
   6.658 +              | _ => make_fun_upds T1 T2)
   6.659          | NONE => process_args t)
   6.660 -    | _ => process_args t
   6.661 +    | _ => process_args t)
   6.662    end
   6.663  
   6.664 -end;
   6.665 +end
     7.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Apr 14 15:33:23 2016 +0200
     7.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Apr 14 15:33:51 2016 +0200
     7.3 @@ -7,17 +7,19 @@
     7.4  signature RANDOM_GENERATORS =
     7.5  sig
     7.6    type seed = Random_Engine.seed
     7.7 -  val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term)
     7.8 -    -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     7.9 -    -> seed -> (('a -> 'b) * (unit -> term)) * seed
    7.10 -  val compile_generator_expr:
    7.11 -    Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option
    7.12 -  val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed)
    7.13 -    -> Proof.context -> Proof.context
    7.14 -  val put_counterexample_report: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed)
    7.15 -    -> Proof.context -> Proof.context
    7.16 +  val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) ->
    7.17 +    (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) ->
    7.18 +    seed -> (('a -> 'b) * (unit -> term)) * seed
    7.19 +  val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list ->
    7.20 +    (bool * term list) option * Quickcheck.report option
    7.21 +  val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural ->
    7.22 +    seed -> (bool * term list) option * seed) -> Proof.context -> Proof.context
    7.23 +  val put_counterexample_report: (unit -> Code_Numeral.natural -> bool ->
    7.24 +    Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed) ->
    7.25 +    Proof.context -> Proof.context
    7.26    val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr ->
    7.27 -    (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
    7.28 +    (string * sort) list -> string list -> string -> string list * string list ->
    7.29 +    typ list * typ list -> theory -> theory
    7.30  end;
    7.31  
    7.32  structure Random_Generators : RANDOM_GENERATORS =
    7.33 @@ -25,22 +27,22 @@
    7.34  
    7.35  (** abstract syntax **)
    7.36  
    7.37 -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
    7.38 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"})
    7.39  val size = @{term "i::natural"};
    7.40  val size_pred = @{term "(i::natural) - 1"};
    7.41  val size' = @{term "j::natural"};
    7.42  val seed = @{term "s::Random.seed"};
    7.43  
    7.44 -val resultT =  @{typ "(bool * term list) option"};
    7.45 +val resultT =  @{typ "(bool \<times> term list) option"};
    7.46  
    7.47 -(** typ "'a => 'b" **)
    7.48 +
    7.49 +(** typ "'a \<Rightarrow> 'b" **)
    7.50  
    7.51  type seed = Random_Engine.seed;
    7.52  
    7.53  fun random_fun T1 T2 eq term_of random random_split seed =
    7.54    let
    7.55 -    val fun_upd = Const (@{const_name fun_upd},
    7.56 -      (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    7.57 +    val fun_upd = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
    7.58      val ((_, t2), seed') = random seed;
    7.59      val (seed'', seed''') = random_split seed';
    7.60  
    7.61 @@ -474,6 +476,7 @@
    7.62  
    7.63  val test_goals =
    7.64    Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
    7.65 +
    7.66    
    7.67  (** setup **)
    7.68