src/HOL/ex/Refute_Examples.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18789 8a5c6fc3ad27
child 21502 7f3ea2b3bab6
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
webertj@14350
     1
(*  Title:      HOL/ex/Refute_Examples.thy
webertj@14350
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Tjark Weber
webertj@15547
     4
    Copyright   2003-2005
webertj@14350
     5
*)
webertj@14350
     6
webertj@14350
     7
(* See 'HOL/Refute.thy' for help. *)
webertj@14350
     8
webertj@14350
     9
header {* Examples for the 'refute' command *}
webertj@14350
    10
webertj@15297
    11
theory Refute_Examples imports Main
webertj@15297
    12
webertj@15297
    13
begin
webertj@14350
    14
webertj@18774
    15
refute_params [satsolver="dpll"]
webertj@18774
    16
webertj@14350
    17
lemma "P \<and> Q"
webertj@14350
    18
  apply (rule conjI)
webertj@14350
    19
  refute 1  -- {* refutes @{term "P"} *}
webertj@14350
    20
  refute 2  -- {* refutes @{term "Q"} *}
webertj@14350
    21
  refute    -- {* equivalent to 'refute 1' *}
webertj@14455
    22
    -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
webertj@14465
    23
  refute [maxsize=5]           -- {* we can override parameters ... *}
webertj@14465
    24
  refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
webertj@14350
    25
oops
webertj@14350
    26
webertj@14455
    27
section {* Examples and Test Cases *}
webertj@14350
    28
webertj@14350
    29
subsection {* Propositional logic *}
webertj@14350
    30
webertj@14350
    31
lemma "True"
webertj@14350
    32
  refute
webertj@14350
    33
  apply auto
webertj@14350
    34
done
webertj@14350
    35
webertj@14350
    36
lemma "False"
webertj@14350
    37
  refute
webertj@14350
    38
oops
webertj@14350
    39
webertj@14350
    40
lemma "P"
webertj@14350
    41
  refute
webertj@14350
    42
oops
webertj@14350
    43
webertj@14350
    44
lemma "~ P"
webertj@14350
    45
  refute
webertj@14350
    46
oops
webertj@14350
    47
webertj@14350
    48
lemma "P & Q"
webertj@14350
    49
  refute
webertj@14350
    50
oops
webertj@14350
    51
webertj@14350
    52
lemma "P | Q"
webertj@14350
    53
  refute
webertj@14350
    54
oops
webertj@14350
    55
webertj@14350
    56
lemma "P \<longrightarrow> Q"
webertj@14350
    57
  refute
webertj@14350
    58
oops
webertj@14350
    59
webertj@14350
    60
lemma "(P::bool) = Q"
webertj@14350
    61
  refute
webertj@14350
    62
oops
webertj@14350
    63
webertj@14350
    64
lemma "(P | Q) \<longrightarrow> (P & Q)"
webertj@14350
    65
  refute
webertj@14350
    66
oops
webertj@14350
    67
webertj@14350
    68
subsection {* Predicate logic *}
webertj@14350
    69
webertj@14455
    70
lemma "P x y z"
webertj@14350
    71
  refute
webertj@14350
    72
oops
webertj@14350
    73
webertj@14350
    74
lemma "P x y \<longrightarrow> P y x"
webertj@14350
    75
  refute
webertj@14350
    76
oops
webertj@14350
    77
webertj@14455
    78
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
webertj@14455
    79
  refute
webertj@14455
    80
oops
webertj@14455
    81
webertj@14350
    82
subsection {* Equality *}
webertj@14350
    83
webertj@14350
    84
lemma "P = True"
webertj@14350
    85
  refute
webertj@14350
    86
oops
webertj@14350
    87
webertj@14350
    88
lemma "P = False"
webertj@14350
    89
  refute
webertj@14350
    90
oops
webertj@14350
    91
webertj@14350
    92
lemma "x = y"
webertj@14350
    93
  refute
webertj@14350
    94
oops
webertj@14350
    95
webertj@14350
    96
lemma "f x = g x"
webertj@14350
    97
  refute
webertj@14350
    98
oops
webertj@14350
    99
webertj@14350
   100
lemma "(f::'a\<Rightarrow>'b) = g"
webertj@14350
   101
  refute
webertj@14350
   102
oops
webertj@14350
   103
webertj@14350
   104
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
webertj@14350
   105
  refute
webertj@14350
   106
oops
webertj@14350
   107
webertj@14350
   108
lemma "distinct [a,b]"
webertj@14809
   109
  refute
webertj@14350
   110
  apply simp
webertj@14350
   111
  refute
webertj@14350
   112
oops
webertj@14350
   113
webertj@14350
   114
subsection {* First-Order Logic *}
webertj@14350
   115
webertj@14350
   116
lemma "\<exists>x. P x"
webertj@14350
   117
  refute
webertj@14350
   118
oops
webertj@14350
   119
webertj@14350
   120
lemma "\<forall>x. P x"
webertj@14350
   121
  refute
webertj@14350
   122
oops
webertj@14350
   123
webertj@14350
   124
lemma "EX! x. P x"
webertj@14350
   125
  refute
webertj@14350
   126
oops
webertj@14350
   127
webertj@14350
   128
lemma "Ex P"
webertj@14350
   129
  refute
webertj@14350
   130
oops
webertj@14350
   131
webertj@14350
   132
lemma "All P"
webertj@14350
   133
  refute
webertj@14350
   134
oops
webertj@14350
   135
webertj@14350
   136
lemma "Ex1 P"
webertj@14350
   137
  refute
webertj@14350
   138
oops
webertj@14350
   139
webertj@14350
   140
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
webertj@14350
   141
  refute
webertj@14350
   142
oops
webertj@14350
   143
webertj@14350
   144
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
webertj@14350
   145
  refute
webertj@14350
   146
oops
webertj@14350
   147
webertj@14350
   148
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
webertj@14350
   149
  refute
webertj@14350
   150
oops
webertj@14350
   151
webertj@14350
   152
text {* A true statement (also testing names of free and bound variables being identical) *}
webertj@14350
   153
webertj@14350
   154
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
webertj@18774
   155
  refute [maxsize=4]
webertj@14350
   156
  apply fast
webertj@14350
   157
done
webertj@14350
   158
webertj@18789
   159
text {* "A type has at most 4 elements." *}
webertj@14350
   160
webertj@18789
   161
lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
webertj@14455
   162
  refute
webertj@14455
   163
oops
webertj@14455
   164
webertj@18789
   165
lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
webertj@15767
   166
  refute  -- {* quantification causes an expansion of the formula; the
webertj@15767
   167
                previous version with free variables is refuted much faster *}
webertj@14350
   168
oops
webertj@14350
   169
webertj@14350
   170
text {* "Every reflexive and symmetric relation is transitive." *}
webertj@14350
   171
webertj@14350
   172
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"
webertj@14489
   173
  refute
webertj@14350
   174
oops
webertj@14350
   175
webertj@14465
   176
text {* The "Drinker's theorem" ... *}
webertj@14350
   177
webertj@14350
   178
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
webertj@14809
   179
  refute [maxsize=4]
webertj@14350
   180
  apply (auto simp add: ext)
webertj@14350
   181
done
webertj@14350
   182
webertj@14465
   183
text {* ... and an incorrect version of it *}
webertj@14350
   184
webertj@14350
   185
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
webertj@14350
   186
  refute
webertj@14350
   187
oops
webertj@14350
   188
webertj@14350
   189
text {* "Every function has a fixed point." *}
webertj@14350
   190
webertj@14350
   191
lemma "\<exists>x. f x = x"
webertj@14350
   192
  refute
webertj@14350
   193
oops
webertj@14350
   194
webertj@14350
   195
text {* "Function composition is commutative." *}
webertj@14350
   196
webertj@14350
   197
lemma "f (g x) = g (f x)"
webertj@14350
   198
  refute
webertj@14350
   199
oops
webertj@14350
   200
webertj@14350
   201
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
webertj@14350
   202
webertj@14350
   203
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
webertj@14350
   204
  refute
webertj@14350
   205
oops
webertj@14350
   206
webertj@14350
   207
subsection {* Higher-Order Logic *}
webertj@14350
   208
webertj@14350
   209
lemma "\<exists>P. P"
webertj@14350
   210
  refute
webertj@14350
   211
  apply auto
webertj@14350
   212
done
webertj@14350
   213
webertj@14350
   214
lemma "\<forall>P. P"
webertj@14350
   215
  refute
webertj@14350
   216
oops
webertj@14350
   217
webertj@14350
   218
lemma "EX! P. P"
webertj@14350
   219
  refute
webertj@14350
   220
  apply auto
webertj@14350
   221
done
webertj@14350
   222
webertj@14350
   223
lemma "EX! P. P x"
webertj@14350
   224
  refute
webertj@14350
   225
oops
webertj@14350
   226
webertj@14350
   227
lemma "P Q | Q x"
webertj@14350
   228
  refute
webertj@14350
   229
oops
webertj@14350
   230
webertj@14455
   231
lemma "P All"
webertj@14455
   232
  refute
webertj@14455
   233
oops
webertj@14455
   234
webertj@14455
   235
lemma "P Ex"
webertj@14455
   236
  refute
webertj@14455
   237
oops
webertj@14455
   238
webertj@14455
   239
lemma "P Ex1"
webertj@14455
   240
  refute
webertj@14455
   241
oops
webertj@14455
   242
webertj@14350
   243
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
webertj@14350
   244
webertj@14350
   245
constdefs
webertj@14350
   246
  "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
webertj@14350
   247
  "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
webertj@14350
   248
  "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
webertj@14350
   249
  "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
webertj@14350
   250
  "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
webertj@14350
   251
  "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
webertj@14350
   252
webertj@14350
   253
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
webertj@14350
   254
  refute
webertj@14350
   255
oops
webertj@14350
   256
webertj@14350
   257
text {* "The union of transitive closures is equal to the transitive closure of unions." *}
webertj@14350
   258
webertj@14350
   259
lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
webertj@14350
   260
        \<longrightarrow> trans_closure TP P
webertj@14350
   261
        \<longrightarrow> trans_closure TR R
webertj@14350
   262
        \<longrightarrow> (T x y = (TP x y | TR x y))"
webertj@16910
   263
  refute
webertj@14350
   264
oops
webertj@14350
   265
webertj@14350
   266
text {* "Every surjective function is invertible." *}
webertj@14350
   267
webertj@14350
   268
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
webertj@14350
   269
  refute
webertj@14350
   270
oops
webertj@14350
   271
webertj@14350
   272
text {* "Every invertible function is surjective." *}
webertj@14350
   273
webertj@14350
   274
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
webertj@14350
   275
  refute
webertj@14350
   276
oops
webertj@14350
   277
webertj@14350
   278
text {* Every point is a fixed point of some function. *}
webertj@14350
   279
webertj@14350
   280
lemma "\<exists>f. f x = x"
webertj@14809
   281
  refute [maxsize=4]
webertj@14350
   282
  apply (rule_tac x="\<lambda>x. x" in exI)
webertj@14350
   283
  apply simp
webertj@14350
   284
done
webertj@14350
   285
webertj@14465
   286
text {* Axiom of Choice: first an incorrect version ... *}
webertj@14350
   287
webertj@14350
   288
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
webertj@14350
   289
  refute
webertj@14350
   290
oops
webertj@14350
   291
webertj@14465
   292
text {* ... and now two correct ones *}
webertj@14350
   293
webertj@14350
   294
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
webertj@14809
   295
  refute [maxsize=4]
webertj@14350
   296
  apply (simp add: choice)
webertj@14350
   297
done
webertj@14350
   298
webertj@14350
   299
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
webertj@15547
   300
  refute [maxsize=2]
webertj@14350
   301
  apply auto
webertj@14350
   302
    apply (simp add: ex1_implies_ex choice)
webertj@14350
   303
  apply (fast intro: ext)
webertj@14350
   304
done
webertj@14350
   305
webertj@14350
   306
subsection {* Meta-logic *}
webertj@14350
   307
webertj@14350
   308
lemma "!!x. P x"
webertj@14350
   309
  refute
webertj@14350
   310
oops
webertj@14350
   311
webertj@14350
   312
lemma "f x == g x"
webertj@14350
   313
  refute
webertj@14350
   314
oops
webertj@14350
   315
webertj@14350
   316
lemma "P \<Longrightarrow> Q"
webertj@14350
   317
  refute
webertj@14350
   318
oops
webertj@14350
   319
webertj@14350
   320
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
webertj@14350
   321
  refute
webertj@14350
   322
oops
webertj@14350
   323
webertj@14350
   324
subsection {* Schematic variables *}
webertj@14350
   325
webertj@14350
   326
lemma "?P"
webertj@14350
   327
  refute
webertj@14350
   328
  apply auto
webertj@14350
   329
done
webertj@14350
   330
webertj@14350
   331
lemma "x = ?y"
webertj@14350
   332
  refute
webertj@14350
   333
  apply auto
webertj@14350
   334
done
webertj@14350
   335
webertj@14350
   336
subsection {* Abstractions *}
webertj@14350
   337
webertj@14350
   338
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
webertj@14350
   339
  refute
webertj@14350
   340
oops
webertj@14350
   341
webertj@14350
   342
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
webertj@14350
   343
  refute
webertj@14350
   344
oops
webertj@14350
   345
webertj@14350
   346
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
webertj@14350
   347
  refute
webertj@14350
   348
  apply simp
webertj@14350
   349
done
webertj@14350
   350
webertj@14350
   351
subsection {* Sets *}
webertj@14350
   352
webertj@14350
   353
lemma "P (A::'a set)"
webertj@14350
   354
  refute
webertj@14350
   355
oops
webertj@14350
   356
webertj@14350
   357
lemma "P (A::'a set set)"
webertj@14350
   358
  refute
webertj@14350
   359
oops
webertj@14350
   360
webertj@14350
   361
lemma "{x. P x} = {y. P y}"
webertj@14489
   362
  refute
webertj@14350
   363
  apply simp
webertj@14350
   364
done
webertj@14350
   365
webertj@14350
   366
lemma "x : {x. P x}"
webertj@14350
   367
  refute
webertj@14350
   368
oops
webertj@14350
   369
webertj@14455
   370
lemma "P op:"
webertj@14455
   371
  refute
webertj@14455
   372
oops
webertj@14455
   373
webertj@14455
   374
lemma "P (op: x)"
webertj@14455
   375
  refute
webertj@14455
   376
oops
webertj@14455
   377
webertj@14455
   378
lemma "P Collect"
webertj@14455
   379
  refute
webertj@14455
   380
oops
webertj@14455
   381
webertj@14350
   382
lemma "A Un B = A Int B"
webertj@14350
   383
  refute
webertj@14350
   384
oops
webertj@14350
   385
webertj@14350
   386
lemma "(A Int B) Un C = (A Un C) Int B"
webertj@14350
   387
  refute
webertj@14350
   388
oops
webertj@14350
   389
webertj@14350
   390
lemma "Ball A P \<longrightarrow> Bex A P"
webertj@14455
   391
  refute
webertj@14455
   392
oops
webertj@14455
   393
webertj@14455
   394
subsection {* arbitrary *}
webertj@14455
   395
webertj@14455
   396
lemma "arbitrary"
webertj@14455
   397
  refute
webertj@14455
   398
oops
webertj@14455
   399
webertj@14455
   400
lemma "P arbitrary"
webertj@14455
   401
  refute
webertj@14455
   402
oops
webertj@14455
   403
webertj@14455
   404
lemma "arbitrary x"
webertj@14455
   405
  refute
webertj@14455
   406
oops
webertj@14455
   407
webertj@14455
   408
lemma "arbitrary arbitrary"
webertj@14455
   409
  refute
webertj@14455
   410
oops
webertj@14455
   411
webertj@14455
   412
subsection {* The *}
webertj@14455
   413
webertj@14455
   414
lemma "The P"
webertj@14455
   415
  refute
webertj@14455
   416
oops
webertj@14455
   417
webertj@14455
   418
lemma "P The"
webertj@14350
   419
  refute
webertj@14350
   420
oops
webertj@14350
   421
webertj@14455
   422
lemma "P (The P)"
webertj@14455
   423
  refute
webertj@14455
   424
oops
webertj@14455
   425
webertj@14455
   426
lemma "(THE x. x=y) = z"
webertj@14455
   427
  refute
webertj@14455
   428
oops
webertj@14455
   429
webertj@14455
   430
lemma "Ex P \<longrightarrow> P (The P)"
webertj@14489
   431
  refute
webertj@14455
   432
oops
webertj@14455
   433
webertj@14455
   434
subsection {* Eps *}
webertj@14455
   435
webertj@14455
   436
lemma "Eps P"
webertj@14455
   437
  refute
webertj@14455
   438
oops
webertj@14455
   439
webertj@14455
   440
lemma "P Eps"
webertj@14455
   441
  refute
webertj@14455
   442
oops
webertj@14455
   443
webertj@14455
   444
lemma "P (Eps P)"
webertj@14455
   445
  refute
webertj@14455
   446
oops
webertj@14455
   447
webertj@14455
   448
lemma "(SOME x. x=y) = z"
webertj@14455
   449
  refute
webertj@14455
   450
oops
webertj@14455
   451
webertj@14455
   452
lemma "Ex P \<longrightarrow> P (Eps P)"
webertj@14489
   453
  refute [maxsize=3]
webertj@14455
   454
  apply (auto simp add: someI)
webertj@14455
   455
done
webertj@14455
   456
webertj@15767
   457
(******************************************************************************)
webertj@15767
   458
webertj@14809
   459
subsection {* Subtypes (typedef), typedecl *}
webertj@14809
   460
webertj@15161
   461
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
webertj@15161
   462
webertj@14809
   463
typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
webertj@14809
   464
  by auto
webertj@14809
   465
webertj@14809
   466
lemma "(x::'a myTdef) = y"
webertj@15547
   467
  refute
webertj@14809
   468
oops
webertj@14809
   469
webertj@14809
   470
typedecl myTdecl
webertj@14809
   471
webertj@14809
   472
typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
webertj@14809
   473
  by auto
webertj@14809
   474
webertj@14809
   475
lemma "P (f::(myTdecl myTdef) T_bij)"
webertj@14809
   476
  refute
webertj@14809
   477
oops
webertj@14809
   478
webertj@15767
   479
(******************************************************************************)
webertj@15767
   480
webertj@14455
   481
subsection {* Inductive datatypes *}
webertj@14350
   482
webertj@15767
   483
text {* With quick\_and\_dirty set, the datatype package does not generate
webertj@15767
   484
  certain axioms for recursion operators.  Without these axioms, refute may
webertj@15767
   485
  find spurious countermodels. *}
webertj@15547
   486
webertj@15547
   487
ML {* reset quick_and_dirty; *}
webertj@15547
   488
webertj@14350
   489
subsubsection {* unit *}
webertj@14350
   490
webertj@14350
   491
lemma "P (x::unit)"
webertj@14350
   492
  refute
webertj@14350
   493
oops
webertj@14350
   494
webertj@14350
   495
lemma "\<forall>x::unit. P x"
webertj@14350
   496
  refute
webertj@14350
   497
oops
webertj@14350
   498
webertj@14350
   499
lemma "P ()"
webertj@14350
   500
  refute
webertj@14350
   501
oops
webertj@14350
   502
webertj@15547
   503
lemma "P (unit_rec u x)"
webertj@15547
   504
  refute
webertj@15547
   505
oops
webertj@15547
   506
webertj@15547
   507
lemma "P (case x of () \<Rightarrow> u)"
webertj@15547
   508
  refute
webertj@15547
   509
oops
webertj@15547
   510
webertj@14455
   511
subsubsection {* option *}
webertj@14455
   512
webertj@14455
   513
lemma "P (x::'a option)"
webertj@14455
   514
  refute
webertj@14455
   515
oops
webertj@14455
   516
webertj@14455
   517
lemma "\<forall>x::'a option. P x"
webertj@14455
   518
  refute
webertj@14455
   519
oops
webertj@14455
   520
webertj@14809
   521
lemma "P None"
webertj@14809
   522
  refute
webertj@14809
   523
oops
webertj@14809
   524
webertj@14455
   525
lemma "P (Some x)"
webertj@14455
   526
  refute
webertj@14455
   527
oops
webertj@14455
   528
webertj@15547
   529
lemma "P (option_rec n s x)"
webertj@15547
   530
  refute
webertj@15547
   531
oops
webertj@15547
   532
webertj@15547
   533
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
webertj@15547
   534
  refute
webertj@15547
   535
oops
webertj@15547
   536
webertj@14350
   537
subsubsection {* * *}
webertj@14350
   538
webertj@14350
   539
lemma "P (x::'a*'b)"
webertj@14455
   540
  refute
webertj@14350
   541
oops
webertj@14350
   542
webertj@14350
   543
lemma "\<forall>x::'a*'b. P x"
webertj@14455
   544
  refute
webertj@14350
   545
oops
webertj@14350
   546
webertj@14350
   547
lemma "P (x,y)"
webertj@14455
   548
  refute
webertj@14350
   549
oops
webertj@14350
   550
webertj@14350
   551
lemma "P (fst x)"
webertj@14455
   552
  refute
webertj@14350
   553
oops
webertj@14350
   554
webertj@14350
   555
lemma "P (snd x)"
webertj@14455
   556
  refute
webertj@14455
   557
oops
webertj@14455
   558
webertj@14455
   559
lemma "P Pair"
webertj@14455
   560
  refute
webertj@14350
   561
oops
webertj@14350
   562
webertj@15547
   563
lemma "P (prod_rec p x)"
webertj@15547
   564
  refute
webertj@15547
   565
oops
webertj@15547
   566
webertj@15547
   567
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
webertj@15547
   568
  refute
webertj@15547
   569
oops
webertj@15547
   570
webertj@14350
   571
subsubsection {* + *}
webertj@14350
   572
webertj@14350
   573
lemma "P (x::'a+'b)"
webertj@14455
   574
  refute
webertj@14350
   575
oops
webertj@14350
   576
webertj@14350
   577
lemma "\<forall>x::'a+'b. P x"
webertj@14455
   578
  refute
webertj@14350
   579
oops
webertj@14350
   580
webertj@14350
   581
lemma "P (Inl x)"
webertj@14455
   582
  refute
webertj@14350
   583
oops
webertj@14350
   584
webertj@14350
   585
lemma "P (Inr x)"
webertj@14455
   586
  refute
webertj@14455
   587
oops
webertj@14455
   588
webertj@14455
   589
lemma "P Inl"
webertj@14455
   590
  refute
webertj@14350
   591
oops
webertj@14350
   592
webertj@15547
   593
lemma "P (sum_rec l r x)"
webertj@15547
   594
  refute
webertj@15547
   595
oops
webertj@15547
   596
webertj@15547
   597
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
webertj@15547
   598
  refute
webertj@15547
   599
oops
webertj@15547
   600
webertj@14350
   601
subsubsection {* Non-recursive datatypes *}
webertj@14350
   602
webertj@14455
   603
datatype T1 = A | B
webertj@14350
   604
webertj@14350
   605
lemma "P (x::T1)"
webertj@14350
   606
  refute
webertj@14350
   607
oops
webertj@14350
   608
webertj@14350
   609
lemma "\<forall>x::T1. P x"
webertj@14350
   610
  refute
webertj@14350
   611
oops
webertj@14350
   612
webertj@14455
   613
lemma "P A"
webertj@14350
   614
  refute
webertj@14350
   615
oops
webertj@14350
   616
webertj@15547
   617
lemma "P (T1_rec a b x)"
webertj@15547
   618
  refute
webertj@15547
   619
oops
webertj@15547
   620
webertj@15547
   621
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
webertj@15547
   622
  refute
webertj@15547
   623
oops
webertj@15547
   624
webertj@14455
   625
datatype 'a T2 = C T1 | D 'a
webertj@14455
   626
webertj@14455
   627
lemma "P (x::'a T2)"
webertj@14350
   628
  refute
webertj@14350
   629
oops
webertj@14350
   630
webertj@14455
   631
lemma "\<forall>x::'a T2. P x"
webertj@14350
   632
  refute
webertj@14350
   633
oops
webertj@14350
   634
webertj@14455
   635
lemma "P D"
webertj@14350
   636
  refute
webertj@14350
   637
oops
webertj@14350
   638
webertj@15547
   639
lemma "P (T2_rec c d x)"
webertj@15547
   640
  refute
webertj@15547
   641
oops
webertj@15547
   642
webertj@15547
   643
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
webertj@15547
   644
  refute
webertj@15547
   645
oops
webertj@15547
   646
webertj@14455
   647
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
webertj@14455
   648
webertj@14809
   649
lemma "P (x::('a,'b) T3)"
webertj@14809
   650
  refute
webertj@14809
   651
oops
webertj@14809
   652
webertj@14809
   653
lemma "\<forall>x::('a,'b) T3. P x"
webertj@14809
   654
  refute
webertj@14809
   655
oops
webertj@14809
   656
webertj@14455
   657
lemma "P E"
webertj@14455
   658
  refute
webertj@14350
   659
oops
webertj@14350
   660
webertj@15547
   661
lemma "P (T3_rec e x)"
webertj@15547
   662
  refute
webertj@15547
   663
oops
webertj@15547
   664
webertj@15547
   665
lemma "P (case x of E f \<Rightarrow> e f)"
webertj@15547
   666
  refute
webertj@15547
   667
oops
webertj@15547
   668
webertj@14350
   669
subsubsection {* Recursive datatypes *}
webertj@14350
   670
webertj@15547
   671
text {* nat *}
webertj@15547
   672
webertj@14809
   673
lemma "P (x::nat)"
webertj@14809
   674
  refute
webertj@14809
   675
oops
webertj@14350
   676
webertj@14809
   677
lemma "\<forall>x::nat. P x"
webertj@14809
   678
  refute
webertj@14350
   679
oops
webertj@14350
   680
webertj@14809
   681
lemma "P (Suc 0)"
webertj@14809
   682
  refute
webertj@14350
   683
oops
webertj@14350
   684
webertj@14809
   685
lemma "P Suc"
webertj@14809
   686
  refute  -- {* @{term "Suc"} is a partial function (regardless of the size
webertj@14809
   687
                of the model), hence @{term "P Suc"} is undefined, hence no
webertj@14809
   688
                model will be found *}
webertj@14350
   689
oops
webertj@14350
   690
webertj@15547
   691
lemma "P (nat_rec zero suc x)"
webertj@15547
   692
  refute
webertj@15547
   693
oops
webertj@15547
   694
webertj@15547
   695
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
webertj@15547
   696
  refute
webertj@15547
   697
oops
webertj@15547
   698
webertj@15547
   699
text {* 'a list *}
webertj@15547
   700
webertj@15547
   701
lemma "P (xs::'a list)"
webertj@15547
   702
  refute
webertj@15547
   703
oops
webertj@15547
   704
webertj@15547
   705
lemma "\<forall>xs::'a list. P xs"
webertj@15547
   706
  refute
webertj@15547
   707
oops
webertj@15547
   708
webertj@15547
   709
lemma "P [x, y]"
webertj@15547
   710
  refute
webertj@15547
   711
oops
webertj@15547
   712
webertj@15547
   713
lemma "P (list_rec nil cons xs)"
webertj@15547
   714
  refute
webertj@15547
   715
oops
webertj@15547
   716
webertj@15547
   717
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
webertj@15547
   718
  refute
webertj@15547
   719
oops
webertj@15547
   720
webertj@15547
   721
lemma "(xs::'a list) = ys"
webertj@15547
   722
  refute
webertj@15547
   723
oops
webertj@15547
   724
webertj@15547
   725
lemma "a # xs = b # xs"
webertj@15547
   726
  refute
webertj@15547
   727
oops
webertj@15547
   728
webertj@14350
   729
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
webertj@14350
   730
webertj@14350
   731
lemma "P (x::'a BinTree)"
webertj@14809
   732
  refute
webertj@14350
   733
oops
webertj@14350
   734
webertj@14350
   735
lemma "\<forall>x::'a BinTree. P x"
webertj@14809
   736
  refute
webertj@14809
   737
oops
webertj@14809
   738
webertj@14809
   739
lemma "P (Node (Leaf x) (Leaf y))"
webertj@14809
   740
  refute
webertj@14350
   741
oops
webertj@14350
   742
webertj@15547
   743
lemma "P (BinTree_rec l n x)"
webertj@15547
   744
  refute
webertj@15547
   745
oops
webertj@15547
   746
webertj@15547
   747
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
webertj@15547
   748
  refute
webertj@15547
   749
oops
webertj@15547
   750
webertj@14350
   751
subsubsection {* Mutually recursive datatypes *}
webertj@14350
   752
webertj@14350
   753
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
webertj@14350
   754
     and 'a bexp = Equal "'a aexp" "'a aexp"
webertj@14350
   755
webertj@14350
   756
lemma "P (x::'a aexp)"
webertj@14809
   757
  refute
webertj@14350
   758
oops
webertj@14350
   759
webertj@14350
   760
lemma "\<forall>x::'a aexp. P x"
webertj@14809
   761
  refute
webertj@14350
   762
oops
webertj@14350
   763
webertj@15547
   764
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
webertj@15547
   765
  refute
webertj@15547
   766
oops
webertj@15547
   767
webertj@14350
   768
lemma "P (x::'a bexp)"
webertj@14809
   769
  refute
webertj@14350
   770
oops
webertj@14350
   771
webertj@14350
   772
lemma "\<forall>x::'a bexp. P x"
webertj@14809
   773
  refute
webertj@14350
   774
oops
webertj@14350
   775
webertj@15547
   776
lemma "P (aexp_bexp_rec_1 number ite equal x)"
webertj@15547
   777
  refute
webertj@15547
   778
oops
webertj@15547
   779
webertj@15547
   780
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
webertj@14809
   781
  refute
webertj@14350
   782
oops
webertj@14350
   783
webertj@15547
   784
lemma "P (aexp_bexp_rec_2 number ite equal x)"
webertj@15767
   785
  refute
webertj@15547
   786
oops
webertj@15547
   787
webertj@15547
   788
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
webertj@15767
   789
  refute
webertj@15547
   790
oops
webertj@15547
   791
webertj@14350
   792
subsubsection {* Other datatype examples *}
webertj@14350
   793
webertj@15547
   794
datatype Trie = TR "Trie list"
webertj@15547
   795
webertj@15547
   796
lemma "P (x::Trie)"
webertj@15547
   797
  refute
webertj@15547
   798
oops
webertj@15547
   799
webertj@15547
   800
lemma "\<forall>x::Trie. P x"
webertj@15547
   801
  refute
webertj@15547
   802
oops
webertj@15547
   803
webertj@15547
   804
lemma "P (TR [TR []])"
webertj@15547
   805
  refute
webertj@15547
   806
oops
webertj@15547
   807
webertj@15767
   808
lemma "P (Trie_rec_1 a b c x)"
webertj@15767
   809
  refute
webertj@15767
   810
oops
webertj@15767
   811
webertj@15767
   812
lemma "P (Trie_rec_2 a b c x)"
webertj@15547
   813
  refute
webertj@15547
   814
oops
webertj@15547
   815
webertj@14809
   816
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
webertj@14350
   817
webertj@14350
   818
lemma "P (x::InfTree)"
webertj@14809
   819
  refute
webertj@14350
   820
oops
webertj@14350
   821
webertj@15547
   822
lemma "\<forall>x::InfTree. P x"
webertj@15547
   823
  refute
webertj@15547
   824
oops
webertj@15547
   825
webertj@15547
   826
lemma "P (Node (\<lambda>n. Leaf))"
webertj@15547
   827
  refute
webertj@15547
   828
oops
webertj@15547
   829
webertj@15547
   830
lemma "P (InfTree_rec leaf node x)"
webertj@15547
   831
  refute
webertj@15547
   832
oops
webertj@15547
   833
webertj@14350
   834
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
webertj@14350
   835
webertj@15547
   836
lemma "P (x::'a lambda)"
webertj@15547
   837
  refute
webertj@15547
   838
oops
webertj@15547
   839
webertj@15547
   840
lemma "\<forall>x::'a lambda. P x"
webertj@15547
   841
  refute
webertj@15547
   842
oops
webertj@15547
   843
webertj@15547
   844
lemma "P (Lam (\<lambda>a. Var a))"
webertj@15547
   845
  refute
webertj@15547
   846
oops
webertj@15547
   847
webertj@15547
   848
lemma "P (lambda_rec v a l x)"
webertj@15547
   849
  refute
webertj@15547
   850
oops
webertj@15547
   851
webertj@15767
   852
text {* Taken from "Inductive datatypes in HOL", p.8: *}
webertj@15767
   853
webertj@15767
   854
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
webertj@15767
   855
datatype 'c U = E "('c, 'c U) T"
webertj@15767
   856
webertj@15767
   857
lemma "P (x::'c U)"
webertj@15767
   858
  refute
webertj@15767
   859
oops
webertj@15767
   860
webertj@15767
   861
lemma "\<forall>x::'c U. P x"
webertj@15767
   862
  refute
webertj@15767
   863
oops
webertj@15767
   864
webertj@15767
   865
lemma "P (E (C (\<lambda>a. True)))"
webertj@15767
   866
  refute
webertj@15767
   867
oops
webertj@15767
   868
webertj@15767
   869
lemma "P (U_rec_1 e f g h i x)"
webertj@15767
   870
  refute
webertj@15767
   871
oops
webertj@15767
   872
webertj@15767
   873
lemma "P (U_rec_2 e f g h i x)"
webertj@15767
   874
  refute
webertj@15767
   875
oops
webertj@15767
   876
webertj@15767
   877
lemma "P (U_rec_3 e f g h i x)"
webertj@15767
   878
  refute
webertj@15767
   879
oops
webertj@15767
   880
webertj@15767
   881
(******************************************************************************)
webertj@15767
   882
webertj@15767
   883
subsection {* Records *}
webertj@15767
   884
webertj@15767
   885
(*TODO: make use of pair types, rather than typedef, for record types*)
webertj@15767
   886
webertj@15767
   887
record ('a, 'b) point =
webertj@15767
   888
  xpos :: 'a
webertj@15767
   889
  ypos :: 'b
webertj@15767
   890
webertj@15767
   891
lemma "(x::('a, 'b) point) = y"
webertj@15767
   892
  refute
webertj@15767
   893
oops
webertj@15767
   894
webertj@15767
   895
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
webertj@15767
   896
  ext :: 'c
webertj@15767
   897
webertj@15767
   898
lemma "(x::('a, 'b, 'c) extpoint) = y"
webertj@15767
   899
  refute
webertj@15767
   900
oops
webertj@15767
   901
webertj@15767
   902
(******************************************************************************)
webertj@15767
   903
webertj@15767
   904
subsection {* Inductively defined sets *}
webertj@15767
   905
webertj@15767
   906
consts
webertj@15767
   907
  arbitrarySet :: "'a set"
webertj@15767
   908
inductive arbitrarySet
webertj@15767
   909
intros
webertj@15767
   910
  "arbitrary : arbitrarySet"
webertj@15767
   911
webertj@15767
   912
lemma "x : arbitrarySet"
webertj@16050
   913
  refute
webertj@15767
   914
oops
webertj@15767
   915
webertj@15767
   916
consts
webertj@15767
   917
  evenCard :: "'a set set"
webertj@15767
   918
inductive evenCard
webertj@15767
   919
intros
webertj@15767
   920
  "{} : evenCard"
webertj@15767
   921
  "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
webertj@15767
   922
webertj@15767
   923
lemma "S : evenCard"
webertj@16050
   924
  refute
webertj@15767
   925
oops
webertj@15767
   926
webertj@15767
   927
consts
webertj@15767
   928
  even :: "nat set"
webertj@15767
   929
  odd  :: "nat set"
webertj@15767
   930
inductive even odd
webertj@15767
   931
intros
webertj@15767
   932
  "0 : even"
webertj@15767
   933
  "n : even \<Longrightarrow> Suc n : odd"
webertj@15767
   934
  "n : odd \<Longrightarrow> Suc n : even"
webertj@15767
   935
webertj@15767
   936
lemma "n : odd"
webertj@16050
   937
  (*refute*)  -- {* unfortunately, this little example already takes too long *}
webertj@15767
   938
oops
webertj@15767
   939
webertj@15767
   940
(******************************************************************************)
webertj@15767
   941
webertj@15767
   942
subsection {* Examples involving special functions *}
webertj@15547
   943
webertj@15547
   944
lemma "card x = 0"
webertj@15547
   945
  refute
webertj@15547
   946
oops
webertj@15547
   947
webertj@15767
   948
lemma "finite x"
webertj@15767
   949
  refute  -- {* no finite countermodel exists *}
webertj@15547
   950
oops
webertj@15547
   951
webertj@15547
   952
lemma "(x::nat) + y = 0"
webertj@15547
   953
  refute
webertj@15547
   954
oops
webertj@15547
   955
webertj@15547
   956
lemma "(x::nat) = x + x"
webertj@15547
   957
  refute
webertj@15547
   958
oops
webertj@15547
   959
webertj@15547
   960
lemma "(x::nat) - y + y = x"
webertj@15547
   961
  refute
webertj@15547
   962
oops
webertj@15547
   963
webertj@15547
   964
lemma "(x::nat) = x * x"
webertj@15547
   965
  refute
webertj@15547
   966
oops
webertj@15547
   967
webertj@15547
   968
lemma "(x::nat) < x + y"
webertj@15547
   969
  refute
webertj@15547
   970
oops
webertj@15547
   971
webertj@15547
   972
lemma "a @ [] = b @ []"
webertj@15547
   973
  refute
webertj@15547
   974
oops
webertj@15547
   975
webertj@15767
   976
lemma "a @ b = b @ a"
webertj@15767
   977
  refute
webertj@15547
   978
oops
webertj@15547
   979
webertj@16050
   980
lemma "f (lfp f) = lfp f"
webertj@16050
   981
  refute
webertj@16050
   982
oops
webertj@16050
   983
webertj@16050
   984
lemma "f (gfp f) = gfp f"
webertj@16050
   985
  refute
webertj@16050
   986
oops
webertj@16050
   987
webertj@16050
   988
lemma "lfp f = gfp f"
webertj@16050
   989
  refute
webertj@16050
   990
oops
webertj@16050
   991
webertj@15767
   992
(******************************************************************************)
webertj@15547
   993
webertj@15547
   994
subsection {* Axiomatic type classes and overloading *}
webertj@15547
   995
webertj@15547
   996
text {* A type class without axioms: *}
webertj@15547
   997
webertj@15547
   998
axclass classA
webertj@15547
   999
webertj@15547
  1000
lemma "P (x::'a::classA)"
webertj@14809
  1001
  refute
webertj@14809
  1002
oops
webertj@14809
  1003
webertj@15547
  1004
text {* The axiom of this type class does not contain any type variables, but is internally converted into one that does: *}
webertj@15547
  1005
webertj@15547
  1006
axclass classB
webertj@15547
  1007
  classB_ax: "P | ~ P"
webertj@15547
  1008
webertj@15547
  1009
lemma "P (x::'a::classB)"
webertj@15547
  1010
  refute
webertj@15547
  1011
oops
webertj@15547
  1012
webertj@15547
  1013
text {* An axiom with a type variable (denoting types which have at least two elements): *}
webertj@15547
  1014
webertj@15547
  1015
axclass classC < type
webertj@15547
  1016
  classC_ax: "\<exists>x y. x \<noteq> y"
webertj@15547
  1017
webertj@15547
  1018
lemma "P (x::'a::classC)"
webertj@15547
  1019
  refute
webertj@15547
  1020
oops
webertj@15547
  1021
webertj@15547
  1022
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
webertj@15547
  1023
  refute  -- {* no countermodel exists *}
webertj@15547
  1024
oops
webertj@15547
  1025
webertj@15547
  1026
text {* A type class for which a constant is defined: *}
webertj@15547
  1027
webertj@15547
  1028
consts
webertj@15547
  1029
  classD_const :: "'a \<Rightarrow> 'a"
webertj@15547
  1030
webertj@15547
  1031
axclass classD < type
webertj@15547
  1032
  classD_ax: "classD_const (classD_const x) = classD_const x"
webertj@15547
  1033
webertj@15547
  1034
lemma "P (x::'a::classD)"
webertj@15547
  1035
  refute
webertj@15547
  1036
oops
webertj@15547
  1037
webertj@15547
  1038
text {* A type class with multiple superclasses: *}
webertj@15547
  1039
webertj@15547
  1040
axclass classE < classC, classD
webertj@15547
  1041
webertj@15547
  1042
lemma "P (x::'a::classE)"
webertj@14809
  1043
  refute
webertj@14809
  1044
oops
webertj@14809
  1045
webertj@15547
  1046
lemma "P (x::'a::{classB, classE})"
webertj@14809
  1047
  refute
webertj@14809
  1048
oops
webertj@14809
  1049
webertj@15547
  1050
text {* OFCLASS: *}
webertj@15547
  1051
webertj@15547
  1052
lemma "OFCLASS('a::type, type_class)"
webertj@15547
  1053
  refute  -- {* no countermodel exists *}
webertj@15547
  1054
  apply intro_classes
webertj@15547
  1055
done
webertj@15547
  1056
webertj@15547
  1057
lemma "OFCLASS('a::classC, type_class)"
webertj@15547
  1058
  refute  -- {* no countermodel exists *}
webertj@15547
  1059
  apply intro_classes
webertj@15547
  1060
done
webertj@15547
  1061
webertj@15547
  1062
lemma "OFCLASS('a, classB_class)"
webertj@15547
  1063
  refute  -- {* no countermodel exists *}
webertj@15547
  1064
  apply intro_classes
webertj@15547
  1065
  apply simp
webertj@15547
  1066
done
webertj@15547
  1067
webertj@15547
  1068
lemma "OFCLASS('a::type, classC_class)"
webertj@15547
  1069
  refute
webertj@15547
  1070
oops
webertj@15547
  1071
webertj@15547
  1072
text {* Overloading: *}
webertj@15547
  1073
webertj@15547
  1074
consts inverse :: "'a \<Rightarrow> 'a"
webertj@15547
  1075
webertj@15547
  1076
defs (overloaded)
webertj@15547
  1077
  inverse_bool: "inverse (b::bool)   == ~ b"
webertj@15547
  1078
  inverse_set : "inverse (S::'a set) == -S"
webertj@15547
  1079
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
webertj@15547
  1080
webertj@15547
  1081
lemma "inverse b"
webertj@15547
  1082
  refute
webertj@15547
  1083
oops
webertj@15547
  1084
webertj@15547
  1085
lemma "P (inverse (S::'a set))"
webertj@15547
  1086
  refute
webertj@15547
  1087
oops
webertj@15547
  1088
webertj@15547
  1089
lemma "P (inverse (p::'a\<times>'b))"
webertj@14809
  1090
  refute
webertj@14350
  1091
oops
webertj@14350
  1092
webertj@18774
  1093
refute_params [satsolver="auto"]
webertj@18774
  1094
webertj@14350
  1095
end