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