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