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