src/HOL/ex/Refute_Examples.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 59987 fbe93138e540 child 61337 4645502c3c64 permissions -rw-r--r--
prefer 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 {* Examples for the 'refute' command *}
```
```     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  -- {* 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 = "cdclite", 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 {* "Every surjective function is invertible." *}
```
```   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 {* "Every invertible function is surjective." *}
```
```   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 {* Every point is a fixed point of some function. *}
```
```   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 {* Axiom of Choice: first an incorrect version ... *}
```
```   282
```
```   283 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
```
```   284 refute [expect = genuine]
```
```   285 oops
```
```   286
```
```   287 text {* ... and now two correct ones *}
```
```   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. EX!y. P x y) \<longrightarrow> (EX!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 {* Meta-logic *}
```
```   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 {* Schematic variables *}
```
```   334
```
```   335 schematic_lemma "?P"
```
```   336 refute [expect = none]
```
```   337 by auto
```
```   338
```
```   339 schematic_lemma "x = ?y"
```
```   340 refute [expect = none]
```
```   341 by auto
```
```   342
```
```   343 (******************************************************************************)
```
```   344
```
```   345 subsubsection {* Abstractions *}
```
```   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 {* Sets *}
```
```   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 {* undefined *}
```
```   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 {* The *}
```
```   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 {* Eps *}
```
```   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 {* Subtypes (typedef), typedecl *}
```
```   474
```
```   475 text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
```
```   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 {* Inductive datatypes *}
```
```   500
```
```   501 text {* unit *}
```
```   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 {* option *}
```
```   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 {* * *}
```
```   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 {* + *}
```
```   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 {* Non-recursive datatypes *}
```
```   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 {* Recursive datatypes *}
```
```   690
```
```   691 text {* nat *}
```
```   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 -- {* @{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 *}
```
```   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 {* 'a list *}
```
```   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 {* Examples involving special functions *}
```
```   799
```
```   800 lemma "card x = 0"
```
```   801 refute [expect = potential]
```
```   802 oops
```
```   803
```
```   804 lemma "finite x"
```
```   805 refute -- {* no finite countermodel exists *}
```
```   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 {* Type classes and overloading *}
```
```   839
```
```   840 text {* A type class without axioms: *}
```
```   841
```
```   842 class classA
```
```   843
```
```   844 lemma "P (x::'a::classA)"
```
```   845 refute [expect = genuine]
```
```   846 oops
```
```   847
```
```   848 text {* An axiom with a type variable (denoting types which have at least two elements): *}
```
```   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 {* A type class for which a constant is defined: *}
```
```   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 {* A type class with multiple superclasses: *}
```
```   872
```
```   873 class classE = classC + classD
```
```   874
```
```   875 lemma "P (x::'a::classE)"
```
```   876 refute [expect = genuine]
```
```   877 oops
```
```   878
```
```   879 text {* OFCLASS: *}
```
```   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 {* Overloading: *}
```
```   894
```
```   895 consts inverse :: "'a \<Rightarrow> 'a"
```
```   896
```
```   897 defs (overloaded)
```
```   898   inverse_bool: "inverse (b::bool)   == ~ b"
```
```   899   inverse_set : "inverse (S::'a set) == -S"
```
```   900   inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
```
```   901
```
```   902 lemma "inverse b"
```
```   903 refute [expect = genuine]
```
```   904 oops
```
```   905
```
```   906 lemma "P (inverse (S::'a set))"
```
```   907 refute [expect = genuine]
```
```   908 oops
```
```   909
```
```   910 lemma "P (inverse (p::'a\<times>'b))"
```
```   911 refute [expect = genuine]
```
```   912 oops
```
```   913
```
```   914 text {* Structured proofs *}
```
```   915
```
```   916 lemma "x = y"
```
```   917 proof cases
```
```   918   assume "x = y"
```
```   919   show ?thesis
```
```   920   refute [expect = none]
```
```   921   refute [no_assms, expect = genuine]
```
```   922   refute [no_assms = false, expect = none]
```
```   923 oops
```
```   924
```
```   925 refute_params [satsolver = "auto"]
```
```   926
```
```   927 end
```