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