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