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