src/HOL/ex/Refute_Examples.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 59987 fbe93138e540
child 61337 4645502c3c64
permissions -rw-r--r--
prefer symbols;
webertj@14350
     1
(*  Title:      HOL/ex/Refute_Examples.thy
webertj@14350
     2
    Author:     Tjark Weber
webertj@21985
     3
    Copyright   2003-2007
wenzelm@32968
     4
wenzelm@32968
     5
See HOL/Refute.thy for help.
webertj@14350
     6
*)
webertj@14350
     7
wenzelm@58889
     8
section {* Examples for the 'refute' command *}
webertj@14350
     9
blanchet@46099
    10
theory Refute_Examples
blanchet@49988
    11
imports "~~/src/HOL/Library/Refute"
webertj@15297
    12
begin
webertj@14350
    13
blanchet@56851
    14
refute_params [satsolver = "cdclite"]
webertj@18774
    15
webertj@14350
    16
lemma "P \<and> Q"
blanchet@46099
    17
apply (rule conjI)
blanchet@46099
    18
refute [expect = genuine] 1  -- {* refutes @{term "P"} *}
blanchet@46099
    19
refute [expect = genuine] 2  -- {* refutes @{term "Q"} *}
blanchet@46099
    20
refute [expect = genuine]    -- {* equivalent to 'refute 1' *}
blanchet@46099
    21
  -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
blanchet@46099
    22
refute [maxsize = 5, expect = genuine]   -- {* we can override parameters ... *}
blanchet@56851
    23
refute [satsolver = "cdclite", expect = genuine] 2
blanchet@46099
    24
  -- {* ... and specify a subgoal at the same time *}
webertj@14350
    25
oops
webertj@14350
    26
webertj@25014
    27
(*****************************************************************************)
webertj@21985
    28
wenzelm@23219
    29
subsection {* Examples and Test Cases *}
webertj@14350
    30
wenzelm@23219
    31
subsubsection {* Propositional logic *}
webertj@14350
    32
webertj@14350
    33
lemma "True"
blanchet@46099
    34
refute [expect = none]
blanchet@46099
    35
by auto
webertj@14350
    36
webertj@14350
    37
lemma "False"
blanchet@46099
    38
refute [expect = genuine]
webertj@14350
    39
oops
webertj@14350
    40
webertj@14350
    41
lemma "P"
blanchet@46099
    42
refute [expect = genuine]
webertj@14350
    43
oops
webertj@14350
    44
webertj@14350
    45
lemma "~ P"
blanchet@46099
    46
refute [expect = genuine]
webertj@14350
    47
oops
webertj@14350
    48
webertj@14350
    49
lemma "P & Q"
blanchet@46099
    50
refute [expect = genuine]
webertj@14350
    51
oops
webertj@14350
    52
webertj@14350
    53
lemma "P | Q"
blanchet@46099
    54
refute [expect = genuine]
webertj@14350
    55
oops
webertj@14350
    56
webertj@14350
    57
lemma "P \<longrightarrow> Q"
blanchet@46099
    58
refute [expect = genuine]
webertj@14350
    59
oops
webertj@14350
    60
webertj@14350
    61
lemma "(P::bool) = Q"
blanchet@46099
    62
refute [expect = genuine]
webertj@14350
    63
oops
webertj@14350
    64
webertj@14350
    65
lemma "(P | Q) \<longrightarrow> (P & Q)"
blanchet@46099
    66
refute [expect = genuine]
webertj@14350
    67
oops
webertj@14350
    68
webertj@25014
    69
(*****************************************************************************)
webertj@21985
    70
wenzelm@23219
    71
subsubsection {* Predicate logic *}
webertj@14350
    72
webertj@14455
    73
lemma "P x y z"
blanchet@46099
    74
refute [expect = genuine]
webertj@14350
    75
oops
webertj@14350
    76
webertj@14350
    77
lemma "P x y \<longrightarrow> P y x"
blanchet@46099
    78
refute [expect = genuine]
webertj@14350
    79
oops
webertj@14350
    80
webertj@14455
    81
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
blanchet@46099
    82
refute [expect = genuine]
webertj@14455
    83
oops
webertj@14455
    84
webertj@25014
    85
(*****************************************************************************)
webertj@21985
    86
wenzelm@23219
    87
subsubsection {* Equality *}
webertj@14350
    88
webertj@14350
    89
lemma "P = True"
blanchet@46099
    90
refute [expect = genuine]
webertj@14350
    91
oops
webertj@14350
    92
webertj@14350
    93
lemma "P = False"
blanchet@46099
    94
refute [expect = genuine]
webertj@14350
    95
oops
webertj@14350
    96
webertj@14350
    97
lemma "x = y"
blanchet@46099
    98
refute [expect = genuine]
webertj@14350
    99
oops
webertj@14350
   100
webertj@14350
   101
lemma "f x = g x"
blanchet@46099
   102
refute [expect = genuine]
webertj@14350
   103
oops
webertj@14350
   104
webertj@14350
   105
lemma "(f::'a\<Rightarrow>'b) = g"
blanchet@46099
   106
refute [expect = genuine]
webertj@14350
   107
oops
webertj@14350
   108
webertj@14350
   109
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
blanchet@46099
   110
refute [expect = genuine]
webertj@14350
   111
oops
webertj@14350
   112
blanchet@46099
   113
lemma "distinct [a, b]"
blanchet@46099
   114
(* refute *)
blanchet@46099
   115
apply simp
blanchet@46099
   116
refute [expect = genuine]
webertj@14350
   117
oops
webertj@14350
   118
webertj@25014
   119
(*****************************************************************************)
webertj@21985
   120
wenzelm@23219
   121
subsubsection {* First-Order Logic *}
webertj@14350
   122
webertj@14350
   123
lemma "\<exists>x. P x"
blanchet@46099
   124
refute [expect = genuine]
webertj@14350
   125
oops
webertj@14350
   126
webertj@14350
   127
lemma "\<forall>x. P x"
blanchet@46099
   128
refute [expect = genuine]
webertj@14350
   129
oops
webertj@14350
   130
webertj@14350
   131
lemma "EX! x. P x"
blanchet@46099
   132
refute [expect = genuine]
webertj@14350
   133
oops
webertj@14350
   134
webertj@14350
   135
lemma "Ex P"
blanchet@46099
   136
refute [expect = genuine]
webertj@14350
   137
oops
webertj@14350
   138
webertj@14350
   139
lemma "All P"
blanchet@46099
   140
refute [expect = genuine]
webertj@14350
   141
oops
webertj@14350
   142
webertj@14350
   143
lemma "Ex1 P"
blanchet@46099
   144
refute [expect = genuine]
webertj@14350
   145
oops
webertj@14350
   146
webertj@14350
   147
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
blanchet@46099
   148
refute [expect = genuine]
webertj@14350
   149
oops
webertj@14350
   150
webertj@14350
   151
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
blanchet@46099
   152
refute [expect = genuine]
webertj@14350
   153
oops
webertj@14350
   154
webertj@14350
   155
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
blanchet@46099
   156
refute [expect = genuine]
webertj@14350
   157
oops
webertj@14350
   158
webertj@14350
   159
text {* A true statement (also testing names of free and bound variables being identical) *}
webertj@14350
   160
webertj@14350
   161
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
blanchet@46099
   162
refute [maxsize = 4, expect = none]
blanchet@46099
   163
by fast
webertj@14350
   164
webertj@18789
   165
text {* "A type has at most 4 elements." *}
webertj@14350
   166
webertj@18789
   167
lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
blanchet@46099
   168
refute [expect = genuine]
webertj@14455
   169
oops
webertj@14455
   170
webertj@18789
   171
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"
blanchet@46099
   172
refute [expect = genuine]
webertj@14350
   173
oops
webertj@14350
   174
webertj@14350
   175
text {* "Every reflexive and symmetric relation is transitive." *}
webertj@14350
   176
webertj@14350
   177
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@46099
   178
refute [expect = genuine]
webertj@14350
   179
oops
webertj@14350
   180
webertj@14465
   181
text {* The "Drinker's theorem" ... *}
webertj@14350
   182
webertj@14350
   183
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
blanchet@46099
   184
refute [maxsize = 4, expect = none]
blanchet@46099
   185
by (auto simp add: ext)
webertj@14350
   186
webertj@14465
   187
text {* ... and an incorrect version of it *}
webertj@14350
   188
webertj@14350
   189
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
blanchet@46099
   190
refute [expect = genuine]
webertj@14350
   191
oops
webertj@14350
   192
webertj@14350
   193
text {* "Every function has a fixed point." *}
webertj@14350
   194
webertj@14350
   195
lemma "\<exists>x. f x = x"
blanchet@46099
   196
refute [expect = genuine]
webertj@14350
   197
oops
webertj@14350
   198
webertj@14350
   199
text {* "Function composition is commutative." *}
webertj@14350
   200
webertj@14350
   201
lemma "f (g x) = g (f x)"
blanchet@46099
   202
refute [expect = genuine]
webertj@14350
   203
oops
webertj@14350
   204
webertj@14350
   205
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
webertj@14350
   206
webertj@14350
   207
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
blanchet@46099
   208
refute [expect = genuine]
webertj@14350
   209
oops
webertj@14350
   210
webertj@25014
   211
(*****************************************************************************)
webertj@21985
   212
wenzelm@23219
   213
subsubsection {* Higher-Order Logic *}
webertj@14350
   214
webertj@14350
   215
lemma "\<exists>P. P"
blanchet@46099
   216
refute [expect = none]
blanchet@46099
   217
by auto
webertj@14350
   218
webertj@14350
   219
lemma "\<forall>P. P"
blanchet@46099
   220
refute [expect = genuine]
webertj@14350
   221
oops
webertj@14350
   222
webertj@14350
   223
lemma "EX! P. P"
blanchet@46099
   224
refute [expect = none]
blanchet@46099
   225
by auto
webertj@14350
   226
webertj@14350
   227
lemma "EX! P. P x"
blanchet@46099
   228
refute [expect = genuine]
webertj@14350
   229
oops
webertj@14350
   230
webertj@14350
   231
lemma "P Q | Q x"
blanchet@46099
   232
refute [expect = genuine]
webertj@14350
   233
oops
webertj@14350
   234
webertj@21985
   235
lemma "x \<noteq> All"
blanchet@46099
   236
refute [expect = genuine]
webertj@14455
   237
oops
webertj@14455
   238
webertj@21985
   239
lemma "x \<noteq> Ex"
blanchet@46099
   240
refute [expect = genuine]
webertj@14455
   241
oops
webertj@14455
   242
webertj@21985
   243
lemma "x \<noteq> Ex1"
blanchet@46099
   244
refute [expect = genuine]
webertj@14455
   245
oops
webertj@14455
   246
webertj@14350
   247
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
webertj@14350
   248
haftmann@35416
   249
definition "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
webertj@14350
   250
  "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
haftmann@35416
   251
haftmann@35416
   252
definition "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
webertj@14350
   253
  "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
haftmann@35416
   254
haftmann@35416
   255
definition "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
webertj@14350
   256
  "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
webertj@14350
   257
webertj@14350
   258
lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
blanchet@46099
   259
refute [expect = genuine]
webertj@14350
   260
oops
webertj@14350
   261
webertj@14350
   262
text {* "Every surjective function is invertible." *}
webertj@14350
   263
webertj@14350
   264
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
blanchet@46099
   265
refute [expect = genuine]
webertj@14350
   266
oops
webertj@14350
   267
webertj@14350
   268
text {* "Every invertible function is surjective." *}
webertj@14350
   269
webertj@14350
   270
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
blanchet@46099
   271
refute [expect = genuine]
webertj@14350
   272
oops
webertj@14350
   273
webertj@14350
   274
text {* Every point is a fixed point of some function. *}
webertj@14350
   275
webertj@14350
   276
lemma "\<exists>f. f x = x"
blanchet@46099
   277
refute [maxsize = 4, expect = none]
blanchet@46099
   278
apply (rule_tac x="\<lambda>x. x" in exI)
blanchet@46099
   279
by simp
webertj@14350
   280
webertj@14465
   281
text {* Axiom of Choice: first an incorrect version ... *}
webertj@14350
   282
webertj@14350
   283
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
blanchet@46099
   284
refute [expect = genuine]
webertj@14350
   285
oops
webertj@14350
   286
webertj@14465
   287
text {* ... and now two correct ones *}
webertj@14350
   288
webertj@14350
   289
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
blanchet@46099
   290
refute [maxsize = 4, expect = none]
blanchet@46099
   291
by (simp add: choice)
webertj@14350
   292
webertj@14350
   293
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
blanchet@46099
   294
refute [maxsize = 2, expect = none]
blanchet@46099
   295
apply auto
blanchet@46099
   296
  apply (simp add: ex1_implies_ex choice)
blanchet@46099
   297
by (fast intro: ext)
webertj@14350
   298
webertj@25014
   299
(*****************************************************************************)
webertj@21985
   300
wenzelm@23219
   301
subsubsection {* Meta-logic *}
webertj@14350
   302
webertj@14350
   303
lemma "!!x. P x"
blanchet@46099
   304
refute [expect = genuine]
webertj@14350
   305
oops
webertj@14350
   306
webertj@14350
   307
lemma "f x == g x"
blanchet@46099
   308
refute [expect = genuine]
webertj@14350
   309
oops
webertj@14350
   310
webertj@14350
   311
lemma "P \<Longrightarrow> Q"
blanchet@46099
   312
refute [expect = genuine]
webertj@14350
   313
oops
webertj@14350
   314
webertj@14350
   315
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
blanchet@46099
   316
refute [expect = genuine]
webertj@14350
   317
oops
webertj@14350
   318
wenzelm@56245
   319
lemma "(x == Pure.all) \<Longrightarrow> False"
blanchet@46099
   320
refute [expect = genuine]
webertj@21985
   321
oops
webertj@21985
   322
webertj@21985
   323
lemma "(x == (op ==)) \<Longrightarrow> False"
blanchet@46099
   324
refute [expect = genuine]
webertj@21985
   325
oops
webertj@21985
   326
webertj@21985
   327
lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
blanchet@46099
   328
refute [expect = genuine]
webertj@21985
   329
oops
webertj@21985
   330
webertj@25014
   331
(*****************************************************************************)
webertj@21985
   332
wenzelm@23219
   333
subsubsection {* Schematic variables *}
webertj@14350
   334
wenzelm@36319
   335
schematic_lemma "?P"
blanchet@46099
   336
refute [expect = none]
blanchet@46099
   337
by auto
webertj@14350
   338
wenzelm@36319
   339
schematic_lemma "x = ?y"
blanchet@46099
   340
refute [expect = none]
blanchet@46099
   341
by auto
webertj@14350
   342
webertj@21985
   343
(******************************************************************************)
webertj@21985
   344
wenzelm@23219
   345
subsubsection {* Abstractions *}
webertj@14350
   346
webertj@14350
   347
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
blanchet@46099
   348
refute [expect = genuine]
webertj@14350
   349
oops
webertj@14350
   350
webertj@14350
   351
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
blanchet@46099
   352
refute [expect = genuine]
webertj@14350
   353
oops
webertj@14350
   354
webertj@14350
   355
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
blanchet@46099
   356
refute
blanchet@46099
   357
by simp
webertj@14350
   358
webertj@25014
   359
(*****************************************************************************)
webertj@21985
   360
wenzelm@23219
   361
subsubsection {* Sets *}
webertj@14350
   362
webertj@14350
   363
lemma "P (A::'a set)"
blanchet@46099
   364
refute
webertj@14350
   365
oops
webertj@14350
   366
webertj@14350
   367
lemma "P (A::'a set set)"
blanchet@46099
   368
refute
webertj@14350
   369
oops
webertj@14350
   370
webertj@14350
   371
lemma "{x. P x} = {y. P y}"
blanchet@46099
   372
refute
blanchet@46099
   373
by simp
webertj@14350
   374
webertj@14350
   375
lemma "x : {x. P x}"
blanchet@46099
   376
refute
webertj@14350
   377
oops
webertj@14350
   378
webertj@14455
   379
lemma "P op:"
blanchet@46099
   380
refute
webertj@14455
   381
oops
webertj@14455
   382
webertj@14455
   383
lemma "P (op: x)"
blanchet@46099
   384
refute
webertj@14455
   385
oops
webertj@14455
   386
webertj@14455
   387
lemma "P Collect"
blanchet@46099
   388
refute
webertj@14455
   389
oops
webertj@14455
   390
webertj@14350
   391
lemma "A Un B = A Int B"
blanchet@46099
   392
refute
webertj@14350
   393
oops
webertj@14350
   394
webertj@14350
   395
lemma "(A Int B) Un C = (A Un C) Int B"
blanchet@46099
   396
refute
webertj@14350
   397
oops
webertj@14350
   398
webertj@14350
   399
lemma "Ball A P \<longrightarrow> Bex A P"
blanchet@46099
   400
refute
webertj@14455
   401
oops
webertj@14455
   402
webertj@25014
   403
(*****************************************************************************)
webertj@21985
   404
haftmann@28524
   405
subsubsection {* undefined *}
webertj@14455
   406
haftmann@28524
   407
lemma "undefined"
blanchet@46099
   408
refute [expect = genuine]
webertj@14455
   409
oops
webertj@14455
   410
haftmann@28524
   411
lemma "P undefined"
blanchet@46099
   412
refute [expect = genuine]
webertj@14455
   413
oops
webertj@14455
   414
haftmann@28524
   415
lemma "undefined x"
blanchet@46099
   416
refute [expect = genuine]
webertj@14455
   417
oops
webertj@14455
   418
haftmann@28524
   419
lemma "undefined undefined"
blanchet@46099
   420
refute [expect = genuine]
webertj@14455
   421
oops
webertj@14455
   422
webertj@25014
   423
(*****************************************************************************)
webertj@21985
   424
wenzelm@23219
   425
subsubsection {* The *}
webertj@14455
   426
webertj@14455
   427
lemma "The P"
blanchet@46099
   428
refute [expect = genuine]
webertj@14455
   429
oops
webertj@14455
   430
webertj@14455
   431
lemma "P The"
blanchet@46099
   432
refute [expect = genuine]
webertj@14350
   433
oops
webertj@14350
   434
webertj@14455
   435
lemma "P (The P)"
blanchet@46099
   436
refute [expect = genuine]
webertj@14455
   437
oops
webertj@14455
   438
webertj@14455
   439
lemma "(THE x. x=y) = z"
blanchet@46099
   440
refute [expect = genuine]
webertj@14455
   441
oops
webertj@14455
   442
webertj@14455
   443
lemma "Ex P \<longrightarrow> P (The P)"
blanchet@46099
   444
refute [expect = genuine]
webertj@14455
   445
oops
webertj@14455
   446
webertj@25014
   447
(*****************************************************************************)
webertj@21985
   448
wenzelm@23219
   449
subsubsection {* Eps *}
webertj@14455
   450
webertj@14455
   451
lemma "Eps P"
blanchet@46099
   452
refute [expect = genuine]
webertj@14455
   453
oops
webertj@14455
   454
webertj@14455
   455
lemma "P Eps"
blanchet@46099
   456
refute [expect = genuine]
webertj@14455
   457
oops
webertj@14455
   458
webertj@14455
   459
lemma "P (Eps P)"
blanchet@46099
   460
refute [expect = genuine]
webertj@14455
   461
oops
webertj@14455
   462
webertj@14455
   463
lemma "(SOME x. x=y) = z"
blanchet@46099
   464
refute [expect = genuine]
webertj@14455
   465
oops
webertj@14455
   466
webertj@14455
   467
lemma "Ex P \<longrightarrow> P (Eps P)"
blanchet@46099
   468
refute [maxsize = 3, expect = none]
blanchet@46099
   469
by (auto simp add: someI)
webertj@14455
   470
webertj@25014
   471
(*****************************************************************************)
webertj@15767
   472
wenzelm@23219
   473
subsubsection {* Subtypes (typedef), typedecl *}
webertj@14809
   474
webertj@15161
   475
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
webertj@15161
   476
wenzelm@45694
   477
definition "myTdef = insert (undefined::'a) (undefined::'a set)"
wenzelm@45694
   478
wenzelm@49834
   479
typedef 'a myTdef = "myTdef :: 'a set"
wenzelm@45694
   480
  unfolding myTdef_def by auto
webertj@14809
   481
webertj@14809
   482
lemma "(x::'a myTdef) = y"
blanchet@46099
   483
refute
webertj@14809
   484
oops
webertj@14809
   485
webertj@14809
   486
typedecl myTdecl
webertj@14809
   487
wenzelm@45694
   488
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
wenzelm@45694
   489
wenzelm@49834
   490
typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
wenzelm@45694
   491
  unfolding T_bij_def by auto
webertj@14809
   492
webertj@14809
   493
lemma "P (f::(myTdecl myTdef) T_bij)"
blanchet@46099
   494
refute
webertj@14809
   495
oops
webertj@14809
   496
webertj@25014
   497
(*****************************************************************************)
webertj@15767
   498
wenzelm@23219
   499
subsubsection {* Inductive datatypes *}
webertj@14350
   500
wenzelm@23219
   501
text {* unit *}
webertj@14350
   502
webertj@14350
   503
lemma "P (x::unit)"
blanchet@46099
   504
refute [expect = genuine]
webertj@14350
   505
oops
webertj@14350
   506
webertj@14350
   507
lemma "\<forall>x::unit. P x"
blanchet@46099
   508
refute [expect = genuine]
webertj@14350
   509
oops
webertj@14350
   510
webertj@14350
   511
lemma "P ()"
blanchet@46099
   512
refute [expect = genuine]
webertj@14350
   513
oops
webertj@14350
   514
webertj@15547
   515
lemma "P (case x of () \<Rightarrow> u)"
blanchet@46099
   516
refute [expect = genuine]
webertj@15547
   517
oops
webertj@15547
   518
wenzelm@23219
   519
text {* option *}
webertj@14455
   520
webertj@14455
   521
lemma "P (x::'a option)"
blanchet@46099
   522
refute [expect = genuine]
webertj@14455
   523
oops
webertj@14455
   524
webertj@14455
   525
lemma "\<forall>x::'a option. P x"
blanchet@46099
   526
refute [expect = genuine]
webertj@14455
   527
oops
webertj@14455
   528
webertj@14809
   529
lemma "P None"
blanchet@46099
   530
refute [expect = genuine]
webertj@14809
   531
oops
webertj@14809
   532
webertj@14455
   533
lemma "P (Some x)"
blanchet@46099
   534
refute [expect = genuine]
webertj@14455
   535
oops
webertj@14455
   536
webertj@15547
   537
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
blanchet@46099
   538
refute [expect = genuine]
webertj@15547
   539
oops
webertj@15547
   540
wenzelm@23219
   541
text {* * *}
webertj@14350
   542
webertj@14350
   543
lemma "P (x::'a*'b)"
blanchet@46099
   544
refute [expect = genuine]
webertj@14350
   545
oops
webertj@14350
   546
webertj@14350
   547
lemma "\<forall>x::'a*'b. P x"
blanchet@46099
   548
refute [expect = genuine]
webertj@14350
   549
oops
webertj@14350
   550
webertj@25014
   551
lemma "P (x, y)"
blanchet@46099
   552
refute [expect = genuine]
webertj@14350
   553
oops
webertj@14350
   554
webertj@14350
   555
lemma "P (fst x)"
blanchet@46099
   556
refute [expect = genuine]
webertj@14350
   557
oops
webertj@14350
   558
webertj@14350
   559
lemma "P (snd x)"
blanchet@46099
   560
refute [expect = genuine]
webertj@14455
   561
oops
webertj@14455
   562
webertj@14455
   563
lemma "P Pair"
blanchet@46099
   564
refute [expect = genuine]
webertj@14350
   565
oops
webertj@14350
   566
webertj@15547
   567
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
blanchet@46099
   568
refute [expect = genuine]
webertj@15547
   569
oops
webertj@15547
   570
wenzelm@23219
   571
text {* + *}
webertj@14350
   572
webertj@14350
   573
lemma "P (x::'a+'b)"
blanchet@46099
   574
refute [expect = genuine]
webertj@14350
   575
oops
webertj@14350
   576
webertj@14350
   577
lemma "\<forall>x::'a+'b. P x"
blanchet@46099
   578
refute [expect = genuine]
webertj@14350
   579
oops
webertj@14350
   580
webertj@14350
   581
lemma "P (Inl x)"
blanchet@46099
   582
refute [expect = genuine]
webertj@14350
   583
oops
webertj@14350
   584
webertj@14350
   585
lemma "P (Inr x)"
blanchet@46099
   586
refute [expect = genuine]
webertj@14455
   587
oops
webertj@14455
   588
webertj@14455
   589
lemma "P Inl"
blanchet@46099
   590
refute [expect = genuine]
webertj@14350
   591
oops
webertj@14350
   592
webertj@15547
   593
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
blanchet@46099
   594
refute [expect = genuine]
webertj@15547
   595
oops
webertj@15547
   596
wenzelm@23219
   597
text {* Non-recursive datatypes *}
webertj@14350
   598
blanchet@58310
   599
datatype T1 = A | B
webertj@14350
   600
webertj@14350
   601
lemma "P (x::T1)"
blanchet@46099
   602
refute [expect = genuine]
webertj@14350
   603
oops
webertj@14350
   604
webertj@14350
   605
lemma "\<forall>x::T1. P x"
blanchet@46099
   606
refute [expect = genuine]
webertj@14350
   607
oops
webertj@14350
   608
webertj@14455
   609
lemma "P A"
blanchet@46099
   610
refute [expect = genuine]
webertj@14350
   611
oops
webertj@14350
   612
webertj@25014
   613
lemma "P B"
blanchet@46099
   614
refute [expect = genuine]
webertj@25014
   615
oops
webertj@25014
   616
blanchet@55416
   617
lemma "rec_T1 a b A = a"
blanchet@46099
   618
refute [expect = none]
blanchet@46099
   619
by simp
webertj@25014
   620
blanchet@55416
   621
lemma "rec_T1 a b B = b"
blanchet@46099
   622
refute [expect = none]
blanchet@46099
   623
by simp
webertj@25014
   624
blanchet@55416
   625
lemma "P (rec_T1 a b x)"
blanchet@46099
   626
refute [expect = genuine]
webertj@15547
   627
oops
webertj@15547
   628
webertj@15547
   629
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
blanchet@46099
   630
refute [expect = genuine]
webertj@15547
   631
oops
webertj@15547
   632
blanchet@58310
   633
datatype 'a T2 = C T1 | D 'a
webertj@14455
   634
webertj@14455
   635
lemma "P (x::'a T2)"
blanchet@46099
   636
refute [expect = genuine]
webertj@14350
   637
oops
webertj@14350
   638
webertj@14455
   639
lemma "\<forall>x::'a T2. P x"
blanchet@46099
   640
refute [expect = genuine]
webertj@14350
   641
oops
webertj@14350
   642
webertj@14455
   643
lemma "P D"
blanchet@46099
   644
refute [expect = genuine]
webertj@14350
   645
oops
webertj@14350
   646
blanchet@55416
   647
lemma "rec_T2 c d (C x) = c x"
blanchet@46099
   648
refute [maxsize = 4, expect = none]
blanchet@46099
   649
by simp
webertj@25014
   650
blanchet@55416
   651
lemma "rec_T2 c d (D x) = d x"
blanchet@46099
   652
refute [maxsize = 4, expect = none]
blanchet@46099
   653
by simp
webertj@25014
   654
blanchet@55416
   655
lemma "P (rec_T2 c d x)"
blanchet@46099
   656
refute [expect = genuine]
webertj@15547
   657
oops
webertj@15547
   658
webertj@15547
   659
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
blanchet@46099
   660
refute [expect = genuine]
webertj@15547
   661
oops
webertj@15547
   662
blanchet@58310
   663
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
webertj@14455
   664
webertj@14809
   665
lemma "P (x::('a,'b) T3)"
blanchet@46099
   666
refute [expect = genuine]
webertj@14809
   667
oops
webertj@14809
   668
webertj@14809
   669
lemma "\<forall>x::('a,'b) T3. P x"
blanchet@46099
   670
refute [expect = genuine]
webertj@14809
   671
oops
webertj@14809
   672
webertj@14455
   673
lemma "P E"
blanchet@46099
   674
refute [expect = genuine]
webertj@14350
   675
oops
webertj@14350
   676
blanchet@55416
   677
lemma "rec_T3 e (E x) = e x"
blanchet@46099
   678
refute [maxsize = 2, expect = none]
blanchet@46099
   679
by simp
webertj@25014
   680
blanchet@55416
   681
lemma "P (rec_T3 e x)"
blanchet@46099
   682
refute [expect = genuine]
webertj@15547
   683
oops
webertj@15547
   684
webertj@15547
   685
lemma "P (case x of E f \<Rightarrow> e f)"
blanchet@46099
   686
refute [expect = genuine]
webertj@15547
   687
oops
webertj@15547
   688
wenzelm@23219
   689
text {* Recursive datatypes *}
webertj@14350
   690
webertj@15547
   691
text {* nat *}
webertj@15547
   692
webertj@14809
   693
lemma "P (x::nat)"
blanchet@46099
   694
refute [expect = potential]
webertj@14809
   695
oops
webertj@14350
   696
webertj@14809
   697
lemma "\<forall>x::nat. P x"
blanchet@46099
   698
refute [expect = potential]
webertj@14350
   699
oops
webertj@14350
   700
webertj@14809
   701
lemma "P (Suc 0)"
blanchet@46099
   702
refute [expect = potential]
webertj@14350
   703
oops
webertj@14350
   704
webertj@14809
   705
lemma "P Suc"
blanchet@46099
   706
refute [maxsize = 3, expect = none]
blanchet@46099
   707
-- {* @{term Suc} is a partial function (regardless of the size
blanchet@46099
   708
      of the model), hence @{term "P Suc"} is undefined and no
blanchet@46099
   709
      model will be found *}
webertj@14350
   710
oops
webertj@14350
   711
blanchet@55415
   712
lemma "rec_nat zero suc 0 = zero"
blanchet@46099
   713
refute [expect = none]
blanchet@46099
   714
by simp
webertj@25014
   715
blanchet@55415
   716
lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
blanchet@46099
   717
refute [maxsize = 2, expect = none]
blanchet@46099
   718
by simp
webertj@25014
   719
blanchet@55415
   720
lemma "P (rec_nat zero suc x)"
blanchet@46099
   721
refute [expect = potential]
webertj@15547
   722
oops
webertj@15547
   723
webertj@15547
   724
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
blanchet@46099
   725
refute [expect = potential]
webertj@15547
   726
oops
webertj@15547
   727
webertj@15547
   728
text {* 'a list *}
webertj@15547
   729
webertj@15547
   730
lemma "P (xs::'a list)"
blanchet@46099
   731
refute [expect = potential]
webertj@15547
   732
oops
webertj@15547
   733
webertj@15547
   734
lemma "\<forall>xs::'a list. P xs"
blanchet@46099
   735
refute [expect = potential]
webertj@15547
   736
oops
webertj@15547
   737
webertj@15547
   738
lemma "P [x, y]"
blanchet@46099
   739
refute [expect = potential]
webertj@15547
   740
oops
webertj@15547
   741
blanchet@55413
   742
lemma "rec_list nil cons [] = nil"
blanchet@46099
   743
refute [maxsize = 3, expect = none]
blanchet@46099
   744
by simp
webertj@25014
   745
blanchet@55413
   746
lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
blanchet@46099
   747
refute [maxsize = 2, expect = none]
blanchet@46099
   748
by simp
webertj@25014
   749
blanchet@55413
   750
lemma "P (rec_list nil cons xs)"
blanchet@46099
   751
refute [expect = potential]
webertj@15547
   752
oops
webertj@15547
   753
webertj@15547
   754
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
blanchet@46099
   755
refute [expect = potential]
webertj@15547
   756
oops
webertj@15547
   757
webertj@15547
   758
lemma "(xs::'a list) = ys"
blanchet@46099
   759
refute [expect = potential]
webertj@15547
   760
oops
webertj@15547
   761
webertj@15547
   762
lemma "a # xs = b # xs"
blanchet@46099
   763
refute [expect = potential]
webertj@15547
   764
oops
webertj@15547
   765
blanchet@58310
   766
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
webertj@25014
   767
webertj@25014
   768
lemma "P (x::BitList)"
blanchet@46099
   769
refute [expect = potential]
webertj@25014
   770
oops
webertj@25014
   771
webertj@25014
   772
lemma "\<forall>x::BitList. P x"
blanchet@46099
   773
refute [expect = potential]
webertj@25014
   774
oops
webertj@25014
   775
webertj@25014
   776
lemma "P (Bit0 (Bit1 BitListNil))"
blanchet@46099
   777
refute [expect = potential]
webertj@25014
   778
oops
webertj@25014
   779
blanchet@55416
   780
lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
blanchet@46099
   781
refute [maxsize = 4, expect = none]
blanchet@46099
   782
by simp
webertj@25014
   783
blanchet@55416
   784
lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
blanchet@46099
   785
refute [maxsize = 2, expect = none]
blanchet@46099
   786
by simp
webertj@25014
   787
blanchet@55416
   788
lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
blanchet@46099
   789
refute [maxsize = 2, expect = none]
blanchet@46099
   790
by simp
webertj@25014
   791
blanchet@55416
   792
lemma "P (rec_BitList nil bit0 bit1 x)"
blanchet@46099
   793
refute [expect = potential]
webertj@25014
   794
oops
webertj@25014
   795
webertj@25014
   796
(*****************************************************************************)
webertj@15767
   797
wenzelm@23219
   798
subsubsection {* Examples involving special functions *}
webertj@15547
   799
webertj@15547
   800
lemma "card x = 0"
blanchet@58143
   801
refute [expect = potential]
webertj@15547
   802
oops
webertj@15547
   803
webertj@15767
   804
lemma "finite x"
blanchet@46099
   805
refute -- {* no finite countermodel exists *}
webertj@15547
   806
oops
webertj@15547
   807
webertj@15547
   808
lemma "(x::nat) + y = 0"
blanchet@46099
   809
refute [expect = potential]
webertj@15547
   810
oops
webertj@15547
   811
webertj@15547
   812
lemma "(x::nat) = x + x"
blanchet@46099
   813
refute [expect = potential]
webertj@15547
   814
oops
webertj@15547
   815
webertj@15547
   816
lemma "(x::nat) - y + y = x"
blanchet@46099
   817
refute [expect = potential]
webertj@15547
   818
oops
webertj@15547
   819
webertj@15547
   820
lemma "(x::nat) = x * x"
blanchet@46099
   821
refute [expect = potential]
webertj@15547
   822
oops
webertj@15547
   823
webertj@15547
   824
lemma "(x::nat) < x + y"
blanchet@46099
   825
refute [expect = potential]
webertj@15547
   826
oops
webertj@15547
   827
webertj@21985
   828
lemma "xs @ [] = ys @ []"
blanchet@46099
   829
refute [expect = potential]
webertj@15547
   830
oops
webertj@15547
   831
webertj@21985
   832
lemma "xs @ ys = ys @ xs"
blanchet@46099
   833
refute [expect = potential]
webertj@15547
   834
oops
webertj@15547
   835
webertj@25014
   836
(*****************************************************************************)
webertj@15547
   837
haftmann@35315
   838
subsubsection {* Type classes and overloading *}
webertj@15547
   839
webertj@15547
   840
text {* A type class without axioms: *}
webertj@15547
   841
haftmann@35315
   842
class classA
webertj@15547
   843
webertj@15547
   844
lemma "P (x::'a::classA)"
blanchet@46099
   845
refute [expect = genuine]
webertj@14809
   846
oops
webertj@14809
   847
webertj@15547
   848
text {* An axiom with a type variable (denoting types which have at least two elements): *}
webertj@15547
   849
haftmann@35315
   850
class classC =
haftmann@35315
   851
  assumes classC_ax: "\<exists>x y. x \<noteq> y"
webertj@15547
   852
webertj@15547
   853
lemma "P (x::'a::classC)"
blanchet@46099
   854
refute [expect = genuine]
webertj@15547
   855
oops
webertj@15547
   856
webertj@15547
   857
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
blanchet@46099
   858
(* refute [expect = none] FIXME *)
webertj@15547
   859
oops
webertj@15547
   860
webertj@15547
   861
text {* A type class for which a constant is defined: *}
webertj@15547
   862
haftmann@35315
   863
class classD =
haftmann@35315
   864
  fixes classD_const :: "'a \<Rightarrow> 'a"
haftmann@35315
   865
  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
webertj@15547
   866
webertj@15547
   867
lemma "P (x::'a::classD)"
blanchet@46099
   868
refute [expect = genuine]
webertj@15547
   869
oops
webertj@15547
   870
webertj@15547
   871
text {* A type class with multiple superclasses: *}
webertj@15547
   872
haftmann@35315
   873
class classE = classC + classD
webertj@15547
   874
webertj@15547
   875
lemma "P (x::'a::classE)"
blanchet@46099
   876
refute [expect = genuine]
webertj@14809
   877
oops
webertj@14809
   878
webertj@15547
   879
text {* OFCLASS: *}
webertj@15547
   880
webertj@15547
   881
lemma "OFCLASS('a::type, type_class)"
blanchet@46099
   882
refute [expect = none]
blanchet@46099
   883
by intro_classes
webertj@15547
   884
webertj@15547
   885
lemma "OFCLASS('a::classC, type_class)"
blanchet@46099
   886
refute [expect = none]
blanchet@46099
   887
by intro_classes
webertj@15547
   888
webertj@15547
   889
lemma "OFCLASS('a::type, classC_class)"
blanchet@46099
   890
refute [expect = genuine]
webertj@15547
   891
oops
webertj@15547
   892
webertj@15547
   893
text {* Overloading: *}
webertj@15547
   894
webertj@15547
   895
consts inverse :: "'a \<Rightarrow> 'a"
webertj@15547
   896
webertj@15547
   897
defs (overloaded)
webertj@15547
   898
  inverse_bool: "inverse (b::bool)   == ~ b"
webertj@15547
   899
  inverse_set : "inverse (S::'a set) == -S"
webertj@15547
   900
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
webertj@15547
   901
webertj@15547
   902
lemma "inverse b"
blanchet@46099
   903
refute [expect = genuine]
webertj@15547
   904
oops
webertj@15547
   905
webertj@15547
   906
lemma "P (inverse (S::'a set))"
blanchet@46099
   907
refute [expect = genuine]
webertj@15547
   908
oops
webertj@15547
   909
webertj@15547
   910
lemma "P (inverse (p::'a\<times>'b))"
blanchet@46099
   911
refute [expect = genuine]
webertj@14350
   912
oops
webertj@14350
   913
blanchet@34120
   914
text {* Structured proofs *}
blanchet@34120
   915
blanchet@34120
   916
lemma "x = y"
blanchet@34120
   917
proof cases
blanchet@34120
   918
  assume "x = y"
blanchet@34120
   919
  show ?thesis
blanchet@46099
   920
  refute [expect = none]
blanchet@46099
   921
  refute [no_assms, expect = genuine]
blanchet@46099
   922
  refute [no_assms = false, expect = none]
blanchet@34120
   923
oops
blanchet@34120
   924
blanchet@46099
   925
refute_params [satsolver = "auto"]
webertj@18774
   926
webertj@14350
   927
end