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