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