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