src/HOL/ex/Refute_Examples.thy
author wenzelm
Fri Sep 16 21:28:09 2016 +0200 (2016-09-16)
changeset 63901 4ce989e962e0
parent 62148 e410c6287103
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
more symbols;
     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 section \<open>Examples for the 'refute' command\<close>
     9 
    10 theory Refute_Examples
    11 imports "~~/src/HOL/Library/Refute"
    12 begin
    13 
    14 refute_params [satsolver = "cdclite"]
    15 
    16 lemma "P \<and> Q"
    17 apply (rule conjI)
    18 refute [expect = genuine] 1  \<comment> \<open>refutes @{term "P"}\<close>
    19 refute [expect = genuine] 2  \<comment> \<open>refutes @{term "Q"}\<close>
    20 refute [expect = genuine]    \<comment> \<open>equivalent to 'refute 1'\<close>
    21   \<comment> \<open>here 'refute 3' would cause an exception, since we only have 2 subgoals\<close>
    22 refute [maxsize = 5, expect = genuine]   \<comment> \<open>we can override parameters ...\<close>
    23 refute [satsolver = "cdclite", expect = genuine] 2
    24   \<comment> \<open>... and specify a subgoal at the same time\<close>
    25 oops
    26 
    27 (*****************************************************************************)
    28 
    29 subsection \<open>Examples and Test Cases\<close>
    30 
    31 subsubsection \<open>Propositional logic\<close>
    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 \<open>Predicate logic\<close>
    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 \<open>Equality\<close>
    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 \<open>First-Order Logic\<close>
   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 "\<exists>!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> (\<exists>!x. P x)"
   156 refute [expect = genuine]
   157 oops
   158 
   159 text \<open>A true statement (also testing names of free and bound variables being identical)\<close>
   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 \<open>"A type has at most 4 elements."\<close>
   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 \<open>"Every reflexive and symmetric relation is transitive."\<close>
   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 \<open>The "Drinker's theorem" ...\<close>
   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 \<open>... and an incorrect version of it\<close>
   188 
   189 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
   190 refute [expect = genuine]
   191 oops
   192 
   193 text \<open>"Every function has a fixed point."\<close>
   194 
   195 lemma "\<exists>x. f x = x"
   196 refute [expect = genuine]
   197 oops
   198 
   199 text \<open>"Function composition is commutative."\<close>
   200 
   201 lemma "f (g x) = g (f x)"
   202 refute [expect = genuine]
   203 oops
   204 
   205 text \<open>"Two functions that are equivalent wrt.\ the same predicate 'P' are equal."\<close>
   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 \<open>Higher-Order Logic\<close>
   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 "\<exists>!P. P"
   224 refute [expect = none]
   225 by auto
   226 
   227 lemma "\<exists>!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 \<open>"The transitive closure 'T' of an arbitrary relation 'P' is non-empty."\<close>
   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 \<open>"Every surjective function is invertible."\<close>
   263 
   264 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
   265 refute [expect = genuine]
   266 oops
   267 
   268 text \<open>"Every invertible function is surjective."\<close>
   269 
   270 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   271 refute [expect = genuine]
   272 oops
   273 
   274 text \<open>Every point is a fixed point of some function.\<close>
   275 
   276 lemma "\<exists>f. f x = x"
   277 refute [maxsize = 4, expect = none]
   278 apply (rule_tac x="\<lambda>x. x" in exI)
   279 by simp
   280 
   281 text \<open>Axiom of Choice: first an incorrect version ...\<close>
   282 
   283 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   284 refute [expect = genuine]
   285 oops
   286 
   287 text \<open>... and now two correct ones\<close>
   288 
   289 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
   290 refute [maxsize = 4, expect = none]
   291 by (simp add: choice)
   292 
   293 lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   294 refute [maxsize = 2, expect = none]
   295 apply auto
   296   apply (simp add: ex1_implies_ex choice)
   297 by (fast intro: ext)
   298 
   299 (*****************************************************************************)
   300 
   301 subsubsection \<open>Meta-logic\<close>
   302 
   303 lemma "!!x. P x"
   304 refute [expect = genuine]
   305 oops
   306 
   307 lemma "f x == g x"
   308 refute [expect = genuine]
   309 oops
   310 
   311 lemma "P \<Longrightarrow> Q"
   312 refute [expect = genuine]
   313 oops
   314 
   315 lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
   316 refute [expect = genuine]
   317 oops
   318 
   319 lemma "(x == Pure.all) \<Longrightarrow> False"
   320 refute [expect = genuine]
   321 oops
   322 
   323 lemma "(x == (op ==)) \<Longrightarrow> False"
   324 refute [expect = genuine]
   325 oops
   326 
   327 lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
   328 refute [expect = genuine]
   329 oops
   330 
   331 (*****************************************************************************)
   332 
   333 subsubsection \<open>Schematic variables\<close>
   334 
   335 schematic_goal "?P"
   336 refute [expect = none]
   337 by auto
   338 
   339 schematic_goal "x = ?y"
   340 refute [expect = none]
   341 by auto
   342 
   343 (******************************************************************************)
   344 
   345 subsubsection \<open>Abstractions\<close>
   346 
   347 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
   348 refute [expect = genuine]
   349 oops
   350 
   351 lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
   352 refute [expect = genuine]
   353 oops
   354 
   355 lemma "(\<lambda>x. x) = (\<lambda>y. y)"
   356 refute
   357 by simp
   358 
   359 (*****************************************************************************)
   360 
   361 subsubsection \<open>Sets\<close>
   362 
   363 lemma "P (A::'a set)"
   364 refute
   365 oops
   366 
   367 lemma "P (A::'a set set)"
   368 refute
   369 oops
   370 
   371 lemma "{x. P x} = {y. P y}"
   372 refute
   373 by simp
   374 
   375 lemma "x : {x. P x}"
   376 refute
   377 oops
   378 
   379 lemma "P op:"
   380 refute
   381 oops
   382 
   383 lemma "P (op: x)"
   384 refute
   385 oops
   386 
   387 lemma "P Collect"
   388 refute
   389 oops
   390 
   391 lemma "A Un B = A Int B"
   392 refute
   393 oops
   394 
   395 lemma "(A Int B) Un C = (A Un C) Int B"
   396 refute
   397 oops
   398 
   399 lemma "Ball A P \<longrightarrow> Bex A P"
   400 refute
   401 oops
   402 
   403 (*****************************************************************************)
   404 
   405 subsubsection \<open>undefined\<close>
   406 
   407 lemma "undefined"
   408 refute [expect = genuine]
   409 oops
   410 
   411 lemma "P undefined"
   412 refute [expect = genuine]
   413 oops
   414 
   415 lemma "undefined x"
   416 refute [expect = genuine]
   417 oops
   418 
   419 lemma "undefined undefined"
   420 refute [expect = genuine]
   421 oops
   422 
   423 (*****************************************************************************)
   424 
   425 subsubsection \<open>The\<close>
   426 
   427 lemma "The P"
   428 refute [expect = genuine]
   429 oops
   430 
   431 lemma "P The"
   432 refute [expect = genuine]
   433 oops
   434 
   435 lemma "P (The P)"
   436 refute [expect = genuine]
   437 oops
   438 
   439 lemma "(THE x. x=y) = z"
   440 refute [expect = genuine]
   441 oops
   442 
   443 lemma "Ex P \<longrightarrow> P (The P)"
   444 refute [expect = genuine]
   445 oops
   446 
   447 (*****************************************************************************)
   448 
   449 subsubsection \<open>Eps\<close>
   450 
   451 lemma "Eps P"
   452 refute [expect = genuine]
   453 oops
   454 
   455 lemma "P Eps"
   456 refute [expect = genuine]
   457 oops
   458 
   459 lemma "P (Eps P)"
   460 refute [expect = genuine]
   461 oops
   462 
   463 lemma "(SOME x. x=y) = z"
   464 refute [expect = genuine]
   465 oops
   466 
   467 lemma "Ex P \<longrightarrow> P (Eps P)"
   468 refute [maxsize = 3, expect = none]
   469 by (auto simp add: someI)
   470 
   471 (*****************************************************************************)
   472 
   473 subsubsection \<open>Subtypes (typedef), typedecl\<close>
   474 
   475 text \<open>A completely unspecified non-empty subset of @{typ "'a"}:\<close>
   476 
   477 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
   478 
   479 typedef 'a myTdef = "myTdef :: 'a set"
   480   unfolding myTdef_def by auto
   481 
   482 lemma "(x::'a myTdef) = y"
   483 refute
   484 oops
   485 
   486 typedecl myTdecl
   487 
   488 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   489 
   490 typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   491   unfolding T_bij_def by auto
   492 
   493 lemma "P (f::(myTdecl myTdef) T_bij)"
   494 refute
   495 oops
   496 
   497 (*****************************************************************************)
   498 
   499 subsubsection \<open>Inductive datatypes\<close>
   500 
   501 text \<open>unit\<close>
   502 
   503 lemma "P (x::unit)"
   504 refute [expect = genuine]
   505 oops
   506 
   507 lemma "\<forall>x::unit. P x"
   508 refute [expect = genuine]
   509 oops
   510 
   511 lemma "P ()"
   512 refute [expect = genuine]
   513 oops
   514 
   515 lemma "P (case x of () \<Rightarrow> u)"
   516 refute [expect = genuine]
   517 oops
   518 
   519 text \<open>option\<close>
   520 
   521 lemma "P (x::'a option)"
   522 refute [expect = genuine]
   523 oops
   524 
   525 lemma "\<forall>x::'a option. P x"
   526 refute [expect = genuine]
   527 oops
   528 
   529 lemma "P None"
   530 refute [expect = genuine]
   531 oops
   532 
   533 lemma "P (Some x)"
   534 refute [expect = genuine]
   535 oops
   536 
   537 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
   538 refute [expect = genuine]
   539 oops
   540 
   541 text \<open>*\<close>
   542 
   543 lemma "P (x::'a*'b)"
   544 refute [expect = genuine]
   545 oops
   546 
   547 lemma "\<forall>x::'a*'b. P x"
   548 refute [expect = genuine]
   549 oops
   550 
   551 lemma "P (x, y)"
   552 refute [expect = genuine]
   553 oops
   554 
   555 lemma "P (fst x)"
   556 refute [expect = genuine]
   557 oops
   558 
   559 lemma "P (snd x)"
   560 refute [expect = genuine]
   561 oops
   562 
   563 lemma "P Pair"
   564 refute [expect = genuine]
   565 oops
   566 
   567 lemma "P (case x of Pair a b \<Rightarrow> p a b)"
   568 refute [expect = genuine]
   569 oops
   570 
   571 text \<open>+\<close>
   572 
   573 lemma "P (x::'a+'b)"
   574 refute [expect = genuine]
   575 oops
   576 
   577 lemma "\<forall>x::'a+'b. P x"
   578 refute [expect = genuine]
   579 oops
   580 
   581 lemma "P (Inl x)"
   582 refute [expect = genuine]
   583 oops
   584 
   585 lemma "P (Inr x)"
   586 refute [expect = genuine]
   587 oops
   588 
   589 lemma "P Inl"
   590 refute [expect = genuine]
   591 oops
   592 
   593 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
   594 refute [expect = genuine]
   595 oops
   596 
   597 text \<open>Non-recursive datatypes\<close>
   598 
   599 datatype T1 = A | B
   600 
   601 lemma "P (x::T1)"
   602 refute [expect = genuine]
   603 oops
   604 
   605 lemma "\<forall>x::T1. P x"
   606 refute [expect = genuine]
   607 oops
   608 
   609 lemma "P A"
   610 refute [expect = genuine]
   611 oops
   612 
   613 lemma "P B"
   614 refute [expect = genuine]
   615 oops
   616 
   617 lemma "rec_T1 a b A = a"
   618 refute [expect = none]
   619 by simp
   620 
   621 lemma "rec_T1 a b B = b"
   622 refute [expect = none]
   623 by simp
   624 
   625 lemma "P (rec_T1 a b x)"
   626 refute [expect = genuine]
   627 oops
   628 
   629 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
   630 refute [expect = genuine]
   631 oops
   632 
   633 datatype 'a T2 = C T1 | D 'a
   634 
   635 lemma "P (x::'a T2)"
   636 refute [expect = genuine]
   637 oops
   638 
   639 lemma "\<forall>x::'a T2. P x"
   640 refute [expect = genuine]
   641 oops
   642 
   643 lemma "P D"
   644 refute [expect = genuine]
   645 oops
   646 
   647 lemma "rec_T2 c d (C x) = c x"
   648 refute [maxsize = 4, expect = none]
   649 by simp
   650 
   651 lemma "rec_T2 c d (D x) = d x"
   652 refute [maxsize = 4, expect = none]
   653 by simp
   654 
   655 lemma "P (rec_T2 c d x)"
   656 refute [expect = genuine]
   657 oops
   658 
   659 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
   660 refute [expect = genuine]
   661 oops
   662 
   663 datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
   664 
   665 lemma "P (x::('a,'b) T3)"
   666 refute [expect = genuine]
   667 oops
   668 
   669 lemma "\<forall>x::('a,'b) T3. P x"
   670 refute [expect = genuine]
   671 oops
   672 
   673 lemma "P E"
   674 refute [expect = genuine]
   675 oops
   676 
   677 lemma "rec_T3 e (E x) = e x"
   678 refute [maxsize = 2, expect = none]
   679 by simp
   680 
   681 lemma "P (rec_T3 e x)"
   682 refute [expect = genuine]
   683 oops
   684 
   685 lemma "P (case x of E f \<Rightarrow> e f)"
   686 refute [expect = genuine]
   687 oops
   688 
   689 text \<open>Recursive datatypes\<close>
   690 
   691 text \<open>nat\<close>
   692 
   693 lemma "P (x::nat)"
   694 refute [expect = potential]
   695 oops
   696 
   697 lemma "\<forall>x::nat. P x"
   698 refute [expect = potential]
   699 oops
   700 
   701 lemma "P (Suc 0)"
   702 refute [expect = potential]
   703 oops
   704 
   705 lemma "P Suc"
   706 refute [maxsize = 3, expect = none]
   707 \<comment> \<open>@{term Suc} is a partial function (regardless of the size
   708       of the model), hence @{term "P Suc"} is undefined and no
   709       model will be found\<close>
   710 oops
   711 
   712 lemma "rec_nat zero suc 0 = zero"
   713 refute [expect = none]
   714 by simp
   715 
   716 lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
   717 refute [maxsize = 2, expect = none]
   718 by simp
   719 
   720 lemma "P (rec_nat zero suc x)"
   721 refute [expect = potential]
   722 oops
   723 
   724 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
   725 refute [expect = potential]
   726 oops
   727 
   728 text \<open>'a list\<close>
   729 
   730 lemma "P (xs::'a list)"
   731 refute [expect = potential]
   732 oops
   733 
   734 lemma "\<forall>xs::'a list. P xs"
   735 refute [expect = potential]
   736 oops
   737 
   738 lemma "P [x, y]"
   739 refute [expect = potential]
   740 oops
   741 
   742 lemma "rec_list nil cons [] = nil"
   743 refute [maxsize = 3, expect = none]
   744 by simp
   745 
   746 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
   747 refute [maxsize = 2, expect = none]
   748 by simp
   749 
   750 lemma "P (rec_list nil cons xs)"
   751 refute [expect = potential]
   752 oops
   753 
   754 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
   755 refute [expect = potential]
   756 oops
   757 
   758 lemma "(xs::'a list) = ys"
   759 refute [expect = potential]
   760 oops
   761 
   762 lemma "a # xs = b # xs"
   763 refute [expect = potential]
   764 oops
   765 
   766 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
   767 
   768 lemma "P (x::BitList)"
   769 refute [expect = potential]
   770 oops
   771 
   772 lemma "\<forall>x::BitList. P x"
   773 refute [expect = potential]
   774 oops
   775 
   776 lemma "P (Bit0 (Bit1 BitListNil))"
   777 refute [expect = potential]
   778 oops
   779 
   780 lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
   781 refute [maxsize = 4, expect = none]
   782 by simp
   783 
   784 lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
   785 refute [maxsize = 2, expect = none]
   786 by simp
   787 
   788 lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
   789 refute [maxsize = 2, expect = none]
   790 by simp
   791 
   792 lemma "P (rec_BitList nil bit0 bit1 x)"
   793 refute [expect = potential]
   794 oops
   795 
   796 (*****************************************************************************)
   797 
   798 subsubsection \<open>Examples involving special functions\<close>
   799 
   800 lemma "card x = 0"
   801 refute [expect = potential]
   802 oops
   803 
   804 lemma "finite x"
   805 refute \<comment> \<open>no finite countermodel exists\<close>
   806 oops
   807 
   808 lemma "(x::nat) + y = 0"
   809 refute [expect = potential]
   810 oops
   811 
   812 lemma "(x::nat) = x + x"
   813 refute [expect = potential]
   814 oops
   815 
   816 lemma "(x::nat) - y + y = x"
   817 refute [expect = potential]
   818 oops
   819 
   820 lemma "(x::nat) = x * x"
   821 refute [expect = potential]
   822 oops
   823 
   824 lemma "(x::nat) < x + y"
   825 refute [expect = potential]
   826 oops
   827 
   828 lemma "xs @ [] = ys @ []"
   829 refute [expect = potential]
   830 oops
   831 
   832 lemma "xs @ ys = ys @ xs"
   833 refute [expect = potential]
   834 oops
   835 
   836 (*****************************************************************************)
   837 
   838 subsubsection \<open>Type classes and overloading\<close>
   839 
   840 text \<open>A type class without axioms:\<close>
   841 
   842 class classA
   843 
   844 lemma "P (x::'a::classA)"
   845 refute [expect = genuine]
   846 oops
   847 
   848 text \<open>An axiom with a type variable (denoting types which have at least two elements):\<close>
   849 
   850 class classC =
   851   assumes classC_ax: "\<exists>x y. x \<noteq> y"
   852 
   853 lemma "P (x::'a::classC)"
   854 refute [expect = genuine]
   855 oops
   856 
   857 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
   858 (* refute [expect = none] FIXME *)
   859 oops
   860 
   861 text \<open>A type class for which a constant is defined:\<close>
   862 
   863 class classD =
   864   fixes classD_const :: "'a \<Rightarrow> 'a"
   865   assumes classD_ax: "classD_const (classD_const x) = classD_const x"
   866 
   867 lemma "P (x::'a::classD)"
   868 refute [expect = genuine]
   869 oops
   870 
   871 text \<open>A type class with multiple superclasses:\<close>
   872 
   873 class classE = classC + classD
   874 
   875 lemma "P (x::'a::classE)"
   876 refute [expect = genuine]
   877 oops
   878 
   879 text \<open>OFCLASS:\<close>
   880 
   881 lemma "OFCLASS('a::type, type_class)"
   882 refute [expect = none]
   883 by intro_classes
   884 
   885 lemma "OFCLASS('a::classC, type_class)"
   886 refute [expect = none]
   887 by intro_classes
   888 
   889 lemma "OFCLASS('a::type, classC_class)"
   890 refute [expect = genuine]
   891 oops
   892 
   893 text \<open>Overloading:\<close>
   894 
   895 consts inverse :: "'a \<Rightarrow> 'a"
   896 
   897 overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
   898 begin
   899   definition "inverse (b::bool) \<equiv> \<not> b"
   900 end
   901 
   902 overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
   903 begin
   904   definition "inverse (S::'a set) \<equiv> -S"
   905 end
   906 
   907 overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
   908 begin
   909   definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
   910 end
   911 
   912 lemma "inverse b"
   913 refute [expect = genuine]
   914 oops
   915 
   916 lemma "P (inverse (S::'a set))"
   917 refute [expect = genuine]
   918 oops
   919 
   920 lemma "P (inverse (p::'a\<times>'b))"
   921 refute [expect = genuine]
   922 oops
   923 
   924 text \<open>Structured proofs\<close>
   925 
   926 lemma "x = y"
   927 proof cases
   928   assume "x = y"
   929   show ?thesis
   930   refute [expect = none]
   931   refute [no_assms, expect = genuine]
   932   refute [no_assms = false, expect = none]
   933 oops
   934 
   935 refute_params [satsolver = "auto"]
   936 
   937 end