1(* Title: HOL/Quickcheck_Exhaustive.thy 2 Author: Lukas Bulwahn, TU Muenchen 3*) 4 5section \<open>A simple counterexample generator performing exhaustive testing\<close> 6 7theory Quickcheck_Exhaustive 8imports Quickcheck_Random 9keywords "quickcheck_generator" :: thy_decl 10begin 11 12subsection \<open>Basic operations for exhaustive generators\<close> 13 14definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" (infixr "orelse" 55) 15 where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)" 16 17 18subsection \<open>Exhaustive generator type classes\<close> 19 20class exhaustive = term_of + 21 fixes exhaustive :: "('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 22 23class full_exhaustive = term_of + 24 fixes full_exhaustive :: 25 "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 26 27instantiation natural :: full_exhaustive 28begin 29 30function full_exhaustive_natural' :: 31 "(natural \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 32 natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 33 where "full_exhaustive_natural' f d i = 34 (if d < i then None 35 else (f (i, \<lambda>_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))" 36by pat_completeness auto 37 38termination 39 by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) 40 41definition "full_exhaustive f d = full_exhaustive_natural' f d 0" 42 43instance .. 44 45end 46 47instantiation natural :: exhaustive 48begin 49 50function exhaustive_natural' :: 51 "(natural \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 52 where "exhaustive_natural' f d i = 53 (if d < i then None 54 else (f i orelse exhaustive_natural' f d (i + 1)))" 55by pat_completeness auto 56 57termination 58 by (relation "measure (\<lambda>(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) 59 60definition "exhaustive f d = exhaustive_natural' f d 0" 61 62instance .. 63 64end 65 66instantiation integer :: exhaustive 67begin 68 69function exhaustive_integer' :: 70 "(integer \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option" 71 where "exhaustive_integer' f d i = 72 (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))" 73by pat_completeness auto 74 75termination 76 by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))") 77 (auto simp add: less_integer_def nat_of_integer_def) 78 79definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" 80 81instance .. 82 83end 84 85instantiation integer :: full_exhaustive 86begin 87 88function full_exhaustive_integer' :: 89 "(integer \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 90 integer \<Rightarrow> integer \<Rightarrow> (bool \<times> term list) option" 91 where "full_exhaustive_integer' f d i = 92 (if d < i then None 93 else 94 (case f (i, \<lambda>_. Code_Evaluation.term_of i) of 95 Some t \<Rightarrow> Some t 96 | None \<Rightarrow> full_exhaustive_integer' f d (i + 1)))" 97by pat_completeness auto 98 99termination 100 by (relation "measure (\<lambda>(_, d, i). nat_of_integer (d + 1 - i))") 101 (auto simp add: less_integer_def nat_of_integer_def) 102 103definition "full_exhaustive f d = 104 full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" 105 106instance .. 107 108end 109 110instantiation nat :: exhaustive 111begin 112 113definition "exhaustive f d = exhaustive (\<lambda>x. f (nat_of_natural x)) d" 114 115instance .. 116 117end 118 119instantiation nat :: full_exhaustive 120begin 121 122definition "full_exhaustive f d = 123 full_exhaustive (\<lambda>(x, xt). f (nat_of_natural x, \<lambda>_. Code_Evaluation.term_of (nat_of_natural x))) d" 124 125instance .. 126 127end 128 129instantiation int :: exhaustive 130begin 131 132function exhaustive_int' :: 133 "(int \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option" 134 where "exhaustive_int' f d i = 135 (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))" 136by pat_completeness auto 137 138termination 139 by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto 140 141definition "exhaustive f d = 142 exhaustive_int' f (int_of_integer (integer_of_natural d)) 143 (- (int_of_integer (integer_of_natural d)))" 144 145instance .. 146 147end 148 149instantiation int :: full_exhaustive 150begin 151 152function full_exhaustive_int' :: 153 "(int \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 154 int \<Rightarrow> int \<Rightarrow> (bool \<times> term list) option" 155 where "full_exhaustive_int' f d i = 156 (if d < i then None 157 else 158 (case f (i, \<lambda>_. Code_Evaluation.term_of i) of 159 Some t \<Rightarrow> Some t 160 | None \<Rightarrow> full_exhaustive_int' f d (i + 1)))" 161by pat_completeness auto 162 163termination 164 by (relation "measure (\<lambda>(_, d, i). nat (d + 1 - i))") auto 165 166definition "full_exhaustive f d = 167 full_exhaustive_int' f (int_of_integer (integer_of_natural d)) 168 (- (int_of_integer (integer_of_natural d)))" 169 170instance .. 171 172end 173 174instantiation prod :: (exhaustive, exhaustive) exhaustive 175begin 176 177definition "exhaustive f d = exhaustive (\<lambda>x. exhaustive (\<lambda>y. f ((x, y))) d) d" 178 179instance .. 180 181end 182 183definition (in term_syntax) 184 [code_unfold]: "valtermify_pair x y = 185 Code_Evaluation.valtermify (Pair :: 'a::typerep \<Rightarrow> 'b::typerep \<Rightarrow> 'a \<times> 'b) {\<cdot>} x {\<cdot>} y" 186 187instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive 188begin 189 190definition "full_exhaustive f d = 191 full_exhaustive (\<lambda>x. full_exhaustive (\<lambda>y. f (valtermify_pair x y)) d) d" 192 193instance .. 194 195end 196 197instantiation set :: (exhaustive) exhaustive 198begin 199 200fun exhaustive_set 201where 202 "exhaustive_set f i = 203 (if i = 0 then None 204 else 205 f {} orelse 206 exhaustive_set 207 (\<lambda>A. f A orelse exhaustive (\<lambda>x. if x \<in> A then None else f (insert x A)) (i - 1)) (i - 1))" 208 209instance .. 210 211end 212 213instantiation set :: (full_exhaustive) full_exhaustive 214begin 215 216fun full_exhaustive_set 217where 218 "full_exhaustive_set f i = 219 (if i = 0 then None 220 else 221 f valterm_emptyset orelse 222 full_exhaustive_set 223 (\<lambda>A. f A orelse Quickcheck_Exhaustive.full_exhaustive 224 (\<lambda>x. if fst x \<in> fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))" 225 226instance .. 227 228end 229 230instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive 231begin 232 233fun exhaustive_fun' :: 234 "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 235where 236 "exhaustive_fun' f i d = 237 (exhaustive (\<lambda>b. f (\<lambda>_. b)) d) orelse 238 (if i > 1 then 239 exhaustive_fun' 240 (\<lambda>g. exhaustive (\<lambda>a. exhaustive (\<lambda>b. f (g(a := b))) d) d) (i - 1) d else None)" 241 242definition exhaustive_fun :: 243 "(('a \<Rightarrow> 'b) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 244 where "exhaustive_fun f d = exhaustive_fun' f d d" 245 246instance .. 247 248end 249 250definition [code_unfold]: 251 "valtermify_absdummy = 252 (\<lambda>(v, t). 253 (\<lambda>_::'a. v, 254 \<lambda>u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))" 255 256definition (in term_syntax) 257 [code_unfold]: "valtermify_fun_upd g a b = 258 Code_Evaluation.valtermify 259 (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) {\<cdot>} g {\<cdot>} a {\<cdot>} b" 260 261instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive 262begin 263 264fun full_exhaustive_fun' :: 265 "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 266 natural \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" 267where 268 "full_exhaustive_fun' f i d = 269 full_exhaustive (\<lambda>v. f (valtermify_absdummy v)) d orelse 270 (if i > 1 then 271 full_exhaustive_fun' 272 (\<lambda>g. full_exhaustive 273 (\<lambda>a. full_exhaustive (\<lambda>b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d 274 else None)" 275 276definition full_exhaustive_fun :: 277 "(('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 278 natural \<Rightarrow> (bool \<times> term list) option" 279 where "full_exhaustive_fun f d = full_exhaustive_fun' f d d" 280 281instance .. 282 283end 284 285subsubsection \<open>A smarter enumeration scheme for functions over finite datatypes\<close> 286 287class check_all = enum + term_of + 288 fixes check_all :: "('a \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool * term list) option" 289 fixes enum_term_of :: "'a itself \<Rightarrow> unit \<Rightarrow> term list" 290 291fun check_all_n_lists :: "('a::check_all list \<times> (unit \<Rightarrow> term list) \<Rightarrow> 292 (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" 293where 294 "check_all_n_lists f n = 295 (if n = 0 then f ([], (\<lambda>_. [])) 296 else check_all (\<lambda>(x, xt). 297 check_all_n_lists (\<lambda>(xs, xst). f ((x # xs), (\<lambda>_. (xt () # xst ())))) (n - 1)))" 298 299definition (in term_syntax) 300 [code_unfold]: "termify_fun_upd g a b = 301 (Code_Evaluation.termify 302 (fun_upd :: ('a::typerep \<Rightarrow> 'b::typerep) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b) <\<cdot>> g <\<cdot>> a <\<cdot>> b)" 303 304definition mk_map_term :: 305 "(unit \<Rightarrow> typerep) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> 306 (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> unit \<Rightarrow> term" 307 where "mk_map_term T1 T2 domm rng = 308 (\<lambda>_. 309 let 310 T1 = T1 (); 311 T2 = T2 (); 312 update_term = 313 (\<lambda>g (a, b). 314 Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App 315 (Code_Evaluation.Const (STR ''Fun.fun_upd'') 316 (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], 317 Typerep.Typerep (STR ''fun'') [T1, 318 Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) 319 g) a) b) 320 in 321 List.foldl update_term 322 (Code_Evaluation.Abs (STR ''x'') T1 323 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" 324 325instantiation "fun" :: ("{equal,check_all}", check_all) check_all 326begin 327 328definition 329 "check_all f = 330 (let 331 mk_term = 332 mk_map_term 333 (\<lambda>_. Typerep.typerep (TYPE('a))) 334 (\<lambda>_. Typerep.typerep (TYPE('b))) 335 (enum_term_of (TYPE('a))); 336 enum = (Enum.enum :: 'a list) 337 in 338 check_all_n_lists 339 (\<lambda>(ys, yst). f (the \<circ> map_of (zip enum ys), mk_term yst)) 340 (natural_of_nat (length enum)))" 341 342definition enum_term_of_fun :: "('a \<Rightarrow> 'b) itself \<Rightarrow> unit \<Rightarrow> term list" 343 where "enum_term_of_fun = 344 (\<lambda>_ _. 345 let 346 enum_term_of_a = enum_term_of (TYPE('a)); 347 mk_term = 348 mk_map_term 349 (\<lambda>_. Typerep.typerep (TYPE('a))) 350 (\<lambda>_. Typerep.typerep (TYPE('b))) 351 enum_term_of_a 352 in 353 map (\<lambda>ys. mk_term (\<lambda>_. ys) ()) 354 (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" 355 356instance .. 357 358end 359 360fun (in term_syntax) check_all_subsets :: 361 "(('a::typerep) set \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> 362 ('a \<times> (unit \<Rightarrow> term)) list \<Rightarrow> (bool \<times> term list) option" 363where 364 "check_all_subsets f [] = f valterm_emptyset" 365| "check_all_subsets f (x # xs) = 366 check_all_subsets (\<lambda>s. case f s of Some ts \<Rightarrow> Some ts | None \<Rightarrow> f (valtermify_insert x s)) xs" 367 368 369definition (in term_syntax) 370 [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)" 371 372definition (in term_syntax) 373 [code_unfold]: "termify_insert x s = 374 Code_Evaluation.termify (insert :: ('a::typerep) \<Rightarrow> 'a set \<Rightarrow> 'a set) <\<cdot>> x <\<cdot>> s" 375 376definition (in term_syntax) setify :: "('a::typerep) itself \<Rightarrow> term list \<Rightarrow> term" 377where 378 "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" 379 380instantiation set :: (check_all) check_all 381begin 382 383definition 384 "check_all_set f = 385 check_all_subsets f 386 (zip (Enum.enum :: 'a list) 387 (map (\<lambda>a. \<lambda>u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))" 388 389definition enum_term_of_set :: "'a set itself \<Rightarrow> unit \<Rightarrow> term list" 390 where "enum_term_of_set _ _ = 391 map (setify (TYPE('a))) (subseqs (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))" 392 393instance .. 394 395end 396 397instantiation unit :: check_all 398begin 399 400definition "check_all f = f (Code_Evaluation.valtermify ())" 401 402definition enum_term_of_unit :: "unit itself \<Rightarrow> unit \<Rightarrow> term list" 403 where "enum_term_of_unit = (\<lambda>_ _. [Code_Evaluation.term_of ()])" 404 405instance .. 406 407end 408 409 410instantiation bool :: check_all 411begin 412 413definition 414 "check_all f = 415 (case f (Code_Evaluation.valtermify False) of 416 Some x' \<Rightarrow> Some x' 417 | None \<Rightarrow> f (Code_Evaluation.valtermify True))" 418 419definition enum_term_of_bool :: "bool itself \<Rightarrow> unit \<Rightarrow> term list" 420 where "enum_term_of_bool = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" 421 422instance .. 423 424end 425 426definition (in term_syntax) [code_unfold]: 427 "termify_pair x y = 428 Code_Evaluation.termify (Pair :: 'a::typerep \<Rightarrow> 'b :: typerep \<Rightarrow> 'a * 'b) <\<cdot>> x <\<cdot>> y" 429 430instantiation prod :: (check_all, check_all) check_all 431begin 432 433definition "check_all f = check_all (\<lambda>x. check_all (\<lambda>y. f (valtermify_pair x y)))" 434 435definition enum_term_of_prod :: "('a * 'b) itself \<Rightarrow> unit \<Rightarrow> term list" 436 where "enum_term_of_prod = 437 (\<lambda>_ _. 438 map (\<lambda>(x, y). termify_pair TYPE('a) TYPE('b) x y) 439 (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" 440 441instance .. 442 443end 444 445definition (in term_syntax) 446 [code_unfold]: "valtermify_Inl x = 447 Code_Evaluation.valtermify (Inl :: 'a::typerep \<Rightarrow> 'a + 'b :: typerep) {\<cdot>} x" 448 449definition (in term_syntax) 450 [code_unfold]: "valtermify_Inr x = 451 Code_Evaluation.valtermify (Inr :: 'b::typerep \<Rightarrow> 'a::typerep + 'b) {\<cdot>} x" 452 453instantiation sum :: (check_all, check_all) check_all 454begin 455 456definition 457 "check_all f = check_all (\<lambda>a. f (valtermify_Inl a)) orelse check_all (\<lambda>b. f (valtermify_Inr b))" 458 459definition enum_term_of_sum :: "('a + 'b) itself \<Rightarrow> unit \<Rightarrow> term list" 460 where "enum_term_of_sum = 461 (\<lambda>_ _. 462 let 463 T1 = Typerep.typerep (TYPE('a)); 464 T2 = Typerep.typerep (TYPE('b)) 465 in 466 map 467 (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') 468 (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) 469 (enum_term_of (TYPE('a)) ()) @ 470 map 471 (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') 472 (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) 473 (enum_term_of (TYPE('b)) ()))" 474 475instance .. 476 477end 478 479instantiation char :: check_all 480begin 481 482primrec check_all_char' :: 483 "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> char list \<Rightarrow> (bool \<times> term list) option" 484 where "check_all_char' f [] = None" 485 | "check_all_char' f (c # cs) = f (c, \<lambda>_. Code_Evaluation.term_of c) 486 orelse check_all_char' f cs" 487 488definition check_all_char :: 489 "(char \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option" 490 where "check_all f = check_all_char' f Enum.enum" 491 492definition enum_term_of_char :: "char itself \<Rightarrow> unit \<Rightarrow> term list" 493where 494 "enum_term_of_char = (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: char list))" 495 496instance .. 497 498end 499 500instantiation option :: (check_all) check_all 501begin 502 503definition 504 "check_all f = 505 f (Code_Evaluation.valtermify (None :: 'a option)) orelse 506 check_all 507 (\<lambda>(x, t). 508 f 509 (Some x, 510 \<lambda>_. Code_Evaluation.App 511 (Code_Evaluation.Const (STR ''Option.option.Some'') 512 (Typerep.Typerep (STR ''fun'') 513 [Typerep.typerep TYPE('a), 514 Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))" 515 516definition enum_term_of_option :: "'a option itself \<Rightarrow> unit \<Rightarrow> term list" 517 where "enum_term_of_option = 518 (\<lambda> _ _. 519 Code_Evaluation.term_of (None :: 'a option) # 520 (map 521 (Code_Evaluation.App 522 (Code_Evaluation.Const (STR ''Option.option.Some'') 523 (Typerep.Typerep (STR ''fun'') 524 [Typerep.typerep TYPE('a), 525 Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) 526 (enum_term_of (TYPE('a)) ())))" 527 528instance .. 529 530end 531 532 533instantiation Enum.finite_1 :: check_all 534begin 535 536definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)" 537 538definition enum_term_of_finite_1 :: "Enum.finite_1 itself \<Rightarrow> unit \<Rightarrow> term list" 539 where "enum_term_of_finite_1 = (\<lambda>_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])" 540 541instance .. 542 543end 544 545instantiation Enum.finite_2 :: check_all 546begin 547 548definition 549 "check_all f = 550 (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse 551 f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))" 552 553definition enum_term_of_finite_2 :: "Enum.finite_2 itself \<Rightarrow> unit \<Rightarrow> term list" 554 where "enum_term_of_finite_2 = 555 (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" 556 557instance .. 558 559end 560 561instantiation Enum.finite_3 :: check_all 562begin 563 564definition 565 "check_all f = 566 (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse 567 f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse 568 f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))" 569 570definition enum_term_of_finite_3 :: "Enum.finite_3 itself \<Rightarrow> unit \<Rightarrow> term list" 571 where "enum_term_of_finite_3 = 572 (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" 573 574instance .. 575 576end 577 578instantiation Enum.finite_4 :: check_all 579begin 580 581definition 582 "check_all f = 583 f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse 584 f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse 585 f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse 586 f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)" 587 588definition enum_term_of_finite_4 :: "Enum.finite_4 itself \<Rightarrow> unit \<Rightarrow> term list" 589 where "enum_term_of_finite_4 = 590 (\<lambda>_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))" 591 592instance .. 593 594end 595 596subsection \<open>Bounded universal quantifiers\<close> 597 598class bounded_forall = 599 fixes bounded_forall :: "('a \<Rightarrow> bool) \<Rightarrow> natural \<Rightarrow> bool" 600 601 602subsection \<open>Fast exhaustive combinators\<close> 603 604class fast_exhaustive = term_of + 605 fixes fast_exhaustive :: "('a \<Rightarrow> unit) \<Rightarrow> natural \<Rightarrow> unit" 606 607axiomatization throw_Counterexample :: "term list \<Rightarrow> unit" 608axiomatization catch_Counterexample :: "unit \<Rightarrow> term list option" 609 610code_printing 611 constant throw_Counterexample \<rightharpoonup> 612 (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)" 613| constant catch_Counterexample \<rightharpoonup> 614 (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \<Rightarrow> SOME ts)" 615 616 617subsection \<open>Continuation passing style functions as plus monad\<close> 618 619type_synonym 'a cps = "('a \<Rightarrow> term list option) \<Rightarrow> term list option" 620 621definition cps_empty :: "'a cps" 622 where "cps_empty = (\<lambda>cont. None)" 623 624definition cps_single :: "'a \<Rightarrow> 'a cps" 625 where "cps_single v = (\<lambda>cont. cont v)" 626 627definition cps_bind :: "'a cps \<Rightarrow> ('a \<Rightarrow> 'b cps) \<Rightarrow> 'b cps" 628 where "cps_bind m f = (\<lambda>cont. m (\<lambda>a. (f a) cont))" 629 630definition cps_plus :: "'a cps \<Rightarrow> 'a cps \<Rightarrow> 'a cps" 631 where "cps_plus a b = (\<lambda>c. case a c of None \<Rightarrow> b c | Some x \<Rightarrow> Some x)" 632 633definition cps_if :: "bool \<Rightarrow> unit cps" 634 where "cps_if b = (if b then cps_single () else cps_empty)" 635 636definition cps_not :: "unit cps \<Rightarrow> unit cps" 637 where "cps_not n = (\<lambda>c. case n (\<lambda>u. Some []) of None \<Rightarrow> c () | Some _ \<Rightarrow> None)" 638 639type_synonym 'a pos_bound_cps = 640 "('a \<Rightarrow> (bool * term list) option) \<Rightarrow> natural \<Rightarrow> (bool * term list) option" 641 642definition pos_bound_cps_empty :: "'a pos_bound_cps" 643 where "pos_bound_cps_empty = (\<lambda>cont i. None)" 644 645definition pos_bound_cps_single :: "'a \<Rightarrow> 'a pos_bound_cps" 646 where "pos_bound_cps_single v = (\<lambda>cont i. cont v)" 647 648definition pos_bound_cps_bind :: "'a pos_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b pos_bound_cps) \<Rightarrow> 'b pos_bound_cps" 649 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)))" 650 651definition pos_bound_cps_plus :: "'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps \<Rightarrow> 'a pos_bound_cps" 652 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)" 653 654definition pos_bound_cps_if :: "bool \<Rightarrow> unit pos_bound_cps" 655 where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" 656 657datatype (plugins only: code extraction) (dead 'a) unknown = 658 Unknown | Known 'a 659 660datatype (plugins only: code extraction) (dead 'a) three_valued = 661 Unknown_value | Value 'a | No_value 662 663type_synonym 'a neg_bound_cps = 664 "('a unknown \<Rightarrow> term list three_valued) \<Rightarrow> natural \<Rightarrow> term list three_valued" 665 666definition neg_bound_cps_empty :: "'a neg_bound_cps" 667 where "neg_bound_cps_empty = (\<lambda>cont i. No_value)" 668 669definition neg_bound_cps_single :: "'a \<Rightarrow> 'a neg_bound_cps" 670 where "neg_bound_cps_single v = (\<lambda>cont i. cont (Known v))" 671 672definition neg_bound_cps_bind :: "'a neg_bound_cps \<Rightarrow> ('a \<Rightarrow> 'b neg_bound_cps) \<Rightarrow> 'b neg_bound_cps" 673 where "neg_bound_cps_bind m f = 674 (\<lambda>cont i. 675 if i = 0 then cont Unknown 676 else m (\<lambda>a. case a of Unknown \<Rightarrow> cont Unknown | Known a' \<Rightarrow> f a' cont i) (i - 1))" 677 678definition neg_bound_cps_plus :: "'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps \<Rightarrow> 'a neg_bound_cps" 679 where "neg_bound_cps_plus a b = 680 (\<lambda>c i. 681 case a c i of 682 No_value \<Rightarrow> b c i 683 | Value x \<Rightarrow> Value x 684 | Unknown_value \<Rightarrow> 685 (case b c i of 686 No_value \<Rightarrow> Unknown_value 687 | Value x \<Rightarrow> Value x 688 | Unknown_value \<Rightarrow> Unknown_value))" 689 690definition neg_bound_cps_if :: "bool \<Rightarrow> unit neg_bound_cps" 691 where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)" 692 693definition neg_bound_cps_not :: "unit pos_bound_cps \<Rightarrow> unit neg_bound_cps" 694 where "neg_bound_cps_not n = 695 (\<lambda>c i. case n (\<lambda>u. Some (True, [])) i of None \<Rightarrow> c (Known ()) | Some _ \<Rightarrow> No_value)" 696 697definition pos_bound_cps_not :: "unit neg_bound_cps \<Rightarrow> unit pos_bound_cps" 698 where "pos_bound_cps_not n = 699 (\<lambda>c i. case n (\<lambda>u. Value []) i of No_value \<Rightarrow> c () | Value _ \<Rightarrow> None | Unknown_value \<Rightarrow> None)" 700 701 702subsection \<open>Defining generators for any first-order data type\<close> 703 704axiomatization unknown :: 'a 705 706notation (output) unknown ("?") 707 708ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close> 709 710declare [[quickcheck_batch_tester = exhaustive]] 711 712 713subsection \<open>Defining generators for abstract types\<close> 714 715ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close> 716 717hide_fact (open) orelse_def 718no_notation orelse (infixr "orelse" 55) 719 720hide_const valtermify_absdummy valtermify_fun_upd 721 valterm_emptyset valtermify_insert 722 valtermify_pair valtermify_Inl valtermify_Inr 723 termify_fun_upd term_emptyset termify_insert termify_pair setify 724 725hide_const (open) 726 exhaustive full_exhaustive 727 exhaustive_int' full_exhaustive_int' 728 exhaustive_integer' full_exhaustive_integer' 729 exhaustive_natural' full_exhaustive_natural' 730 throw_Counterexample catch_Counterexample 731 check_all enum_term_of 732 orelse unknown mk_map_term check_all_n_lists check_all_subsets 733 734hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued 735 736hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not 737 pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind 738 pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not 739 neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind 740 neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not 741 Unknown Known Unknown_value Value No_value 742 743end 744