src/HOL/ex/Refute_Examples.thy
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 55867 79b915f26533
child 56815 848d507584db
permissions -rw-r--r--
more qualified names;
     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 == Pure.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 "P (case x of () \<Rightarrow> u)"
   529 refute [expect = genuine]
   530 oops
   531 
   532 text {* option *}
   533 
   534 lemma "P (x::'a option)"
   535 refute [expect = genuine]
   536 oops
   537 
   538 lemma "\<forall>x::'a option. P x"
   539 refute [expect = genuine]
   540 oops
   541 
   542 lemma "P None"
   543 refute [expect = genuine]
   544 oops
   545 
   546 lemma "P (Some x)"
   547 refute [expect = genuine]
   548 oops
   549 
   550 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
   551 refute [expect = genuine]
   552 oops
   553 
   554 text {* * *}
   555 
   556 lemma "P (x::'a*'b)"
   557 refute [expect = genuine]
   558 oops
   559 
   560 lemma "\<forall>x::'a*'b. P x"
   561 refute [expect = genuine]
   562 oops
   563 
   564 lemma "P (x, y)"
   565 refute [expect = genuine]
   566 oops
   567 
   568 lemma "P (fst x)"
   569 refute [expect = genuine]
   570 oops
   571 
   572 lemma "P (snd x)"
   573 refute [expect = genuine]
   574 oops
   575 
   576 lemma "P Pair"
   577 refute [expect = genuine]
   578 oops
   579 
   580 lemma "P (case x of Pair a b \<Rightarrow> p a b)"
   581 refute [expect = genuine]
   582 oops
   583 
   584 text {* + *}
   585 
   586 lemma "P (x::'a+'b)"
   587 refute [expect = genuine]
   588 oops
   589 
   590 lemma "\<forall>x::'a+'b. P x"
   591 refute [expect = genuine]
   592 oops
   593 
   594 lemma "P (Inl x)"
   595 refute [expect = genuine]
   596 oops
   597 
   598 lemma "P (Inr x)"
   599 refute [expect = genuine]
   600 oops
   601 
   602 lemma "P Inl"
   603 refute [expect = genuine]
   604 oops
   605 
   606 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
   607 refute [expect = genuine]
   608 oops
   609 
   610 text {* Non-recursive datatypes *}
   611 
   612 datatype T1 = A | B
   613 
   614 lemma "P (x::T1)"
   615 refute [expect = genuine]
   616 oops
   617 
   618 lemma "\<forall>x::T1. P x"
   619 refute [expect = genuine]
   620 oops
   621 
   622 lemma "P A"
   623 refute [expect = genuine]
   624 oops
   625 
   626 lemma "P B"
   627 refute [expect = genuine]
   628 oops
   629 
   630 lemma "rec_T1 a b A = a"
   631 refute [expect = none]
   632 by simp
   633 
   634 lemma "rec_T1 a b B = b"
   635 refute [expect = none]
   636 by simp
   637 
   638 lemma "P (rec_T1 a b x)"
   639 refute [expect = genuine]
   640 oops
   641 
   642 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
   643 refute [expect = genuine]
   644 oops
   645 
   646 datatype 'a T2 = C T1 | D 'a
   647 
   648 lemma "P (x::'a T2)"
   649 refute [expect = genuine]
   650 oops
   651 
   652 lemma "\<forall>x::'a T2. P x"
   653 refute [expect = genuine]
   654 oops
   655 
   656 lemma "P D"
   657 refute [expect = genuine]
   658 oops
   659 
   660 lemma "rec_T2 c d (C x) = c x"
   661 refute [maxsize = 4, expect = none]
   662 by simp
   663 
   664 lemma "rec_T2 c d (D x) = d x"
   665 refute [maxsize = 4, expect = none]
   666 by simp
   667 
   668 lemma "P (rec_T2 c d x)"
   669 refute [expect = genuine]
   670 oops
   671 
   672 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
   673 refute [expect = genuine]
   674 oops
   675 
   676 datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
   677 
   678 lemma "P (x::('a,'b) T3)"
   679 refute [expect = genuine]
   680 oops
   681 
   682 lemma "\<forall>x::('a,'b) T3. P x"
   683 refute [expect = genuine]
   684 oops
   685 
   686 lemma "P E"
   687 refute [expect = genuine]
   688 oops
   689 
   690 lemma "rec_T3 e (E x) = e x"
   691 refute [maxsize = 2, expect = none]
   692 by simp
   693 
   694 lemma "P (rec_T3 e x)"
   695 refute [expect = genuine]
   696 oops
   697 
   698 lemma "P (case x of E f \<Rightarrow> e f)"
   699 refute [expect = genuine]
   700 oops
   701 
   702 text {* Recursive datatypes *}
   703 
   704 text {* nat *}
   705 
   706 lemma "P (x::nat)"
   707 refute [expect = potential]
   708 oops
   709 
   710 lemma "\<forall>x::nat. P x"
   711 refute [expect = potential]
   712 oops
   713 
   714 lemma "P (Suc 0)"
   715 refute [expect = potential]
   716 oops
   717 
   718 lemma "P Suc"
   719 refute [maxsize = 3, expect = none]
   720 -- {* @{term Suc} is a partial function (regardless of the size
   721       of the model), hence @{term "P Suc"} is undefined and no
   722       model will be found *}
   723 oops
   724 
   725 lemma "rec_nat zero suc 0 = zero"
   726 refute [expect = none]
   727 by simp
   728 
   729 lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
   730 refute [maxsize = 2, expect = none]
   731 by simp
   732 
   733 lemma "P (rec_nat zero suc x)"
   734 refute [expect = potential]
   735 oops
   736 
   737 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
   738 refute [expect = potential]
   739 oops
   740 
   741 text {* 'a list *}
   742 
   743 lemma "P (xs::'a list)"
   744 refute [expect = potential]
   745 oops
   746 
   747 lemma "\<forall>xs::'a list. P xs"
   748 refute [expect = potential]
   749 oops
   750 
   751 lemma "P [x, y]"
   752 refute [expect = potential]
   753 oops
   754 
   755 lemma "rec_list nil cons [] = nil"
   756 refute [maxsize = 3, expect = none]
   757 by simp
   758 
   759 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
   760 refute [maxsize = 2, expect = none]
   761 by simp
   762 
   763 lemma "P (rec_list nil cons xs)"
   764 refute [expect = potential]
   765 oops
   766 
   767 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
   768 refute [expect = potential]
   769 oops
   770 
   771 lemma "(xs::'a list) = ys"
   772 refute [expect = potential]
   773 oops
   774 
   775 lemma "a # xs = b # xs"
   776 refute [expect = potential]
   777 oops
   778 
   779 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
   780 
   781 lemma "P (x::BitList)"
   782 refute [expect = potential]
   783 oops
   784 
   785 lemma "\<forall>x::BitList. P x"
   786 refute [expect = potential]
   787 oops
   788 
   789 lemma "P (Bit0 (Bit1 BitListNil))"
   790 refute [expect = potential]
   791 oops
   792 
   793 lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
   794 refute [maxsize = 4, expect = none]
   795 by simp
   796 
   797 lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
   798 refute [maxsize = 2, expect = none]
   799 by simp
   800 
   801 lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
   802 refute [maxsize = 2, expect = none]
   803 by simp
   804 
   805 lemma "P (rec_BitList nil bit0 bit1 x)"
   806 refute [expect = potential]
   807 oops
   808 
   809 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
   810 
   811 lemma "P (x::'a BinTree)"
   812 refute [expect = potential]
   813 oops
   814 
   815 lemma "\<forall>x::'a BinTree. P x"
   816 refute [expect = potential]
   817 oops
   818 
   819 lemma "P (Node (Leaf x) (Leaf y))"
   820 refute [expect = potential]
   821 oops
   822 
   823 lemma "rec_BinTree l n (Leaf x) = l x"
   824   refute [maxsize = 1, expect = none]
   825   (* The "maxsize = 1" tests are a bit pointless: for some formulae
   826      below, refute will find no countermodel simply because this
   827      size makes involved terms undefined.  Unfortunately, any
   828      larger size already takes too long. *)
   829 by simp
   830 
   831 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
   832 refute [maxsize = 1, expect = none]
   833 by simp
   834 
   835 lemma "P (rec_BinTree l n x)"
   836 refute [expect = potential]
   837 oops
   838 
   839 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
   840 refute [expect = potential]
   841 oops
   842 
   843 text {* Mutually recursive datatypes *}
   844 
   845 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
   846      and 'a bexp = Equal "'a aexp" "'a aexp"
   847 
   848 lemma "P (x::'a aexp)"
   849 refute [expect = potential]
   850 oops
   851 
   852 lemma "\<forall>x::'a aexp. P x"
   853 refute [expect = potential]
   854 oops
   855 
   856 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
   857 refute [expect = potential]
   858 oops
   859 
   860 lemma "P (x::'a bexp)"
   861 refute [expect = potential]
   862 oops
   863 
   864 lemma "\<forall>x::'a bexp. P x"
   865 refute [expect = potential]
   866 oops
   867 
   868 lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
   869 refute [maxsize = 1, expect = none]
   870 by simp
   871 
   872 lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
   873 refute [maxsize = 1, expect = none]
   874 by simp
   875 
   876 lemma "P (rec_aexp_bexp_1 number ite equal x)"
   877 refute [expect = potential]
   878 oops
   879 
   880 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
   881 refute [expect = potential]
   882 oops
   883 
   884 lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
   885 refute [maxsize = 1, expect = none]
   886 by simp
   887 
   888 lemma "P (rec_aexp_bexp_2 number ite equal x)"
   889 refute [expect = potential]
   890 oops
   891 
   892 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
   893 refute [expect = potential]
   894 oops
   895 
   896 datatype X = A | B X | C Y
   897      and Y = D X | E Y | F
   898 
   899 lemma "P (x::X)"
   900 refute [expect = potential]
   901 oops
   902 
   903 lemma "P (y::Y)"
   904 refute [expect = potential]
   905 oops
   906 
   907 lemma "P (B (B A))"
   908 refute [expect = potential]
   909 oops
   910 
   911 lemma "P (B (C F))"
   912 refute [expect = potential]
   913 oops
   914 
   915 lemma "P (C (D A))"
   916 refute [expect = potential]
   917 oops
   918 
   919 lemma "P (C (E F))"
   920 refute [expect = potential]
   921 oops
   922 
   923 lemma "P (D (B A))"
   924 refute [expect = potential]
   925 oops
   926 
   927 lemma "P (D (C F))"
   928 refute [expect = potential]
   929 oops
   930 
   931 lemma "P (E (D A))"
   932 refute [expect = potential]
   933 oops
   934 
   935 lemma "P (E (E F))"
   936 refute [expect = potential]
   937 oops
   938 
   939 lemma "P (C (D (C F)))"
   940 refute [expect = potential]
   941 oops
   942 
   943 lemma "rec_X_Y_1 a b c d e f A = a"
   944 refute [maxsize = 3, expect = none]
   945 by simp
   946 
   947 lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
   948 refute [maxsize = 1, expect = none]
   949 by simp
   950 
   951 lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
   952 refute [maxsize = 1, expect = none]
   953 by simp
   954 
   955 lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
   956 refute [maxsize = 1, expect = none]
   957 by simp
   958 
   959 lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
   960 refute [maxsize = 1, expect = none]
   961 by simp
   962 
   963 lemma "rec_X_Y_2 a b c d e f F = f"
   964 refute [maxsize = 3, expect = none]
   965 by simp
   966 
   967 lemma "P (rec_X_Y_1 a b c d e f x)"
   968 refute [expect = potential]
   969 oops
   970 
   971 lemma "P (rec_X_Y_2 a b c d e f y)"
   972 refute [expect = potential]
   973 oops
   974 
   975 text {* Other datatype examples *}
   976 
   977 text {* Indirect recursion is implemented via mutual recursion. *}
   978 
   979 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
   980 
   981 lemma "P (x::XOpt)"
   982 refute [expect = potential]
   983 oops
   984 
   985 lemma "P (CX None)"
   986 refute [expect = potential]
   987 oops
   988 
   989 lemma "P (CX (Some (CX None)))"
   990 refute [expect = potential]
   991 oops
   992 
   993 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
   994 refute [maxsize = 1, expect = none]
   995 by simp
   996 
   997 lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
   998 refute [maxsize = 1, expect = none]
   999 by simp
  1000 
  1001 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
  1002 refute [maxsize = 2, expect = none]
  1003 by simp
  1004 
  1005 lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  1006 refute [maxsize = 1, expect = none]
  1007 by simp
  1008 
  1009 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
  1010 refute [maxsize = 2, expect = none]
  1011 by simp
  1012 
  1013 lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  1014 refute [maxsize = 1, expect = none]
  1015 by simp
  1016 
  1017 lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
  1018 refute [expect = potential]
  1019 oops
  1020 
  1021 lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
  1022 refute [expect = potential]
  1023 oops
  1024 
  1025 lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
  1026 refute [expect = potential]
  1027 oops
  1028 
  1029 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
  1030 
  1031 lemma "P (x::'a YOpt)"
  1032 refute [expect = potential]
  1033 oops
  1034 
  1035 lemma "P (CY None)"
  1036 refute [expect = potential]
  1037 oops
  1038 
  1039 lemma "P (CY (Some (\<lambda>a. CY None)))"
  1040 refute [expect = potential]
  1041 oops
  1042 
  1043 lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
  1044 refute [maxsize = 1, expect = none]
  1045 by simp
  1046 
  1047 lemma "rec_YOpt_2 cy n s None = n"
  1048 refute [maxsize = 2, expect = none]
  1049 by simp
  1050 
  1051 lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
  1052 refute [maxsize = 1, expect = none]
  1053 by simp
  1054 
  1055 lemma "P (rec_YOpt_1 cy n s x)"
  1056 refute [expect = potential]
  1057 oops
  1058 
  1059 lemma "P (rec_YOpt_2 cy n s x)"
  1060 refute [expect = potential]
  1061 oops
  1062 
  1063 datatype Trie = TR "Trie list"
  1064 
  1065 lemma "P (x::Trie)"
  1066 refute [expect = potential]
  1067 oops
  1068 
  1069 lemma "\<forall>x::Trie. P x"
  1070 refute [expect = potential]
  1071 oops
  1072 
  1073 lemma "P (TR [TR []])"
  1074 refute [expect = potential]
  1075 oops
  1076 
  1077 lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
  1078 refute [maxsize = 1, expect = none]
  1079 by simp
  1080 
  1081 lemma "rec_Trie_2 tr nil cons [] = nil"
  1082 refute [maxsize = 3, expect = none]
  1083 by simp
  1084 
  1085 lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
  1086 refute [maxsize = 1, expect = none]
  1087 by simp
  1088 
  1089 lemma "P (rec_Trie_1 tr nil cons x)"
  1090 refute [expect = potential]
  1091 oops
  1092 
  1093 lemma "P (rec_Trie_2 tr nil cons x)"
  1094 refute [expect = potential]
  1095 oops
  1096 
  1097 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
  1098 
  1099 lemma "P (x::InfTree)"
  1100 refute [expect = potential]
  1101 oops
  1102 
  1103 lemma "\<forall>x::InfTree. P x"
  1104 refute [expect = potential]
  1105 oops
  1106 
  1107 lemma "P (Node (\<lambda>n. Leaf))"
  1108 refute [expect = potential]
  1109 oops
  1110 
  1111 lemma "rec_InfTree leaf node Leaf = leaf"
  1112 refute [maxsize = 2, expect = none]
  1113 by simp
  1114 
  1115 lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
  1116 refute [maxsize = 1, expect = none]
  1117 by simp
  1118 
  1119 lemma "P (rec_InfTree leaf node x)"
  1120 refute [expect = potential]
  1121 oops
  1122 
  1123 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
  1124 
  1125 lemma "P (x::'a lambda)"
  1126 refute [expect = potential]
  1127 oops
  1128 
  1129 lemma "\<forall>x::'a lambda. P x"
  1130 refute [expect = potential]
  1131 oops
  1132 
  1133 lemma "P (Lam (\<lambda>a. Var a))"
  1134 refute [expect = potential]
  1135 oops
  1136 
  1137 lemma "rec_lambda var app lam (Var x) = var x"
  1138 refute [maxsize = 1, expect = none]
  1139 by simp
  1140 
  1141 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
  1142 refute [maxsize = 1, expect = none]
  1143 by simp
  1144 
  1145 lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
  1146 refute [maxsize = 1, expect = none]
  1147 by simp
  1148 
  1149 lemma "P (rec_lambda v a l x)"
  1150 refute [expect = potential]
  1151 oops
  1152 
  1153 text {* Taken from "Inductive datatypes in HOL", p.8: *}
  1154 
  1155 datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
  1156 datatype 'c U = E "('c, 'c U) T"
  1157 
  1158 lemma "P (x::'c U)"
  1159 refute [expect = potential]
  1160 oops
  1161 
  1162 lemma "\<forall>x::'c U. P x"
  1163 refute [expect = potential]
  1164 oops
  1165 
  1166 lemma "P (E (C (\<lambda>a. True)))"
  1167 refute [expect = potential]
  1168 oops
  1169 
  1170 lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
  1171 refute [maxsize = 1, expect = none]
  1172 by simp
  1173 
  1174 lemma "rec_U_2 e c d nil cons (C x) = c x"
  1175 refute [maxsize = 1, expect = none]
  1176 by simp
  1177 
  1178 lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
  1179 refute [maxsize = 1, expect = none]
  1180 by simp
  1181 
  1182 lemma "rec_U_3 e c d nil cons [] = nil"
  1183 refute [maxsize = 2, expect = none]
  1184 by simp
  1185 
  1186 lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
  1187 refute [maxsize = 1, expect = none]
  1188 by simp
  1189 
  1190 lemma "P (rec_U_1 e c d nil cons x)"
  1191 refute [expect = potential]
  1192 oops
  1193 
  1194 lemma "P (rec_U_2 e c d nil cons x)"
  1195 refute [expect = potential]
  1196 oops
  1197 
  1198 lemma "P (rec_U_3 e c d nil cons x)"
  1199 refute [expect = potential]
  1200 oops
  1201 
  1202 (*****************************************************************************)
  1203 
  1204 subsubsection {* Records *}
  1205 
  1206 (*TODO: make use of pair types, rather than typedef, for record types*)
  1207 
  1208 record ('a, 'b) point =
  1209   xpos :: 'a
  1210   ypos :: 'b
  1211 
  1212 lemma "(x::('a, 'b) point) = y"
  1213 refute
  1214 oops
  1215 
  1216 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
  1217   ext :: 'c
  1218 
  1219 lemma "(x::('a, 'b, 'c) extpoint) = y"
  1220 refute
  1221 oops
  1222 
  1223 (*****************************************************************************)
  1224 
  1225 subsubsection {* Inductively defined sets *}
  1226 
  1227 inductive_set arbitrarySet :: "'a set"
  1228 where
  1229   "undefined : arbitrarySet"
  1230 
  1231 lemma "x : arbitrarySet"
  1232 refute
  1233 oops
  1234 
  1235 inductive_set evenCard :: "'a set set"
  1236 where
  1237   "{} : evenCard"
  1238 | "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
  1239 
  1240 lemma "S : evenCard"
  1241 refute
  1242 oops
  1243 
  1244 inductive_set
  1245   even :: "nat set"
  1246   and odd  :: "nat set"
  1247 where
  1248   "0 : even"
  1249 | "n : even \<Longrightarrow> Suc n : odd"
  1250 | "n : odd \<Longrightarrow> Suc n : even"
  1251 
  1252 lemma "n : odd"
  1253 (* refute *)  (* TODO: there seems to be an issue here with undefined terms
  1254                        because of the recursive datatype "nat" *)
  1255 oops
  1256 
  1257 consts f :: "'a \<Rightarrow> 'a"
  1258 
  1259 inductive_set
  1260   a_even :: "'a set"
  1261   and a_odd :: "'a set"
  1262 where
  1263   "undefined : a_even"
  1264 | "x : a_even \<Longrightarrow> f x : a_odd"
  1265 | "x : a_odd \<Longrightarrow> f x : a_even"
  1266 
  1267 lemma "x : a_odd"
  1268 (* refute [expect = genuine] -- {* finds a model of size 2 *}
  1269    NO LONGER WORKS since "lfp"'s interpreter is disabled *)
  1270 oops
  1271 
  1272 (*****************************************************************************)
  1273 
  1274 subsubsection {* Examples involving special functions *}
  1275 
  1276 lemma "card x = 0"
  1277 refute
  1278 oops
  1279 
  1280 lemma "finite x"
  1281 refute -- {* no finite countermodel exists *}
  1282 oops
  1283 
  1284 lemma "(x::nat) + y = 0"
  1285 refute [expect = potential]
  1286 oops
  1287 
  1288 lemma "(x::nat) = x + x"
  1289 refute [expect = potential]
  1290 oops
  1291 
  1292 lemma "(x::nat) - y + y = x"
  1293 refute [expect = potential]
  1294 oops
  1295 
  1296 lemma "(x::nat) = x * x"
  1297 refute [expect = potential]
  1298 oops
  1299 
  1300 lemma "(x::nat) < x + y"
  1301 refute [expect = potential]
  1302 oops
  1303 
  1304 lemma "xs @ [] = ys @ []"
  1305 refute [expect = potential]
  1306 oops
  1307 
  1308 lemma "xs @ ys = ys @ xs"
  1309 refute [expect = potential]
  1310 oops
  1311 
  1312 lemma "f (lfp f) = lfp f"
  1313 refute
  1314 oops
  1315 
  1316 lemma "f (gfp f) = gfp f"
  1317 refute
  1318 oops
  1319 
  1320 lemma "lfp f = gfp f"
  1321 refute
  1322 oops
  1323 
  1324 (*****************************************************************************)
  1325 
  1326 subsubsection {* Type classes and overloading *}
  1327 
  1328 text {* A type class without axioms: *}
  1329 
  1330 class classA
  1331 
  1332 lemma "P (x::'a::classA)"
  1333 refute [expect = genuine]
  1334 oops
  1335 
  1336 text {* An axiom with a type variable (denoting types which have at least two elements): *}
  1337 
  1338 class classC =
  1339   assumes classC_ax: "\<exists>x y. x \<noteq> y"
  1340 
  1341 lemma "P (x::'a::classC)"
  1342 refute [expect = genuine]
  1343 oops
  1344 
  1345 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
  1346 (* refute [expect = none] FIXME *)
  1347 oops
  1348 
  1349 text {* A type class for which a constant is defined: *}
  1350 
  1351 class classD =
  1352   fixes classD_const :: "'a \<Rightarrow> 'a"
  1353   assumes classD_ax: "classD_const (classD_const x) = classD_const x"
  1354 
  1355 lemma "P (x::'a::classD)"
  1356 refute [expect = genuine]
  1357 oops
  1358 
  1359 text {* A type class with multiple superclasses: *}
  1360 
  1361 class classE = classC + classD
  1362 
  1363 lemma "P (x::'a::classE)"
  1364 refute [expect = genuine]
  1365 oops
  1366 
  1367 text {* OFCLASS: *}
  1368 
  1369 lemma "OFCLASS('a::type, type_class)"
  1370 refute [expect = none]
  1371 by intro_classes
  1372 
  1373 lemma "OFCLASS('a::classC, type_class)"
  1374 refute [expect = none]
  1375 by intro_classes
  1376 
  1377 lemma "OFCLASS('a::type, classC_class)"
  1378 refute [expect = genuine]
  1379 oops
  1380 
  1381 text {* Overloading: *}
  1382 
  1383 consts inverse :: "'a \<Rightarrow> 'a"
  1384 
  1385 defs (overloaded)
  1386   inverse_bool: "inverse (b::bool)   == ~ b"
  1387   inverse_set : "inverse (S::'a set) == -S"
  1388   inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
  1389 
  1390 lemma "inverse b"
  1391 refute [expect = genuine]
  1392 oops
  1393 
  1394 lemma "P (inverse (S::'a set))"
  1395 refute [expect = genuine]
  1396 oops
  1397 
  1398 lemma "P (inverse (p::'a\<times>'b))"
  1399 refute [expect = genuine]
  1400 oops
  1401 
  1402 text {* Structured proofs *}
  1403 
  1404 lemma "x = y"
  1405 proof cases
  1406   assume "x = y"
  1407   show ?thesis
  1408   refute [expect = none]
  1409   refute [no_assms, expect = genuine]
  1410   refute [no_assms = false, expect = none]
  1411 oops
  1412 
  1413 refute_params [satsolver = "auto"]
  1414 
  1415 end