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