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