src/HOL/Nitpick_Examples/Core_Nits.thy
 author blanchet Fri Oct 23 18:59:24 2009 +0200 (2009-10-23) changeset 33197 de6285ebcc05 child 33199 6c9b2a94a69c permissions -rw-r--r--
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
```     1 (*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
```
```     2     Author:     Jasmin Blanchette, TU Muenchen
```
```     3     Copyright   2009
```
```     4
```
```     5 Examples featuring Nitpick's functional core.
```
```     6 *)
```
```     7
```
```     8 header {* Examples Featuring Nitpick's Functional Core *}
```
```     9
```
```    10 theory Core_Nits
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 subsection {* Curry in a Hurry *}
```
```    15
```
```    16 lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
```
```    17 nitpick [card = 1\<midarrow>4, expect = none]
```
```    18 nitpick [card = 100, expect = none, timeout = none]
```
```    19 by auto
```
```    20
```
```    21 lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
```
```    22 nitpick [card = 2]
```
```    23 nitpick [card = 1\<midarrow>4, expect = none]
```
```    24 nitpick [card = 10, expect = none]
```
```    25 by auto
```
```    26
```
```    27 lemma "split (curry f) = f"
```
```    28 nitpick [card = 1\<midarrow>4, expect = none]
```
```    29 nitpick [card = 10, expect = none]
```
```    30 nitpick [card = 40, expect = none]
```
```    31 by auto
```
```    32
```
```    33 lemma "curry (split f) = f"
```
```    34 nitpick [card = 1\<midarrow>4, expect = none]
```
```    35 nitpick [card = 40, expect = none]
```
```    36 by auto
```
```    37
```
```    38 lemma "(split o curry) f = f"
```
```    39 nitpick [card = 1\<midarrow>4, expect = none]
```
```    40 nitpick [card = 40, expect = none]
```
```    41 by auto
```
```    42
```
```    43 lemma "(curry o split) f = f"
```
```    44 nitpick [card = 1\<midarrow>4, expect = none]
```
```    45 nitpick [card = 1000, expect = none]
```
```    46 by auto
```
```    47
```
```    48 lemma "(split o curry) f = (\<lambda>x. x) f"
```
```    49 nitpick [card = 1\<midarrow>4, expect = none]
```
```    50 nitpick [card = 40, expect = none]
```
```    51 by auto
```
```    52
```
```    53 lemma "(curry o split) f = (\<lambda>x. x) f"
```
```    54 nitpick [card = 1\<midarrow>4, expect = none]
```
```    55 nitpick [card = 40, expect = none]
```
```    56 by auto
```
```    57
```
```    58 lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
```
```    59 nitpick [card = 1\<midarrow>4, expect = none]
```
```    60 nitpick [card = 40, expect = none]
```
```    61 by auto
```
```    62
```
```    63 lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
```
```    64 nitpick [card = 1\<midarrow>4, expect = none]
```
```    65 nitpick [card = 1000, expect = none]
```
```    66 by auto
```
```    67
```
```    68 lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
```
```    69 nitpick [card = 1\<midarrow>4, expect = none]
```
```    70 nitpick [card = 1000, expect = none]
```
```    71 by auto
```
```    72
```
```    73 lemma "split o curry = (\<lambda>x. x)"
```
```    74 nitpick [card = 1\<midarrow>4, expect = none]
```
```    75 nitpick [card = 40, expect = none]
```
```    76 apply (rule ext)+
```
```    77 by auto
```
```    78
```
```    79 lemma "curry o split = (\<lambda>x. x)"
```
```    80 nitpick [card = 1\<midarrow>4, expect = none]
```
```    81 nitpick [card = 100, expect = none]
```
```    82 apply (rule ext)+
```
```    83 by auto
```
```    84
```
```    85 lemma "split (\<lambda>x y. f (x, y)) = f"
```
```    86 nitpick [card = 1\<midarrow>4, expect = none]
```
```    87 nitpick [card = 40, expect = none]
```
```    88 by auto
```
```    89
```
```    90 subsection {* Representations *}
```
```    91
```
```    92 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
```
```    93 nitpick [expect = none]
```
```    94 by auto
```
```    95
```
```    96 lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
```
```    97 nitpick [card 'a = 35, card 'b = 34, expect = genuine]
```
```    98 nitpick [card = 1\<midarrow>15, mono, expect = none]
```
```    99 oops
```
```   100
```
```   101 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
```
```   102 nitpick [card = 1, expect = genuine]
```
```   103 nitpick [card = 2, expect = genuine]
```
```   104 nitpick [card = 5, expect = genuine]
```
```   105 oops
```
```   106
```
```   107 lemma "P (\<lambda>x. x)"
```
```   108 nitpick [card = 1, expect = genuine]
```
```   109 nitpick [card = 5, expect = genuine]
```
```   110 oops
```
```   111
```
```   112 lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
```
```   113 nitpick [card = 1\<midarrow>6, expect = none]
```
```   114 nitpick [card = 20, expect = none]
```
```   115 by auto
```
```   116
```
```   117 lemma "fst (a, b) = a"
```
```   118 nitpick [card = 1\<midarrow>20, expect = none]
```
```   119 by auto
```
```   120
```
```   121 lemma "\<exists>P. P = Id"
```
```   122 nitpick [card = 1\<midarrow>4, expect = none]
```
```   123 by auto
```
```   124
```
```   125 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
```
```   126 nitpick [card = 1\<midarrow>3, expect = none]
```
```   127 by auto
```
```   128
```
```   129 lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
```
```   130 nitpick [card = 1\<midarrow>6, expect = none]
```
```   131 by auto
```
```   132
```
```   133 lemma "Id (a, a)"
```
```   134 nitpick [card = 1\<midarrow>100, expect = none]
```
```   135 by (auto simp: Id_def Collect_def)
```
```   136
```
```   137 lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
```
```   138 nitpick [card = 1\<midarrow>20, expect = none]
```
```   139 by (auto simp: Id_def Collect_def)
```
```   140
```
```   141 lemma "UNIV (x\<Colon>'a\<times>'a)"
```
```   142 nitpick [card = 1\<midarrow>50, expect = none]
```
```   143 sorry
```
```   144
```
```   145 lemma "{} = A - A"
```
```   146 nitpick [card = 1\<midarrow>100, expect = none]
```
```   147 by auto
```
```   148
```
```   149 lemma "g = Let (A \<or> B)"
```
```   150 nitpick [card = 1, expect = none]
```
```   151 nitpick [card = 2, expect = genuine]
```
```   152 nitpick [card = 20, expect = genuine]
```
```   153 oops
```
```   154
```
```   155 lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
```
```   156 nitpick [expect = none]
```
```   157 by auto
```
```   158
```
```   159 lemma "A \<subseteq> B"
```
```   160 nitpick [card = 100, expect = genuine]
```
```   161 oops
```
```   162
```
```   163 lemma "A = {b}"
```
```   164 nitpick [card = 100, expect = genuine]
```
```   165 oops
```
```   166
```
```   167 lemma "{a, b} = {b}"
```
```   168 nitpick [card = 100, expect = genuine]
```
```   169 oops
```
```   170
```
```   171 lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
```
```   172 nitpick [card = 1, expect = genuine]
```
```   173 nitpick [card = 2, expect = genuine]
```
```   174 nitpick [card = 4, expect = genuine]
```
```   175 nitpick [card = 20, expect = genuine]
```
```   176 nitpick [card = 10, dont_box, expect = genuine]
```
```   177 oops
```
```   178
```
```   179 lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
```
```   180 nitpick [card = 3, expect = genuine]
```
```   181 nitpick [card = 3, dont_box, expect = genuine]
```
```   182 nitpick [card = 5, expect = genuine]
```
```   183 nitpick [card = 10, expect = genuine]
```
```   184 oops
```
```   185
```
```   186 lemma "f (a, b) = x"
```
```   187 nitpick [card = 3, expect = genuine]
```
```   188 nitpick [card = 10, expect = genuine]
```
```   189 nitpick [card = 16, expect = genuine]
```
```   190 nitpick [card = 30, expect = genuine]
```
```   191 oops
```
```   192
```
```   193 lemma "f (a, a) = f (c, d)"
```
```   194 nitpick [card = 4, expect = genuine]
```
```   195 nitpick [card = 20, expect = genuine]
```
```   196 oops
```
```   197
```
```   198 lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
```
```   199 nitpick [card = 2, expect = none]
```
```   200 by auto
```
```   201
```
```   202 lemma "\<exists>F. F a b = G a b"
```
```   203 nitpick [card = 3, expect = none]
```
```   204 by auto
```
```   205
```
```   206 lemma "f = split"
```
```   207 nitpick [card = 1, expect = none]
```
```   208 nitpick [card = 2, expect = genuine]
```
```   209 oops
```
```   210
```
```   211 lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
```
```   212 nitpick [card = 20, expect = none]
```
```   213 by auto
```
```   214
```
```   215 lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
```
```   216        A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
```
```   217 nitpick [card = 1\<midarrow>50, expect = none]
```
```   218 by auto
```
```   219
```
```   220 lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
```
```   221 nitpick [card = 3, expect = genuine]
```
```   222 nitpick [card = 4, expect = genuine]
```
```   223 nitpick [card = 8, expect = genuine]
```
```   224 oops
```
```   225
```
```   226 subsection {* Quantifiers *}
```
```   227
```
```   228 lemma "x = y"
```
```   229 nitpick [card 'a = 1, expect = none]
```
```   230 nitpick [card 'a = 2, expect = genuine]
```
```   231 nitpick [card 'a = 100, expect = genuine]
```
```   232 nitpick [card 'a = 1000, expect = genuine]
```
```   233 oops
```
```   234
```
```   235 lemma "\<forall>x. x = y"
```
```   236 nitpick [card 'a = 1, expect = none]
```
```   237 nitpick [card 'a = 2, expect = genuine]
```
```   238 nitpick [card 'a = 100, expect = genuine]
```
```   239 nitpick [card 'a = 1000, expect = genuine]
```
```   240 oops
```
```   241
```
```   242 lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
```
```   243 nitpick [card 'a = 1, expect = genuine]
```
```   244 nitpick [card 'a = 2, expect = genuine]
```
```   245 nitpick [card 'a = 100, expect = genuine]
```
```   246 nitpick [card 'a = 1000, expect = genuine]
```
```   247 oops
```
```   248
```
```   249 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
```
```   250 nitpick [card 'a = 1\<midarrow>10, expect = none]
```
```   251 by auto
```
```   252
```
```   253 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
```
```   254 nitpick [card = 1\<midarrow>40, expect = none]
```
```   255 by auto
```
```   256
```
```   257 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
```
```   258 nitpick [card = 1\<midarrow>5, expect = none]
```
```   259 by auto
```
```   260
```
```   261 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
```
```   262 nitpick [card = 1\<midarrow>5, expect = none]
```
```   263 by auto
```
```   264
```
```   265 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
```
```   266 nitpick [card = 1\<midarrow>2, expect = genuine]
```
```   267 nitpick [card = 3, expect = genuine]
```
```   268 oops
```
```   269
```
```   270 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
```
```   271        f u v w x y z = f u (g u) w (h u w) y (k u w y)"
```
```   272 nitpick [card = 1\<midarrow>2, expect = none]
```
```   273 nitpick [card = 3, expect = none]
```
```   274 nitpick [card = 4, expect = none]
```
```   275 sorry
```
```   276
```
```   277 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
```
```   278        f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
```
```   279 nitpick [card = 1\<midarrow>2, expect = genuine]
```
```   280 oops
```
```   281
```
```   282 lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
```
```   283        f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
```
```   284 nitpick [card = 1\<midarrow>2, expect = genuine]
```
```   285 oops
```
```   286
```
```   287 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
```
```   288        f u v w x = f u (g u) w (h u w)"
```
```   289 nitpick [card = 1\<midarrow>2, expect = none]
```
```   290 sorry
```
```   291
```
```   292 lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
```
```   293        f u v w x = f u (g u w) w (h u)"
```
```   294 nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
```
```   295 oops
```
```   296
```
```   297 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
```
```   298        f u v w x = f u (g u) w (h u w)"
```
```   299 nitpick [card = 1\<midarrow>2, dont_box, expect = none]
```
```   300 sorry
```
```   301
```
```   302 lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
```
```   303        f u v w x = f u (g u w) w (h u)"
```
```   304 nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
```
```   305 oops
```
```   306
```
```   307 lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
```
```   308 nitpick [card = 1, expect = genuine]
```
```   309 nitpick [card = 2\<midarrow>5, expect = none]
```
```   310 oops
```
```   311
```
```   312 lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
```
```   313 nitpick [card = 1, expect = genuine]
```
```   314 nitpick [card = 2, expect = none]
```
```   315 oops
```
```   316
```
```   317 lemma "\<forall>x. if (\<exists>y. x = y) then True else False"
```
```   318 nitpick [expect = none]
```
```   319 sorry
```
```   320
```
```   321 lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
```
```   322 nitpick [expect = none]
```
```   323 sorry
```
```   324
```
```   325 lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
```
```   326 nitpick [expect = none]
```
```   327 by auto
```
```   328
```
```   329 lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
```
```   330 nitpick [expect = none]
```
```   331 by auto
```
```   332
```
```   333 lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
```
```   334 nitpick [card 'a = 1, expect = genuine]
```
```   335 nitpick [card 'a = 2, expect = genuine]
```
```   336 nitpick [card 'a = 3, expect = genuine]
```
```   337 nitpick [card 'a = 4, expect = genuine]
```
```   338 nitpick [card 'a = 5, expect = genuine]
```
```   339 oops
```
```   340
```
```   341 lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
```
```   342            else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
```
```   343 nitpick [expect = none]
```
```   344 by auto
```
```   345
```
```   346 lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x)
```
```   347            else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
```
```   348 nitpick [expect = none]
```
```   349 by auto
```
```   350
```
```   351 lemma "let x = (\<forall>x. P x) in if x then x else \<not> x"
```
```   352 nitpick [expect = none]
```
```   353 by auto
```
```   354
```
```   355 lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x"
```
```   356 nitpick [expect = none]
```
```   357 by auto
```
```   358
```
```   359 subsection {* Schematic Variables *}
```
```   360
```
```   361 lemma "x = ?x"
```
```   362 nitpick [expect = none]
```
```   363 by auto
```
```   364
```
```   365 lemma "\<forall>x. x = ?x"
```
```   366 nitpick [expect = genuine]
```
```   367 oops
```
```   368
```
```   369 lemma "\<exists>x. x = ?x"
```
```   370 nitpick [expect = none]
```
```   371 by auto
```
```   372
```
```   373 lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
```
```   374 nitpick [expect = none]
```
```   375 by auto
```
```   376
```
```   377 lemma "\<forall>x. ?x = ?y"
```
```   378 nitpick [expect = none]
```
```   379 by auto
```
```   380
```
```   381 lemma "\<exists>x. ?x = ?y"
```
```   382 nitpick [expect = none]
```
```   383 by auto
```
```   384
```
```   385 subsection {* Known Constants *}
```
```   386
```
```   387 lemma "x \<equiv> all \<Longrightarrow> False"
```
```   388 nitpick [card = 1, expect = genuine]
```
```   389 nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
```
```   390 nitpick [card = 2, expect = genuine]
```
```   391 nitpick [card = 8, expect = genuine]
```
```   392 nitpick [card = 10, expect = unknown]
```
```   393 oops
```
```   394
```
```   395 lemma "\<And>x. f x y = f x y"
```
```   396 nitpick [expect = none]
```
```   397 oops
```
```   398
```
```   399 lemma "\<And>x. f x y = f y x"
```
```   400 nitpick [expect = genuine]
```
```   401 oops
```
```   402
```
```   403 lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
```
```   404 nitpick [expect = none]
```
```   405 by auto
```
```   406
```
```   407 lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
```
```   408 nitpick [expect = genuine]
```
```   409 oops
```
```   410
```
```   411 lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
```
```   412 nitpick [expect = none]
```
```   413 by auto
```
```   414
```
```   415 lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
```
```   416 nitpick [card = 1, expect = genuine]
```
```   417 nitpick [card = 2, expect = genuine]
```
```   418 nitpick [card = 3, expect = genuine]
```
```   419 nitpick [card = 4, expect = genuine]
```
```   420 nitpick [card = 5, expect = genuine]
```
```   421 nitpick [card = 100, expect = genuine]
```
```   422 oops
```
```   423
```
```   424 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
```
```   425 nitpick [expect = none]
```
```   426 by auto
```
```   427
```
```   428 lemma "P x \<equiv> P x"
```
```   429 nitpick [card = 1\<midarrow>10, expect = none]
```
```   430 by auto
```
```   431
```
```   432 lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
```
```   433 nitpick [card = 1\<midarrow>10, expect = none]
```
```   434 by auto
```
```   435
```
```   436 lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
```
```   437 nitpick [card = 1\<midarrow>10, expect = none]
```
```   438 by auto
```
```   439
```
```   440 lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
```
```   441 nitpick [expect = genuine]
```
```   442 oops
```
```   443
```
```   444 lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))"
```
```   445 nitpick [expect = none]
```
```   446 by auto
```
```   447
```
```   448 lemma "P x \<Longrightarrow> P x"
```
```   449 nitpick [card = 1\<midarrow>10, expect = none]
```
```   450 by auto
```
```   451
```
```   452 lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
```
```   453 nitpick [expect = none]
```
```   454 by auto
```
```   455
```
```   456 lemma "True \<Longrightarrow> False"
```
```   457 nitpick [expect = genuine]
```
```   458 oops
```
```   459
```
```   460 lemma "x = Not"
```
```   461 nitpick [expect = genuine]
```
```   462 oops
```
```   463
```
```   464 lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))"
```
```   465 nitpick [expect = none]
```
```   466 by auto
```
```   467
```
```   468 lemma "x = True"
```
```   469 nitpick [expect = genuine]
```
```   470 oops
```
```   471
```
```   472 lemma "x = False"
```
```   473 nitpick [expect = genuine]
```
```   474 oops
```
```   475
```
```   476 lemma "x = undefined"
```
```   477 nitpick [expect = genuine]
```
```   478 oops
```
```   479
```
```   480 lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined"
```
```   481 nitpick [expect = genuine]
```
```   482 oops
```
```   483
```
```   484 lemma "undefined = undefined"
```
```   485 nitpick [expect = none]
```
```   486 by auto
```
```   487
```
```   488 lemma "f undefined = f undefined"
```
```   489 nitpick [expect = none]
```
```   490 by auto
```
```   491
```
```   492 lemma "f undefined = g undefined"
```
```   493 nitpick [card = 33, expect = genuine]
```
```   494 oops
```
```   495
```
```   496 lemma "\<exists>!x. x = undefined"
```
```   497 nitpick [card = 30, expect = none]
```
```   498 by auto
```
```   499
```
```   500 lemma "x = All \<Longrightarrow> False"
```
```   501 nitpick [card = 1, dont_box, expect = genuine]
```
```   502 nitpick [card = 2, dont_box, expect = genuine]
```
```   503 nitpick [card = 8, dont_box, expect = genuine]
```
```   504 nitpick [card = 10, dont_box, expect = unknown]
```
```   505 oops
```
```   506
```
```   507 lemma "\<forall>x. f x y = f x y"
```
```   508 nitpick [expect = none]
```
```   509 oops
```
```   510
```
```   511 lemma "\<forall>x. f x y = f y x"
```
```   512 nitpick [expect = genuine]
```
```   513 oops
```
```   514
```
```   515 lemma "All (\<lambda>x. f x y = f x y) = True"
```
```   516 nitpick [expect = none]
```
```   517 by auto
```
```   518
```
```   519 lemma "All (\<lambda>x. f x y = f x y) = False"
```
```   520 nitpick [expect = genuine]
```
```   521 oops
```
```   522
```
```   523 lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
```
```   524 nitpick [expect = none]
```
```   525 by auto
```
```   526
```
```   527 lemma "x = Ex \<Longrightarrow> False"
```
```   528 nitpick [card = 1, dont_box, expect = genuine]
```
```   529 nitpick [card = 2, dont_box, expect = genuine]
```
```   530 nitpick [card = 8, dont_box, expect = genuine]
```
```   531 nitpick [card = 10, dont_box, expect = unknown]
```
```   532 oops
```
```   533
```
```   534 lemma "\<exists>x. f x y = f x y"
```
```   535 nitpick [expect = none]
```
```   536 oops
```
```   537
```
```   538 lemma "\<exists>x. f x y = f y x"
```
```   539 nitpick [expect = none]
```
```   540 oops
```
```   541
```
```   542 lemma "Ex (\<lambda>x. f x y = f x y) = True"
```
```   543 nitpick [expect = none]
```
```   544 by auto
```
```   545
```
```   546 lemma "Ex (\<lambda>x. f x y = f y x) = True"
```
```   547 nitpick [expect = none]
```
```   548 by auto
```
```   549
```
```   550 lemma "Ex (\<lambda>x. f x y = f x y) = False"
```
```   551 nitpick [expect = genuine]
```
```   552 oops
```
```   553
```
```   554 lemma "Ex (\<lambda>x. f x y = f y x) = False"
```
```   555 nitpick [expect = genuine]
```
```   556 oops
```
```   557
```
```   558 lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
```
```   559 nitpick [expect = none]
```
```   560 by auto
```
```   561
```
```   562 lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))"
```
```   563 nitpick [expect = none]
```
```   564 by auto
```
```   565
```
```   566 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
```
```   567       "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
```
```   568 nitpick [expect = none]
```
```   569 by auto
```
```   570
```
```   571 lemma "x = y \<Longrightarrow> y = x"
```
```   572 nitpick [expect = none]
```
```   573 by auto
```
```   574
```
```   575 lemma "x = y \<Longrightarrow> f x = f y"
```
```   576 nitpick [expect = none]
```
```   577 by auto
```
```   578
```
```   579 lemma "x = y \<and> y = z \<Longrightarrow> x = z"
```
```   580 nitpick [expect = none]
```
```   581 by auto
```
```   582
```
```   583 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
```
```   584       "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
```
```   585 nitpick [expect = none]
```
```   586 by auto
```
```   587
```
```   588 lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
```
```   589 nitpick [expect = none]
```
```   590 by auto
```
```   591
```
```   592 lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b"
```
```   593 nitpick [expect = none]
```
```   594 by auto
```
```   595
```
```   596 lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
```
```   597 nitpick [expect = none]
```
```   598 by auto
```
```   599
```
```   600 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
```
```   601       "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
```
```   602 nitpick [expect = none]
```
```   603 by auto
```
```   604
```
```   605 lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
```
```   606 nitpick [expect = none]
```
```   607 by auto
```
```   608
```
```   609 lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
```
```   610 nitpick [expect = none]
```
```   611 by auto
```
```   612
```
```   613 lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
```
```   614 nitpick [expect = none]
```
```   615 by auto
```
```   616
```
```   617 lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
```
```   618 nitpick [expect = none]
```
```   619 by auto
```
```   620
```
```   621 lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
```
```   622 nitpick [expect = none]
```
```   623 by auto
```
```   624
```
```   625 lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
```
```   626 nitpick [expect = none]
```
```   627 by auto
```
```   628
```
```   629 lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))"
```
```   630 nitpick [expect = none]
```
```   631 by auto
```
```   632
```
```   633 lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
```
```   634       "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
```
```   635       "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
```
```   636 nitpick [expect = none]
```
```   637 by auto
```
```   638
```
```   639 lemma "fst (x, y) = x"
```
```   640 nitpick [expect = none]
```
```   641 by (simp add: fst_def)
```
```   642
```
```   643 lemma "snd (x, y) = y"
```
```   644 nitpick [expect = none]
```
```   645 by (simp add: snd_def)
```
```   646
```
```   647 lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x"
```
```   648 nitpick [expect = none]
```
```   649 by (simp add: fst_def)
```
```   650
```
```   651 lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y"
```
```   652 nitpick [expect = none]
```
```   653 by (simp add: snd_def)
```
```   654
```
```   655 lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x"
```
```   656 nitpick [expect = none]
```
```   657 by (simp add: fst_def)
```
```   658
```
```   659 lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y"
```
```   660 nitpick [expect = none]
```
```   661 by (simp add: snd_def)
```
```   662
```
```   663 lemma "fst (x\<Colon>'a\<times>'b, y) = x"
```
```   664 nitpick [expect = none]
```
```   665 by (simp add: fst_def)
```
```   666
```
```   667 lemma "snd (x\<Colon>'a\<times>'b, y) = y"
```
```   668 nitpick [expect = none]
```
```   669 by (simp add: snd_def)
```
```   670
```
```   671 lemma "fst (x, y\<Colon>'a\<times>'b) = x"
```
```   672 nitpick [expect = none]
```
```   673 by (simp add: fst_def)
```
```   674
```
```   675 lemma "snd (x, y\<Colon>'a\<times>'b) = y"
```
```   676 nitpick [expect = none]
```
```   677 by (simp add: snd_def)
```
```   678
```
```   679 lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
```
```   680 nitpick [expect = none]
```
```   681 by (simp add: fst_def)
```
```   682
```
```   683 lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
```
```   684 nitpick [expect = none]
```
```   685 by (simp add: snd_def)
```
```   686
```
```   687 lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
```
```   688 nitpick [expect = none]
```
```   689 by auto
```
```   690
```
```   691 lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
```
```   692 nitpick [expect = none]
```
```   693 by auto
```
```   694
```
```   695 lemma "fst (x, y) = snd (y, x)"
```
```   696 nitpick [expect = none]
```
```   697 by auto
```
```   698
```
```   699 lemma "(x, x) \<in> Id"
```
```   700 nitpick [expect = none]
```
```   701 by auto
```
```   702
```
```   703 lemma "(x, y) \<in> Id \<Longrightarrow> x = y"
```
```   704 nitpick [expect = none]
```
```   705 by auto
```
```   706
```
```   707 lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
```
```   708 nitpick [expect = none]
```
```   709 by auto
```
```   710
```
```   711 lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
```
```   712 nitpick [expect = none]
```
```   713 by (simp add: curry_def)
```
```   714
```
```   715 lemma "{} = (\<lambda>x. False)"
```
```   716 nitpick [expect = none]
```
```   717 by (metis Collect_def bot_set_eq empty_def)
```
```   718
```
```   719 lemma "x \<in> {}"
```
```   720 nitpick [expect = genuine]
```
```   721 oops
```
```   722
```
```   723 lemma "{a, b} = {b}"
```
```   724 nitpick [expect = genuine]
```
```   725 oops
```
```   726
```
```   727 lemma "{a, b} \<noteq> {b}"
```
```   728 nitpick [expect = genuine]
```
```   729 oops
```
```   730
```
```   731 lemma "{a} = {b}"
```
```   732 nitpick [expect = genuine]
```
```   733 oops
```
```   734
```
```   735 lemma "{a} \<noteq> {b}"
```
```   736 nitpick [expect = genuine]
```
```   737 oops
```
```   738
```
```   739 lemma "{a, b, c} = {c, b, a}"
```
```   740 nitpick [expect = none]
```
```   741 by auto
```
```   742
```
```   743 lemma "UNIV = (\<lambda>x. True)"
```
```   744 nitpick [expect = none]
```
```   745 by (simp only: UNIV_def Collect_def)
```
```   746
```
```   747 lemma "UNIV x = True"
```
```   748 nitpick [expect = none]
```
```   749 by (simp only: UNIV_def Collect_def)
```
```   750
```
```   751 lemma "x \<notin> UNIV"
```
```   752 nitpick [expect = genuine]
```
```   753 oops
```
```   754
```
```   755 lemma "op \<in> = (\<lambda>x P. P x)"
```
```   756 nitpick [expect = none]
```
```   757 apply (rule ext)
```
```   758 apply (rule ext)
```
```   759 by (simp add: mem_def)
```
```   760
```
```   761 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
```
```   762 nitpick [expect = none]
```
```   763 apply (rule ext)
```
```   764 apply (rule ext)
```
```   765 by (simp add: mem_def)
```
```   766
```
```   767 lemma "P x = (x \<in> P)"
```
```   768 nitpick [expect = none]
```
```   769 by (simp add: mem_def)
```
```   770
```
```   771 lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
```
```   772 nitpick [expect = none]
```
```   773 by simp
```
```   774
```
```   775 lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
```
```   776 nitpick [expect = none]
```
```   777 by simp
```
```   778
```
```   779 lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
```
```   780 nitpick [card = 1\<midarrow>2, expect = none]
```
```   781 by auto
```
```   782
```
```   783 lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
```
```   784 nitpick [card = 1\<midarrow>3, expect = none]
```
```   785 apply (rule ext)
```
```   786 by auto
```
```   787
```
```   788 lemma "(x, x) \<in> rtrancl {(y, y)}"
```
```   789 nitpick [expect = none]
```
```   790 by auto
```
```   791
```
```   792 lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
```
```   793 nitpick [card = 1\<midarrow>2, expect = none]
```
```   794 by auto
```
```   795
```
```   796 lemma "((x, x), (x, x)) \<in> rtrancl {}"
```
```   797 nitpick [expect = none]
```
```   798 by auto
```
```   799
```
```   800 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
```
```   801 nitpick [card = 1\<midarrow>5, expect = none]
```
```   802 by auto
```
```   803
```
```   804 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
```
```   805 nitpick [card = 1\<midarrow>5, expect = none]
```
```   806 by auto
```
```   807
```
```   808 lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
```
```   809 nitpick [expect = none]
```
```   810 by auto
```
```   811
```
```   812 lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
```
```   813 nitpick [expect = none]
```
```   814 by auto
```
```   815
```
```   816 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
```
```   817 nitpick [card = 1\<midarrow>5, expect = none]
```
```   818 by auto
```
```   819
```
```   820 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
```
```   821 nitpick [card = 1\<midarrow>5, expect = none]
```
```   822 by auto
```
```   823
```
```   824 lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
```
```   825 nitpick [card = 1\<midarrow>5, expect = none]
```
```   826 by auto
```
```   827
```
```   828 lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
```
```   829 nitpick [expect = none]
```
```   830 by auto
```
```   831
```
```   832 lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
```
```   833 nitpick [card = 1\<midarrow>5, expect = none]
```
```   834 by auto
```
```   835
```
```   836 lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
```
```   837 nitpick [card = 1\<midarrow>5, expect = none]
```
```   838 by auto
```
```   839
```
```   840 lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
```
```   841 nitpick [card = 1\<midarrow>5, expect = none]
```
```   842 by auto
```
```   843
```
```   844 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
```
```   845 nitpick [card = 1\<midarrow>5, expect = none]
```
```   846 by auto
```
```   847
```
```   848 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
```
```   849 nitpick [card = 1\<midarrow>5, expect = none]
```
```   850 by auto
```
```   851
```
```   852 lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
```
```   853 nitpick [card = 1\<midarrow>5, expect = none]
```
```   854 by auto
```
```   855
```
```   856 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
```
```   857 nitpick [card = 1\<midarrow>5, expect = none]
```
```   858 by auto
```
```   859
```
```   860 lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
```
```   861 nitpick [card = 1\<midarrow>5, expect = none]
```
```   862 by auto
```
```   863
```
```   864 lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
```
```   865 nitpick [card = 1\<midarrow>5, expect = none]
```
```   866 by auto
```
```   867
```
```   868 lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
```
```   869 nitpick [card = 5, expect = genuine]
```
```   870 oops
```
```   871
```
```   872 lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B"
```
```   873 nitpick [expect = none]
```
```   874 by auto
```
```   875
```
```   876 lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
```
```   877 nitpick [expect = none]
```
```   878 by auto
```
```   879
```
```   880 lemma "A \<union> - A = UNIV"
```
```   881 nitpick [expect = none]
```
```   882 by auto
```
```   883
```
```   884 lemma "A \<inter> - A = {}"
```
```   885 nitpick [expect = none]
```
```   886 by auto
```
```   887
```
```   888 lemma "A = -(A\<Colon>'a set)"
```
```   889 nitpick [card 'a = 10, expect = genuine]
```
```   890 oops
```
```   891
```
```   892 lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
```
```   893 nitpick [expect = none]
```
```   894 oops
```
```   895
```
```   896 lemma "finite A"
```
```   897 nitpick [expect = none]
```
```   898 oops
```
```   899
```
```   900 lemma "finite A \<Longrightarrow> finite B"
```
```   901 nitpick [expect = none]
```
```   902 oops
```
```   903
```
```   904 lemma "All finite"
```
```   905 nitpick [expect = none]
```
```   906 oops
```
```   907
```
```   908 subsection {* The and Eps *}
```
```   909
```
```   910 lemma "x = The"
```
```   911 nitpick [card = 5, expect = genuine]
```
```   912 oops
```
```   913
```
```   914 lemma "\<exists>x. x = The"
```
```   915 nitpick [card = 1\<midarrow>3]
```
```   916 by auto
```
```   917
```
```   918 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
```
```   919 nitpick [expect = none]
```
```   920 by auto
```
```   921
```
```   922 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z"
```
```   923 nitpick [expect = genuine]
```
```   924 oops
```
```   925
```
```   926 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
```
```   927 nitpick [card = 2, expect = none]
```
```   928 nitpick [card = 3\<midarrow>5, expect = genuine]
```
```   929 oops
```
```   930
```
```   931 lemma "P x \<Longrightarrow> P (The P)"
```
```   932 nitpick [card = 1, expect = none]
```
```   933 nitpick [card = 1\<midarrow>2, expect = none]
```
```   934 nitpick [card = 3\<midarrow>5, expect = genuine]
```
```   935 nitpick [card = 8, expect = genuine]
```
```   936 oops
```
```   937
```
```   938 lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
```
```   939 nitpick [expect = genuine]
```
```   940 oops
```
```   941
```
```   942 lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
```
```   943 nitpick [card = 1\<midarrow>5, expect = none]
```
```   944 by auto
```
```   945
```
```   946 lemma "x = Eps"
```
```   947 nitpick [card = 5, expect = genuine]
```
```   948 oops
```
```   949
```
```   950 lemma "\<exists>x. x = Eps"
```
```   951 nitpick [card = 1\<midarrow>3, expect = none]
```
```   952 by auto
```
```   953
```
```   954 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
```
```   955 nitpick [expect = none]
```
```   956 by auto
```
```   957
```
```   958 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z"
```
```   959 nitpick [expect = genuine]
```
```   960 apply auto
```
```   961 oops
```
```   962
```
```   963 lemma "P x \<Longrightarrow> P (Eps P)"
```
```   964 nitpick [card = 1\<midarrow>8, expect = none]
```
```   965 by (metis exE_some)
```
```   966
```
```   967 lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
```
```   968 nitpick [expect = genuine]
```
```   969 oops
```
```   970
```
```   971 lemma "P (Eps P)"
```
```   972 nitpick [expect = genuine]
```
```   973 oops
```
```   974
```
```   975 lemma "(P\<Colon>nat set) (Eps P)"
```
```   976 nitpick [expect = genuine]
```
```   977 oops
```
```   978
```
```   979 lemma "\<not> P (Eps P)"
```
```   980 nitpick [expect = genuine]
```
```   981 oops
```
```   982
```
```   983 lemma "\<not> (P\<Colon>nat set) (Eps P)"
```
```   984 nitpick [expect = genuine]
```
```   985 oops
```
```   986
```
```   987 lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
```
```   988 nitpick [expect = none]
```
```   989 sorry
```
```   990
```
```   991 lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
```
```   992 nitpick [expect = none]
```
```   993 sorry
```
```   994
```
```   995 lemma "P (The P)"
```
```   996 nitpick [expect = genuine]
```
```   997 oops
```
```   998
```
```   999 lemma "(P\<Colon>nat set) (The P)"
```
```  1000 nitpick [expect = genuine]
```
```  1001 oops
```
```  1002
```
```  1003 lemma "\<not> P (The P)"
```
```  1004 nitpick [expect = genuine]
```
```  1005 oops
```
```  1006
```
```  1007 lemma "\<not> (P\<Colon>nat set) (The P)"
```
```  1008 nitpick [expect = genuine]
```
```  1009 oops
```
```  1010
```
```  1011 lemma "The P \<noteq> x"
```
```  1012 nitpick [expect = genuine]
```
```  1013 oops
```
```  1014
```
```  1015 lemma "The P \<noteq> (x\<Colon>nat)"
```
```  1016 nitpick [expect = genuine]
```
```  1017 oops
```
```  1018
```
```  1019 lemma "P x \<Longrightarrow> P (The P)"
```
```  1020 nitpick [expect = genuine]
```
```  1021 oops
```
```  1022
```
```  1023 lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)"
```
```  1024 nitpick [expect = genuine]
```
```  1025 oops
```
```  1026
```
```  1027 lemma "P = {x} \<Longrightarrow> P (The P)"
```
```  1028 nitpick [expect = none]
```
```  1029 oops
```
```  1030
```
```  1031 lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
```
```  1032 nitpick [expect = none]
```
```  1033 oops
```
```  1034
```
```  1035 consts Q :: 'a
```
```  1036
```
```  1037 lemma "Q (Eps Q)"
```
```  1038 nitpick [expect = genuine]
```
```  1039 oops
```
```  1040
```
```  1041 lemma "(Q\<Colon>nat set) (Eps Q)"
```
```  1042 nitpick [expect = none]
```
```  1043 oops
```
```  1044
```
```  1045 lemma "\<not> Q (Eps Q)"
```
```  1046 nitpick [expect = genuine]
```
```  1047 oops
```
```  1048
```
```  1049 lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
```
```  1050 nitpick [expect = genuine]
```
```  1051 oops
```
```  1052
```
```  1053 lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
```
```  1054 nitpick [expect = none]
```
```  1055 sorry
```
```  1056
```
```  1057 lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
```
```  1058 nitpick [expect = none]
```
```  1059 sorry
```
```  1060
```
```  1061 lemma "Q (The Q)"
```
```  1062 nitpick [expect = genuine]
```
```  1063 oops
```
```  1064
```
```  1065 lemma "(Q\<Colon>nat set) (The Q)"
```
```  1066 nitpick [expect = genuine]
```
```  1067 oops
```
```  1068
```
```  1069 lemma "\<not> Q (The Q)"
```
```  1070 nitpick [expect = genuine]
```
```  1071 oops
```
```  1072
```
```  1073 lemma "\<not> (Q\<Colon>nat set) (The Q)"
```
```  1074 nitpick [expect = genuine]
```
```  1075 oops
```
```  1076
```
```  1077 lemma "The Q \<noteq> x"
```
```  1078 nitpick [expect = genuine]
```
```  1079 oops
```
```  1080
```
```  1081 lemma "The Q \<noteq> (x\<Colon>nat)"
```
```  1082 nitpick [expect = genuine]
```
```  1083 oops
```
```  1084
```
```  1085 lemma "Q x \<Longrightarrow> Q (The Q)"
```
```  1086 nitpick [expect = genuine]
```
```  1087 oops
```
```  1088
```
```  1089 lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)"
```
```  1090 nitpick [expect = genuine]
```
```  1091 oops
```
```  1092
```
```  1093 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
```
```  1094 nitpick [expect = none]
```
```  1095 oops
```
```  1096
```
```  1097 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
```
```  1098 nitpick [expect = none]
```
```  1099 oops
```
```  1100
```
```  1101 subsection {* Destructors and Recursors *}
```
```  1102
```
```  1103 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
```
```  1104 nitpick [card = 2, expect = none]
```
```  1105 by auto
```
```  1106
```
```  1107 lemma "bool_rec x y True = x"
```
```  1108 nitpick [card = 2, expect = none]
```
```  1109 by auto
```
```  1110
```
```  1111 lemma "bool_rec x y False = y"
```
```  1112 nitpick [card = 2, expect = none]
```
```  1113 by auto
```
```  1114
```
```  1115 lemma "(x\<Colon>bool) = bool_rec x x True"
```
```  1116 nitpick [card = 2, expect = none]
```
```  1117 by auto
```
```  1118
```
```  1119 lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"
```
```  1120 nitpick [expect = none]
```
```  1121 sorry
```
```  1122
```
```  1123 end
```