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