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