src/HOL/Nitpick_Examples/Refute_Nits.thy
author blanchet
Mon Feb 22 19:31:00 2010 +0100 (2010-02-22)
changeset 35284 9edc2bd6d2bd
parent 35087 e385fa507468
child 35338 38848da259c0
permissions -rw-r--r--
enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
     1 (*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009, 2010
     4 
     5 Refute examples adapted to Nitpick.
     6 *)
     7 
     8 header {* Refute Examples Adapted to Nitpick *}
     9 
    10 theory Refute_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
    15                 timeout = 60 s]
    16 
    17 lemma "P \<and> Q"
    18 apply (rule conjI)
    19 nitpick [expect = genuine] 1
    20 nitpick [expect = genuine] 2
    21 nitpick [expect = genuine]
    22 nitpick [card = 5, expect = genuine]
    23 nitpick [sat_solver = SAT4J, expect = genuine] 2
    24 oops
    25 
    26 subsection {* Examples and Test Cases *}
    27 
    28 subsubsection {* Propositional logic *}
    29 
    30 lemma "True"
    31 nitpick [expect = none]
    32 apply auto
    33 done
    34 
    35 lemma "False"
    36 nitpick [expect = genuine]
    37 oops
    38 
    39 lemma "P"
    40 nitpick [expect = genuine]
    41 oops
    42 
    43 lemma "\<not> P"
    44 nitpick [expect = genuine]
    45 oops
    46 
    47 lemma "P \<and> Q"
    48 nitpick [expect = genuine]
    49 oops
    50 
    51 lemma "P \<or> Q"
    52 nitpick [expect = genuine]
    53 oops
    54 
    55 lemma "P \<longrightarrow> Q"
    56 nitpick [expect = genuine]
    57 oops
    58 
    59 lemma "(P\<Colon>bool) = Q"
    60 nitpick [expect = genuine]
    61 oops
    62 
    63 lemma "(P \<or> Q) \<longrightarrow> (P \<and> Q)"
    64 nitpick [expect = genuine]
    65 oops
    66 
    67 subsubsection {* Predicate logic *}
    68 
    69 lemma "P x y z"
    70 nitpick [expect = genuine]
    71 oops
    72 
    73 lemma "P x y \<longrightarrow> P y x"
    74 nitpick [expect = genuine]
    75 oops
    76 
    77 lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
    78 nitpick [expect = genuine]
    79 oops
    80 
    81 subsubsection {* Equality *}
    82 
    83 lemma "P = True"
    84 nitpick [expect = genuine]
    85 oops
    86 
    87 lemma "P = False"
    88 nitpick [expect = genuine]
    89 oops
    90 
    91 lemma "x = y"
    92 nitpick [expect = genuine]
    93 oops
    94 
    95 lemma "f x = g x"
    96 nitpick [expect = genuine]
    97 oops
    98 
    99 lemma "(f\<Colon>'a\<Rightarrow>'b) = g"
   100 nitpick [expect = genuine]
   101 oops
   102 
   103 lemma "(f\<Colon>('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
   104 nitpick [expect = genuine]
   105 oops
   106 
   107 lemma "distinct [a, b]"
   108 nitpick [expect = genuine]
   109 apply simp
   110 nitpick [expect = genuine]
   111 oops
   112 
   113 subsubsection {* First-Order Logic *}
   114 
   115 lemma "\<exists>x. P x"
   116 nitpick [expect = genuine]
   117 oops
   118 
   119 lemma "\<forall>x. P x"
   120 nitpick [expect = genuine]
   121 oops
   122 
   123 lemma "\<exists>!x. P x"
   124 nitpick [expect = genuine]
   125 oops
   126 
   127 lemma "Ex P"
   128 nitpick [expect = genuine]
   129 oops
   130 
   131 lemma "All P"
   132 nitpick [expect = genuine]
   133 oops
   134 
   135 lemma "Ex1 P"
   136 nitpick [expect = genuine]
   137 oops
   138 
   139 lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
   140 nitpick [expect = genuine]
   141 oops
   142 
   143 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
   144 nitpick [expect = genuine]
   145 oops
   146 
   147 lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   148 nitpick [expect = genuine]
   149 oops
   150 
   151 text {* A true statement (also testing names of free and bound variables being identical) *}
   152 
   153 lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
   154 nitpick [expect = none]
   155 apply fast
   156 done
   157 
   158 text {* "A type has at most 4 elements." *}
   159 
   160 lemma "\<not> distinct [a, b, c, d, e]"
   161 nitpick [expect = genuine]
   162 apply simp
   163 nitpick [expect = genuine]
   164 oops
   165 
   166 lemma "distinct [a, b, c, d]"
   167 nitpick [expect = genuine]
   168 apply simp
   169 nitpick [expect = genuine]
   170 oops
   171 
   172 text {* "Every reflexive and symmetric relation is transitive." *}
   173 
   174 lemma "\<lbrakk>\<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x\<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
   175 nitpick [expect = genuine]
   176 oops
   177 
   178 text {* The ``Drinker's theorem'' *}
   179 
   180 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
   181 nitpick [expect = none]
   182 apply (auto simp add: ext)
   183 done
   184 
   185 text {* And an incorrect version of it *}
   186 
   187 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   188 nitpick [expect = genuine]
   189 oops
   190 
   191 text {* "Every function has a fixed point." *}
   192 
   193 lemma "\<exists>x. f x = x"
   194 nitpick [expect = genuine]
   195 oops
   196 
   197 text {* "Function composition is commutative." *}
   198 
   199 lemma "f (g x) = g (f x)"
   200 nitpick [expect = genuine]
   201 oops
   202 
   203 text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
   204 
   205 lemma "((P\<Colon>('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
   206 nitpick [expect = genuine]
   207 oops
   208 
   209 subsubsection {* Higher-Order Logic *}
   210 
   211 lemma "\<exists>P. P"
   212 nitpick [expect = none]
   213 apply auto
   214 done
   215 
   216 lemma "\<forall>P. P"
   217 nitpick [expect = genuine]
   218 oops
   219 
   220 lemma "\<exists>!P. P"
   221 nitpick [expect = none]
   222 apply auto
   223 done
   224 
   225 lemma "\<exists>!P. P x"
   226 nitpick [expect = genuine]
   227 oops
   228 
   229 lemma "P Q \<or> Q x"
   230 nitpick [expect = genuine]
   231 oops
   232 
   233 lemma "x \<noteq> All"
   234 nitpick [expect = genuine]
   235 oops
   236 
   237 lemma "x \<noteq> Ex"
   238 nitpick [expect = genuine]
   239 oops
   240 
   241 lemma "x \<noteq> Ex1"
   242 nitpick [expect = genuine]
   243 oops
   244 
   245 text {* ``The transitive closure of an arbitrary relation is non-empty.'' *}
   246 
   247 constdefs
   248 "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   249 "trans P \<equiv> (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
   250 "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   251 "subset P Q \<equiv> (ALL x y. P x y \<longrightarrow> Q x y)"
   252 "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   253 "trans_closure P Q \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
   254 
   255 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
   256 nitpick [expect = genuine]
   257 oops
   258 
   259 text {* ``The union of transitive closures is equal to the transitive closure of unions.'' *}
   260 
   261 lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
   262  \<longrightarrow> trans_closure TP P
   263  \<longrightarrow> trans_closure TR R
   264  \<longrightarrow> (T x y = (TP x y \<or> TR x y))"
   265 nitpick [expect = genuine]
   266 oops
   267 
   268 text {* ``Every surjective function is invertible.'' *}
   269 
   270 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
   271 nitpick [expect = genuine]
   272 oops
   273 
   274 text {* ``Every invertible function is surjective.'' *}
   275 
   276 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   277 nitpick [expect = genuine]
   278 oops
   279 
   280 text {* ``Every point is a fixed point of some function.'' *}
   281 
   282 lemma "\<exists>f. f x = x"
   283 nitpick [card = 1\<midarrow>7, expect = none]
   284 apply (rule_tac x = "\<lambda>x. x" in exI)
   285 apply simp
   286 done
   287 
   288 text {* Axiom of Choice: first an incorrect version *}
   289 
   290 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   291 nitpick [expect = genuine]
   292 oops
   293 
   294 text {* And now two correct ones *}
   295 
   296 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   297 nitpick [card = 1-4, expect = none]
   298 apply (simp add: choice)
   299 done
   300 
   301 lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   302 nitpick [card = 1-3, expect = none]
   303 apply auto
   304  apply (simp add: ex1_implies_ex choice)
   305 apply (fast intro: ext)
   306 done
   307 
   308 subsubsection {* Metalogic *}
   309 
   310 lemma "\<And>x. P x"
   311 nitpick [expect = genuine]
   312 oops
   313 
   314 lemma "f x \<equiv> g x"
   315 nitpick [expect = genuine]
   316 oops
   317 
   318 lemma "P \<Longrightarrow> Q"
   319 nitpick [expect = genuine]
   320 oops
   321 
   322 lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
   323 nitpick [expect = genuine]
   324 oops
   325 
   326 lemma "(x \<equiv> all) \<Longrightarrow> False"
   327 nitpick [expect = genuine]
   328 oops
   329 
   330 lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
   331 nitpick [expect = genuine]
   332 oops
   333 
   334 lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
   335 nitpick [expect = genuine]
   336 oops
   337 
   338 subsubsection {* Schematic Variables *}
   339 
   340 lemma "?P"
   341 nitpick [expect = none]
   342 apply auto
   343 done
   344 
   345 lemma "x = ?y"
   346 nitpick [expect = none]
   347 apply auto
   348 done
   349 
   350 subsubsection {* Abstractions *}
   351 
   352 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
   353 nitpick [expect = genuine]
   354 oops
   355 
   356 lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
   357 nitpick [expect = genuine]
   358 oops
   359 
   360 lemma "(\<lambda>x. x) = (\<lambda>y. y)"
   361 nitpick [expect = none]
   362 apply simp
   363 done
   364 
   365 subsubsection {* Sets *}
   366 
   367 lemma "P (A\<Colon>'a set)"
   368 nitpick [expect = genuine]
   369 oops
   370 
   371 lemma "P (A\<Colon>'a set set)"
   372 nitpick [expect = genuine]
   373 oops
   374 
   375 lemma "{x. P x} = {y. P y}"
   376 nitpick [expect = none]
   377 apply simp
   378 done
   379 
   380 lemma "x \<in> {x. P x}"
   381 nitpick [expect = genuine]
   382 oops
   383 
   384 lemma "P (op \<in>)"
   385 nitpick [expect = genuine]
   386 oops
   387 
   388 lemma "P (op \<in> x)"
   389 nitpick [expect = genuine]
   390 oops
   391 
   392 lemma "P Collect"
   393 nitpick [expect = genuine]
   394 oops
   395 
   396 lemma "A Un B = A Int B"
   397 nitpick [expect = genuine]
   398 oops
   399 
   400 lemma "(A Int B) Un C = (A Un C) Int B"
   401 nitpick [expect = genuine]
   402 oops
   403 
   404 lemma "Ball A P \<longrightarrow> Bex A P"
   405 nitpick [expect = genuine]
   406 oops
   407 
   408 subsubsection {* @{const undefined} *}
   409 
   410 lemma "undefined"
   411 nitpick [expect = genuine]
   412 oops
   413 
   414 lemma "P undefined"
   415 nitpick [expect = genuine]
   416 oops
   417 
   418 lemma "undefined x"
   419 nitpick [expect = genuine]
   420 oops
   421 
   422 lemma "undefined undefined"
   423 nitpick [expect = genuine]
   424 oops
   425 
   426 subsubsection {* @{const The} *}
   427 
   428 lemma "The P"
   429 nitpick [expect = genuine]
   430 oops
   431 
   432 lemma "P The"
   433 nitpick [expect = genuine]
   434 oops
   435 
   436 lemma "P (The P)"
   437 nitpick [expect = genuine]
   438 oops
   439 
   440 lemma "(THE x. x=y) = z"
   441 nitpick [expect = genuine]
   442 oops
   443 
   444 lemma "Ex P \<longrightarrow> P (The P)"
   445 nitpick [expect = genuine]
   446 oops
   447 
   448 subsubsection {* @{const Eps} *}
   449 
   450 lemma "Eps P"
   451 nitpick [expect = genuine]
   452 oops
   453 
   454 lemma "P Eps"
   455 nitpick [expect = genuine]
   456 oops
   457 
   458 lemma "P (Eps P)"
   459 nitpick [expect = genuine]
   460 oops
   461 
   462 lemma "(SOME x. x=y) = z"
   463 nitpick [expect = genuine]
   464 oops
   465 
   466 lemma "Ex P \<longrightarrow> P (Eps P)"
   467 nitpick [expect = none]
   468 apply (auto simp add: someI)
   469 done
   470 
   471 subsubsection {* Operations on Natural Numbers *}
   472 
   473 lemma "(x\<Colon>nat) + y = 0"
   474 nitpick [expect = genuine]
   475 oops
   476 
   477 lemma "(x\<Colon>nat) = x + x"
   478 nitpick [expect = genuine]
   479 oops
   480 
   481 lemma "(x\<Colon>nat) - y + y = x"
   482 nitpick [expect = genuine]
   483 oops
   484 
   485 lemma "(x\<Colon>nat) = x * x"
   486 nitpick [expect = genuine]
   487 oops
   488 
   489 lemma "(x\<Colon>nat) < x + y"
   490 nitpick [card = 1, expect = genuine]
   491 nitpick [card = 2-5, expect = genuine]
   492 oops
   493 
   494 text {* \<times> *}
   495 
   496 lemma "P (x\<Colon>'a\<times>'b)"
   497 nitpick [expect = genuine]
   498 oops
   499 
   500 lemma "\<forall>x\<Colon>'a\<times>'b. P x"
   501 nitpick [expect = genuine]
   502 oops
   503 
   504 lemma "P (x, y)"
   505 nitpick [expect = genuine]
   506 oops
   507 
   508 lemma "P (fst x)"
   509 nitpick [expect = genuine]
   510 oops
   511 
   512 lemma "P (snd x)"
   513 nitpick [expect = genuine]
   514 oops
   515 
   516 lemma "P Pair"
   517 nitpick [expect = genuine]
   518 oops
   519 
   520 lemma "prod_rec f p = f (fst p) (snd p)"
   521 nitpick [expect = none]
   522 by (case_tac p) auto
   523 
   524 lemma "prod_rec f (a, b) = f a b"
   525 nitpick [expect = none]
   526 by auto
   527 
   528 lemma "P (prod_rec f x)"
   529 nitpick [expect = genuine]
   530 oops
   531 
   532 lemma "P (case x of Pair a b \<Rightarrow> f a b)"
   533 nitpick [expect = genuine]
   534 oops
   535 
   536 subsubsection {* Subtypes (typedef), typedecl *}
   537 
   538 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
   539 
   540 typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
   541 by auto
   542 
   543 lemma "(x\<Colon>'a myTdef) = y"
   544 nitpick [expect = genuine]
   545 oops
   546 
   547 typedecl myTdecl
   548 
   549 typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   550 by auto
   551 
   552 lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
   553 nitpick [expect = genuine]
   554 oops
   555 
   556 subsubsection {* Inductive Datatypes *}
   557 
   558 text {* unit *}
   559 
   560 lemma "P (x\<Colon>unit)"
   561 nitpick [expect = genuine]
   562 oops
   563 
   564 lemma "\<forall>x\<Colon>unit. P x"
   565 nitpick [expect = genuine]
   566 oops
   567 
   568 lemma "P ()"
   569 nitpick [expect = genuine]
   570 oops
   571 
   572 lemma "unit_rec u x = u"
   573 nitpick [expect = none]
   574 apply simp
   575 done
   576 
   577 lemma "P (unit_rec u x)"
   578 nitpick [expect = genuine]
   579 oops
   580 
   581 lemma "P (case x of () \<Rightarrow> u)"
   582 nitpick [expect = genuine]
   583 oops
   584 
   585 text {* option *}
   586 
   587 lemma "P (x\<Colon>'a option)"
   588 nitpick [expect = genuine]
   589 oops
   590 
   591 lemma "\<forall>x\<Colon>'a option. P x"
   592 nitpick [expect = genuine]
   593 oops
   594 
   595 lemma "P None"
   596 nitpick [expect = genuine]
   597 oops
   598 
   599 lemma "P (Some x)"
   600 nitpick [expect = genuine]
   601 oops
   602 
   603 lemma "option_rec n s None = n"
   604 nitpick [expect = none]
   605 apply simp
   606 done
   607 
   608 lemma "option_rec n s (Some x) = s x"
   609 nitpick [expect = none]
   610 apply simp
   611 done
   612 
   613 lemma "P (option_rec n s x)"
   614 nitpick [expect = genuine]
   615 oops
   616 
   617 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
   618 nitpick [expect = genuine]
   619 oops
   620 
   621 text {* + *}
   622 
   623 lemma "P (x\<Colon>'a+'b)"
   624 nitpick [expect = genuine]
   625 oops
   626 
   627 lemma "\<forall>x\<Colon>'a+'b. P x"
   628 nitpick [expect = genuine]
   629 oops
   630 
   631 lemma "P (Inl x)"
   632 nitpick [expect = genuine]
   633 oops
   634 
   635 lemma "P (Inr x)"
   636 nitpick [expect = genuine]
   637 oops
   638 
   639 lemma "P Inl"
   640 nitpick [expect = genuine]
   641 oops
   642 
   643 lemma "sum_rec l r (Inl x) = l x"
   644 nitpick [expect = none]
   645 apply simp
   646 done
   647 
   648 lemma "sum_rec l r (Inr x) = r x"
   649 nitpick [expect = none]
   650 apply simp
   651 done
   652 
   653 lemma "P (sum_rec l r x)"
   654 nitpick [expect = genuine]
   655 oops
   656 
   657 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
   658 nitpick [expect = genuine]
   659 oops
   660 
   661 text {* Non-recursive datatypes *}
   662 
   663 datatype T1 = A | B
   664 
   665 lemma "P (x\<Colon>T1)"
   666 nitpick [expect = genuine]
   667 oops
   668 
   669 lemma "\<forall>x\<Colon>T1. P x"
   670 nitpick [expect = genuine]
   671 oops
   672 
   673 lemma "P A"
   674 nitpick [expect = genuine]
   675 oops
   676 
   677 lemma "P B"
   678 nitpick [expect = genuine]
   679 oops
   680 
   681 lemma "T1_rec a b A = a"
   682 nitpick [expect = none]
   683 apply simp
   684 done
   685 
   686 lemma "T1_rec a b B = b"
   687 nitpick [expect = none]
   688 apply simp
   689 done
   690 
   691 lemma "P (T1_rec a b x)"
   692 nitpick [expect = genuine]
   693 oops
   694 
   695 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
   696 nitpick [expect = genuine]
   697 oops
   698 
   699 datatype 'a T2 = C T1 | D 'a
   700 
   701 lemma "P (x\<Colon>'a T2)"
   702 nitpick [expect = genuine]
   703 oops
   704 
   705 lemma "\<forall>x\<Colon>'a T2. P x"
   706 nitpick [expect = genuine]
   707 oops
   708 
   709 lemma "P D"
   710 nitpick [expect = genuine]
   711 oops
   712 
   713 lemma "T2_rec c d (C x) = c x"
   714 nitpick [expect = none]
   715 apply simp
   716 done
   717 
   718 lemma "T2_rec c d (D x) = d x"
   719 nitpick [expect = none]
   720 apply simp
   721 done
   722 
   723 lemma "P (T2_rec c d x)"
   724 nitpick [expect = genuine]
   725 oops
   726 
   727 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
   728 nitpick [expect = genuine]
   729 oops
   730 
   731 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
   732 
   733 lemma "P (x\<Colon>('a, 'b) T3)"
   734 nitpick [expect = genuine]
   735 oops
   736 
   737 lemma "\<forall>x\<Colon>('a, 'b) T3. P x"
   738 nitpick [expect = genuine]
   739 oops
   740 
   741 lemma "P E"
   742 nitpick [expect = genuine]
   743 oops
   744 
   745 lemma "T3_rec e (E x) = e x"
   746 nitpick [card = 1\<midarrow>4, expect = none]
   747 apply simp
   748 done
   749 
   750 lemma "P (T3_rec e x)"
   751 nitpick [expect = genuine]
   752 oops
   753 
   754 lemma "P (case x of E f \<Rightarrow> e f)"
   755 nitpick [expect = genuine]
   756 oops
   757 
   758 text {* Recursive datatypes *}
   759 
   760 text {* nat *}
   761 
   762 lemma "P (x\<Colon>nat)"
   763 nitpick [expect = genuine]
   764 oops
   765 
   766 lemma "\<forall>x\<Colon>nat. P x"
   767 nitpick [expect = genuine]
   768 oops
   769 
   770 lemma "P (Suc 0)"
   771 nitpick [expect = genuine]
   772 oops
   773 
   774 lemma "P Suc"
   775 nitpick [card = 1\<midarrow>7, expect = none]
   776 oops
   777 
   778 lemma "nat_rec zero suc 0 = zero"
   779 nitpick [expect = none]
   780 apply simp
   781 done
   782 
   783 lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
   784 nitpick [expect = none]
   785 apply simp
   786 done
   787 
   788 lemma "P (nat_rec zero suc x)"
   789 nitpick [expect = genuine]
   790 oops
   791 
   792 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
   793 nitpick [expect = genuine]
   794 oops
   795 
   796 text {* 'a list *}
   797 
   798 lemma "P (xs\<Colon>'a list)"
   799 nitpick [expect = genuine]
   800 oops
   801 
   802 lemma "\<forall>xs\<Colon>'a list. P xs"
   803 nitpick [expect = genuine]
   804 oops
   805 
   806 lemma "P [x, y]"
   807 nitpick [expect = genuine]
   808 oops
   809 
   810 lemma "list_rec nil cons [] = nil"
   811 nitpick [card = 1\<midarrow>5, expect = none]
   812 apply simp
   813 done
   814 
   815 lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
   816 nitpick [card = 1\<midarrow>5, expect = none]
   817 apply simp
   818 done
   819 
   820 lemma "P (list_rec nil cons xs)"
   821 nitpick [expect = genuine]
   822 oops
   823 
   824 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
   825 nitpick [expect = genuine]
   826 oops
   827 
   828 lemma "(xs\<Colon>'a list) = ys"
   829 nitpick [expect = genuine]
   830 oops
   831 
   832 lemma "a # xs = b # xs"
   833 nitpick [expect = genuine]
   834 oops
   835 
   836 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
   837 
   838 lemma "P (x\<Colon>BitList)"
   839 nitpick [expect = genuine]
   840 oops
   841 
   842 lemma "\<forall>x\<Colon>BitList. P x"
   843 nitpick [expect = genuine]
   844 oops
   845 
   846 lemma "P (Bit0 (Bit1 BitListNil))"
   847 nitpick [expect = genuine]
   848 oops
   849 
   850 lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
   851 nitpick [expect = none]
   852 apply simp
   853 done
   854 
   855 lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
   856 nitpick [expect = none]
   857 apply simp
   858 done
   859 
   860 lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
   861 nitpick [expect = none]
   862 apply simp
   863 done
   864 
   865 lemma "P (BitList_rec nil bit0 bit1 x)"
   866 nitpick [expect = genuine]
   867 oops
   868 
   869 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   870 
   871 lemma "P (x\<Colon>'a BinTree)"
   872 nitpick [expect = genuine]
   873 oops
   874 
   875 lemma "\<forall>x\<Colon>'a BinTree. P x"
   876 nitpick [expect = genuine]
   877 oops
   878 
   879 lemma "P (Node (Leaf x) (Leaf y))"
   880 nitpick [expect = genuine]
   881 oops
   882 
   883 lemma "BinTree_rec l n (Leaf x) = l x"
   884 nitpick [expect = none]
   885 apply simp
   886 done
   887 
   888 lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
   889 nitpick [card = 1\<midarrow>5, expect = none]
   890 apply simp
   891 done
   892 
   893 lemma "P (BinTree_rec l n x)"
   894 nitpick [expect = genuine]
   895 oops
   896 
   897 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
   898 nitpick [expect = genuine]
   899 oops
   900 
   901 text {* Mutually recursive datatypes *}
   902 
   903 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   904  and 'a bexp = Equal "'a aexp" "'a aexp"
   905 
   906 lemma "P (x\<Colon>'a aexp)"
   907 nitpick [expect = genuine]
   908 oops
   909 
   910 lemma "\<forall>x\<Colon>'a aexp. P x"
   911 nitpick [expect = genuine]
   912 oops
   913 
   914 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
   915 nitpick [expect = genuine]
   916 oops
   917 
   918 lemma "P (x\<Colon>'a bexp)"
   919 nitpick [expect = genuine]
   920 oops
   921 
   922 lemma "\<forall>x\<Colon>'a bexp. P x"
   923 nitpick [expect = genuine]
   924 oops
   925 
   926 lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
   927 nitpick [card = 1\<midarrow>3, expect = none]
   928 apply simp
   929 done
   930 
   931 lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
   932 nitpick [card = 1\<midarrow>3, expect = none]
   933 apply simp
   934 done
   935 
   936 lemma "P (aexp_bexp_rec_1 number ite equal x)"
   937 nitpick [expect = genuine]
   938 oops
   939 
   940 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
   941 nitpick [expect = genuine]
   942 oops
   943 
   944 lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
   945 nitpick [card = 1\<midarrow>3, expect = none]
   946 apply simp
   947 done
   948 
   949 lemma "P (aexp_bexp_rec_2 number ite equal x)"
   950 nitpick [expect = genuine]
   951 oops
   952 
   953 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
   954 nitpick [expect = genuine]
   955 oops
   956 
   957 datatype X = A | B X | C Y
   958      and Y = D X | E Y | F
   959 
   960 lemma "P (x\<Colon>X)"
   961 nitpick [expect = genuine]
   962 oops
   963 
   964 lemma "P (y\<Colon>Y)"
   965 nitpick [expect = genuine]
   966 oops
   967 
   968 lemma "P (B (B A))"
   969 nitpick [expect = genuine]
   970 oops
   971 
   972 lemma "P (B (C F))"
   973 nitpick [expect = genuine]
   974 oops
   975 
   976 lemma "P (C (D A))"
   977 nitpick [expect = genuine]
   978 oops
   979 
   980 lemma "P (C (E F))"
   981 nitpick [expect = genuine]
   982 oops
   983 
   984 lemma "P (D (B A))"
   985 nitpick [expect = genuine]
   986 oops
   987 
   988 lemma "P (D (C F))"
   989 nitpick [expect = genuine]
   990 oops
   991 
   992 lemma "P (E (D A))"
   993 nitpick [expect = genuine]
   994 oops
   995 
   996 lemma "P (E (E F))"
   997 nitpick [expect = genuine]
   998 oops
   999 
  1000 lemma "P (C (D (C F)))"
  1001 nitpick [expect = genuine]
  1002 oops
  1003 
  1004 lemma "X_Y_rec_1 a b c d e f A = a"
  1005 nitpick [card = 1\<midarrow>5, expect = none]
  1006 apply simp
  1007 done
  1008 
  1009 lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
  1010 nitpick [card = 1\<midarrow>5, expect = none]
  1011 apply simp
  1012 done
  1013 
  1014 lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
  1015 nitpick [card = 1\<midarrow>5, expect = none]
  1016 apply simp
  1017 done
  1018 
  1019 lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
  1020 nitpick [card = 1\<midarrow>5, expect = none]
  1021 apply simp
  1022 done
  1023 
  1024 lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
  1025 nitpick [card = 1\<midarrow>5, expect = none]
  1026 apply simp
  1027 done
  1028 
  1029 lemma "X_Y_rec_2 a b c d e f F = f"
  1030 nitpick [card = 1\<midarrow>5, expect = none]
  1031 apply simp
  1032 done
  1033 
  1034 lemma "P (X_Y_rec_1 a b c d e f x)"
  1035 nitpick [expect = genuine]
  1036 oops
  1037 
  1038 lemma "P (X_Y_rec_2 a b c d e f y)"
  1039 nitpick [expect = genuine]
  1040 oops
  1041 
  1042 text {* Other datatype examples *}
  1043 
  1044 text {* Indirect recursion is implemented via mutual recursion. *}
  1045 
  1046 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  1047 
  1048 lemma "P (x\<Colon>XOpt)"
  1049 nitpick [expect = genuine]
  1050 oops
  1051 
  1052 lemma "P (CX None)"
  1053 nitpick [expect = genuine]
  1054 oops
  1055 
  1056 lemma "P (CX (Some (CX None)))"
  1057 nitpick [expect = genuine]
  1058 oops
  1059 
  1060 lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
  1061 nitpick [card = 1\<midarrow>5, expect = none]
  1062 apply simp
  1063 done
  1064 
  1065 lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
  1066 nitpick [card = 1\<midarrow>3, expect = none]
  1067 apply simp
  1068 done
  1069 
  1070 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
  1071 nitpick [card = 1\<midarrow>4, expect = none]
  1072 apply simp
  1073 done
  1074 
  1075 lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  1076 nitpick [card = 1\<midarrow>4, expect = none]
  1077 apply simp
  1078 done
  1079 
  1080 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
  1081 nitpick [card = 1\<midarrow>4, expect = none]
  1082 apply simp
  1083 done
  1084 
  1085 lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  1086 nitpick [card = 1\<midarrow>4, expect = none]
  1087 apply simp
  1088 done
  1089 
  1090 lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
  1091 nitpick [expect = genuine]
  1092 oops
  1093 
  1094 lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
  1095 nitpick [expect = genuine]
  1096 oops
  1097 
  1098 lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
  1099 nitpick [expect = genuine]
  1100 oops
  1101 
  1102 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  1103 
  1104 lemma "P (x\<Colon>'a YOpt)"
  1105 nitpick [expect = genuine]
  1106 oops
  1107 
  1108 lemma "P (CY None)"
  1109 nitpick [expect = genuine]
  1110 oops
  1111 
  1112 lemma "P (CY (Some (\<lambda>a. CY None)))"
  1113 nitpick [expect = genuine]
  1114 oops
  1115 
  1116 lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
  1117 nitpick [card = 1\<midarrow>2, expect = none]
  1118 apply simp
  1119 done
  1120 
  1121 lemma "YOpt_rec_2 cy n s None = n"
  1122 nitpick [card = 1\<midarrow>2, expect = none]
  1123 apply simp
  1124 done
  1125 
  1126 lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
  1127 nitpick [card = 1\<midarrow>2, expect = none]
  1128 apply simp
  1129 done
  1130 
  1131 lemma "P (YOpt_rec_1 cy n s x)"
  1132 nitpick [expect = genuine]
  1133 oops
  1134 
  1135 lemma "P (YOpt_rec_2 cy n s x)"
  1136 nitpick [expect = genuine]
  1137 oops
  1138 
  1139 datatype Trie = TR "Trie list"
  1140 
  1141 lemma "P (x\<Colon>Trie)"
  1142 nitpick [expect = genuine]
  1143 oops
  1144 
  1145 lemma "\<forall>x\<Colon>Trie. P x"
  1146 nitpick [expect = genuine]
  1147 oops
  1148 
  1149 lemma "P (TR [TR []])"
  1150 nitpick [expect = genuine]
  1151 oops
  1152 
  1153 lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
  1154 nitpick [card = 1\<midarrow>4, expect = none]
  1155 apply simp
  1156 done
  1157 
  1158 lemma "Trie_rec_2 tr nil cons [] = nil"
  1159 nitpick [card = 1\<midarrow>4, expect = none]
  1160 apply simp
  1161 done
  1162 
  1163 lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
  1164 nitpick [card = 1\<midarrow>4, expect = none]
  1165 apply simp
  1166 done
  1167 
  1168 lemma "P (Trie_rec_1 tr nil cons x)"
  1169 nitpick [card = 1, expect = genuine]
  1170 oops
  1171 
  1172 lemma "P (Trie_rec_2 tr nil cons x)"
  1173 nitpick [card = 1, expect = genuine]
  1174 oops
  1175 
  1176 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  1177 
  1178 lemma "P (x\<Colon>InfTree)"
  1179 nitpick [expect = genuine]
  1180 oops
  1181 
  1182 lemma "\<forall>x\<Colon>InfTree. P x"
  1183 nitpick [expect = genuine]
  1184 oops
  1185 
  1186 lemma "P (Node (\<lambda>n. Leaf))"
  1187 nitpick [expect = genuine]
  1188 oops
  1189 
  1190 lemma "InfTree_rec leaf node Leaf = leaf"
  1191 nitpick [card = 1\<midarrow>3, expect = none]
  1192 apply simp
  1193 done
  1194 
  1195 lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
  1196 nitpick [card = 1\<midarrow>3, expect = none]
  1197 apply simp
  1198 done
  1199 
  1200 lemma "P (InfTree_rec leaf node x)"
  1201 nitpick [expect = genuine]
  1202 oops
  1203 
  1204 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
  1205 
  1206 lemma "P (x\<Colon>'a lambda)"
  1207 nitpick [expect = genuine]
  1208 oops
  1209 
  1210 lemma "\<forall>x\<Colon>'a lambda. P x"
  1211 nitpick [expect = genuine]
  1212 oops
  1213 
  1214 lemma "P (Lam (\<lambda>a. Var a))"
  1215 nitpick [card = 1\<midarrow>5, expect = none]
  1216 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
  1217 oops
  1218 
  1219 lemma "lambda_rec var app lam (Var x) = var x"
  1220 nitpick [card = 1\<midarrow>3, expect = none]
  1221 apply simp
  1222 done
  1223 
  1224 lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
  1225 nitpick [card = 1\<midarrow>3, expect = none]
  1226 apply simp
  1227 done
  1228 
  1229 lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
  1230 nitpick [card = 1\<midarrow>3, expect = none]
  1231 apply simp
  1232 done
  1233 
  1234 lemma "P (lambda_rec v a l x)"
  1235 nitpick [expect = genuine]
  1236 oops
  1237 
  1238 text {* Taken from "Inductive datatypes in HOL", p. 8: *}
  1239 
  1240 datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
  1241 datatype 'c U = E "('c, 'c U) T"
  1242 
  1243 lemma "P (x\<Colon>'c U)"
  1244 nitpick [expect = genuine]
  1245 oops
  1246 
  1247 lemma "\<forall>x\<Colon>'c U. P x"
  1248 nitpick [expect = genuine]
  1249 oops
  1250 
  1251 lemma "P (E (C (\<lambda>a. True)))"
  1252 nitpick [expect = genuine]
  1253 oops
  1254 
  1255 lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
  1256 nitpick [card = 1\<midarrow>3, expect = none]
  1257 apply simp
  1258 done
  1259 
  1260 lemma "U_rec_2 e c d nil cons (C x) = c x"
  1261 nitpick [card = 1\<midarrow>3, expect = none]
  1262 apply simp
  1263 done
  1264 
  1265 lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
  1266 nitpick [card = 1\<midarrow>3, expect = none]
  1267 apply simp
  1268 done
  1269 
  1270 lemma "U_rec_3 e c d nil cons [] = nil"
  1271 nitpick [card = 1\<midarrow>3, expect = none]
  1272 apply simp
  1273 done
  1274 
  1275 lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
  1276 nitpick [card = 1\<midarrow>3, expect = none]
  1277 apply simp
  1278 done
  1279 
  1280 lemma "P (U_rec_1 e c d nil cons x)"
  1281 nitpick [expect = genuine]
  1282 oops
  1283 
  1284 lemma "P (U_rec_2 e c d nil cons x)"
  1285 nitpick [card = 1, expect = genuine]
  1286 oops
  1287 
  1288 lemma "P (U_rec_3 e c d nil cons x)"
  1289 nitpick [card = 1, expect = genuine]
  1290 oops
  1291 
  1292 subsubsection {* Records *}
  1293 
  1294 record ('a, 'b) point =
  1295   xpos :: 'a
  1296   ypos :: 'b
  1297 
  1298 lemma "(x\<Colon>('a, 'b) point) = y"
  1299 nitpick [expect = genuine]
  1300 oops
  1301 
  1302 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
  1303   ext :: 'c
  1304 
  1305 lemma "(x\<Colon>('a, 'b, 'c) extpoint) = y"
  1306 nitpick [expect = genuine]
  1307 oops
  1308 
  1309 subsubsection {* Inductively Defined Sets *}
  1310 
  1311 inductive_set undefinedSet :: "'a set" where
  1312 "undefined \<in> undefinedSet"
  1313 
  1314 lemma "x \<in> undefinedSet"
  1315 nitpick [expect = genuine]
  1316 oops
  1317 
  1318 inductive_set evenCard :: "'a set set"
  1319 where
  1320 "{} \<in> evenCard" |
  1321 "\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
  1322 
  1323 lemma "S \<in> evenCard"
  1324 nitpick [expect = genuine]
  1325 oops
  1326 
  1327 inductive_set
  1328 even :: "nat set"
  1329 and odd :: "nat set"
  1330 where
  1331 "0 \<in> even" |
  1332 "n \<in> even \<Longrightarrow> Suc n \<in> odd" |
  1333 "n \<in> odd \<Longrightarrow> Suc n \<in> even"
  1334 
  1335 lemma "n \<in> odd"
  1336 nitpick [expect = genuine]
  1337 oops
  1338 
  1339 consts f :: "'a \<Rightarrow> 'a"
  1340 
  1341 inductive_set a_even :: "'a set" and a_odd :: "'a set" where
  1342 "undefined \<in> a_even" |
  1343 "x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
  1344 "x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
  1345 
  1346 lemma "x \<in> a_odd"
  1347 nitpick [expect = genuine]
  1348 oops
  1349 
  1350 subsubsection {* Examples Involving Special Functions *}
  1351 
  1352 lemma "card x = 0"
  1353 nitpick [expect = genuine]
  1354 oops
  1355 
  1356 lemma "finite x"
  1357 nitpick [expect = none]
  1358 oops
  1359 
  1360 lemma "xs @ [] = ys @ []"
  1361 nitpick [expect = genuine]
  1362 oops
  1363 
  1364 lemma "xs @ ys = ys @ xs"
  1365 nitpick [expect = genuine]
  1366 oops
  1367 
  1368 lemma "f (lfp f) = lfp f"
  1369 nitpick [card = 2, expect = genuine]
  1370 oops
  1371 
  1372 lemma "f (gfp f) = gfp f"
  1373 nitpick [card = 2, expect = genuine]
  1374 oops
  1375 
  1376 lemma "lfp f = gfp f"
  1377 nitpick [card = 2, expect = genuine]
  1378 oops
  1379 
  1380 subsubsection {* Axiomatic Type Classes and Overloading *}
  1381 
  1382 text {* A type class without axioms: *}
  1383 
  1384 axclass classA
  1385 
  1386 lemma "P (x\<Colon>'a\<Colon>classA)"
  1387 nitpick [expect = genuine]
  1388 oops
  1389 
  1390 text {* The axiom of this type class does not contain any type variables: *}
  1391 
  1392 axclass classB
  1393 classB_ax: "P \<or> \<not> P"
  1394 
  1395 lemma "P (x\<Colon>'a\<Colon>classB)"
  1396 nitpick [expect = genuine]
  1397 oops
  1398 
  1399 text {* An axiom with a type variable (denoting types which have at least two elements): *}
  1400 
  1401 axclass classC < type
  1402 classC_ax: "\<exists>x y. x \<noteq> y"
  1403 
  1404 lemma "P (x\<Colon>'a\<Colon>classC)"
  1405 nitpick [expect = genuine]
  1406 oops
  1407 
  1408 lemma "\<exists>x y. (x\<Colon>'a\<Colon>classC) \<noteq> y"
  1409 nitpick [expect = none]
  1410 sorry
  1411 
  1412 text {* A type class for which a constant is defined: *}
  1413 
  1414 consts
  1415 classD_const :: "'a \<Rightarrow> 'a"
  1416 
  1417 axclass classD < type
  1418 classD_ax: "classD_const (classD_const x) = classD_const x"
  1419 
  1420 lemma "P (x\<Colon>'a\<Colon>classD)"
  1421 nitpick [expect = genuine]
  1422 oops
  1423 
  1424 text {* A type class with multiple superclasses: *}
  1425 
  1426 axclass classE < classC, classD
  1427 
  1428 lemma "P (x\<Colon>'a\<Colon>classE)"
  1429 nitpick [expect = genuine]
  1430 oops
  1431 
  1432 lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
  1433 nitpick [expect = genuine]
  1434 oops
  1435 
  1436 text {* OFCLASS: *}
  1437 
  1438 lemma "OFCLASS('a\<Colon>type, type_class)"
  1439 nitpick [expect = none]
  1440 apply intro_classes
  1441 done
  1442 
  1443 lemma "OFCLASS('a\<Colon>classC, type_class)"
  1444 nitpick [expect = none]
  1445 apply intro_classes
  1446 done
  1447 
  1448 lemma "OFCLASS('a, classB_class)"
  1449 nitpick [expect = none]
  1450 apply intro_classes
  1451 apply simp
  1452 done
  1453 
  1454 lemma "OFCLASS('a\<Colon>type, classC_class)"
  1455 nitpick [expect = genuine]
  1456 oops
  1457 
  1458 text {* Overloading: *}
  1459 
  1460 consts inverse :: "'a \<Rightarrow> 'a"
  1461 
  1462 defs (overloaded)
  1463 inverse_bool: "inverse (b\<Colon>bool) \<equiv> \<not> b"
  1464 inverse_set: "inverse (S\<Colon>'a set) \<equiv> -S"
  1465 inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
  1466 
  1467 lemma "inverse b"
  1468 nitpick [expect = genuine]
  1469 oops
  1470 
  1471 lemma "P (inverse (S\<Colon>'a set))"
  1472 nitpick [expect = genuine]
  1473 oops
  1474 
  1475 lemma "P (inverse (p\<Colon>'a\<times>'b))"
  1476 nitpick [expect = genuine]
  1477 oops
  1478 
  1479 end