src/HOL/Nitpick_Examples/Refute_Nits.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 61337 4645502c3c64
child 63167 0909deb8059b
permissions -rw-r--r--
eliminated old defs;
     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 section {* Refute Examples Adapted to Nitpick *}
     9 
    10 theory Refute_Nits
    11 imports Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 1-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::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::'a\<Rightarrow>'b) = g"
   100 nitpick [expect = genuine]
   101 oops
   102 
   103 lemma "(f::('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::('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-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> Pure.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_goal "?P"
   344 nitpick [expect = none]
   345 apply auto
   346 done
   347 
   348 schematic_goal "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::'a set)"
   371 nitpick [expect = genuine]
   372 oops
   373 
   374 lemma "P (A::'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::nat) + y = 0"
   477 nitpick [expect = genuine]
   478 oops
   479 
   480 lemma "(x::nat) = x + x"
   481 nitpick [expect = genuine]
   482 oops
   483 
   484 lemma "(x::nat) - y + y = x"
   485 nitpick [expect = genuine]
   486 oops
   487 
   488 lemma "(x::nat) = x * x"
   489 nitpick [expect = genuine]
   490 oops
   491 
   492 lemma "(x::nat) < x + y"
   493 nitpick [card = 1, expect = genuine]
   494 oops
   495 
   496 text {* \<times> *}
   497 
   498 lemma "P (x::'a\<times>'b)"
   499 nitpick [expect = genuine]
   500 oops
   501 
   502 lemma "\<forall>x::'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 "P (case x of Pair a b \<Rightarrow> f a b)"
   523 nitpick [expect = genuine]
   524 oops
   525 
   526 subsubsection {* Subtypes (typedef), typedecl *}
   527 
   528 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
   529 
   530 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
   531 
   532 typedef 'a myTdef = "myTdef :: 'a set"
   533 unfolding myTdef_def by auto
   534 
   535 lemma "(x::'a myTdef) = y"
   536 nitpick [expect = genuine]
   537 oops
   538 
   539 typedecl myTdecl
   540 
   541 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   542 
   543 typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   544 unfolding T_bij_def by auto
   545 
   546 lemma "P (f::(myTdecl myTdef) T_bij)"
   547 nitpick [expect = genuine]
   548 oops
   549 
   550 subsubsection {* Inductive Datatypes *}
   551 
   552 text {* unit *}
   553 
   554 lemma "P (x::unit)"
   555 nitpick [expect = genuine]
   556 oops
   557 
   558 lemma "\<forall>x::unit. P x"
   559 nitpick [expect = genuine]
   560 oops
   561 
   562 lemma "P ()"
   563 nitpick [expect = genuine]
   564 oops
   565 
   566 lemma "P (case x of () \<Rightarrow> u)"
   567 nitpick [expect = genuine]
   568 oops
   569 
   570 text {* option *}
   571 
   572 lemma "P (x::'a option)"
   573 nitpick [expect = genuine]
   574 oops
   575 
   576 lemma "\<forall>x::'a option. P x"
   577 nitpick [expect = genuine]
   578 oops
   579 
   580 lemma "P None"
   581 nitpick [expect = genuine]
   582 oops
   583 
   584 lemma "P (Some x)"
   585 nitpick [expect = genuine]
   586 oops
   587 
   588 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
   589 nitpick [expect = genuine]
   590 oops
   591 
   592 text {* + *}
   593 
   594 lemma "P (x::'a+'b)"
   595 nitpick [expect = genuine]
   596 oops
   597 
   598 lemma "\<forall>x::'a+'b. P x"
   599 nitpick [expect = genuine]
   600 oops
   601 
   602 lemma "P (Inl x)"
   603 nitpick [expect = genuine]
   604 oops
   605 
   606 lemma "P (Inr x)"
   607 nitpick [expect = genuine]
   608 oops
   609 
   610 lemma "P Inl"
   611 nitpick [expect = genuine]
   612 oops
   613 
   614 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
   615 nitpick [expect = genuine]
   616 oops
   617 
   618 text {* Non-recursive datatypes *}
   619 
   620 datatype T1 = A | B
   621 
   622 lemma "P (x::T1)"
   623 nitpick [expect = genuine]
   624 oops
   625 
   626 lemma "\<forall>x::T1. P x"
   627 nitpick [expect = genuine]
   628 oops
   629 
   630 lemma "P A"
   631 nitpick [expect = genuine]
   632 oops
   633 
   634 lemma "P B"
   635 nitpick [expect = genuine]
   636 oops
   637 
   638 lemma "rec_T1 a b A = a"
   639 nitpick [expect = none]
   640 apply simp
   641 done
   642 
   643 lemma "rec_T1 a b B = b"
   644 nitpick [expect = none]
   645 apply simp
   646 done
   647 
   648 lemma "P (rec_T1 a b x)"
   649 nitpick [expect = genuine]
   650 oops
   651 
   652 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
   653 nitpick [expect = genuine]
   654 oops
   655 
   656 datatype 'a T2 = C T1 | D 'a
   657 
   658 lemma "P (x::'a T2)"
   659 nitpick [expect = genuine]
   660 oops
   661 
   662 lemma "\<forall>x::'a T2. P x"
   663 nitpick [expect = genuine]
   664 oops
   665 
   666 lemma "P D"
   667 nitpick [expect = genuine]
   668 oops
   669 
   670 lemma "rec_T2 c d (C x) = c x"
   671 nitpick [expect = none]
   672 apply simp
   673 done
   674 
   675 lemma "rec_T2 c d (D x) = d x"
   676 nitpick [expect = none]
   677 apply simp
   678 done
   679 
   680 lemma "P (rec_T2 c d x)"
   681 nitpick [expect = genuine]
   682 oops
   683 
   684 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
   685 nitpick [expect = genuine]
   686 oops
   687 
   688 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
   689 
   690 lemma "P (x::('a, 'b) T3)"
   691 nitpick [expect = genuine]
   692 oops
   693 
   694 lemma "\<forall>x::('a, 'b) T3. P x"
   695 nitpick [expect = genuine]
   696 oops
   697 
   698 lemma "P E"
   699 nitpick [expect = genuine]
   700 oops
   701 
   702 lemma "rec_T3 e (E x) = e x"
   703 nitpick [card = 1-4, expect = none]
   704 apply simp
   705 done
   706 
   707 lemma "P (rec_T3 e x)"
   708 nitpick [expect = genuine]
   709 oops
   710 
   711 lemma "P (case x of E f \<Rightarrow> e f)"
   712 nitpick [expect = genuine]
   713 oops
   714 
   715 text {* Recursive datatypes *}
   716 
   717 text {* nat *}
   718 
   719 lemma "P (x::nat)"
   720 nitpick [expect = genuine]
   721 oops
   722 
   723 lemma "\<forall>x::nat. P x"
   724 nitpick [expect = genuine]
   725 oops
   726 
   727 lemma "P (Suc 0)"
   728 nitpick [expect = genuine]
   729 oops
   730 
   731 lemma "P Suc"
   732 nitpick [card = 1-7, expect = none]
   733 oops
   734 
   735 lemma "rec_nat zero suc 0 = zero"
   736 nitpick [expect = none]
   737 apply simp
   738 done
   739 
   740 lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
   741 nitpick [expect = none]
   742 apply simp
   743 done
   744 
   745 lemma "P (rec_nat zero suc x)"
   746 nitpick [expect = genuine]
   747 oops
   748 
   749 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
   750 nitpick [expect = genuine]
   751 oops
   752 
   753 text {* 'a list *}
   754 
   755 lemma "P (xs::'a list)"
   756 nitpick [expect = genuine]
   757 oops
   758 
   759 lemma "\<forall>xs::'a list. P xs"
   760 nitpick [expect = genuine]
   761 oops
   762 
   763 lemma "P [x, y]"
   764 nitpick [expect = genuine]
   765 oops
   766 
   767 lemma "rec_list nil cons [] = nil"
   768 nitpick [card = 1-5, expect = none]
   769 apply simp
   770 done
   771 
   772 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
   773 nitpick [card = 1-5, expect = none]
   774 apply simp
   775 done
   776 
   777 lemma "P (rec_list nil cons xs)"
   778 nitpick [expect = genuine]
   779 oops
   780 
   781 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
   782 nitpick [expect = genuine]
   783 oops
   784 
   785 lemma "(xs::'a list) = ys"
   786 nitpick [expect = genuine]
   787 oops
   788 
   789 lemma "a # xs = b # xs"
   790 nitpick [expect = genuine]
   791 oops
   792 
   793 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
   794 
   795 lemma "P (x::BitList)"
   796 nitpick [expect = genuine]
   797 oops
   798 
   799 lemma "\<forall>x::BitList. P x"
   800 nitpick [expect = genuine]
   801 oops
   802 
   803 lemma "P (Bit0 (Bit1 BitListNil))"
   804 nitpick [expect = genuine]
   805 oops
   806 
   807 lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
   808 nitpick [expect = none]
   809 apply simp
   810 done
   811 
   812 lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
   813 nitpick [expect = none]
   814 apply simp
   815 done
   816 
   817 lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
   818 nitpick [expect = none]
   819 apply simp
   820 done
   821 
   822 lemma "P (rec_BitList nil bit0 bit1 x)"
   823 nitpick [expect = genuine]
   824 oops
   825 
   826 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   827 
   828 lemma "P (x::'a BinTree)"
   829 nitpick [expect = genuine]
   830 oops
   831 
   832 lemma "\<forall>x::'a BinTree. P x"
   833 nitpick [expect = genuine]
   834 oops
   835 
   836 lemma "P (Node (Leaf x) (Leaf y))"
   837 nitpick [expect = genuine]
   838 oops
   839 
   840 lemma "rec_BinTree l n (Leaf x) = l x"
   841 nitpick [expect = none]
   842 apply simp
   843 done
   844 
   845 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
   846 nitpick [card = 1-5, expect = none]
   847 apply simp
   848 done
   849 
   850 lemma "P (rec_BinTree l n x)"
   851 nitpick [expect = genuine]
   852 oops
   853 
   854 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
   855 nitpick [expect = genuine]
   856 oops
   857 
   858 text {* Mutually recursive datatypes *}
   859 
   860 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   861  and 'a bexp = Equal "'a aexp" "'a aexp"
   862 
   863 lemma "P (x::'a aexp)"
   864 nitpick [expect = genuine]
   865 oops
   866 
   867 lemma "\<forall>x::'a aexp. P x"
   868 nitpick [expect = genuine]
   869 oops
   870 
   871 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
   872 nitpick [expect = genuine]
   873 oops
   874 
   875 lemma "P (x::'a bexp)"
   876 nitpick [expect = genuine]
   877 oops
   878 
   879 lemma "\<forall>x::'a bexp. P x"
   880 nitpick [expect = genuine]
   881 oops
   882 
   883 lemma "rec_aexp number ite equal (Number x) = number x"
   884 nitpick [card = 1-3, expect = none]
   885 apply simp
   886 done
   887 
   888 lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
   889 nitpick [card = 1-3, expect = none]
   890 apply simp
   891 done
   892 
   893 lemma "P (rec_aexp number ite equal x)"
   894 nitpick [expect = genuine]
   895 oops
   896 
   897 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
   898 nitpick [expect = genuine]
   899 oops
   900 
   901 lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
   902 nitpick [card = 1-3, expect = none]
   903 apply simp
   904 done
   905 
   906 lemma "P (rec_bexp number ite equal x)"
   907 nitpick [expect = genuine]
   908 oops
   909 
   910 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
   911 nitpick [expect = genuine]
   912 oops
   913 
   914 datatype X = A | B X | C Y and Y = D X | E Y | F
   915 
   916 lemma "P (x::X)"
   917 nitpick [expect = genuine]
   918 oops
   919 
   920 lemma "P (y::Y)"
   921 nitpick [expect = genuine]
   922 oops
   923 
   924 lemma "P (B (B A))"
   925 nitpick [expect = genuine]
   926 oops
   927 
   928 lemma "P (B (C F))"
   929 nitpick [expect = genuine]
   930 oops
   931 
   932 lemma "P (C (D A))"
   933 nitpick [expect = genuine]
   934 oops
   935 
   936 lemma "P (C (E F))"
   937 nitpick [expect = genuine]
   938 oops
   939 
   940 lemma "P (D (B A))"
   941 nitpick [expect = genuine]
   942 oops
   943 
   944 lemma "P (D (C F))"
   945 nitpick [expect = genuine]
   946 oops
   947 
   948 lemma "P (E (D A))"
   949 nitpick [expect = genuine]
   950 oops
   951 
   952 lemma "P (E (E F))"
   953 nitpick [expect = genuine]
   954 oops
   955 
   956 lemma "P (C (D (C F)))"
   957 nitpick [expect = genuine]
   958 oops
   959 
   960 lemma "rec_X a b c d e f A = a"
   961 nitpick [card = 1-5, expect = none]
   962 apply simp
   963 done
   964 
   965 lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
   966 nitpick [card = 1-5, expect = none]
   967 apply simp
   968 done
   969 
   970 lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
   971 nitpick [card = 1-5, expect = none]
   972 apply simp
   973 done
   974 
   975 lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
   976 nitpick [card = 1-5, expect = none]
   977 apply simp
   978 done
   979 
   980 lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
   981 nitpick [card = 1-5, expect = none]
   982 apply simp
   983 done
   984 
   985 lemma "rec_Y a b c d e f F = f"
   986 nitpick [card = 1-5, expect = none]
   987 apply simp
   988 done
   989 
   990 lemma "P (rec_X a b c d e f x)"
   991 nitpick [expect = genuine]
   992 oops
   993 
   994 lemma "P (rec_Y a b c d e f y)"
   995 nitpick [expect = genuine]
   996 oops
   997 
   998 text {* Other datatype examples *}
   999 
  1000 text {* Indirect recursion is implemented via mutual recursion. *}
  1001 
  1002 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
  1003 
  1004 lemma "P (x::XOpt)"
  1005 nitpick [expect = genuine]
  1006 oops
  1007 
  1008 lemma "P (CX None)"
  1009 nitpick [expect = genuine]
  1010 oops
  1011 
  1012 lemma "P (CX (Some (CX None)))"
  1013 nitpick [expect = genuine]
  1014 oops
  1015 
  1016 lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
  1017 nitpick [expect = genuine]
  1018 oops
  1019 
  1020 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  1021 
  1022 lemma "P (x::'a YOpt)"
  1023 nitpick [expect = genuine]
  1024 oops
  1025 
  1026 lemma "P (CY None)"
  1027 nitpick [expect = genuine]
  1028 oops
  1029 
  1030 lemma "P (CY (Some (\<lambda>a. CY None)))"
  1031 nitpick [expect = genuine]
  1032 oops
  1033 
  1034 datatype Trie = TR "Trie list"
  1035 
  1036 lemma "P (x::Trie)"
  1037 nitpick [expect = genuine]
  1038 oops
  1039 
  1040 lemma "\<forall>x::Trie. P x"
  1041 nitpick [expect = genuine]
  1042 oops
  1043 
  1044 lemma "P (TR [TR []])"
  1045 nitpick [expect = genuine]
  1046 oops
  1047 
  1048 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  1049 
  1050 lemma "P (x::InfTree)"
  1051 nitpick [expect = genuine]
  1052 oops
  1053 
  1054 lemma "\<forall>x::InfTree. P x"
  1055 nitpick [expect = genuine]
  1056 oops
  1057 
  1058 lemma "P (Node (\<lambda>n. Leaf))"
  1059 nitpick [expect = genuine]
  1060 oops
  1061 
  1062 lemma "rec_InfTree leaf node Leaf = leaf"
  1063 nitpick [card = 1-3, expect = none]
  1064 apply simp
  1065 done
  1066 
  1067 lemma "rec_InfTree leaf node (Node g) = node ((\<lambda>InfTree. (InfTree, rec_InfTree leaf node InfTree)) \<circ> g)"
  1068 nitpick [card = 1-3, expect = none]
  1069 apply simp
  1070 done
  1071 
  1072 lemma "P (rec_InfTree leaf node x)"
  1073 nitpick [expect = genuine]
  1074 oops
  1075 
  1076 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
  1077 
  1078 lemma "P (x::'a lambda)"
  1079 nitpick [expect = genuine]
  1080 oops
  1081 
  1082 lemma "\<forall>x::'a lambda. P x"
  1083 nitpick [expect = genuine]
  1084 oops
  1085 
  1086 lemma "P (Lam (\<lambda>a. Var a))"
  1087 nitpick [card = 1-5, expect = none]
  1088 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
  1089 oops
  1090 
  1091 lemma "rec_lambda var app lam (Var x) = var x"
  1092 nitpick [card = 1-3, expect = none]
  1093 apply simp
  1094 done
  1095 
  1096 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
  1097 nitpick [card = 1-3, expect = none]
  1098 apply simp
  1099 done
  1100 
  1101 lemma "rec_lambda var app lam (Lam x) = lam ((\<lambda>lambda. (lambda, rec_lambda var app lam lambda)) \<circ> x)"
  1102 nitpick [card = 1-3, expect = none]
  1103 apply simp
  1104 done
  1105 
  1106 lemma "P (rec_lambda v a l x)"
  1107 nitpick [expect = genuine]
  1108 oops
  1109 
  1110 text {* Taken from "Inductive datatypes in HOL", p. 8: *}
  1111 
  1112 datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
  1113 datatype 'c U = E "('c, 'c U) T"
  1114 
  1115 lemma "P (x::'c U)"
  1116 nitpick [expect = genuine]
  1117 oops
  1118 
  1119 lemma "\<forall>x::'c U. P x"
  1120 nitpick [expect = genuine]
  1121 oops
  1122 
  1123 lemma "P (E (C (\<lambda>a. True)))"
  1124 nitpick [expect = genuine]
  1125 oops
  1126 
  1127 subsubsection {* Records *}
  1128 
  1129 record ('a, 'b) point =
  1130   xpos :: 'a
  1131   ypos :: 'b
  1132 
  1133 lemma "(x::('a, 'b) point) = y"
  1134 nitpick [expect = genuine]
  1135 oops
  1136 
  1137 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
  1138   ext :: 'c
  1139 
  1140 lemma "(x::('a, 'b, 'c) extpoint) = y"
  1141 nitpick [expect = genuine]
  1142 oops
  1143 
  1144 subsubsection {* Inductively Defined Sets *}
  1145 
  1146 inductive_set undefinedSet :: "'a set" where
  1147 "undefined \<in> undefinedSet"
  1148 
  1149 lemma "x \<in> undefinedSet"
  1150 nitpick [expect = genuine]
  1151 oops
  1152 
  1153 inductive_set evenCard :: "'a set set"
  1154 where
  1155 "{} \<in> evenCard" |
  1156 "\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
  1157 
  1158 lemma "S \<in> evenCard"
  1159 nitpick [expect = genuine]
  1160 oops
  1161 
  1162 inductive_set
  1163 even :: "nat set"
  1164 and odd :: "nat set"
  1165 where
  1166 "0 \<in> even" |
  1167 "n \<in> even \<Longrightarrow> Suc n \<in> odd" |
  1168 "n \<in> odd \<Longrightarrow> Suc n \<in> even"
  1169 
  1170 lemma "n \<in> odd"
  1171 nitpick [expect = genuine]
  1172 oops
  1173 
  1174 consts f :: "'a \<Rightarrow> 'a"
  1175 
  1176 inductive_set a_even :: "'a set" and a_odd :: "'a set" where
  1177 "undefined \<in> a_even" |
  1178 "x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
  1179 "x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
  1180 
  1181 lemma "x \<in> a_odd"
  1182 nitpick [expect = genuine]
  1183 oops
  1184 
  1185 subsubsection {* Examples Involving Special Functions *}
  1186 
  1187 lemma "card x = 0"
  1188 nitpick [expect = genuine]
  1189 oops
  1190 
  1191 lemma "finite x"
  1192 nitpick [expect = none]
  1193 oops
  1194 
  1195 lemma "xs @ [] = ys @ []"
  1196 nitpick [expect = genuine]
  1197 oops
  1198 
  1199 lemma "xs @ ys = ys @ xs"
  1200 nitpick [expect = genuine]
  1201 oops
  1202 
  1203 lemma "f (lfp f) = lfp f"
  1204 nitpick [card = 2, expect = genuine]
  1205 oops
  1206 
  1207 lemma "f (gfp f) = gfp f"
  1208 nitpick [card = 2, expect = genuine]
  1209 oops
  1210 
  1211 lemma "lfp f = gfp f"
  1212 nitpick [card = 2, expect = genuine]
  1213 oops
  1214 
  1215 subsubsection {* Axiomatic Type Classes and Overloading *}
  1216 
  1217 text {* A type class without axioms: *}
  1218 
  1219 class classA
  1220 
  1221 lemma "P (x::'a::classA)"
  1222 nitpick [expect = genuine]
  1223 oops
  1224 
  1225 text {* An axiom with a type variable (denoting types which have at least two elements): *}
  1226 
  1227 class classC =
  1228   assumes classC_ax: "\<exists>x y. x \<noteq> y"
  1229 
  1230 lemma "P (x::'a::classC)"
  1231 nitpick [expect = genuine]
  1232 oops
  1233 
  1234 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
  1235 nitpick [expect = none]
  1236 sorry
  1237 
  1238 text {* A type class for which a constant is defined: *}
  1239 
  1240 class classD =
  1241   fixes classD_const :: "'a \<Rightarrow> 'a"
  1242   assumes classD_ax: "classD_const (classD_const x) = classD_const x"
  1243 
  1244 lemma "P (x::'a::classD)"
  1245 nitpick [expect = genuine]
  1246 oops
  1247 
  1248 text {* A type class with multiple superclasses: *}
  1249 
  1250 class classE = classC + classD
  1251 
  1252 lemma "P (x::'a::classE)"
  1253 nitpick [expect = genuine]
  1254 oops
  1255 
  1256 text {* OFCLASS: *}
  1257 
  1258 lemma "OFCLASS('a::type, type_class)"
  1259 nitpick [expect = none]
  1260 apply intro_classes
  1261 done
  1262 
  1263 lemma "OFCLASS('a::classC, type_class)"
  1264 nitpick [expect = none]
  1265 apply intro_classes
  1266 done
  1267 
  1268 lemma "OFCLASS('a::type, classC_class)"
  1269 nitpick [expect = genuine]
  1270 oops
  1271 
  1272 text {* Overloading: *}
  1273 
  1274 consts inverse :: "'a \<Rightarrow> 'a"
  1275 
  1276 overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
  1277 begin
  1278   definition "inverse (b::bool) \<equiv> \<not> b"
  1279 end
  1280 
  1281 overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
  1282 begin
  1283   definition "inverse (S::'a set) \<equiv> -S"
  1284 end
  1285 
  1286 overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
  1287 begin
  1288   definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
  1289 end
  1290 
  1291 lemma "inverse b"
  1292 nitpick [expect = genuine]
  1293 oops
  1294 
  1295 lemma "P (inverse (S::'a set))"
  1296 nitpick [expect = genuine]
  1297 oops
  1298 
  1299 lemma "P (inverse (p::'a\<times>'b))"
  1300 nitpick [expect = genuine]
  1301 oops
  1302 
  1303 end