src/HOL/Nitpick_Examples/Refute_Nits.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 35087 e385fa507468
child 35284 9edc2bd6d2bd
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
blanchet@33197
     4
blanchet@33197
     5
Refute examples adapted to Nitpick.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Refute Examples Adapted to Nitpick *}
blanchet@33197
     9
blanchet@33197
    10
theory Refute_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@35078
    14
nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
blanchet@34083
    15
blanchet@33197
    16
lemma "P \<and> Q"
blanchet@33197
    17
apply (rule conjI)
blanchet@33197
    18
nitpick [expect = genuine] 1
blanchet@33197
    19
nitpick [expect = genuine] 2
blanchet@33197
    20
nitpick [expect = genuine]
blanchet@33197
    21
nitpick [card = 5, expect = genuine]
blanchet@33735
    22
nitpick [sat_solver = SAT4J, expect = genuine] 2
blanchet@33197
    23
oops
blanchet@33197
    24
blanchet@33197
    25
subsection {* Examples and Test Cases *}
blanchet@33197
    26
blanchet@33197
    27
subsubsection {* Propositional logic *}
blanchet@33197
    28
blanchet@33197
    29
lemma "True"
blanchet@33197
    30
nitpick [expect = none]
blanchet@33197
    31
apply auto
blanchet@33197
    32
done
blanchet@33197
    33
blanchet@33197
    34
lemma "False"
blanchet@33197
    35
nitpick [expect = genuine]
blanchet@33197
    36
oops
blanchet@33197
    37
blanchet@33197
    38
lemma "P"
blanchet@33197
    39
nitpick [expect = genuine]
blanchet@33197
    40
oops
blanchet@33197
    41
blanchet@33197
    42
lemma "\<not> P"
blanchet@33197
    43
nitpick [expect = genuine]
blanchet@33197
    44
oops
blanchet@33197
    45
blanchet@33197
    46
lemma "P \<and> Q"
blanchet@33197
    47
nitpick [expect = genuine]
blanchet@33197
    48
oops
blanchet@33197
    49
blanchet@33197
    50
lemma "P \<or> Q"
blanchet@33197
    51
nitpick [expect = genuine]
blanchet@33197
    52
oops
blanchet@33197
    53
blanchet@33197
    54
lemma "P \<longrightarrow> Q"
blanchet@33197
    55
nitpick [expect = genuine]
blanchet@33197
    56
oops
blanchet@33197
    57
blanchet@33197
    58
lemma "(P\<Colon>bool) = Q"
blanchet@33197
    59
nitpick [expect = genuine]
blanchet@33197
    60
oops
blanchet@33197
    61
blanchet@33197
    62
lemma "(P \<or> Q) \<longrightarrow> (P \<and> Q)"
blanchet@33197
    63
nitpick [expect = genuine]
blanchet@33197
    64
oops
blanchet@33197
    65
blanchet@33197
    66
subsubsection {* Predicate logic *}
blanchet@33197
    67
blanchet@33197
    68
lemma "P x y z"
blanchet@33197
    69
nitpick [expect = genuine]
blanchet@33197
    70
oops
blanchet@33197
    71
blanchet@33197
    72
lemma "P x y \<longrightarrow> P y x"
blanchet@33197
    73
nitpick [expect = genuine]
blanchet@33197
    74
oops
blanchet@33197
    75
blanchet@33197
    76
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
blanchet@33197
    77
nitpick [expect = genuine]
blanchet@33197
    78
oops
blanchet@33197
    79
blanchet@33197
    80
subsubsection {* Equality *}
blanchet@33197
    81
blanchet@33197
    82
lemma "P = True"
blanchet@33197
    83
nitpick [expect = genuine]
blanchet@33197
    84
oops
blanchet@33197
    85
blanchet@33197
    86
lemma "P = False"
blanchet@33197
    87
nitpick [expect = genuine]
blanchet@33197
    88
oops
blanchet@33197
    89
blanchet@33197
    90
lemma "x = y"
blanchet@33197
    91
nitpick [expect = genuine]
blanchet@33197
    92
oops
blanchet@33197
    93
blanchet@33197
    94
lemma "f x = g x"
blanchet@33197
    95
nitpick [expect = genuine]
blanchet@33197
    96
oops
blanchet@33197
    97
blanchet@33197
    98
lemma "(f\<Colon>'a\<Rightarrow>'b) = g"
blanchet@33197
    99
nitpick [expect = genuine]
blanchet@33197
   100
oops
blanchet@33197
   101
blanchet@33197
   102
lemma "(f\<Colon>('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
blanchet@33197
   103
nitpick [expect = genuine]
blanchet@33197
   104
oops
blanchet@33197
   105
blanchet@33197
   106
lemma "distinct [a, b]"
blanchet@33197
   107
nitpick [expect = genuine]
blanchet@33197
   108
apply simp
blanchet@33197
   109
nitpick [expect = genuine]
blanchet@33197
   110
oops
blanchet@33197
   111
blanchet@33197
   112
subsubsection {* First-Order Logic *}
blanchet@33197
   113
blanchet@33197
   114
lemma "\<exists>x. P x"
blanchet@33197
   115
nitpick [expect = genuine]
blanchet@33197
   116
oops
blanchet@33197
   117
blanchet@33197
   118
lemma "\<forall>x. P x"
blanchet@33197
   119
nitpick [expect = genuine]
blanchet@33197
   120
oops
blanchet@33197
   121
blanchet@33197
   122
lemma "\<exists>!x. P x"
blanchet@33197
   123
nitpick [expect = genuine]
blanchet@33197
   124
oops
blanchet@33197
   125
blanchet@33197
   126
lemma "Ex P"
blanchet@33197
   127
nitpick [expect = genuine]
blanchet@33197
   128
oops
blanchet@33197
   129
blanchet@33197
   130
lemma "All P"
blanchet@33197
   131
nitpick [expect = genuine]
blanchet@33197
   132
oops
blanchet@33197
   133
blanchet@33197
   134
lemma "Ex1 P"
blanchet@33197
   135
nitpick [expect = genuine]
blanchet@33197
   136
oops
blanchet@33197
   137
blanchet@33197
   138
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
blanchet@33197
   139
nitpick [expect = genuine]
blanchet@33197
   140
oops
blanchet@33197
   141
blanchet@33197
   142
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
blanchet@33197
   143
nitpick [expect = genuine]
blanchet@33197
   144
oops
blanchet@33197
   145
blanchet@33197
   146
lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
blanchet@33197
   147
nitpick [expect = genuine]
blanchet@33197
   148
oops
blanchet@33197
   149
blanchet@33197
   150
text {* A true statement (also testing names of free and bound variables being identical) *}
blanchet@33197
   151
blanchet@33197
   152
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
blanchet@33197
   153
nitpick [expect = none]
blanchet@33197
   154
apply fast
blanchet@33197
   155
done
blanchet@33197
   156
blanchet@33197
   157
text {* "A type has at most 4 elements." *}
blanchet@33197
   158
blanchet@33197
   159
lemma "\<not> distinct [a, b, c, d, e]"
blanchet@33197
   160
nitpick [expect = genuine]
blanchet@33197
   161
apply simp
blanchet@33197
   162
nitpick [expect = genuine]
blanchet@33197
   163
oops
blanchet@33197
   164
blanchet@33197
   165
lemma "distinct [a, b, c, d]"
blanchet@33197
   166
nitpick [expect = genuine]
blanchet@33197
   167
apply simp
blanchet@33197
   168
nitpick [expect = genuine]
blanchet@33197
   169
oops
blanchet@33197
   170
blanchet@33197
   171
text {* "Every reflexive and symmetric relation is transitive." *}
blanchet@33197
   172
blanchet@33197
   173
lemma "\<lbrakk>\<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x\<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
blanchet@33197
   174
nitpick [expect = genuine]
blanchet@33197
   175
oops
blanchet@33197
   176
blanchet@33197
   177
text {* The "Drinker's theorem" ... *}
blanchet@33197
   178
blanchet@33197
   179
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
blanchet@33197
   180
nitpick [expect = none]
blanchet@33197
   181
apply (auto simp add: ext)
blanchet@33197
   182
done
blanchet@33197
   183
blanchet@33197
   184
text {* ... and an incorrect version of it *}
blanchet@33197
   185
blanchet@33197
   186
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
blanchet@33197
   187
nitpick [expect = genuine]
blanchet@33197
   188
oops
blanchet@33197
   189
blanchet@33197
   190
text {* "Every function has a fixed point." *}
blanchet@33197
   191
blanchet@33197
   192
lemma "\<exists>x. f x = x"
blanchet@33197
   193
nitpick [expect = genuine]
blanchet@33197
   194
oops
blanchet@33197
   195
blanchet@33197
   196
text {* "Function composition is commutative." *}
blanchet@33197
   197
blanchet@33197
   198
lemma "f (g x) = g (f x)"
blanchet@33197
   199
nitpick [expect = genuine]
blanchet@33197
   200
oops
blanchet@33197
   201
blanchet@33197
   202
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
blanchet@33197
   203
blanchet@33197
   204
lemma "((P\<Colon>('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
blanchet@33197
   205
nitpick [expect = genuine]
blanchet@33197
   206
oops
blanchet@33197
   207
blanchet@33197
   208
subsubsection {* Higher-Order Logic *}
blanchet@33197
   209
blanchet@33197
   210
lemma "\<exists>P. P"
blanchet@33197
   211
nitpick [expect = none]
blanchet@33197
   212
apply auto
blanchet@33197
   213
done
blanchet@33197
   214
blanchet@33197
   215
lemma "\<forall>P. P"
blanchet@33197
   216
nitpick [expect = genuine]
blanchet@33197
   217
oops
blanchet@33197
   218
blanchet@33197
   219
lemma "\<exists>!P. P"
blanchet@33197
   220
nitpick [expect = none]
blanchet@33197
   221
apply auto
blanchet@33197
   222
done
blanchet@33197
   223
blanchet@33197
   224
lemma "\<exists>!P. P x"
blanchet@33197
   225
nitpick [expect = genuine]
blanchet@33197
   226
oops
blanchet@33197
   227
blanchet@33197
   228
lemma "P Q \<or> Q x"
blanchet@33197
   229
nitpick [expect = genuine]
blanchet@33197
   230
oops
blanchet@33197
   231
blanchet@33197
   232
lemma "x \<noteq> All"
blanchet@33197
   233
nitpick [expect = genuine]
blanchet@33197
   234
oops
blanchet@33197
   235
blanchet@33197
   236
lemma "x \<noteq> Ex"
blanchet@33197
   237
nitpick [expect = genuine]
blanchet@33197
   238
oops
blanchet@33197
   239
blanchet@33197
   240
lemma "x \<noteq> Ex1"
blanchet@33197
   241
nitpick [expect = genuine]
blanchet@33197
   242
oops
blanchet@33197
   243
blanchet@33197
   244
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
blanchet@33197
   245
blanchet@33197
   246
constdefs
blanchet@33197
   247
"trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
blanchet@33197
   248
"trans P \<equiv> (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
blanchet@33197
   249
"subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
blanchet@33197
   250
"subset P Q \<equiv> (ALL x y. P x y \<longrightarrow> Q x y)"
blanchet@33197
   251
"trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
blanchet@33197
   252
"trans_closure P Q \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
blanchet@33197
   253
blanchet@33197
   254
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
blanchet@33197
   255
nitpick [expect = genuine]
blanchet@33197
   256
oops
blanchet@33197
   257
blanchet@33197
   258
text {* "The union of transitive closures is equal to the transitive closure of unions." *}
blanchet@33197
   259
blanchet@33197
   260
lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
blanchet@33197
   261
 \<longrightarrow> trans_closure TP P
blanchet@33197
   262
 \<longrightarrow> trans_closure TR R
blanchet@33197
   263
 \<longrightarrow> (T x y = (TP x y \<or> TR x y))"
blanchet@33197
   264
nitpick [expect = genuine]
blanchet@33197
   265
oops
blanchet@33197
   266
blanchet@33197
   267
text {* "Every surjective function is invertible." *}
blanchet@33197
   268
blanchet@33197
   269
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
blanchet@33197
   270
nitpick [expect = genuine]
blanchet@33197
   271
oops
blanchet@33197
   272
blanchet@33197
   273
text {* "Every invertible function is surjective." *}
blanchet@33197
   274
blanchet@33197
   275
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
blanchet@33197
   276
nitpick [expect = genuine]
blanchet@33197
   277
oops
blanchet@33197
   278
blanchet@33197
   279
text {* Every point is a fixed point of some function. *}
blanchet@33197
   280
blanchet@33197
   281
lemma "\<exists>f. f x = x"
blanchet@33197
   282
nitpick [card = 1\<midarrow>7, expect = none]
blanchet@33197
   283
apply (rule_tac x = "\<lambda>x. x" in exI)
blanchet@33197
   284
apply simp
blanchet@33197
   285
done
blanchet@33197
   286
blanchet@33197
   287
text {* Axiom of Choice: first an incorrect version ... *}
blanchet@33197
   288
blanchet@33197
   289
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
blanchet@33197
   290
nitpick [expect = genuine]
blanchet@33197
   291
oops
blanchet@33197
   292
blanchet@33197
   293
text {* ... and now two correct ones *}
blanchet@33197
   294
blanchet@33197
   295
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
blanchet@33197
   296
nitpick [card = 1-5, expect = none]
blanchet@33197
   297
apply (simp add: choice)
blanchet@33197
   298
done
blanchet@33197
   299
blanchet@33197
   300
lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
blanchet@33197
   301
nitpick [card = 1-4, expect = none]
blanchet@33197
   302
apply auto
blanchet@33197
   303
 apply (simp add: ex1_implies_ex choice)
blanchet@33197
   304
apply (fast intro: ext)
blanchet@33197
   305
done
blanchet@33197
   306
blanchet@33197
   307
subsubsection {* Metalogic *}
blanchet@33197
   308
blanchet@33197
   309
lemma "\<And>x. P x"
blanchet@33197
   310
nitpick [expect = genuine]
blanchet@33197
   311
oops
blanchet@33197
   312
blanchet@33197
   313
lemma "f x \<equiv> g x"
blanchet@33197
   314
nitpick [expect = genuine]
blanchet@33197
   315
oops
blanchet@33197
   316
blanchet@33197
   317
lemma "P \<Longrightarrow> Q"
blanchet@33197
   318
nitpick [expect = genuine]
blanchet@33197
   319
oops
blanchet@33197
   320
blanchet@33197
   321
lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
blanchet@33197
   322
nitpick [expect = genuine]
blanchet@33197
   323
oops
blanchet@33197
   324
blanchet@33197
   325
lemma "(x \<equiv> all) \<Longrightarrow> False"
blanchet@33197
   326
nitpick [expect = genuine]
blanchet@33197
   327
oops
blanchet@33197
   328
blanchet@33197
   329
lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
blanchet@33197
   330
nitpick [expect = genuine]
blanchet@33197
   331
oops
blanchet@33197
   332
blanchet@33197
   333
lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
blanchet@33197
   334
nitpick [expect = genuine]
blanchet@33197
   335
oops
blanchet@33197
   336
blanchet@33197
   337
subsubsection {* Schematic Variables *}
blanchet@33197
   338
blanchet@33197
   339
lemma "?P"
blanchet@33197
   340
nitpick [expect = none]
blanchet@33197
   341
apply auto
blanchet@33197
   342
done
blanchet@33197
   343
blanchet@33197
   344
lemma "x = ?y"
blanchet@33197
   345
nitpick [expect = none]
blanchet@33197
   346
apply auto
blanchet@33197
   347
done
blanchet@33197
   348
blanchet@33197
   349
subsubsection {* Abstractions *}
blanchet@33197
   350
blanchet@33197
   351
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
blanchet@33197
   352
nitpick [expect = genuine]
blanchet@33197
   353
oops
blanchet@33197
   354
blanchet@33197
   355
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
blanchet@33197
   356
nitpick [expect = genuine]
blanchet@33197
   357
oops
blanchet@33197
   358
blanchet@33197
   359
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
blanchet@33197
   360
nitpick [expect = none]
blanchet@33197
   361
apply simp
blanchet@33197
   362
done
blanchet@33197
   363
blanchet@33197
   364
subsubsection {* Sets *}
blanchet@33197
   365
blanchet@33197
   366
lemma "P (A\<Colon>'a set)"
blanchet@33197
   367
nitpick [expect = genuine]
blanchet@33197
   368
oops
blanchet@33197
   369
blanchet@33197
   370
lemma "P (A\<Colon>'a set set)"
blanchet@33197
   371
nitpick [expect = genuine]
blanchet@33197
   372
oops
blanchet@33197
   373
blanchet@33197
   374
lemma "{x. P x} = {y. P y}"
blanchet@33197
   375
nitpick [expect = none]
blanchet@33197
   376
apply simp
blanchet@33197
   377
done
blanchet@33197
   378
blanchet@33197
   379
lemma "x \<in> {x. P x}"
blanchet@33197
   380
nitpick [expect = genuine]
blanchet@33197
   381
oops
blanchet@33197
   382
blanchet@33197
   383
lemma "P (op \<in>)"
blanchet@33197
   384
nitpick [expect = genuine]
blanchet@33197
   385
oops
blanchet@33197
   386
blanchet@33197
   387
lemma "P (op \<in> x)"
blanchet@33197
   388
nitpick [expect = genuine]
blanchet@33197
   389
oops
blanchet@33197
   390
blanchet@33197
   391
lemma "P Collect"
blanchet@33197
   392
nitpick [expect = genuine]
blanchet@33197
   393
oops
blanchet@33197
   394
blanchet@33197
   395
lemma "A Un B = A Int B"
blanchet@33197
   396
nitpick [expect = genuine]
blanchet@33197
   397
oops
blanchet@33197
   398
blanchet@33197
   399
lemma "(A Int B) Un C = (A Un C) Int B"
blanchet@33197
   400
nitpick [expect = genuine]
blanchet@33197
   401
oops
blanchet@33197
   402
blanchet@33197
   403
lemma "Ball A P \<longrightarrow> Bex A P"
blanchet@33197
   404
nitpick [expect = genuine]
blanchet@33197
   405
oops
blanchet@33197
   406
blanchet@33197
   407
subsubsection {* @{const undefined} *}
blanchet@33197
   408
blanchet@33197
   409
lemma "undefined"
blanchet@33197
   410
nitpick [expect = genuine]
blanchet@33197
   411
oops
blanchet@33197
   412
blanchet@33197
   413
lemma "P undefined"
blanchet@33197
   414
nitpick [expect = genuine]
blanchet@33197
   415
oops
blanchet@33197
   416
blanchet@33197
   417
lemma "undefined x"
blanchet@33197
   418
nitpick [expect = genuine]
blanchet@33197
   419
oops
blanchet@33197
   420
blanchet@33197
   421
lemma "undefined undefined"
blanchet@33197
   422
nitpick [expect = genuine]
blanchet@33197
   423
oops
blanchet@33197
   424
blanchet@33197
   425
subsubsection {* @{const The} *}
blanchet@33197
   426
blanchet@33197
   427
lemma "The P"
blanchet@33197
   428
nitpick [expect = genuine]
blanchet@33197
   429
oops
blanchet@33197
   430
blanchet@33197
   431
lemma "P The"
blanchet@33197
   432
nitpick [expect = genuine]
blanchet@33197
   433
oops
blanchet@33197
   434
blanchet@33197
   435
lemma "P (The P)"
blanchet@33197
   436
nitpick [expect = genuine]
blanchet@33197
   437
oops
blanchet@33197
   438
blanchet@33197
   439
lemma "(THE x. x=y) = z"
blanchet@33197
   440
nitpick [expect = genuine]
blanchet@33197
   441
oops
blanchet@33197
   442
blanchet@33197
   443
lemma "Ex P \<longrightarrow> P (The P)"
blanchet@33197
   444
nitpick [expect = genuine]
blanchet@33197
   445
oops
blanchet@33197
   446
blanchet@33197
   447
subsubsection {* @{const Eps} *}
blanchet@33197
   448
blanchet@33197
   449
lemma "Eps P"
blanchet@33197
   450
nitpick [expect = genuine]
blanchet@33197
   451
oops
blanchet@33197
   452
blanchet@33197
   453
lemma "P Eps"
blanchet@33197
   454
nitpick [expect = genuine]
blanchet@33197
   455
oops
blanchet@33197
   456
blanchet@33197
   457
lemma "P (Eps P)"
blanchet@33197
   458
nitpick [expect = genuine]
blanchet@33197
   459
oops
blanchet@33197
   460
blanchet@33197
   461
lemma "(SOME x. x=y) = z"
blanchet@33197
   462
nitpick [expect = genuine]
blanchet@33197
   463
oops
blanchet@33197
   464
blanchet@33197
   465
lemma "Ex P \<longrightarrow> P (Eps P)"
blanchet@33197
   466
nitpick [expect = none]
blanchet@33197
   467
apply (auto simp add: someI)
blanchet@33197
   468
done
blanchet@33197
   469
blanchet@33197
   470
subsubsection {* Operations on Natural Numbers *}
blanchet@33197
   471
blanchet@33197
   472
lemma "(x\<Colon>nat) + y = 0"
blanchet@33197
   473
nitpick [expect = genuine]
blanchet@33197
   474
oops
blanchet@33197
   475
blanchet@33197
   476
lemma "(x\<Colon>nat) = x + x"
blanchet@33197
   477
nitpick [expect = genuine]
blanchet@33197
   478
oops
blanchet@33197
   479
blanchet@33197
   480
lemma "(x\<Colon>nat) - y + y = x"
blanchet@33197
   481
nitpick [expect = genuine]
blanchet@33197
   482
oops
blanchet@33197
   483
blanchet@33197
   484
lemma "(x\<Colon>nat) = x * x"
blanchet@33197
   485
nitpick [expect = genuine]
blanchet@33197
   486
oops
blanchet@33197
   487
blanchet@33197
   488
lemma "(x\<Colon>nat) < x + y"
blanchet@33197
   489
nitpick [card = 1, expect = genuine]
blanchet@33197
   490
nitpick [card = 2-5, expect = genuine]
blanchet@33197
   491
oops
blanchet@33197
   492
blanchet@33197
   493
text {* \<times> *}
blanchet@33197
   494
blanchet@33197
   495
lemma "P (x\<Colon>'a\<times>'b)"
blanchet@33197
   496
nitpick [expect = genuine]
blanchet@33197
   497
oops
blanchet@33197
   498
blanchet@33197
   499
lemma "\<forall>x\<Colon>'a\<times>'b. P x"
blanchet@33197
   500
nitpick [expect = genuine]
blanchet@33197
   501
oops
blanchet@33197
   502
blanchet@33197
   503
lemma "P (x, y)"
blanchet@33197
   504
nitpick [expect = genuine]
blanchet@33197
   505
oops
blanchet@33197
   506
blanchet@33197
   507
lemma "P (fst x)"
blanchet@33197
   508
nitpick [expect = genuine]
blanchet@33197
   509
oops
blanchet@33197
   510
blanchet@33197
   511
lemma "P (snd x)"
blanchet@33197
   512
nitpick [expect = genuine]
blanchet@33197
   513
oops
blanchet@33197
   514
blanchet@33197
   515
lemma "P Pair"
blanchet@33197
   516
nitpick [expect = genuine]
blanchet@33197
   517
oops
blanchet@33197
   518
blanchet@33197
   519
lemma "prod_rec f p = f (fst p) (snd p)"
blanchet@33197
   520
nitpick [expect = none]
blanchet@33197
   521
by (case_tac p) auto
blanchet@33197
   522
blanchet@33197
   523
lemma "prod_rec f (a, b) = f a b"
blanchet@33197
   524
nitpick [expect = none]
blanchet@33197
   525
by auto
blanchet@33197
   526
blanchet@33197
   527
lemma "P (prod_rec f x)"
blanchet@33197
   528
nitpick [expect = genuine]
blanchet@33197
   529
oops
blanchet@33197
   530
blanchet@33197
   531
lemma "P (case x of Pair a b \<Rightarrow> f a b)"
blanchet@33197
   532
nitpick [expect = genuine]
blanchet@33197
   533
oops
blanchet@33197
   534
blanchet@33197
   535
subsubsection {* Subtypes (typedef), typedecl *}
blanchet@33197
   536
blanchet@33197
   537
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
blanchet@33197
   538
blanchet@33197
   539
typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
blanchet@33197
   540
by auto
blanchet@33197
   541
blanchet@33197
   542
lemma "(x\<Colon>'a myTdef) = y"
blanchet@33197
   543
nitpick [expect = genuine]
blanchet@33197
   544
oops
blanchet@33197
   545
blanchet@33197
   546
typedecl myTdecl
blanchet@33197
   547
blanchet@33197
   548
typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
blanchet@33197
   549
by auto
blanchet@33197
   550
blanchet@33197
   551
lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
blanchet@33197
   552
nitpick [expect = genuine]
blanchet@33197
   553
oops
blanchet@33197
   554
blanchet@33197
   555
subsubsection {* Inductive Datatypes *}
blanchet@33197
   556
blanchet@33197
   557
text {* unit *}
blanchet@33197
   558
blanchet@33197
   559
lemma "P (x\<Colon>unit)"
blanchet@33197
   560
nitpick [expect = genuine]
blanchet@33197
   561
oops
blanchet@33197
   562
blanchet@33197
   563
lemma "\<forall>x\<Colon>unit. P x"
blanchet@33197
   564
nitpick [expect = genuine]
blanchet@33197
   565
oops
blanchet@33197
   566
blanchet@33197
   567
lemma "P ()"
blanchet@33197
   568
nitpick [expect = genuine]
blanchet@33197
   569
oops
blanchet@33197
   570
blanchet@33197
   571
lemma "unit_rec u x = u"
blanchet@33197
   572
nitpick [expect = none]
blanchet@33197
   573
apply simp
blanchet@33197
   574
done
blanchet@33197
   575
blanchet@33197
   576
lemma "P (unit_rec u x)"
blanchet@33197
   577
nitpick [expect = genuine]
blanchet@33197
   578
oops
blanchet@33197
   579
blanchet@33197
   580
lemma "P (case x of () \<Rightarrow> u)"
blanchet@33197
   581
nitpick [expect = genuine]
blanchet@33197
   582
oops
blanchet@33197
   583
blanchet@33197
   584
text {* option *}
blanchet@33197
   585
blanchet@33197
   586
lemma "P (x\<Colon>'a option)"
blanchet@33197
   587
nitpick [expect = genuine]
blanchet@33197
   588
oops
blanchet@33197
   589
blanchet@33197
   590
lemma "\<forall>x\<Colon>'a option. P x"
blanchet@33197
   591
nitpick [expect = genuine]
blanchet@33197
   592
oops
blanchet@33197
   593
blanchet@33197
   594
lemma "P None"
blanchet@33197
   595
nitpick [expect = genuine]
blanchet@33197
   596
oops
blanchet@33197
   597
blanchet@33197
   598
lemma "P (Some x)"
blanchet@33197
   599
nitpick [expect = genuine]
blanchet@33197
   600
oops
blanchet@33197
   601
blanchet@33197
   602
lemma "option_rec n s None = n"
blanchet@33197
   603
nitpick [expect = none]
blanchet@33197
   604
apply simp
blanchet@33197
   605
done
blanchet@33197
   606
blanchet@33197
   607
lemma "option_rec n s (Some x) = s x"
blanchet@33197
   608
nitpick [expect = none]
blanchet@33197
   609
apply simp
blanchet@33197
   610
done
blanchet@33197
   611
blanchet@33197
   612
lemma "P (option_rec n s x)"
blanchet@33197
   613
nitpick [expect = genuine]
blanchet@33197
   614
oops
blanchet@33197
   615
blanchet@33197
   616
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
blanchet@33197
   617
nitpick [expect = genuine]
blanchet@33197
   618
oops
blanchet@33197
   619
blanchet@33197
   620
text {* + *}
blanchet@33197
   621
blanchet@33197
   622
lemma "P (x\<Colon>'a+'b)"
blanchet@33197
   623
nitpick [expect = genuine]
blanchet@33197
   624
oops
blanchet@33197
   625
blanchet@33197
   626
lemma "\<forall>x\<Colon>'a+'b. P x"
blanchet@33197
   627
nitpick [expect = genuine]
blanchet@33197
   628
oops
blanchet@33197
   629
blanchet@33197
   630
lemma "P (Inl x)"
blanchet@33197
   631
nitpick [expect = genuine]
blanchet@33197
   632
oops
blanchet@33197
   633
blanchet@33197
   634
lemma "P (Inr x)"
blanchet@33197
   635
nitpick [expect = genuine]
blanchet@33197
   636
oops
blanchet@33197
   637
blanchet@33197
   638
lemma "P Inl"
blanchet@33197
   639
nitpick [expect = genuine]
blanchet@33197
   640
oops
blanchet@33197
   641
blanchet@33197
   642
lemma "sum_rec l r (Inl x) = l x"
blanchet@33197
   643
nitpick [expect = none]
blanchet@33197
   644
apply simp
blanchet@33197
   645
done
blanchet@33197
   646
blanchet@33197
   647
lemma "sum_rec l r (Inr x) = r x"
blanchet@33197
   648
nitpick [expect = none]
blanchet@33197
   649
apply simp
blanchet@33197
   650
done
blanchet@33197
   651
blanchet@33197
   652
lemma "P (sum_rec l r x)"
blanchet@33197
   653
nitpick [expect = genuine]
blanchet@33197
   654
oops
blanchet@33197
   655
blanchet@33197
   656
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
blanchet@33197
   657
nitpick [expect = genuine]
blanchet@33197
   658
oops
blanchet@33197
   659
blanchet@33197
   660
text {* Non-recursive datatypes *}
blanchet@33197
   661
blanchet@33197
   662
datatype T1 = A | B
blanchet@33197
   663
blanchet@33197
   664
lemma "P (x\<Colon>T1)"
blanchet@33197
   665
nitpick [expect = genuine]
blanchet@33197
   666
oops
blanchet@33197
   667
blanchet@33197
   668
lemma "\<forall>x\<Colon>T1. P x"
blanchet@33197
   669
nitpick [expect = genuine]
blanchet@33197
   670
oops
blanchet@33197
   671
blanchet@33197
   672
lemma "P A"
blanchet@33197
   673
nitpick [expect = genuine]
blanchet@33197
   674
oops
blanchet@33197
   675
blanchet@33197
   676
lemma "P B"
blanchet@33197
   677
nitpick [expect = genuine]
blanchet@33197
   678
oops
blanchet@33197
   679
blanchet@33197
   680
lemma "T1_rec a b A = a"
blanchet@33197
   681
nitpick [expect = none]
blanchet@33197
   682
apply simp
blanchet@33197
   683
done
blanchet@33197
   684
blanchet@33197
   685
lemma "T1_rec a b B = b"
blanchet@33197
   686
nitpick [expect = none]
blanchet@33197
   687
apply simp
blanchet@33197
   688
done
blanchet@33197
   689
blanchet@33197
   690
lemma "P (T1_rec a b x)"
blanchet@33197
   691
nitpick [expect = genuine]
blanchet@33197
   692
oops
blanchet@33197
   693
blanchet@33197
   694
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
blanchet@33197
   695
nitpick [expect = genuine]
blanchet@33197
   696
oops
blanchet@33197
   697
blanchet@33197
   698
datatype 'a T2 = C T1 | D 'a
blanchet@33197
   699
blanchet@33197
   700
lemma "P (x\<Colon>'a T2)"
blanchet@33197
   701
nitpick [expect = genuine]
blanchet@33197
   702
oops
blanchet@33197
   703
blanchet@33197
   704
lemma "\<forall>x\<Colon>'a T2. P x"
blanchet@33197
   705
nitpick [expect = genuine]
blanchet@33197
   706
oops
blanchet@33197
   707
blanchet@33197
   708
lemma "P D"
blanchet@33197
   709
nitpick [expect = genuine]
blanchet@33197
   710
oops
blanchet@33197
   711
blanchet@33197
   712
lemma "T2_rec c d (C x) = c x"
blanchet@33197
   713
nitpick [expect = none]
blanchet@33197
   714
apply simp
blanchet@33197
   715
done
blanchet@33197
   716
blanchet@33197
   717
lemma "T2_rec c d (D x) = d x"
blanchet@33197
   718
nitpick [expect = none]
blanchet@33197
   719
apply simp
blanchet@33197
   720
done
blanchet@33197
   721
blanchet@33197
   722
lemma "P (T2_rec c d x)"
blanchet@33197
   723
nitpick [expect = genuine]
blanchet@33197
   724
oops
blanchet@33197
   725
blanchet@33197
   726
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
blanchet@33197
   727
nitpick [expect = genuine]
blanchet@33197
   728
oops
blanchet@33197
   729
blanchet@33197
   730
datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
blanchet@33197
   731
blanchet@33197
   732
lemma "P (x\<Colon>('a, 'b) T3)"
blanchet@33197
   733
nitpick [expect = genuine]
blanchet@33197
   734
oops
blanchet@33197
   735
blanchet@33197
   736
lemma "\<forall>x\<Colon>('a, 'b) T3. P x"
blanchet@33197
   737
nitpick [expect = genuine]
blanchet@33197
   738
oops
blanchet@33197
   739
blanchet@33197
   740
lemma "P E"
blanchet@33197
   741
nitpick [expect = genuine]
blanchet@33197
   742
oops
blanchet@33197
   743
blanchet@33197
   744
lemma "T3_rec e (E x) = e x"
blanchet@33197
   745
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
   746
apply simp
blanchet@33197
   747
done
blanchet@33197
   748
blanchet@33197
   749
lemma "P (T3_rec e x)"
blanchet@33197
   750
nitpick [expect = genuine]
blanchet@33197
   751
oops
blanchet@33197
   752
blanchet@33197
   753
lemma "P (case x of E f \<Rightarrow> e f)"
blanchet@33197
   754
nitpick [expect = genuine]
blanchet@33197
   755
oops
blanchet@33197
   756
blanchet@33197
   757
text {* Recursive datatypes *}
blanchet@33197
   758
blanchet@33197
   759
text {* nat *}
blanchet@33197
   760
blanchet@33197
   761
lemma "P (x\<Colon>nat)"
blanchet@33197
   762
nitpick [expect = genuine]
blanchet@33197
   763
oops
blanchet@33197
   764
blanchet@33197
   765
lemma "\<forall>x\<Colon>nat. P x"
blanchet@33197
   766
nitpick [expect = genuine]
blanchet@33197
   767
oops
blanchet@33197
   768
blanchet@33197
   769
lemma "P (Suc 0)"
blanchet@33197
   770
nitpick [expect = genuine]
blanchet@33197
   771
oops
blanchet@33197
   772
blanchet@33197
   773
lemma "P Suc"
blanchet@33197
   774
nitpick [card = 1\<midarrow>7, expect = none]
blanchet@33197
   775
oops
blanchet@33197
   776
blanchet@33197
   777
lemma "nat_rec zero suc 0 = zero"
blanchet@33197
   778
nitpick [expect = none]
blanchet@33197
   779
apply simp
blanchet@33197
   780
done
blanchet@33197
   781
blanchet@33197
   782
lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
blanchet@33197
   783
nitpick [expect = none]
blanchet@33197
   784
apply simp
blanchet@33197
   785
done
blanchet@33197
   786
blanchet@33197
   787
lemma "P (nat_rec zero suc x)"
blanchet@33197
   788
nitpick [expect = genuine]
blanchet@33197
   789
oops
blanchet@33197
   790
blanchet@33197
   791
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
blanchet@33197
   792
nitpick [expect = genuine]
blanchet@33197
   793
oops
blanchet@33197
   794
blanchet@33197
   795
text {* 'a list *}
blanchet@33197
   796
blanchet@33197
   797
lemma "P (xs\<Colon>'a list)"
blanchet@33197
   798
nitpick [expect = genuine]
blanchet@33197
   799
oops
blanchet@33197
   800
blanchet@33197
   801
lemma "\<forall>xs\<Colon>'a list. P xs"
blanchet@33197
   802
nitpick [expect = genuine]
blanchet@33197
   803
oops
blanchet@33197
   804
blanchet@33197
   805
lemma "P [x, y]"
blanchet@33197
   806
nitpick [expect = genuine]
blanchet@33197
   807
oops
blanchet@33197
   808
blanchet@33197
   809
lemma "list_rec nil cons [] = nil"
blanchet@33197
   810
nitpick [expect = none]
blanchet@33197
   811
apply simp
blanchet@33197
   812
done
blanchet@33197
   813
blanchet@33197
   814
lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
blanchet@33197
   815
nitpick [expect = none]
blanchet@33197
   816
apply simp
blanchet@33197
   817
done
blanchet@33197
   818
blanchet@33197
   819
lemma "P (list_rec nil cons xs)"
blanchet@33197
   820
nitpick [expect = genuine]
blanchet@33197
   821
oops
blanchet@33197
   822
blanchet@33197
   823
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
blanchet@33197
   824
nitpick [expect = genuine]
blanchet@33197
   825
oops
blanchet@33197
   826
blanchet@33197
   827
lemma "(xs\<Colon>'a list) = ys"
blanchet@33197
   828
nitpick [expect = genuine]
blanchet@33197
   829
oops
blanchet@33197
   830
blanchet@33197
   831
lemma "a # xs = b # xs"
blanchet@33197
   832
nitpick [expect = genuine]
blanchet@33197
   833
oops
blanchet@33197
   834
blanchet@33197
   835
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
blanchet@33197
   836
blanchet@33197
   837
lemma "P (x\<Colon>BitList)"
blanchet@33197
   838
nitpick [expect = genuine]
blanchet@33197
   839
oops
blanchet@33197
   840
blanchet@33197
   841
lemma "\<forall>x\<Colon>BitList. P x"
blanchet@33197
   842
nitpick [expect = genuine]
blanchet@33197
   843
oops
blanchet@33197
   844
blanchet@33197
   845
lemma "P (Bit0 (Bit1 BitListNil))"
blanchet@33197
   846
nitpick [expect = genuine]
blanchet@33197
   847
oops
blanchet@33197
   848
blanchet@33197
   849
lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
blanchet@33197
   850
nitpick [expect = none]
blanchet@33197
   851
apply simp
blanchet@33197
   852
done
blanchet@33197
   853
blanchet@33197
   854
lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
blanchet@33197
   855
nitpick [expect = none]
blanchet@33197
   856
apply simp
blanchet@33197
   857
done
blanchet@33197
   858
blanchet@33197
   859
lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
blanchet@33197
   860
nitpick [expect = none]
blanchet@33197
   861
apply simp
blanchet@33197
   862
done
blanchet@33197
   863
blanchet@33197
   864
lemma "P (BitList_rec nil bit0 bit1 x)"
blanchet@33197
   865
nitpick [expect = genuine]
blanchet@33197
   866
oops
blanchet@33197
   867
blanchet@33197
   868
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
blanchet@33197
   869
blanchet@33197
   870
lemma "P (x\<Colon>'a BinTree)"
blanchet@33197
   871
nitpick [expect = genuine]
blanchet@33197
   872
oops
blanchet@33197
   873
blanchet@33197
   874
lemma "\<forall>x\<Colon>'a BinTree. P x"
blanchet@33197
   875
nitpick [expect = genuine]
blanchet@33197
   876
oops
blanchet@33197
   877
blanchet@33197
   878
lemma "P (Node (Leaf x) (Leaf y))"
blanchet@33197
   879
nitpick [expect = genuine]
blanchet@33197
   880
oops
blanchet@33197
   881
blanchet@33197
   882
lemma "BinTree_rec l n (Leaf x) = l x"
blanchet@33197
   883
nitpick [expect = none]
blanchet@33197
   884
apply simp
blanchet@33197
   885
done
blanchet@33197
   886
blanchet@33197
   887
lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
blanchet@35087
   888
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
   889
apply simp
blanchet@33197
   890
done
blanchet@33197
   891
blanchet@33197
   892
lemma "P (BinTree_rec l n x)"
blanchet@33197
   893
nitpick [expect = genuine]
blanchet@33197
   894
oops
blanchet@33197
   895
blanchet@33197
   896
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
blanchet@33197
   897
nitpick [expect = genuine]
blanchet@33197
   898
oops
blanchet@33197
   899
blanchet@33197
   900
text {* Mutually recursive datatypes *}
blanchet@33197
   901
blanchet@33197
   902
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
blanchet@33197
   903
 and 'a bexp = Equal "'a aexp" "'a aexp"
blanchet@33197
   904
blanchet@33197
   905
lemma "P (x\<Colon>'a aexp)"
blanchet@33197
   906
nitpick [expect = genuine]
blanchet@33197
   907
oops
blanchet@33197
   908
blanchet@33197
   909
lemma "\<forall>x\<Colon>'a aexp. P x"
blanchet@33197
   910
nitpick [expect = genuine]
blanchet@33197
   911
oops
blanchet@33197
   912
blanchet@33197
   913
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
blanchet@33197
   914
nitpick [expect = genuine]
blanchet@33197
   915
oops
blanchet@33197
   916
blanchet@33197
   917
lemma "P (x\<Colon>'a bexp)"
blanchet@33197
   918
nitpick [expect = genuine]
blanchet@33197
   919
oops
blanchet@33197
   920
blanchet@33197
   921
lemma "\<forall>x\<Colon>'a bexp. P x"
blanchet@33197
   922
nitpick [expect = genuine]
blanchet@33197
   923
oops
blanchet@33197
   924
blanchet@33197
   925
lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
blanchet@33197
   926
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
   927
apply simp
blanchet@33197
   928
done
blanchet@33197
   929
blanchet@33197
   930
lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
blanchet@33197
   931
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
   932
apply simp
blanchet@33197
   933
done
blanchet@33197
   934
blanchet@33197
   935
lemma "P (aexp_bexp_rec_1 number ite equal x)"
blanchet@33197
   936
nitpick [expect = genuine]
blanchet@33197
   937
oops
blanchet@33197
   938
blanchet@33197
   939
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
blanchet@33197
   940
nitpick [expect = genuine]
blanchet@33197
   941
oops
blanchet@33197
   942
blanchet@33197
   943
lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
blanchet@33197
   944
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
   945
apply simp
blanchet@33197
   946
done
blanchet@33197
   947
blanchet@33197
   948
lemma "P (aexp_bexp_rec_2 number ite equal x)"
blanchet@33197
   949
nitpick [expect = genuine]
blanchet@33197
   950
oops
blanchet@33197
   951
blanchet@33197
   952
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
blanchet@33197
   953
nitpick [expect = genuine]
blanchet@33197
   954
oops
blanchet@33197
   955
blanchet@33197
   956
datatype X = A | B X | C Y
blanchet@33197
   957
     and Y = D X | E Y | F
blanchet@33197
   958
blanchet@33197
   959
lemma "P (x\<Colon>X)"
blanchet@33197
   960
nitpick [expect = genuine]
blanchet@33197
   961
oops
blanchet@33197
   962
blanchet@33197
   963
lemma "P (y\<Colon>Y)"
blanchet@33197
   964
nitpick [expect = genuine]
blanchet@33197
   965
oops
blanchet@33197
   966
blanchet@33197
   967
lemma "P (B (B A))"
blanchet@33197
   968
nitpick [expect = genuine]
blanchet@33197
   969
oops
blanchet@33197
   970
blanchet@33197
   971
lemma "P (B (C F))"
blanchet@33197
   972
nitpick [expect = genuine]
blanchet@33197
   973
oops
blanchet@33197
   974
blanchet@33197
   975
lemma "P (C (D A))"
blanchet@33197
   976
nitpick [expect = genuine]
blanchet@33197
   977
oops
blanchet@33197
   978
blanchet@33197
   979
lemma "P (C (E F))"
blanchet@33197
   980
nitpick [expect = genuine]
blanchet@33197
   981
oops
blanchet@33197
   982
blanchet@33197
   983
lemma "P (D (B A))"
blanchet@33197
   984
nitpick [expect = genuine]
blanchet@33197
   985
oops
blanchet@33197
   986
blanchet@33197
   987
lemma "P (D (C F))"
blanchet@33197
   988
nitpick [expect = genuine]
blanchet@33197
   989
oops
blanchet@33197
   990
blanchet@33197
   991
lemma "P (E (D A))"
blanchet@33197
   992
nitpick [expect = genuine]
blanchet@33197
   993
oops
blanchet@33197
   994
blanchet@33197
   995
lemma "P (E (E F))"
blanchet@33197
   996
nitpick [expect = genuine]
blanchet@33197
   997
oops
blanchet@33197
   998
blanchet@33197
   999
lemma "P (C (D (C F)))"
blanchet@33197
  1000
nitpick [expect = genuine]
blanchet@33197
  1001
oops
blanchet@33197
  1002
blanchet@33197
  1003
lemma "X_Y_rec_1 a b c d e f A = a"
blanchet@33197
  1004
nitpick [expect = none]
blanchet@33197
  1005
apply simp
blanchet@33197
  1006
done
blanchet@33197
  1007
blanchet@33197
  1008
lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
blanchet@33197
  1009
nitpick [expect = none]
blanchet@33197
  1010
apply simp
blanchet@33197
  1011
done
blanchet@33197
  1012
blanchet@33197
  1013
lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
blanchet@33197
  1014
nitpick [expect = none]
blanchet@33197
  1015
apply simp
blanchet@33197
  1016
done
blanchet@33197
  1017
blanchet@33197
  1018
lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
blanchet@33197
  1019
nitpick [expect = none]
blanchet@33197
  1020
apply simp
blanchet@33197
  1021
done
blanchet@33197
  1022
blanchet@33197
  1023
lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
blanchet@33197
  1024
nitpick [expect = none]
blanchet@33197
  1025
apply simp
blanchet@33197
  1026
done
blanchet@33197
  1027
blanchet@33197
  1028
lemma "X_Y_rec_2 a b c d e f F = f"
blanchet@33197
  1029
nitpick [expect = none]
blanchet@33197
  1030
apply simp
blanchet@33197
  1031
done
blanchet@33197
  1032
blanchet@33197
  1033
lemma "P (X_Y_rec_1 a b c d e f x)"
blanchet@33197
  1034
nitpick [expect = genuine]
blanchet@33197
  1035
oops
blanchet@33197
  1036
blanchet@33197
  1037
lemma "P (X_Y_rec_2 a b c d e f y)"
blanchet@33197
  1038
nitpick [expect = genuine]
blanchet@33197
  1039
oops
blanchet@33197
  1040
blanchet@33197
  1041
text {* Other datatype examples *}
blanchet@33197
  1042
blanchet@33197
  1043
text {* Indirect recursion is implemented via mutual recursion. *}
blanchet@33197
  1044
blanchet@33197
  1045
datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
blanchet@33197
  1046
blanchet@33197
  1047
lemma "P (x\<Colon>XOpt)"
blanchet@33197
  1048
nitpick [expect = genuine]
blanchet@33197
  1049
oops
blanchet@33197
  1050
blanchet@33197
  1051
lemma "P (CX None)"
blanchet@33197
  1052
nitpick [expect = genuine]
blanchet@33197
  1053
oops
blanchet@33197
  1054
blanchet@33197
  1055
lemma "P (CX (Some (CX None)))"
blanchet@33197
  1056
nitpick [expect = genuine]
blanchet@33197
  1057
oops
blanchet@33197
  1058
blanchet@33197
  1059
lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1060
nitpick [card = 1\<midarrow>6, expect = none]
blanchet@33197
  1061
apply simp
blanchet@33197
  1062
done
blanchet@33197
  1063
blanchet@33197
  1064
lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
blanchet@33197
  1065
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
  1066
apply simp
blanchet@33197
  1067
done
blanchet@33197
  1068
blanchet@33197
  1069
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
blanchet@33197
  1070
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
  1071
apply simp
blanchet@33197
  1072
done
blanchet@33197
  1073
blanchet@33197
  1074
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1075
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
  1076
apply simp
blanchet@33197
  1077
done
blanchet@33197
  1078
blanchet@33197
  1079
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
blanchet@33197
  1080
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
  1081
apply simp
blanchet@33197
  1082
done
blanchet@33197
  1083
blanchet@33197
  1084
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1085
nitpick [card = 1\<midarrow>4, expect = none]
blanchet@33197
  1086
apply simp
blanchet@33197
  1087
done
blanchet@33197
  1088
blanchet@33197
  1089
lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1090
nitpick [expect = genuine]
blanchet@33197
  1091
oops
blanchet@33197
  1092
blanchet@33197
  1093
lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1094
nitpick [expect = genuine]
blanchet@33197
  1095
oops
blanchet@33197
  1096
blanchet@33197
  1097
lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
blanchet@33197
  1098
nitpick [expect = genuine]
blanchet@33197
  1099
oops
blanchet@33197
  1100
blanchet@33197
  1101
datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
blanchet@33197
  1102
blanchet@33197
  1103
lemma "P (x\<Colon>'a YOpt)"
blanchet@33197
  1104
nitpick [expect = genuine]
blanchet@33197
  1105
oops
blanchet@33197
  1106
blanchet@33197
  1107
lemma "P (CY None)"
blanchet@33197
  1108
nitpick [expect = genuine]
blanchet@33197
  1109
oops
blanchet@33197
  1110
blanchet@33197
  1111
lemma "P (CY (Some (\<lambda>a. CY None)))"
blanchet@33197
  1112
nitpick [expect = genuine]
blanchet@33197
  1113
oops
blanchet@33197
  1114
blanchet@33197
  1115
lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
blanchet@33197
  1116
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
  1117
apply simp
blanchet@33197
  1118
done
blanchet@33197
  1119
blanchet@33197
  1120
lemma "YOpt_rec_2 cy n s None = n"
blanchet@33197
  1121
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
  1122
apply simp
blanchet@33197
  1123
done
blanchet@33197
  1124
blanchet@33197
  1125
lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
blanchet@33197
  1126
nitpick [card = 1\<midarrow>2, expect = none]
blanchet@33197
  1127
apply simp
blanchet@33197
  1128
done
blanchet@33197
  1129
blanchet@33197
  1130
lemma "P (YOpt_rec_1 cy n s x)"
blanchet@33197
  1131
nitpick [expect = genuine]
blanchet@33197
  1132
oops
blanchet@33197
  1133
blanchet@33197
  1134
lemma "P (YOpt_rec_2 cy n s x)"
blanchet@33197
  1135
nitpick [expect = genuine]
blanchet@33197
  1136
oops
blanchet@33197
  1137
blanchet@33197
  1138
datatype Trie = TR "Trie list"
blanchet@33197
  1139
blanchet@33197
  1140
lemma "P (x\<Colon>Trie)"
blanchet@33197
  1141
nitpick [expect = genuine]
blanchet@33197
  1142
oops
blanchet@33197
  1143
blanchet@33197
  1144
lemma "\<forall>x\<Colon>Trie. P x"
blanchet@33197
  1145
nitpick [expect = genuine]
blanchet@33197
  1146
oops
blanchet@33197
  1147
blanchet@33197
  1148
lemma "P (TR [TR []])"
blanchet@33197
  1149
nitpick [expect = genuine]
blanchet@33197
  1150
oops
blanchet@33197
  1151
blanchet@33197
  1152
lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
blanchet@33197
  1153
nitpick [card = 1\<midarrow>6, expect = none]
blanchet@33197
  1154
apply simp
blanchet@33197
  1155
done
blanchet@33197
  1156
blanchet@33197
  1157
lemma "Trie_rec_2 tr nil cons [] = nil"
blanchet@33197
  1158
nitpick [card = 1\<midarrow>6, expect = none]
blanchet@33197
  1159
apply simp
blanchet@33197
  1160
done
blanchet@33197
  1161
blanchet@33197
  1162
lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
blanchet@33197
  1163
nitpick [card = 1\<midarrow>6, expect = none]
blanchet@33197
  1164
apply simp
blanchet@33197
  1165
done
blanchet@33197
  1166
blanchet@33197
  1167
lemma "P (Trie_rec_1 tr nil cons x)"
blanchet@33197
  1168
nitpick [card = 1, expect = genuine]
blanchet@33197
  1169
oops
blanchet@33197
  1170
blanchet@33197
  1171
lemma "P (Trie_rec_2 tr nil cons x)"
blanchet@33197
  1172
nitpick [card = 1, expect = genuine]
blanchet@33197
  1173
oops
blanchet@33197
  1174
blanchet@33197
  1175
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
blanchet@33197
  1176
blanchet@33197
  1177
lemma "P (x\<Colon>InfTree)"
blanchet@33197
  1178
nitpick [expect = genuine]
blanchet@33197
  1179
oops
blanchet@33197
  1180
blanchet@33197
  1181
lemma "\<forall>x\<Colon>InfTree. P x"
blanchet@33197
  1182
nitpick [expect = genuine]
blanchet@33197
  1183
oops
blanchet@33197
  1184
blanchet@33197
  1185
lemma "P (Node (\<lambda>n. Leaf))"
blanchet@33197
  1186
nitpick [expect = genuine]
blanchet@33197
  1187
oops
blanchet@33197
  1188
blanchet@33197
  1189
lemma "InfTree_rec leaf node Leaf = leaf"
blanchet@33197
  1190
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1191
apply simp
blanchet@33197
  1192
done
blanchet@33197
  1193
blanchet@33197
  1194
lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
blanchet@33197
  1195
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1196
apply simp
blanchet@33197
  1197
done
blanchet@33197
  1198
blanchet@33197
  1199
lemma "P (InfTree_rec leaf node x)"
blanchet@33197
  1200
nitpick [expect = genuine]
blanchet@33197
  1201
oops
blanchet@33197
  1202
blanchet@33197
  1203
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
blanchet@33197
  1204
blanchet@33197
  1205
lemma "P (x\<Colon>'a lambda)"
blanchet@33197
  1206
nitpick [expect = genuine]
blanchet@33197
  1207
oops
blanchet@33197
  1208
blanchet@33197
  1209
lemma "\<forall>x\<Colon>'a lambda. P x"
blanchet@33197
  1210
nitpick [expect = genuine]
blanchet@33197
  1211
oops
blanchet@33197
  1212
blanchet@33197
  1213
lemma "P (Lam (\<lambda>a. Var a))"
blanchet@33197
  1214
nitpick [card = 1\<midarrow>5, expect = none]
blanchet@33197
  1215
nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
blanchet@33197
  1216
oops
blanchet@33197
  1217
blanchet@33197
  1218
lemma "lambda_rec var app lam (Var x) = var x"
blanchet@33197
  1219
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1220
apply simp
blanchet@33197
  1221
done
blanchet@33197
  1222
blanchet@33197
  1223
lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
blanchet@33197
  1224
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1225
apply simp
blanchet@33197
  1226
done
blanchet@33197
  1227
blanchet@33197
  1228
lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
blanchet@33197
  1229
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1230
apply simp
blanchet@33197
  1231
done
blanchet@33197
  1232
blanchet@33197
  1233
lemma "P (lambda_rec v a l x)"
blanchet@33197
  1234
nitpick [expect = genuine]
blanchet@33197
  1235
oops
blanchet@33197
  1236
blanchet@33197
  1237
text {* Taken from "Inductive datatypes in HOL", p. 8: *}
blanchet@33197
  1238
blanchet@33197
  1239
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
blanchet@33197
  1240
datatype 'c U = E "('c, 'c U) T"
blanchet@33197
  1241
blanchet@33197
  1242
lemma "P (x\<Colon>'c U)"
blanchet@33197
  1243
nitpick [expect = genuine]
blanchet@33197
  1244
oops
blanchet@33197
  1245
blanchet@33197
  1246
lemma "\<forall>x\<Colon>'c U. P x"
blanchet@33197
  1247
nitpick [expect = genuine]
blanchet@33197
  1248
oops
blanchet@33197
  1249
blanchet@33197
  1250
lemma "P (E (C (\<lambda>a. True)))"
blanchet@33197
  1251
nitpick [expect = genuine]
blanchet@33197
  1252
oops
blanchet@33197
  1253
blanchet@33197
  1254
lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
blanchet@33197
  1255
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1256
apply simp
blanchet@33197
  1257
done
blanchet@33197
  1258
blanchet@33197
  1259
lemma "U_rec_2 e c d nil cons (C x) = c x"
blanchet@33197
  1260
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1261
apply simp
blanchet@33197
  1262
done
blanchet@33197
  1263
blanchet@33197
  1264
lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
blanchet@33197
  1265
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1266
apply simp
blanchet@33197
  1267
done
blanchet@33197
  1268
blanchet@33197
  1269
lemma "U_rec_3 e c d nil cons [] = nil"
blanchet@33197
  1270
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1271
apply simp
blanchet@33197
  1272
done
blanchet@33197
  1273
blanchet@33197
  1274
lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
blanchet@33197
  1275
nitpick [card = 1\<midarrow>3, expect = none]
blanchet@33197
  1276
apply simp
blanchet@33197
  1277
done
blanchet@33197
  1278
blanchet@33197
  1279
lemma "P (U_rec_1 e c d nil cons x)"
blanchet@33197
  1280
nitpick [expect = genuine]
blanchet@33197
  1281
oops
blanchet@33197
  1282
blanchet@33197
  1283
lemma "P (U_rec_2 e c d nil cons x)"
blanchet@33197
  1284
nitpick [card = 1, expect = genuine]
blanchet@33197
  1285
oops
blanchet@33197
  1286
blanchet@33197
  1287
lemma "P (U_rec_3 e c d nil cons x)"
blanchet@33197
  1288
nitpick [card = 1, expect = genuine]
blanchet@33197
  1289
oops
blanchet@33197
  1290
blanchet@33197
  1291
subsubsection {* Records *}
blanchet@33197
  1292
blanchet@33197
  1293
record ('a, 'b) point =
blanchet@33197
  1294
  xpos :: 'a
blanchet@33197
  1295
  ypos :: 'b
blanchet@33197
  1296
blanchet@33197
  1297
lemma "(x\<Colon>('a, 'b) point) = y"
blanchet@33197
  1298
nitpick [expect = genuine]
blanchet@33197
  1299
oops
blanchet@33197
  1300
blanchet@33197
  1301
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
blanchet@33197
  1302
  ext :: 'c
blanchet@33197
  1303
blanchet@33197
  1304
lemma "(x\<Colon>('a, 'b, 'c) extpoint) = y"
blanchet@33197
  1305
nitpick [expect = genuine]
blanchet@33197
  1306
oops
blanchet@33197
  1307
blanchet@33197
  1308
subsubsection {* Inductively Defined Sets *}
blanchet@33197
  1309
blanchet@33197
  1310
inductive_set undefinedSet :: "'a set" where
blanchet@33197
  1311
"undefined \<in> undefinedSet"
blanchet@33197
  1312
blanchet@33197
  1313
lemma "x \<in> undefinedSet"
blanchet@33197
  1314
nitpick [expect = genuine]
blanchet@33197
  1315
oops
blanchet@33197
  1316
blanchet@33197
  1317
inductive_set evenCard :: "'a set set"
blanchet@33197
  1318
where
blanchet@33197
  1319
"{} \<in> evenCard" |
blanchet@33197
  1320
"\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
blanchet@33197
  1321
blanchet@33197
  1322
lemma "S \<in> evenCard"
blanchet@33197
  1323
nitpick [expect = genuine]
blanchet@33197
  1324
oops
blanchet@33197
  1325
blanchet@33197
  1326
inductive_set
blanchet@33197
  1327
even :: "nat set"
blanchet@33197
  1328
and odd :: "nat set"
blanchet@33197
  1329
where
blanchet@33197
  1330
"0 \<in> even" |
blanchet@33197
  1331
"n \<in> even \<Longrightarrow> Suc n \<in> odd" |
blanchet@33197
  1332
"n \<in> odd \<Longrightarrow> Suc n \<in> even"
blanchet@33197
  1333
blanchet@33197
  1334
lemma "n \<in> odd"
blanchet@33197
  1335
nitpick [expect = genuine]
blanchet@33197
  1336
oops
blanchet@33197
  1337
blanchet@33197
  1338
consts f :: "'a \<Rightarrow> 'a"
blanchet@33197
  1339
blanchet@33197
  1340
inductive_set a_even :: "'a set" and a_odd :: "'a set" where
blanchet@33197
  1341
"undefined \<in> a_even" |
blanchet@33197
  1342
"x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
blanchet@33197
  1343
"x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
blanchet@33197
  1344
blanchet@33197
  1345
lemma "x \<in> a_odd"
blanchet@33197
  1346
nitpick [expect = genuine]
blanchet@33197
  1347
oops
blanchet@33197
  1348
blanchet@33197
  1349
subsubsection {* Examples Involving Special Functions *}
blanchet@33197
  1350
blanchet@33197
  1351
lemma "card x = 0"
blanchet@33197
  1352
nitpick [expect = genuine]
blanchet@33197
  1353
oops
blanchet@33197
  1354
blanchet@33197
  1355
lemma "finite x"
blanchet@33197
  1356
nitpick [expect = none]
blanchet@33197
  1357
oops
blanchet@33197
  1358
blanchet@33197
  1359
lemma "xs @ [] = ys @ []"
blanchet@33197
  1360
nitpick [expect = genuine]
blanchet@33197
  1361
oops
blanchet@33197
  1362
blanchet@33197
  1363
lemma "xs @ ys = ys @ xs"
blanchet@33197
  1364
nitpick [expect = genuine]
blanchet@33197
  1365
oops
blanchet@33197
  1366
blanchet@33197
  1367
lemma "f (lfp f) = lfp f"
blanchet@33197
  1368
nitpick [expect = genuine]
blanchet@33197
  1369
oops
blanchet@33197
  1370
blanchet@33197
  1371
lemma "f (gfp f) = gfp f"
blanchet@33197
  1372
nitpick [expect = genuine]
blanchet@33197
  1373
oops
blanchet@33197
  1374
blanchet@33197
  1375
lemma "lfp f = gfp f"
blanchet@33197
  1376
nitpick [expect = genuine]
blanchet@33197
  1377
oops
blanchet@33197
  1378
blanchet@33197
  1379
subsubsection {* Axiomatic Type Classes and Overloading *}
blanchet@33197
  1380
blanchet@33197
  1381
text {* A type class without axioms: *}
blanchet@33197
  1382
blanchet@33197
  1383
axclass classA
blanchet@33197
  1384
blanchet@33197
  1385
lemma "P (x\<Colon>'a\<Colon>classA)"
blanchet@33197
  1386
nitpick [expect = genuine]
blanchet@33197
  1387
oops
blanchet@33197
  1388
blanchet@33197
  1389
text {* The axiom of this type class does not contain any type variables: *}
blanchet@33197
  1390
blanchet@33197
  1391
axclass classB
blanchet@33197
  1392
classB_ax: "P \<or> \<not> P"
blanchet@33197
  1393
blanchet@33197
  1394
lemma "P (x\<Colon>'a\<Colon>classB)"
blanchet@33197
  1395
nitpick [expect = genuine]
blanchet@33197
  1396
oops
blanchet@33197
  1397
blanchet@33197
  1398
text {* An axiom with a type variable (denoting types which have at least two elements): *}
blanchet@33197
  1399
blanchet@33197
  1400
axclass classC < type
blanchet@33197
  1401
classC_ax: "\<exists>x y. x \<noteq> y"
blanchet@33197
  1402
blanchet@33197
  1403
lemma "P (x\<Colon>'a\<Colon>classC)"
blanchet@33197
  1404
nitpick [expect = genuine]
blanchet@33197
  1405
oops
blanchet@33197
  1406
blanchet@33197
  1407
lemma "\<exists>x y. (x\<Colon>'a\<Colon>classC) \<noteq> y"
blanchet@33197
  1408
nitpick [expect = none]
blanchet@33197
  1409
sorry
blanchet@33197
  1410
blanchet@33197
  1411
text {* A type class for which a constant is defined: *}
blanchet@33197
  1412
blanchet@33197
  1413
consts
blanchet@33197
  1414
classD_const :: "'a \<Rightarrow> 'a"
blanchet@33197
  1415
blanchet@33197
  1416
axclass classD < type
blanchet@33197
  1417
classD_ax: "classD_const (classD_const x) = classD_const x"
blanchet@33197
  1418
blanchet@33197
  1419
lemma "P (x\<Colon>'a\<Colon>classD)"
blanchet@33197
  1420
nitpick [expect = genuine]
blanchet@33197
  1421
oops
blanchet@33197
  1422
blanchet@33197
  1423
text {* A type class with multiple superclasses: *}
blanchet@33197
  1424
blanchet@33197
  1425
axclass classE < classC, classD
blanchet@33197
  1426
blanchet@33197
  1427
lemma "P (x\<Colon>'a\<Colon>classE)"
blanchet@33197
  1428
nitpick [expect = genuine]
blanchet@33197
  1429
oops
blanchet@33197
  1430
blanchet@33197
  1431
lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
blanchet@33197
  1432
nitpick [expect = genuine]
blanchet@33197
  1433
oops
blanchet@33197
  1434
blanchet@33197
  1435
text {* OFCLASS: *}
blanchet@33197
  1436
blanchet@33197
  1437
lemma "OFCLASS('a\<Colon>type, type_class)"
blanchet@33197
  1438
nitpick [expect = none]
blanchet@33197
  1439
apply intro_classes
blanchet@33197
  1440
done
blanchet@33197
  1441
blanchet@33197
  1442
lemma "OFCLASS('a\<Colon>classC, type_class)"
blanchet@33197
  1443
nitpick [expect = none]
blanchet@33197
  1444
apply intro_classes
blanchet@33197
  1445
done
blanchet@33197
  1446
blanchet@33197
  1447
lemma "OFCLASS('a, classB_class)"
blanchet@33197
  1448
nitpick [expect = none]
blanchet@33197
  1449
apply intro_classes
blanchet@33197
  1450
apply simp
blanchet@33197
  1451
done
blanchet@33197
  1452
blanchet@33197
  1453
lemma "OFCLASS('a\<Colon>type, classC_class)"
blanchet@33197
  1454
nitpick [expect = genuine]
blanchet@33197
  1455
oops
blanchet@33197
  1456
blanchet@33197
  1457
text {* Overloading: *}
blanchet@33197
  1458
blanchet@33197
  1459
consts inverse :: "'a \<Rightarrow> 'a"
blanchet@33197
  1460
blanchet@33197
  1461
defs (overloaded)
blanchet@33197
  1462
inverse_bool: "inverse (b\<Colon>bool) \<equiv> \<not> b"
blanchet@33197
  1463
inverse_set: "inverse (S\<Colon>'a set) \<equiv> -S"
blanchet@33197
  1464
inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
blanchet@33197
  1465
blanchet@33197
  1466
lemma "inverse b"
blanchet@33197
  1467
nitpick [expect = genuine]
blanchet@33197
  1468
oops
blanchet@33197
  1469
blanchet@33197
  1470
lemma "P (inverse (S\<Colon>'a set))"
blanchet@33197
  1471
nitpick [expect = genuine]
blanchet@33197
  1472
oops
blanchet@33197
  1473
blanchet@33197
  1474
lemma "P (inverse (p\<Colon>'a\<times>'b))"
blanchet@33197
  1475
nitpick [expect = genuine]
blanchet@33197
  1476
oops
blanchet@33197
  1477
blanchet@33197
  1478
end