wneuper/isa: src/HOL/Nitpick_Examples/Core

     1 (*  Title:      HOL/Nitpick_Examples/Core_Nits.thy

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009

     5 Examples featuring Nitpick's functional core.

     6 *)

     8 header {* Examples Featuring Nitpick's Functional Core *}

    10 theory Core_Nits

    11 imports Main

    12 begin

    14 nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]

    16 subsection {* Curry in a Hurry *}

    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

    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

    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

    35 lemma "curry (split f) = f"

    36 nitpick [card = 1\<midarrow>4, expect = none]

    37 nitpick [card = 40, expect = none]

    38 by auto

    40 lemma "(split o curry) f = f"

    41 nitpick [card = 1\<midarrow>4, expect = none]

    42 nitpick [card = 40, expect = none]

    43 by auto

    45 lemma "(curry o split) f = f"

    46 nitpick [card = 1\<midarrow>4, expect = none]

    47 nitpick [card = 1000, expect = none]

    48 by auto

    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

    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

    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

    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

    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

    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

    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

    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

    92 subsection {* Representations *}

    94 lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"

    95 nitpick [expect = none]

    96 by auto

    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

   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

   109 lemma "P (\<lambda>x. x)"

   110 nitpick [card = 1, expect = genuine]

   111 nitpick [card = 5, expect = genuine]

   112 oops

   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

   119 lemma "fst (a, b) = a"

   120 nitpick [card = 1\<midarrow>20, expect = none]

   121 by auto

   123 lemma "\<exists>P. P = Id"

   124 nitpick [card = 1\<midarrow>4, expect = none]

   125 by auto

   127 lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"

   128 nitpick [card = 1\<midarrow>3, expect = none]

   129 by auto

   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

   135 lemma "Id (a, a)"

   136 nitpick [card = 1\<midarrow>100, expect = none]

   137 by (auto simp: Id_def Collect_def)

   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)

   143 lemma "UNIV (x\<Colon>'a\<times>'a)"

   144 nitpick [card = 1\<midarrow>50, expect = none]

   145 sorry

   147 lemma "{} = A - A"

   148 nitpick [card = 1\<midarrow>100, expect = none]

   149 by auto

   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

   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

   161 lemma "A \<subseteq> B"

   162 nitpick [card = 100, expect = genuine]

   163 oops

   165 lemma "A = {b}"

   166 nitpick [card = 100, expect = genuine]

   167 oops

   169 lemma "{a, b} = {b}"

   170 nitpick [card = 100, expect = genuine]

   171 oops

   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

   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

   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

   195 lemma "f (a, a) = f (c, d)"

   196 nitpick [card = 4, expect = genuine]

   197 nitpick [card = 20, expect = genuine]

   198 oops

   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

   204 lemma "\<exists>F. F a b = G a b"

   205 nitpick [card = 3, expect = none]

   206 by auto

   208 lemma "f = split"

   209 nitpick [card = 1, expect = none]

   210 nitpick [card = 2, expect = genuine]

   211 oops

   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

   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

   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

   228 subsection {* Quantifiers *}

   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

   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

   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

   251 lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"

   252 nitpick [card 'a = 1\<midarrow>10, expect = none]

   253 by auto

   255 lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"

   256 nitpick [card = 1\<midarrow>40, expect = none]

   257 by auto

   259 lemma "\<forall>x. \<exists>y. f x y = f x (g x)"

   260 nitpick [card = 1\<midarrow>5, expect = none]

   261 by auto

   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

   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

   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

   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

   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

   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

   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

   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

   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

   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

   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

   319 lemma "\<forall>x. if (\<exists>y. x = y) then True else False"

   320 nitpick [expect = none]

   321 sorry

   323 lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"

   324 nitpick [expect = none]

   325 sorry

   327 lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"

   328 nitpick [expect = none]

   329 by auto

   331 lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"

   332 nitpick [expect = none]

   333 by auto

   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

   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

   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

   353 lemma "let x = (\<forall>x. P x) in if x then x else \<not> x"

   354 nitpick [expect = none]

   355 by auto

   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

   361 subsection {* Schematic Variables *}

   363 lemma "x = ?x"

   364 nitpick [expect = none]

   365 by auto

   367 lemma "\<forall>x. x = ?x"

   368 nitpick [expect = genuine]

   369 oops

   371 lemma "\<exists>x. x = ?x"

   372 nitpick [expect = none]

   373 by auto

   375 lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"

   376 nitpick [expect = none]

   377 by auto

   379 lemma "\<forall>x. ?x = ?y"

   380 nitpick [expect = none]

   381 by auto

   383 lemma "\<exists>x. ?x = ?y"

   384 nitpick [expect = none]

   385 by auto

   387 subsection {* Known Constants *}

   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

   397 lemma "\<And>x. f x y = f x y"

   398 nitpick [expect = none]

   399 oops

   401 lemma "\<And>x. f x y = f y x"

   402 nitpick [expect = genuine]

   403 oops

   405 lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"

   406 nitpick [expect = none]

   407 by auto

   409 lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"

   410 nitpick [expect = genuine]

   411 oops

   413 lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"

   414 nitpick [expect = none]

   415 by auto

   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

   426 lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"

   427 nitpick [expect = none]

   428 by auto

   430 lemma "P x \<equiv> P x"

   431 nitpick [card = 1\<midarrow>10, expect = none]

   432 by auto

   434 lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"

   435 nitpick [card = 1\<midarrow>10, expect = none]

   436 by auto

   438 lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"

   439 nitpick [card = 1\<midarrow>10, expect = none]

   440 by auto

   442 lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"

   443 nitpick [expect = genuine]

   444 oops

   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

   450 lemma "P x \<Longrightarrow> P x"

   451 nitpick [card = 1\<midarrow>10, expect = none]

   452 by auto

   454 lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"

   455 nitpick [expect = none]

   456 by auto

   458 lemma "True \<Longrightarrow> False"

   459 nitpick [expect = genuine]

   460 oops

   462 lemma "x = Not"

   463 nitpick [expect = genuine]

   464 oops

   466 lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))"

   467 nitpick [expect = none]

   468 by auto

   470 lemma "x = True"

   471 nitpick [expect = genuine]

   472 oops

   474 lemma "x = False"

   475 nitpick [expect = genuine]

   476 oops

   478 lemma "x = undefined"

   479 nitpick [expect = genuine]

   480 oops

   482 lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined"

   483 nitpick [expect = genuine]

   484 oops

   486 lemma "undefined = undefined"

   487 nitpick [expect = none]

   488 by auto

   490 lemma "f undefined = f undefined"

   491 nitpick [expect = none]

   492 by auto

   494 lemma "f undefined = g undefined"

   495 nitpick [card = 33, expect = genuine]

   496 oops

   498 lemma "\<exists>!x. x = undefined"

   499 nitpick [card = 30, expect = none]

   500 by auto

   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

   509 lemma "\<forall>x. f x y = f x y"

   510 nitpick [expect = none]

   511 oops

   513 lemma "\<forall>x. f x y = f y x"

   514 nitpick [expect = genuine]

   515 oops

   517 lemma "All (\<lambda>x. f x y = f x y) = True"

   518 nitpick [expect = none]

   519 by auto

   521 lemma "All (\<lambda>x. f x y = f x y) = False"

   522 nitpick [expect = genuine]

   523 oops

   525 lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"

   526 nitpick [expect = none]

   527 by auto

   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

   536 lemma "\<exists>x. f x y = f x y"

   537 nitpick [expect = none]

   538 oops

   540 lemma "\<exists>x. f x y = f y x"

   541 nitpick [expect = none]

   542 oops

   544 lemma "Ex (\<lambda>x. f x y = f x y) = True"

   545 nitpick [expect = none]

   546 by auto

   548 lemma "Ex (\<lambda>x. f x y = f y x) = True"

   549 nitpick [expect = none]

   550 by auto

   552 lemma "Ex (\<lambda>x. f x y = f x y) = False"

   553 nitpick [expect = genuine]

   554 oops

   556 lemma "Ex (\<lambda>x. f x y = f y x) = False"

   557 nitpick [expect = genuine]

   558 oops

   560 lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"

   561 nitpick [expect = none]

   562 by auto

   564 lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))"

   565 nitpick [expect = none]

   566 by auto

   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

   573 lemma "x = y \<Longrightarrow> y = x"

   574 nitpick [expect = none]

   575 by auto

   577 lemma "x = y \<Longrightarrow> f x = f y"

   578 nitpick [expect = none]

   579 by auto

   581 lemma "x = y \<and> y = z \<Longrightarrow> x = z"

   582 nitpick [expect = none]

   583 by auto

   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

   590 lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"

   591 nitpick [expect = none]

   592 by auto

   594 lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b"

   595 nitpick [expect = none]

   596 by auto

   598 lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"

   599 nitpick [expect = none]

   600 by auto

   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

   607 lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"

   608 nitpick [expect = none]

   609 by auto

   611 lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"

   612 nitpick [expect = none]

   613 by auto

   615 lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"

   616 nitpick [expect = none]

   617 by auto

   619 lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"

   620 nitpick [expect = none]

   621 by auto

   623 lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"

   624 nitpick [expect = none]

   625 by auto

   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

   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

   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

   641 lemma "fst (x, y) = x"

   642 nitpick [expect = none]

   643 by (simp add: fst_def)

   645 lemma "snd (x, y) = y"

   646 nitpick [expect = none]

   647 by (simp add: snd_def)

   649 lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x"

   650 nitpick [expect = none]

   651 by (simp add: fst_def)

   653 lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y"

   654 nitpick [expect = none]

   655 by (simp add: snd_def)

   657 lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x"

   658 nitpick [expect = none]

   659 by (simp add: fst_def)

   661 lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y"

   662 nitpick [expect = none]

   663 by (simp add: snd_def)

   665 lemma "fst (x\<Colon>'a\<times>'b, y) = x"

   666 nitpick [expect = none]

   667 by (simp add: fst_def)

   669 lemma "snd (x\<Colon>'a\<times>'b, y) = y"

   670 nitpick [expect = none]

   671 by (simp add: snd_def)

   673 lemma "fst (x, y\<Colon>'a\<times>'b) = x"

   674 nitpick [expect = none]

   675 by (simp add: fst_def)

   677 lemma "snd (x, y\<Colon>'a\<times>'b) = y"

   678 nitpick [expect = none]

   679 by (simp add: snd_def)

   681 lemma "fst p = (THE a. \<exists>b. p = Pair a b)"

   682 nitpick [expect = none]

   683 by (simp add: fst_def)

   685 lemma "snd p = (THE b. \<exists>a. p = Pair a b)"

   686 nitpick [expect = none]

   687 by (simp add: snd_def)

   689 lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"

   690 nitpick [expect = none]

   691 by auto

   693 lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"

   694 nitpick [expect = none]

   695 by auto

   697 lemma "fst (x, y) = snd (y, x)"

   698 nitpick [expect = none]

   699 by auto

   701 lemma "(x, x) \<in> Id"

   702 nitpick [expect = none]

   703 by auto

   705 lemma "(x, y) \<in> Id \<Longrightarrow> x = y"

   706 nitpick [expect = none]

   707 by auto

   709 lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"

   710 nitpick [expect = none]

   711 by auto

   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)

   717 lemma "{} = (\<lambda>x. False)"

   718 nitpick [expect = none]

   719 by (metis Collect_def empty_def)

   721 lemma "x \<in> {}"

   722 nitpick [expect = genuine]

   723 oops

   725 lemma "{a, b} = {b}"

   726 nitpick [expect = genuine]

   727 oops

   729 lemma "{a, b} \<noteq> {b}"

   730 nitpick [expect = genuine]

   731 oops

   733 lemma "{a} = {b}"

   734 nitpick [expect = genuine]

   735 oops

   737 lemma "{a} \<noteq> {b}"

   738 nitpick [expect = genuine]

   739 oops

   741 lemma "{a, b, c} = {c, b, a}"

   742 nitpick [expect = none]

   743 by auto

   745 lemma "UNIV = (\<lambda>x. True)"

   746 nitpick [expect = none]

   747 by (simp only: UNIV_def Collect_def)

   749 lemma "UNIV x = True"

   750 nitpick [expect = none]

   751 by (simp only: UNIV_def Collect_def)

   753 lemma "x \<notin> UNIV"

   754 nitpick [expect = genuine]

   755 oops

   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)

   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)

   769 lemma "P x = (x \<in> P)"

   770 nitpick [expect = none]

   771 by (simp add: mem_def)

   773 lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"

   774 nitpick [expect = none]

   775 by simp

   777 lemma "insert = (\<lambda>x y. insert x (y \<union> y))"

   778 nitpick [expect = none]

   779 by simp

   781 lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"

   782 nitpick [card = 1\<midarrow>2, expect = none]

   783 by auto

   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

   790 lemma "(x, x) \<in> rtrancl {(y, y)}"

   791 nitpick [expect = none]

   792 by auto

   794 lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"

   795 nitpick [card = 1\<midarrow>2, expect = none]

   796 by auto

   798 lemma "((x, x), (x, x)) \<in> rtrancl {}"

   799 nitpick [expect = none]

   800 by auto

   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

   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

   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

   814 lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"

   815 nitpick [expect = none]

   816 by auto

   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

   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

   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

   830 lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"

   831 nitpick [expect = none]

   832 by auto

   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

   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

   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

   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

   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

   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

   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

   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

   866 lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"

   867 nitpick [card = 1\<midarrow>5, expect = none]

   868 by auto

   870 lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"

   871 nitpick [card = 5, expect = genuine]

   872 oops

   874 lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B"

   875 nitpick [expect = none]

   876 by auto

   878 lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"

   879 nitpick [card = 1\<midarrow>7, expect = none]

   880 by auto

   882 lemma "A \<union> - A = UNIV"

   883 nitpick [expect = none]

   884 by auto

   886 lemma "A \<inter> - A = {}"

   887 nitpick [expect = none]

   888 by auto

   890 lemma "A = -(A\<Colon>'a set)"

   891 nitpick [card 'a = 10, expect = genuine]

   892 oops

   894 lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"

   895 nitpick [card = 1\<midarrow>7, expect = none]

   896 oops

   898 lemma "finite A"

   899 nitpick [expect = none]

   900 oops

   902 lemma "finite A \<Longrightarrow> finite B"

   903 nitpick [expect = none]

   904 oops

   906 lemma "All finite"

   907 nitpick [expect = none]

   908 oops

   910 subsection {* The and Eps *}

   912 lemma "x = The"

   913 nitpick [card = 5, expect = genuine]

   914 oops

   916 lemma "\<exists>x. x = The"

   917 nitpick [card = 1\<midarrow>3]

   918 by auto

   920 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"

   921 nitpick [expect = none]

   922 by auto

   924 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z"

   925 nitpick [expect = genuine]

   926 oops

   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

   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

   940 lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"

   941 nitpick [expect = genuine]

   942 oops

   944 lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"

   945 nitpick [card = 1\<midarrow>5, expect = none]

   946 by auto

   948 lemma "x = Eps"

   949 nitpick [card = 5, expect = genuine]

   950 oops

   952 lemma "\<exists>x. x = Eps"

   953 nitpick [card = 1\<midarrow>3, expect = none]

   954 by auto

   956 lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"

   957 nitpick [expect = none]

   958 by auto

   960 lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z"

   961 nitpick [expect = genuine]

   962 apply auto

   963 oops

   965 lemma "P x \<Longrightarrow> P (Eps P)"

   966 nitpick [card = 1\<midarrow>8, expect = none]

   967 by (metis exE_some)

   969 lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"

   970 nitpick [expect = genuine]

   971 oops

   973 lemma "P (Eps P)"

   974 nitpick [expect = genuine]

   975 oops

   977 lemma "(P\<Colon>nat set) (Eps P)"

   978 nitpick [expect = genuine]

   979 oops

   981 lemma "\<not> P (Eps P)"

   982 nitpick [expect = genuine]

   983 oops

   985 lemma "\<not> (P\<Colon>nat set) (Eps P)"

   986 nitpick [expect = genuine]

   987 oops

   989 lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"

   990 nitpick [expect = none]

   991 sorry

   993 lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"

   994 nitpick [expect = none]

   995 sorry

   997 lemma "P (The P)"

   998 nitpick [expect = genuine]

   999 oops

  1001 lemma "(P\<Colon>nat set) (The P)"

  1002 nitpick [expect = genuine]

  1003 oops

  1005 lemma "\<not> P (The P)"

  1006 nitpick [expect = genuine]

  1007 oops

  1009 lemma "\<not> (P\<Colon>nat set) (The P)"

  1010 nitpick [expect = genuine]

  1011 oops

  1013 lemma "The P \<noteq> x"

  1014 nitpick [expect = genuine]

  1015 oops

  1017 lemma "The P \<noteq> (x\<Colon>nat)"

  1018 nitpick [expect = genuine]

  1019 oops

  1021 lemma "P x \<Longrightarrow> P (The P)"

  1022 nitpick [expect = genuine]

  1023 oops

  1025 lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)"

  1026 nitpick [expect = genuine]

  1027 oops

  1029 lemma "P = {x} \<Longrightarrow> P (The P)"

  1030 nitpick [expect = none]

  1031 oops

  1033 lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"

  1034 nitpick [expect = none]

  1035 oops

  1037 consts Q :: 'a

  1039 lemma "Q (Eps Q)"

  1040 nitpick [expect = genuine]

  1041 oops

  1043 lemma "(Q\<Colon>nat set) (Eps Q)"

  1044 nitpick [expect = none]

  1045 oops

  1047 lemma "\<not> Q (Eps Q)"

  1048 nitpick [expect = genuine]

  1049 oops

  1051 lemma "\<not> (Q\<Colon>nat set) (Eps Q)"

  1052 nitpick [expect = genuine]

  1053 oops

  1055 lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"

  1056 nitpick [expect = none]

  1057 sorry

  1059 lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"

  1060 nitpick [expect = none]

  1061 sorry

  1063 lemma "Q (The Q)"

  1064 nitpick [expect = genuine]

  1065 oops

  1067 lemma "(Q\<Colon>nat set) (The Q)"

  1068 nitpick [expect = genuine]

  1069 oops

  1071 lemma "\<not> Q (The Q)"

  1072 nitpick [expect = genuine]

  1073 oops

  1075 lemma "\<not> (Q\<Colon>nat set) (The Q)"

  1076 nitpick [expect = genuine]

  1077 oops

  1079 lemma "The Q \<noteq> x"

  1080 nitpick [expect = genuine]

  1081 oops

  1083 lemma "The Q \<noteq> (x\<Colon>nat)"

  1084 nitpick [expect = genuine]

  1085 oops

  1087 lemma "Q x \<Longrightarrow> Q (The Q)"

  1088 nitpick [expect = genuine]

  1089 oops

  1091 lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)"

  1092 nitpick [expect = genuine]

  1093 oops

  1095 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"

  1096 nitpick [expect = none]

  1097 oops

  1099 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"

  1100 nitpick [expect = none]

  1101 oops

  1103 subsection {* Destructors and Recursors *}

  1105 lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"

  1106 nitpick [card = 2, expect = none]

  1107 by auto

  1109 lemma "bool_rec x y True = x"

  1110 nitpick [card = 2, expect = none]

  1111 by auto

  1113 lemma "bool_rec x y False = y"

  1114 nitpick [card = 2, expect = none]

  1115 by auto

  1117 lemma "(x\<Colon>bool) = bool_rec x x True"

  1118 nitpick [card = 2, expect = none]

  1119 by auto

  1121 lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"

  1122 nitpick [expect = none]

  1123 sorry

  1125 end

author	blanchet
	Fri, 18 Dec 2009 12:00:29 +0100
changeset 34123	8a2c5d7aff51
parent 34083	652719832159
child 35073	cc19e2aef17e
permissions	-rw-r--r--