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