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