src/HOL/Nitpick_Examples/Refute_Nits.thy
 author wenzelm Tue Oct 10 19:23:03 2017 +0200 (2017-10-10) changeset 66831 29ea2b900a05 parent 63167 0909deb8059b child 67399 eab6ce8368fa permissions -rw-r--r--
tuned: each session has at most one defining entry;
```     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 section \<open>Refute Examples Adapted to Nitpick\<close>
```
```     9
```
```    10 theory Refute_Nits
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 nitpick_params [verbose, card = 1-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 \<open>Examples and Test Cases\<close>
```
```    27
```
```    28 subsubsection \<open>Propositional logic\<close>
```
```    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::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 \<open>Predicate logic\<close>
```
```    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 \<open>Equality\<close>
```
```    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::'a\<Rightarrow>'b) = g"
```
```   100 nitpick [expect = genuine]
```
```   101 oops
```
```   102
```
```   103 lemma "(f::('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 \<open>First-Order Logic\<close>
```
```   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 \<open>A true statement (also testing names of free and bound variables being identical)\<close>
```
```   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 \<open>"A type has at most 4 elements."\<close>
```
```   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 \<open>"Every reflexive and symmetric relation is transitive."\<close>
```
```   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 \<open>The ``Drinker's theorem''\<close>
```
```   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 \<open>And an incorrect version of it\<close>
```
```   186
```
```   187 lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
```
```   188 nitpick [expect = genuine]
```
```   189 oops
```
```   190
```
```   191 text \<open>"Every function has a fixed point."\<close>
```
```   192
```
```   193 lemma "\<exists>x. f x = x"
```
```   194 nitpick [expect = genuine]
```
```   195 oops
```
```   196
```
```   197 text \<open>"Function composition is commutative."\<close>
```
```   198
```
```   199 lemma "f (g x) = g (f x)"
```
```   200 nitpick [expect = genuine]
```
```   201 oops
```
```   202
```
```   203 text \<open>"Two functions that are equivalent wrt.\ the same predicate 'P' are equal."\<close>
```
```   204
```
```   205 lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
```
```   206 nitpick [expect = genuine]
```
```   207 oops
```
```   208
```
```   209 subsubsection \<open>Higher-Order Logic\<close>
```
```   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 \<open>``The transitive closure of an arbitrary relation is non-empty.''\<close>
```
```   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 \<open>``The union of transitive closures is equal to the transitive closure of unions.''\<close>
```
```   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 \<open>``Every surjective function is invertible.''\<close>
```
```   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 \<open>``Every invertible function is surjective.''\<close>
```
```   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 \<open>``Every point is a fixed point of some function.''\<close>
```
```   284
```
```   285 lemma "\<exists>f. f x = x"
```
```   286 nitpick [card = 1-7, expect = none]
```
```   287 apply (rule_tac x = "\<lambda>x. x" in exI)
```
```   288 apply simp
```
```   289 done
```
```   290
```
```   291 text \<open>Axiom of Choice: first an incorrect version\<close>
```
```   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 \<open>And now two correct ones\<close>
```
```   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 \<open>Metalogic\<close>
```
```   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> Pure.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 \<open>Schematic Variables\<close>
```
```   342
```
```   343 schematic_goal "?P"
```
```   344 nitpick [expect = none]
```
```   345 apply auto
```
```   346 done
```
```   347
```
```   348 schematic_goal "x = ?y"
```
```   349 nitpick [expect = none]
```
```   350 apply auto
```
```   351 done
```
```   352
```
```   353 subsubsection \<open>Abstractions\<close>
```
```   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 \<open>Sets\<close>
```
```   369
```
```   370 lemma "P (A::'a set)"
```
```   371 nitpick [expect = genuine]
```
```   372 oops
```
```   373
```
```   374 lemma "P (A::'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 \<open>@{const undefined}\<close>
```
```   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 \<open>@{const The}\<close>
```
```   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 \<open>@{const Eps}\<close>
```
```   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 \<open>Operations on Natural Numbers\<close>
```
```   475
```
```   476 lemma "(x::nat) + y = 0"
```
```   477 nitpick [expect = genuine]
```
```   478 oops
```
```   479
```
```   480 lemma "(x::nat) = x + x"
```
```   481 nitpick [expect = genuine]
```
```   482 oops
```
```   483
```
```   484 lemma "(x::nat) - y + y = x"
```
```   485 nitpick [expect = genuine]
```
```   486 oops
```
```   487
```
```   488 lemma "(x::nat) = x * x"
```
```   489 nitpick [expect = genuine]
```
```   490 oops
```
```   491
```
```   492 lemma "(x::nat) < x + y"
```
```   493 nitpick [card = 1, expect = genuine]
```
```   494 oops
```
```   495
```
```   496 text \<open>\<times>\<close>
```
```   497
```
```   498 lemma "P (x::'a\<times>'b)"
```
```   499 nitpick [expect = genuine]
```
```   500 oops
```
```   501
```
```   502 lemma "\<forall>x::'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 "P (case x of Pair a b \<Rightarrow> f a b)"
```
```   523 nitpick [expect = genuine]
```
```   524 oops
```
```   525
```
```   526 subsubsection \<open>Subtypes (typedef), typedecl\<close>
```
```   527
```
```   528 text \<open>A completely unspecified non-empty subset of @{typ "'a"}:\<close>
```
```   529
```
```   530 definition "myTdef = insert (undefined::'a) (undefined::'a set)"
```
```   531
```
```   532 typedef 'a myTdef = "myTdef :: 'a set"
```
```   533 unfolding myTdef_def by auto
```
```   534
```
```   535 lemma "(x::'a myTdef) = y"
```
```   536 nitpick [expect = genuine]
```
```   537 oops
```
```   538
```
```   539 typedecl myTdecl
```
```   540
```
```   541 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
```
```   542
```
```   543 typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
```
```   544 unfolding T_bij_def by auto
```
```   545
```
```   546 lemma "P (f::(myTdecl myTdef) T_bij)"
```
```   547 nitpick [expect = genuine]
```
```   548 oops
```
```   549
```
```   550 subsubsection \<open>Inductive Datatypes\<close>
```
```   551
```
```   552 text \<open>unit\<close>
```
```   553
```
```   554 lemma "P (x::unit)"
```
```   555 nitpick [expect = genuine]
```
```   556 oops
```
```   557
```
```   558 lemma "\<forall>x::unit. P x"
```
```   559 nitpick [expect = genuine]
```
```   560 oops
```
```   561
```
```   562 lemma "P ()"
```
```   563 nitpick [expect = genuine]
```
```   564 oops
```
```   565
```
```   566 lemma "P (case x of () \<Rightarrow> u)"
```
```   567 nitpick [expect = genuine]
```
```   568 oops
```
```   569
```
```   570 text \<open>option\<close>
```
```   571
```
```   572 lemma "P (x::'a option)"
```
```   573 nitpick [expect = genuine]
```
```   574 oops
```
```   575
```
```   576 lemma "\<forall>x::'a option. P x"
```
```   577 nitpick [expect = genuine]
```
```   578 oops
```
```   579
```
```   580 lemma "P None"
```
```   581 nitpick [expect = genuine]
```
```   582 oops
```
```   583
```
```   584 lemma "P (Some x)"
```
```   585 nitpick [expect = genuine]
```
```   586 oops
```
```   587
```
```   588 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
```
```   589 nitpick [expect = genuine]
```
```   590 oops
```
```   591
```
```   592 text \<open>+\<close>
```
```   593
```
```   594 lemma "P (x::'a+'b)"
```
```   595 nitpick [expect = genuine]
```
```   596 oops
```
```   597
```
```   598 lemma "\<forall>x::'a+'b. P x"
```
```   599 nitpick [expect = genuine]
```
```   600 oops
```
```   601
```
```   602 lemma "P (Inl x)"
```
```   603 nitpick [expect = genuine]
```
```   604 oops
```
```   605
```
```   606 lemma "P (Inr x)"
```
```   607 nitpick [expect = genuine]
```
```   608 oops
```
```   609
```
```   610 lemma "P Inl"
```
```   611 nitpick [expect = genuine]
```
```   612 oops
```
```   613
```
```   614 lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
```
```   615 nitpick [expect = genuine]
```
```   616 oops
```
```   617
```
```   618 text \<open>Non-recursive datatypes\<close>
```
```   619
```
```   620 datatype T1 = A | B
```
```   621
```
```   622 lemma "P (x::T1)"
```
```   623 nitpick [expect = genuine]
```
```   624 oops
```
```   625
```
```   626 lemma "\<forall>x::T1. P x"
```
```   627 nitpick [expect = genuine]
```
```   628 oops
```
```   629
```
```   630 lemma "P A"
```
```   631 nitpick [expect = genuine]
```
```   632 oops
```
```   633
```
```   634 lemma "P B"
```
```   635 nitpick [expect = genuine]
```
```   636 oops
```
```   637
```
```   638 lemma "rec_T1 a b A = a"
```
```   639 nitpick [expect = none]
```
```   640 apply simp
```
```   641 done
```
```   642
```
```   643 lemma "rec_T1 a b B = b"
```
```   644 nitpick [expect = none]
```
```   645 apply simp
```
```   646 done
```
```   647
```
```   648 lemma "P (rec_T1 a b x)"
```
```   649 nitpick [expect = genuine]
```
```   650 oops
```
```   651
```
```   652 lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
```
```   653 nitpick [expect = genuine]
```
```   654 oops
```
```   655
```
```   656 datatype 'a T2 = C T1 | D 'a
```
```   657
```
```   658 lemma "P (x::'a T2)"
```
```   659 nitpick [expect = genuine]
```
```   660 oops
```
```   661
```
```   662 lemma "\<forall>x::'a T2. P x"
```
```   663 nitpick [expect = genuine]
```
```   664 oops
```
```   665
```
```   666 lemma "P D"
```
```   667 nitpick [expect = genuine]
```
```   668 oops
```
```   669
```
```   670 lemma "rec_T2 c d (C x) = c x"
```
```   671 nitpick [expect = none]
```
```   672 apply simp
```
```   673 done
```
```   674
```
```   675 lemma "rec_T2 c d (D x) = d x"
```
```   676 nitpick [expect = none]
```
```   677 apply simp
```
```   678 done
```
```   679
```
```   680 lemma "P (rec_T2 c d x)"
```
```   681 nitpick [expect = genuine]
```
```   682 oops
```
```   683
```
```   684 lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
```
```   685 nitpick [expect = genuine]
```
```   686 oops
```
```   687
```
```   688 datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
```
```   689
```
```   690 lemma "P (x::('a, 'b) T3)"
```
```   691 nitpick [expect = genuine]
```
```   692 oops
```
```   693
```
```   694 lemma "\<forall>x::('a, 'b) T3. P x"
```
```   695 nitpick [expect = genuine]
```
```   696 oops
```
```   697
```
```   698 lemma "P E"
```
```   699 nitpick [expect = genuine]
```
```   700 oops
```
```   701
```
```   702 lemma "rec_T3 e (E x) = e x"
```
```   703 nitpick [card = 1-4, expect = none]
```
```   704 apply simp
```
```   705 done
```
```   706
```
```   707 lemma "P (rec_T3 e x)"
```
```   708 nitpick [expect = genuine]
```
```   709 oops
```
```   710
```
```   711 lemma "P (case x of E f \<Rightarrow> e f)"
```
```   712 nitpick [expect = genuine]
```
```   713 oops
```
```   714
```
```   715 text \<open>Recursive datatypes\<close>
```
```   716
```
```   717 text \<open>nat\<close>
```
```   718
```
```   719 lemma "P (x::nat)"
```
```   720 nitpick [expect = genuine]
```
```   721 oops
```
```   722
```
```   723 lemma "\<forall>x::nat. P x"
```
```   724 nitpick [expect = genuine]
```
```   725 oops
```
```   726
```
```   727 lemma "P (Suc 0)"
```
```   728 nitpick [expect = genuine]
```
```   729 oops
```
```   730
```
```   731 lemma "P Suc"
```
```   732 nitpick [card = 1-7, expect = none]
```
```   733 oops
```
```   734
```
```   735 lemma "rec_nat zero suc 0 = zero"
```
```   736 nitpick [expect = none]
```
```   737 apply simp
```
```   738 done
```
```   739
```
```   740 lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
```
```   741 nitpick [expect = none]
```
```   742 apply simp
```
```   743 done
```
```   744
```
```   745 lemma "P (rec_nat zero suc x)"
```
```   746 nitpick [expect = genuine]
```
```   747 oops
```
```   748
```
```   749 lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
```
```   750 nitpick [expect = genuine]
```
```   751 oops
```
```   752
```
```   753 text \<open>'a list\<close>
```
```   754
```
```   755 lemma "P (xs::'a list)"
```
```   756 nitpick [expect = genuine]
```
```   757 oops
```
```   758
```
```   759 lemma "\<forall>xs::'a list. P xs"
```
```   760 nitpick [expect = genuine]
```
```   761 oops
```
```   762
```
```   763 lemma "P [x, y]"
```
```   764 nitpick [expect = genuine]
```
```   765 oops
```
```   766
```
```   767 lemma "rec_list nil cons [] = nil"
```
```   768 nitpick [card = 1-5, expect = none]
```
```   769 apply simp
```
```   770 done
```
```   771
```
```   772 lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
```
```   773 nitpick [card = 1-5, expect = none]
```
```   774 apply simp
```
```   775 done
```
```   776
```
```   777 lemma "P (rec_list nil cons xs)"
```
```   778 nitpick [expect = genuine]
```
```   779 oops
```
```   780
```
```   781 lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
```
```   782 nitpick [expect = genuine]
```
```   783 oops
```
```   784
```
```   785 lemma "(xs::'a list) = ys"
```
```   786 nitpick [expect = genuine]
```
```   787 oops
```
```   788
```
```   789 lemma "a # xs = b # xs"
```
```   790 nitpick [expect = genuine]
```
```   791 oops
```
```   792
```
```   793 datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
```
```   794
```
```   795 lemma "P (x::BitList)"
```
```   796 nitpick [expect = genuine]
```
```   797 oops
```
```   798
```
```   799 lemma "\<forall>x::BitList. P x"
```
```   800 nitpick [expect = genuine]
```
```   801 oops
```
```   802
```
```   803 lemma "P (Bit0 (Bit1 BitListNil))"
```
```   804 nitpick [expect = genuine]
```
```   805 oops
```
```   806
```
```   807 lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
```
```   808 nitpick [expect = none]
```
```   809 apply simp
```
```   810 done
```
```   811
```
```   812 lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
```
```   813 nitpick [expect = none]
```
```   814 apply simp
```
```   815 done
```
```   816
```
```   817 lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
```
```   818 nitpick [expect = none]
```
```   819 apply simp
```
```   820 done
```
```   821
```
```   822 lemma "P (rec_BitList nil bit0 bit1 x)"
```
```   823 nitpick [expect = genuine]
```
```   824 oops
```
```   825
```
```   826 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
```
```   827
```
```   828 lemma "P (x::'a BinTree)"
```
```   829 nitpick [expect = genuine]
```
```   830 oops
```
```   831
```
```   832 lemma "\<forall>x::'a BinTree. P x"
```
```   833 nitpick [expect = genuine]
```
```   834 oops
```
```   835
```
```   836 lemma "P (Node (Leaf x) (Leaf y))"
```
```   837 nitpick [expect = genuine]
```
```   838 oops
```
```   839
```
```   840 lemma "rec_BinTree l n (Leaf x) = l x"
```
```   841 nitpick [expect = none]
```
```   842 apply simp
```
```   843 done
```
```   844
```
```   845 lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
```
```   846 nitpick [card = 1-5, expect = none]
```
```   847 apply simp
```
```   848 done
```
```   849
```
```   850 lemma "P (rec_BinTree l n x)"
```
```   851 nitpick [expect = genuine]
```
```   852 oops
```
```   853
```
```   854 lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
```
```   855 nitpick [expect = genuine]
```
```   856 oops
```
```   857
```
```   858 text \<open>Mutually recursive datatypes\<close>
```
```   859
```
```   860 datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
```
```   861  and 'a bexp = Equal "'a aexp" "'a aexp"
```
```   862
```
```   863 lemma "P (x::'a aexp)"
```
```   864 nitpick [expect = genuine]
```
```   865 oops
```
```   866
```
```   867 lemma "\<forall>x::'a aexp. P x"
```
```   868 nitpick [expect = genuine]
```
```   869 oops
```
```   870
```
```   871 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
```
```   872 nitpick [expect = genuine]
```
```   873 oops
```
```   874
```
```   875 lemma "P (x::'a bexp)"
```
```   876 nitpick [expect = genuine]
```
```   877 oops
```
```   878
```
```   879 lemma "\<forall>x::'a bexp. P x"
```
```   880 nitpick [expect = genuine]
```
```   881 oops
```
```   882
```
```   883 lemma "rec_aexp number ite equal (Number x) = number x"
```
```   884 nitpick [card = 1-3, expect = none]
```
```   885 apply simp
```
```   886 done
```
```   887
```
```   888 lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
```
```   889 nitpick [card = 1-3, expect = none]
```
```   890 apply simp
```
```   891 done
```
```   892
```
```   893 lemma "P (rec_aexp number ite equal x)"
```
```   894 nitpick [expect = genuine]
```
```   895 oops
```
```   896
```
```   897 lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
```
```   898 nitpick [expect = genuine]
```
```   899 oops
```
```   900
```
```   901 lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
```
```   902 nitpick [card = 1-3, expect = none]
```
```   903 apply simp
```
```   904 done
```
```   905
```
```   906 lemma "P (rec_bexp number ite equal x)"
```
```   907 nitpick [expect = genuine]
```
```   908 oops
```
```   909
```
```   910 lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
```
```   911 nitpick [expect = genuine]
```
```   912 oops
```
```   913
```
```   914 datatype X = A | B X | C Y and Y = D X | E Y | F
```
```   915
```
```   916 lemma "P (x::X)"
```
```   917 nitpick [expect = genuine]
```
```   918 oops
```
```   919
```
```   920 lemma "P (y::Y)"
```
```   921 nitpick [expect = genuine]
```
```   922 oops
```
```   923
```
```   924 lemma "P (B (B A))"
```
```   925 nitpick [expect = genuine]
```
```   926 oops
```
```   927
```
```   928 lemma "P (B (C F))"
```
```   929 nitpick [expect = genuine]
```
```   930 oops
```
```   931
```
```   932 lemma "P (C (D A))"
```
```   933 nitpick [expect = genuine]
```
```   934 oops
```
```   935
```
```   936 lemma "P (C (E F))"
```
```   937 nitpick [expect = genuine]
```
```   938 oops
```
```   939
```
```   940 lemma "P (D (B A))"
```
```   941 nitpick [expect = genuine]
```
```   942 oops
```
```   943
```
```   944 lemma "P (D (C F))"
```
```   945 nitpick [expect = genuine]
```
```   946 oops
```
```   947
```
```   948 lemma "P (E (D A))"
```
```   949 nitpick [expect = genuine]
```
```   950 oops
```
```   951
```
```   952 lemma "P (E (E F))"
```
```   953 nitpick [expect = genuine]
```
```   954 oops
```
```   955
```
```   956 lemma "P (C (D (C F)))"
```
```   957 nitpick [expect = genuine]
```
```   958 oops
```
```   959
```
```   960 lemma "rec_X a b c d e f A = a"
```
```   961 nitpick [card = 1-5, expect = none]
```
```   962 apply simp
```
```   963 done
```
```   964
```
```   965 lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
```
```   966 nitpick [card = 1-5, expect = none]
```
```   967 apply simp
```
```   968 done
```
```   969
```
```   970 lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
```
```   971 nitpick [card = 1-5, expect = none]
```
```   972 apply simp
```
```   973 done
```
```   974
```
```   975 lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
```
```   976 nitpick [card = 1-5, expect = none]
```
```   977 apply simp
```
```   978 done
```
```   979
```
```   980 lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
```
```   981 nitpick [card = 1-5, expect = none]
```
```   982 apply simp
```
```   983 done
```
```   984
```
```   985 lemma "rec_Y a b c d e f F = f"
```
```   986 nitpick [card = 1-5, expect = none]
```
```   987 apply simp
```
```   988 done
```
```   989
```
```   990 lemma "P (rec_X a b c d e f x)"
```
```   991 nitpick [expect = genuine]
```
```   992 oops
```
```   993
```
```   994 lemma "P (rec_Y a b c d e f y)"
```
```   995 nitpick [expect = genuine]
```
```   996 oops
```
```   997
```
```   998 text \<open>Other datatype examples\<close>
```
```   999
```
```  1000 text \<open>Indirect recursion is implemented via mutual recursion.\<close>
```
```  1001
```
```  1002 datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
```
```  1003
```
```  1004 lemma "P (x::XOpt)"
```
```  1005 nitpick [expect = genuine]
```
```  1006 oops
```
```  1007
```
```  1008 lemma "P (CX None)"
```
```  1009 nitpick [expect = genuine]
```
```  1010 oops
```
```  1011
```
```  1012 lemma "P (CX (Some (CX None)))"
```
```  1013 nitpick [expect = genuine]
```
```  1014 oops
```
```  1015
```
```  1016 lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
```
```  1017 nitpick [expect = genuine]
```
```  1018 oops
```
```  1019
```
```  1020 datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
```
```  1021
```
```  1022 lemma "P (x::'a YOpt)"
```
```  1023 nitpick [expect = genuine]
```
```  1024 oops
```
```  1025
```
```  1026 lemma "P (CY None)"
```
```  1027 nitpick [expect = genuine]
```
```  1028 oops
```
```  1029
```
```  1030 lemma "P (CY (Some (\<lambda>a. CY None)))"
```
```  1031 nitpick [expect = genuine]
```
```  1032 oops
```
```  1033
```
```  1034 datatype Trie = TR "Trie list"
```
```  1035
```
```  1036 lemma "P (x::Trie)"
```
```  1037 nitpick [expect = genuine]
```
```  1038 oops
```
```  1039
```
```  1040 lemma "\<forall>x::Trie. P x"
```
```  1041 nitpick [expect = genuine]
```
```  1042 oops
```
```  1043
```
```  1044 lemma "P (TR [TR []])"
```
```  1045 nitpick [expect = genuine]
```
```  1046 oops
```
```  1047
```
```  1048 datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
```
```  1049
```
```  1050 lemma "P (x::InfTree)"
```
```  1051 nitpick [expect = genuine]
```
```  1052 oops
```
```  1053
```
```  1054 lemma "\<forall>x::InfTree. P x"
```
```  1055 nitpick [expect = genuine]
```
```  1056 oops
```
```  1057
```
```  1058 lemma "P (Node (\<lambda>n. Leaf))"
```
```  1059 nitpick [expect = genuine]
```
```  1060 oops
```
```  1061
```
```  1062 lemma "rec_InfTree leaf node Leaf = leaf"
```
```  1063 nitpick [card = 1-3, expect = none]
```
```  1064 apply simp
```
```  1065 done
```
```  1066
```
```  1067 lemma "rec_InfTree leaf node (Node g) = node ((\<lambda>InfTree. (InfTree, rec_InfTree leaf node InfTree)) \<circ> g)"
```
```  1068 nitpick [card = 1-3, expect = none]
```
```  1069 apply simp
```
```  1070 done
```
```  1071
```
```  1072 lemma "P (rec_InfTree leaf node x)"
```
```  1073 nitpick [expect = genuine]
```
```  1074 oops
```
```  1075
```
```  1076 datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
```
```  1077
```
```  1078 lemma "P (x::'a lambda)"
```
```  1079 nitpick [expect = genuine]
```
```  1080 oops
```
```  1081
```
```  1082 lemma "\<forall>x::'a lambda. P x"
```
```  1083 nitpick [expect = genuine]
```
```  1084 oops
```
```  1085
```
```  1086 lemma "P (Lam (\<lambda>a. Var a))"
```
```  1087 nitpick [card = 1-5, expect = none]
```
```  1088 nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
```
```  1089 oops
```
```  1090
```
```  1091 lemma "rec_lambda var app lam (Var x) = var x"
```
```  1092 nitpick [card = 1-3, expect = none]
```
```  1093 apply simp
```
```  1094 done
```
```  1095
```
```  1096 lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
```
```  1097 nitpick [card = 1-3, expect = none]
```
```  1098 apply simp
```
```  1099 done
```
```  1100
```
```  1101 lemma "rec_lambda var app lam (Lam x) = lam ((\<lambda>lambda. (lambda, rec_lambda var app lam lambda)) \<circ> x)"
```
```  1102 nitpick [card = 1-3, expect = none]
```
```  1103 apply simp
```
```  1104 done
```
```  1105
```
```  1106 lemma "P (rec_lambda v a l x)"
```
```  1107 nitpick [expect = genuine]
```
```  1108 oops
```
```  1109
```
```  1110 text \<open>Taken from "Inductive datatypes in HOL", p. 8:\<close>
```
```  1111
```
```  1112 datatype (dead 'a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
```
```  1113 datatype 'c U = E "('c, 'c U) T"
```
```  1114
```
```  1115 lemma "P (x::'c U)"
```
```  1116 nitpick [expect = genuine]
```
```  1117 oops
```
```  1118
```
```  1119 lemma "\<forall>x::'c U. P x"
```
```  1120 nitpick [expect = genuine]
```
```  1121 oops
```
```  1122
```
```  1123 lemma "P (E (C (\<lambda>a. True)))"
```
```  1124 nitpick [expect = genuine]
```
```  1125 oops
```
```  1126
```
```  1127 subsubsection \<open>Records\<close>
```
```  1128
```
```  1129 record ('a, 'b) point =
```
```  1130   xpos :: 'a
```
```  1131   ypos :: 'b
```
```  1132
```
```  1133 lemma "(x::('a, 'b) point) = y"
```
```  1134 nitpick [expect = genuine]
```
```  1135 oops
```
```  1136
```
```  1137 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
```
```  1138   ext :: 'c
```
```  1139
```
```  1140 lemma "(x::('a, 'b, 'c) extpoint) = y"
```
```  1141 nitpick [expect = genuine]
```
```  1142 oops
```
```  1143
```
```  1144 subsubsection \<open>Inductively Defined Sets\<close>
```
```  1145
```
```  1146 inductive_set undefinedSet :: "'a set" where
```
```  1147 "undefined \<in> undefinedSet"
```
```  1148
```
```  1149 lemma "x \<in> undefinedSet"
```
```  1150 nitpick [expect = genuine]
```
```  1151 oops
```
```  1152
```
```  1153 inductive_set evenCard :: "'a set set"
```
```  1154 where
```
```  1155 "{} \<in> evenCard" |
```
```  1156 "\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
```
```  1157
```
```  1158 lemma "S \<in> evenCard"
```
```  1159 nitpick [expect = genuine]
```
```  1160 oops
```
```  1161
```
```  1162 inductive_set
```
```  1163 even :: "nat set"
```
```  1164 and odd :: "nat set"
```
```  1165 where
```
```  1166 "0 \<in> even" |
```
```  1167 "n \<in> even \<Longrightarrow> Suc n \<in> odd" |
```
```  1168 "n \<in> odd \<Longrightarrow> Suc n \<in> even"
```
```  1169
```
```  1170 lemma "n \<in> odd"
```
```  1171 nitpick [expect = genuine]
```
```  1172 oops
```
```  1173
```
```  1174 consts f :: "'a \<Rightarrow> 'a"
```
```  1175
```
```  1176 inductive_set a_even :: "'a set" and a_odd :: "'a set" where
```
```  1177 "undefined \<in> a_even" |
```
```  1178 "x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
```
```  1179 "x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
```
```  1180
```
```  1181 lemma "x \<in> a_odd"
```
```  1182 nitpick [expect = genuine]
```
```  1183 oops
```
```  1184
```
```  1185 subsubsection \<open>Examples Involving Special Functions\<close>
```
```  1186
```
```  1187 lemma "card x = 0"
```
```  1188 nitpick [expect = genuine]
```
```  1189 oops
```
```  1190
```
```  1191 lemma "finite x"
```
```  1192 nitpick [expect = none]
```
```  1193 oops
```
```  1194
```
```  1195 lemma "xs @ [] = ys @ []"
```
```  1196 nitpick [expect = genuine]
```
```  1197 oops
```
```  1198
```
```  1199 lemma "xs @ ys = ys @ xs"
```
```  1200 nitpick [expect = genuine]
```
```  1201 oops
```
```  1202
```
```  1203 lemma "f (lfp f) = lfp f"
```
```  1204 nitpick [card = 2, expect = genuine]
```
```  1205 oops
```
```  1206
```
```  1207 lemma "f (gfp f) = gfp f"
```
```  1208 nitpick [card = 2, expect = genuine]
```
```  1209 oops
```
```  1210
```
```  1211 lemma "lfp f = gfp f"
```
```  1212 nitpick [card = 2, expect = genuine]
```
```  1213 oops
```
```  1214
```
```  1215 subsubsection \<open>Axiomatic Type Classes and Overloading\<close>
```
```  1216
```
```  1217 text \<open>A type class without axioms:\<close>
```
```  1218
```
```  1219 class classA
```
```  1220
```
```  1221 lemma "P (x::'a::classA)"
```
```  1222 nitpick [expect = genuine]
```
```  1223 oops
```
```  1224
```
```  1225 text \<open>An axiom with a type variable (denoting types which have at least two elements):\<close>
```
```  1226
```
```  1227 class classC =
```
```  1228   assumes classC_ax: "\<exists>x y. x \<noteq> y"
```
```  1229
```
```  1230 lemma "P (x::'a::classC)"
```
```  1231 nitpick [expect = genuine]
```
```  1232 oops
```
```  1233
```
```  1234 lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
```
```  1235 nitpick [expect = none]
```
```  1236 sorry
```
```  1237
```
```  1238 text \<open>A type class for which a constant is defined:\<close>
```
```  1239
```
```  1240 class classD =
```
```  1241   fixes classD_const :: "'a \<Rightarrow> 'a"
```
```  1242   assumes classD_ax: "classD_const (classD_const x) = classD_const x"
```
```  1243
```
```  1244 lemma "P (x::'a::classD)"
```
```  1245 nitpick [expect = genuine]
```
```  1246 oops
```
```  1247
```
```  1248 text \<open>A type class with multiple superclasses:\<close>
```
```  1249
```
```  1250 class classE = classC + classD
```
```  1251
```
```  1252 lemma "P (x::'a::classE)"
```
```  1253 nitpick [expect = genuine]
```
```  1254 oops
```
```  1255
```
```  1256 text \<open>OFCLASS:\<close>
```
```  1257
```
```  1258 lemma "OFCLASS('a::type, type_class)"
```
```  1259 nitpick [expect = none]
```
```  1260 apply intro_classes
```
```  1261 done
```
```  1262
```
```  1263 lemma "OFCLASS('a::classC, type_class)"
```
```  1264 nitpick [expect = none]
```
```  1265 apply intro_classes
```
```  1266 done
```
```  1267
```
```  1268 lemma "OFCLASS('a::type, classC_class)"
```
```  1269 nitpick [expect = genuine]
```
```  1270 oops
```
```  1271
```
```  1272 text \<open>Overloading:\<close>
```
```  1273
```
```  1274 consts inverse :: "'a \<Rightarrow> 'a"
```
```  1275
```
```  1276 overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
```
```  1277 begin
```
```  1278   definition "inverse (b::bool) \<equiv> \<not> b"
```
```  1279 end
```
```  1280
```
```  1281 overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
```
```  1282 begin
```
```  1283   definition "inverse (S::'a set) \<equiv> -S"
```
```  1284 end
```
```  1285
```
```  1286 overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
```
```  1287 begin
```
```  1288   definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
```
```  1289 end
```
```  1290
```
```  1291 lemma "inverse b"
```
```  1292 nitpick [expect = genuine]
```
```  1293 oops
```
```  1294
```
```  1295 lemma "P (inverse (S::'a set))"
```
```  1296 nitpick [expect = genuine]
```
```  1297 oops
```
```  1298
```
```  1299 lemma "P (inverse (p::'a\<times>'b))"
```
```  1300 nitpick [expect = genuine]
```
```  1301 oops
```
```  1302
```
```  1303 end
```