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