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