src/HOL/ex/Refute_Examples.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 49988 ef811090e106
child 55395 4e79187f847e
permissions -rw-r--r--
introduce order topology
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
webertj@14350
     8
header {* 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@46099
    14
refute_params [satsolver = "dpll"]
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@46099
    23
refute [satsolver = "dpll", 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 {* "The union of transitive closures is equal to the transitive closure of unions." *}
webertj@14350
   263
webertj@14350
   264
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
   265
        \<longrightarrow> trans_closure TP P
webertj@14350
   266
        \<longrightarrow> trans_closure TR R
webertj@14350
   267
        \<longrightarrow> (T x y = (TP x y | TR x y))"
blanchet@46099
   268
refute [expect = genuine]
webertj@14350
   269
oops
webertj@14350
   270
webertj@14350
   271
text {* "Every surjective function is invertible." *}
webertj@14350
   272
webertj@14350
   273
lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
blanchet@46099
   274
refute [expect = genuine]
webertj@14350
   275
oops
webertj@14350
   276
webertj@14350
   277
text {* "Every invertible function is surjective." *}
webertj@14350
   278
webertj@14350
   279
lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
blanchet@46099
   280
refute [expect = genuine]
webertj@14350
   281
oops
webertj@14350
   282
webertj@14350
   283
text {* Every point is a fixed point of some function. *}
webertj@14350
   284
webertj@14350
   285
lemma "\<exists>f. f x = x"
blanchet@46099
   286
refute [maxsize = 4, expect = none]
blanchet@46099
   287
apply (rule_tac x="\<lambda>x. x" in exI)
blanchet@46099
   288
by simp
webertj@14350
   289
webertj@14465
   290
text {* Axiom of Choice: first an incorrect version ... *}
webertj@14350
   291
webertj@14350
   292
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
blanchet@46099
   293
refute [expect = genuine]
webertj@14350
   294
oops
webertj@14350
   295
webertj@14465
   296
text {* ... and now two correct ones *}
webertj@14350
   297
webertj@14350
   298
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
blanchet@46099
   299
refute [maxsize = 4, expect = none]
blanchet@46099
   300
by (simp add: choice)
webertj@14350
   301
webertj@14350
   302
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
blanchet@46099
   303
refute [maxsize = 2, expect = none]
blanchet@46099
   304
apply auto
blanchet@46099
   305
  apply (simp add: ex1_implies_ex choice)
blanchet@46099
   306
by (fast intro: ext)
webertj@14350
   307
webertj@25014
   308
(*****************************************************************************)
webertj@21985
   309
wenzelm@23219
   310
subsubsection {* Meta-logic *}
webertj@14350
   311
webertj@14350
   312
lemma "!!x. P x"
blanchet@46099
   313
refute [expect = genuine]
webertj@14350
   314
oops
webertj@14350
   315
webertj@14350
   316
lemma "f x == g x"
blanchet@46099
   317
refute [expect = genuine]
webertj@14350
   318
oops
webertj@14350
   319
webertj@14350
   320
lemma "P \<Longrightarrow> Q"
blanchet@46099
   321
refute [expect = genuine]
webertj@14350
   322
oops
webertj@14350
   323
webertj@14350
   324
lemma "\<lbrakk> P; Q; R \<rbrakk> \<Longrightarrow> S"
blanchet@46099
   325
refute [expect = genuine]
webertj@14350
   326
oops
webertj@14350
   327
webertj@21985
   328
lemma "(x == all) \<Longrightarrow> False"
blanchet@46099
   329
refute [expect = genuine]
webertj@21985
   330
oops
webertj@21985
   331
webertj@21985
   332
lemma "(x == (op ==)) \<Longrightarrow> False"
blanchet@46099
   333
refute [expect = genuine]
webertj@21985
   334
oops
webertj@21985
   335
webertj@21985
   336
lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
blanchet@46099
   337
refute [expect = genuine]
webertj@21985
   338
oops
webertj@21985
   339
webertj@25014
   340
(*****************************************************************************)
webertj@21985
   341
wenzelm@23219
   342
subsubsection {* Schematic variables *}
webertj@14350
   343
wenzelm@36319
   344
schematic_lemma "?P"
blanchet@46099
   345
refute [expect = none]
blanchet@46099
   346
by auto
webertj@14350
   347
wenzelm@36319
   348
schematic_lemma "x = ?y"
blanchet@46099
   349
refute [expect = none]
blanchet@46099
   350
by auto
webertj@14350
   351
webertj@21985
   352
(******************************************************************************)
webertj@21985
   353
wenzelm@23219
   354
subsubsection {* Abstractions *}
webertj@14350
   355
webertj@14350
   356
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
blanchet@46099
   357
refute [expect = genuine]
webertj@14350
   358
oops
webertj@14350
   359
webertj@14350
   360
lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
blanchet@46099
   361
refute [expect = genuine]
webertj@14350
   362
oops
webertj@14350
   363
webertj@14350
   364
lemma "(\<lambda>x. x) = (\<lambda>y. y)"
blanchet@46099
   365
refute
blanchet@46099
   366
by simp
webertj@14350
   367
webertj@25014
   368
(*****************************************************************************)
webertj@21985
   369
wenzelm@23219
   370
subsubsection {* Sets *}
webertj@14350
   371
webertj@14350
   372
lemma "P (A::'a set)"
blanchet@46099
   373
refute
webertj@14350
   374
oops
webertj@14350
   375
webertj@14350
   376
lemma "P (A::'a set set)"
blanchet@46099
   377
refute
webertj@14350
   378
oops
webertj@14350
   379
webertj@14350
   380
lemma "{x. P x} = {y. P y}"
blanchet@46099
   381
refute
blanchet@46099
   382
by simp
webertj@14350
   383
webertj@14350
   384
lemma "x : {x. P x}"
blanchet@46099
   385
refute
webertj@14350
   386
oops
webertj@14350
   387
webertj@14455
   388
lemma "P op:"
blanchet@46099
   389
refute
webertj@14455
   390
oops
webertj@14455
   391
webertj@14455
   392
lemma "P (op: x)"
blanchet@46099
   393
refute
webertj@14455
   394
oops
webertj@14455
   395
webertj@14455
   396
lemma "P Collect"
blanchet@46099
   397
refute
webertj@14455
   398
oops
webertj@14455
   399
webertj@14350
   400
lemma "A Un B = A Int B"
blanchet@46099
   401
refute
webertj@14350
   402
oops
webertj@14350
   403
webertj@14350
   404
lemma "(A Int B) Un C = (A Un C) Int B"
blanchet@46099
   405
refute
webertj@14350
   406
oops
webertj@14350
   407
webertj@14350
   408
lemma "Ball A P \<longrightarrow> Bex A P"
blanchet@46099
   409
refute
webertj@14455
   410
oops
webertj@14455
   411
webertj@25014
   412
(*****************************************************************************)
webertj@21985
   413
haftmann@28524
   414
subsubsection {* undefined *}
webertj@14455
   415
haftmann@28524
   416
lemma "undefined"
blanchet@46099
   417
refute [expect = genuine]
webertj@14455
   418
oops
webertj@14455
   419
haftmann@28524
   420
lemma "P undefined"
blanchet@46099
   421
refute [expect = genuine]
webertj@14455
   422
oops
webertj@14455
   423
haftmann@28524
   424
lemma "undefined x"
blanchet@46099
   425
refute [expect = genuine]
webertj@14455
   426
oops
webertj@14455
   427
haftmann@28524
   428
lemma "undefined undefined"
blanchet@46099
   429
refute [expect = genuine]
webertj@14455
   430
oops
webertj@14455
   431
webertj@25014
   432
(*****************************************************************************)
webertj@21985
   433
wenzelm@23219
   434
subsubsection {* The *}
webertj@14455
   435
webertj@14455
   436
lemma "The P"
blanchet@46099
   437
refute [expect = genuine]
webertj@14455
   438
oops
webertj@14455
   439
webertj@14455
   440
lemma "P The"
blanchet@46099
   441
refute [expect = genuine]
webertj@14350
   442
oops
webertj@14350
   443
webertj@14455
   444
lemma "P (The P)"
blanchet@46099
   445
refute [expect = genuine]
webertj@14455
   446
oops
webertj@14455
   447
webertj@14455
   448
lemma "(THE x. x=y) = z"
blanchet@46099
   449
refute [expect = genuine]
webertj@14455
   450
oops
webertj@14455
   451
webertj@14455
   452
lemma "Ex P \<longrightarrow> P (The P)"
blanchet@46099
   453
refute [expect = genuine]
webertj@14455
   454
oops
webertj@14455
   455
webertj@25014
   456
(*****************************************************************************)
webertj@21985
   457
wenzelm@23219
   458
subsubsection {* Eps *}
webertj@14455
   459
webertj@14455
   460
lemma "Eps P"
blanchet@46099
   461
refute [expect = genuine]
webertj@14455
   462
oops
webertj@14455
   463
webertj@14455
   464
lemma "P Eps"
blanchet@46099
   465
refute [expect = genuine]
webertj@14455
   466
oops
webertj@14455
   467
webertj@14455
   468
lemma "P (Eps P)"
blanchet@46099
   469
refute [expect = genuine]
webertj@14455
   470
oops
webertj@14455
   471
webertj@14455
   472
lemma "(SOME x. x=y) = z"
blanchet@46099
   473
refute [expect = genuine]
webertj@14455
   474
oops
webertj@14455
   475
webertj@14455
   476
lemma "Ex P \<longrightarrow> P (Eps P)"
blanchet@46099
   477
refute [maxsize = 3, expect = none]
blanchet@46099
   478
by (auto simp add: someI)
webertj@14455
   479
webertj@25014
   480
(*****************************************************************************)
webertj@15767
   481
wenzelm@23219
   482
subsubsection {* Subtypes (typedef), typedecl *}
webertj@14809
   483
webertj@15161
   484
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
webertj@15161
   485
wenzelm@45694
   486
definition "myTdef = insert (undefined::'a) (undefined::'a set)"
wenzelm@45694
   487
wenzelm@49834
   488
typedef 'a myTdef = "myTdef :: 'a set"
wenzelm@45694
   489
  unfolding myTdef_def by auto
webertj@14809
   490
webertj@14809
   491
lemma "(x::'a myTdef) = y"
blanchet@46099
   492
refute
webertj@14809
   493
oops
webertj@14809
   494
webertj@14809
   495
typedecl myTdecl
webertj@14809
   496
wenzelm@45694
   497
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
wenzelm@45694
   498
wenzelm@49834
   499
typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
wenzelm@45694
   500
  unfolding T_bij_def by auto
webertj@14809
   501
webertj@14809
   502
lemma "P (f::(myTdecl myTdef) T_bij)"
blanchet@46099
   503
refute
webertj@14809
   504
oops
webertj@14809
   505
webertj@25014
   506
(*****************************************************************************)
webertj@15767
   507
wenzelm@23219
   508
subsubsection {* Inductive datatypes *}
webertj@14350
   509
wenzelm@21502
   510
text {* With @{text quick_and_dirty} set, the datatype package does
wenzelm@21502
   511
  not generate certain axioms for recursion operators.  Without these
blanchet@46099
   512
  axioms, Refute may find spurious countermodels. *}
webertj@15547
   513
wenzelm@23219
   514
text {* unit *}
webertj@14350
   515
webertj@14350
   516
lemma "P (x::unit)"
blanchet@46099
   517
refute [expect = genuine]
webertj@14350
   518
oops
webertj@14350
   519
webertj@14350
   520
lemma "\<forall>x::unit. P x"
blanchet@46099
   521
refute [expect = genuine]
webertj@14350
   522
oops
webertj@14350
   523
webertj@14350
   524
lemma "P ()"
blanchet@46099
   525
refute [expect = genuine]
webertj@14350
   526
oops
webertj@14350
   527
webertj@25014
   528
lemma "unit_rec u x = u"
blanchet@46099
   529
refute [expect = none]
blanchet@46099
   530
by simp
webertj@25014
   531
webertj@15547
   532
lemma "P (unit_rec u x)"
blanchet@46099
   533
refute [expect = genuine]
webertj@15547
   534
oops
webertj@15547
   535
webertj@15547
   536
lemma "P (case x of () \<Rightarrow> u)"
blanchet@46099
   537
refute [expect = genuine]
webertj@15547
   538
oops
webertj@15547
   539
wenzelm@23219
   540
text {* option *}
webertj@14455
   541
webertj@14455
   542
lemma "P (x::'a option)"
blanchet@46099
   543
refute [expect = genuine]
webertj@14455
   544
oops
webertj@14455
   545
webertj@14455
   546
lemma "\<forall>x::'a option. P x"
blanchet@46099
   547
refute [expect = genuine]
webertj@14455
   548
oops
webertj@14455
   549
webertj@14809
   550
lemma "P None"
blanchet@46099
   551
refute [expect = genuine]
webertj@14809
   552
oops
webertj@14809
   553
webertj@14455
   554
lemma "P (Some x)"
blanchet@46099
   555
refute [expect = genuine]
webertj@14455
   556
oops
webertj@14455
   557
webertj@25014
   558
lemma "option_rec n s None = n"
blanchet@46099
   559
refute [expect = none]
blanchet@46099
   560
by simp
webertj@25014
   561
webertj@25014
   562
lemma "option_rec n s (Some x) = s x"
blanchet@46099
   563
refute [maxsize = 4, expect = none]
blanchet@46099
   564
by simp
webertj@25014
   565
webertj@15547
   566
lemma "P (option_rec n s x)"
blanchet@46099
   567
refute [expect = genuine]
webertj@15547
   568
oops
webertj@15547
   569
webertj@15547
   570
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
blanchet@46099
   571
refute [expect = genuine]
webertj@15547
   572
oops
webertj@15547
   573
wenzelm@23219
   574
text {* * *}
webertj@14350
   575
webertj@14350
   576
lemma "P (x::'a*'b)"
blanchet@46099
   577
refute [expect = genuine]
webertj@14350
   578
oops
webertj@14350
   579
webertj@14350
   580
lemma "\<forall>x::'a*'b. P x"
blanchet@46099
   581
refute [expect = genuine]
webertj@14350
   582
oops
webertj@14350
   583
webertj@25014
   584
lemma "P (x, y)"
blanchet@46099
   585
refute [expect = genuine]
webertj@14350
   586
oops
webertj@14350
   587
webertj@14350
   588
lemma "P (fst x)"
blanchet@46099
   589
refute [expect = genuine]
webertj@14350
   590
oops
webertj@14350
   591
webertj@14350
   592
lemma "P (snd x)"
blanchet@46099
   593
refute [expect = genuine]
webertj@14455
   594
oops
webertj@14455
   595
webertj@14455
   596
lemma "P Pair"
blanchet@46099
   597
refute [expect = genuine]
webertj@14350
   598
oops
webertj@14350
   599
webertj@25014
   600
lemma "prod_rec p (a, b) = p a b"
blanchet@46099
   601
refute [maxsize = 2, expect = none]
blanchet@46099
   602
by simp
webertj@25014
   603
webertj@15547
   604
lemma "P (prod_rec p x)"
blanchet@46099
   605
refute [expect = genuine]
webertj@15547
   606
oops
webertj@15547
   607
webertj@15547
   608
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
blanchet@46099
   609
refute [expect = genuine]
webertj@15547
   610
oops
webertj@15547
   611
wenzelm@23219
   612
text {* + *}
webertj@14350
   613
webertj@14350
   614
lemma "P (x::'a+'b)"
blanchet@46099
   615
refute [expect = genuine]
webertj@14350
   616
oops
webertj@14350
   617
webertj@14350
   618
lemma "\<forall>x::'a+'b. P x"
blanchet@46099
   619
refute [expect = genuine]
webertj@14350
   620
oops
webertj@14350
   621
webertj@14350
   622
lemma "P (Inl x)"
blanchet@46099
   623
refute [expect = genuine]
webertj@14350
   624
oops
webertj@14350
   625
webertj@14350
   626
lemma "P (Inr x)"
blanchet@46099
   627
refute [expect = genuine]
webertj@14455
   628
oops
webertj@14455
   629
webertj@14455
   630
lemma "P Inl"
blanchet@46099
   631
refute [expect = genuine]
webertj@14350
   632
oops
webertj@14350
   633
webertj@25014
   634
lemma "sum_rec l r (Inl x) = l x"
blanchet@46099
   635
refute [maxsize = 3, expect = none]
blanchet@46099
   636
by simp
webertj@25014
   637
webertj@25014
   638
lemma "sum_rec l r (Inr x) = r x"
blanchet@46099
   639
refute [maxsize = 3, expect = none]
blanchet@46099
   640
by simp
webertj@25014
   641
webertj@15547
   642
lemma "P (sum_rec l r x)"
blanchet@46099
   643
refute [expect = genuine]
webertj@15547
   644
oops
webertj@15547
   645
webertj@15547
   646
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
blanchet@46099
   647
refute [expect = genuine]
webertj@15547
   648
oops
webertj@15547
   649
wenzelm@23219
   650
text {* Non-recursive datatypes *}
webertj@14350
   651
webertj@14455
   652
datatype T1 = A | B
webertj@14350
   653
webertj@14350
   654
lemma "P (x::T1)"
blanchet@46099
   655
refute [expect = genuine]
webertj@14350
   656
oops
webertj@14350
   657
webertj@14350
   658
lemma "\<forall>x::T1. P x"
blanchet@46099
   659
refute [expect = genuine]
webertj@14350
   660
oops
webertj@14350
   661
webertj@14455
   662
lemma "P A"
blanchet@46099
   663
refute [expect = genuine]
webertj@14350
   664
oops
webertj@14350
   665
webertj@25014
   666
lemma "P B"
blanchet@46099
   667
refute [expect = genuine]
webertj@25014
   668
oops
webertj@25014
   669
webertj@25014
   670
lemma "T1_rec a b A = a"
blanchet@46099
   671
refute [expect = none]
blanchet@46099
   672
by simp
webertj@25014
   673
webertj@25014
   674
lemma "T1_rec a b B = b"
blanchet@46099
   675
refute [expect = none]
blanchet@46099
   676
by simp
webertj@25014
   677
webertj@15547
   678
lemma "P (T1_rec a b x)"
blanchet@46099
   679
refute [expect = genuine]
webertj@15547
   680
oops
webertj@15547
   681
webertj@15547
   682
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
blanchet@46099
   683
refute [expect = genuine]
webertj@15547
   684
oops
webertj@15547
   685
webertj@14455
   686
datatype 'a T2 = C T1 | D 'a
webertj@14455
   687
webertj@14455
   688
lemma "P (x::'a T2)"
blanchet@46099
   689
refute [expect = genuine]
webertj@14350
   690
oops
webertj@14350
   691
webertj@14455
   692
lemma "\<forall>x::'a T2. P x"
blanchet@46099
   693
refute [expect = genuine]
webertj@14350
   694
oops
webertj@14350
   695
webertj@14455
   696
lemma "P D"
blanchet@46099
   697
refute [expect = genuine]
webertj@14350
   698
oops
webertj@14350
   699
webertj@25014
   700
lemma "T2_rec c d (C x) = c x"
blanchet@46099
   701
refute [maxsize = 4, expect = none]
blanchet@46099
   702
by simp
webertj@25014
   703
webertj@25014
   704
lemma "T2_rec c d (D x) = d x"
blanchet@46099
   705
refute [maxsize = 4, expect = none]
blanchet@46099
   706
by simp
webertj@25014
   707
webertj@15547
   708
lemma "P (T2_rec c d x)"
blanchet@46099
   709
refute [expect = genuine]
webertj@15547
   710
oops
webertj@15547
   711
webertj@15547
   712
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
blanchet@46099
   713
refute [expect = genuine]
webertj@15547
   714
oops
webertj@15547
   715
webertj@14455
   716
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
webertj@14455
   717
webertj@14809
   718
lemma "P (x::('a,'b) T3)"
blanchet@46099
   719
refute [expect = genuine]
webertj@14809
   720
oops
webertj@14809
   721
webertj@14809
   722
lemma "\<forall>x::('a,'b) T3. P x"
blanchet@46099
   723
refute [expect = genuine]
webertj@14809
   724
oops
webertj@14809
   725
webertj@14455
   726
lemma "P E"
blanchet@46099
   727
refute [expect = genuine]
webertj@14350
   728
oops
webertj@14350
   729
webertj@25014
   730
lemma "T3_rec e (E x) = e x"
blanchet@46099
   731
refute [maxsize = 2, expect = none]
blanchet@46099
   732
by simp
webertj@25014
   733
webertj@15547
   734
lemma "P (T3_rec e x)"
blanchet@46099
   735
refute [expect = genuine]
webertj@15547
   736
oops
webertj@15547
   737
webertj@15547
   738
lemma "P (case x of E f \<Rightarrow> e f)"
blanchet@46099
   739
refute [expect = genuine]
webertj@15547
   740
oops
webertj@15547
   741
wenzelm@23219
   742
text {* Recursive datatypes *}
webertj@14350
   743
webertj@15547
   744
text {* nat *}
webertj@15547
   745
webertj@14809
   746
lemma "P (x::nat)"
blanchet@46099
   747
refute [expect = potential]
webertj@14809
   748
oops
webertj@14350
   749
webertj@14809
   750
lemma "\<forall>x::nat. P x"
blanchet@46099
   751
refute [expect = potential]
webertj@14350
   752
oops
webertj@14350
   753
webertj@14809
   754
lemma "P (Suc 0)"
blanchet@46099
   755
refute [expect = potential]
webertj@14350
   756
oops
webertj@14350
   757
webertj@14809
   758
lemma "P Suc"
blanchet@46099
   759
refute [maxsize = 3, expect = none]
blanchet@46099
   760
-- {* @{term Suc} is a partial function (regardless of the size
blanchet@46099
   761
      of the model), hence @{term "P Suc"} is undefined and no
blanchet@46099
   762
      model will be found *}
webertj@14350
   763
oops
webertj@14350
   764
webertj@25014
   765
lemma "nat_rec zero suc 0 = zero"
blanchet@46099
   766
refute [expect = none]
blanchet@46099
   767
by simp
webertj@25014
   768
webertj@25014
   769
lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
blanchet@46099
   770
refute [maxsize = 2, expect = none]
blanchet@46099
   771
by simp
webertj@25014
   772
webertj@15547
   773
lemma "P (nat_rec zero suc x)"
blanchet@46099
   774
refute [expect = potential]
webertj@15547
   775
oops
webertj@15547
   776
webertj@15547
   777
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
blanchet@46099
   778
refute [expect = potential]
webertj@15547
   779
oops
webertj@15547
   780
webertj@15547
   781
text {* 'a list *}
webertj@15547
   782
webertj@15547
   783
lemma "P (xs::'a list)"
blanchet@46099
   784
refute [expect = potential]
webertj@15547
   785
oops
webertj@15547
   786
webertj@15547
   787
lemma "\<forall>xs::'a list. P xs"
blanchet@46099
   788
refute [expect = potential]
webertj@15547
   789
oops
webertj@15547
   790
webertj@15547
   791
lemma "P [x, y]"
blanchet@46099
   792
refute [expect = potential]
webertj@15547
   793
oops
webertj@15547
   794
webertj@25014
   795
lemma "list_rec nil cons [] = nil"
blanchet@46099
   796
refute [maxsize = 3, expect = none]
blanchet@46099
   797
by simp
webertj@25014
   798
webertj@25014
   799
lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
blanchet@46099
   800
refute [maxsize = 2, expect = none]
blanchet@46099
   801
by simp
webertj@25014
   802
webertj@15547
   803
lemma "P (list_rec nil cons xs)"
blanchet@46099
   804
refute [expect = potential]
webertj@15547
   805
oops
webertj@15547
   806
webertj@15547
   807
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
blanchet@46099
   808
refute [expect = potential]
webertj@15547
   809
oops
webertj@15547
   810
webertj@15547
   811
lemma "(xs::'a list) = ys"
blanchet@46099
   812
refute [expect = potential]
webertj@15547
   813
oops
webertj@15547
   814
webertj@15547
   815
lemma "a # xs = b # xs"
blanchet@46099
   816
refute [expect = potential]
webertj@15547
   817
oops
webertj@15547
   818
webertj@25014
   819
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
webertj@25014
   820
webertj@25014
   821
lemma "P (x::BitList)"
blanchet@46099
   822
refute [expect = potential]
webertj@25014
   823
oops
webertj@25014
   824
webertj@25014
   825
lemma "\<forall>x::BitList. P x"
blanchet@46099
   826
refute [expect = potential]
webertj@25014
   827
oops
webertj@25014
   828
webertj@25014
   829
lemma "P (Bit0 (Bit1 BitListNil))"
blanchet@46099
   830
refute [expect = potential]
webertj@25014
   831
oops
webertj@25014
   832
webertj@25014
   833
lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
blanchet@46099
   834
refute [maxsize = 4, expect = none]
blanchet@46099
   835
by simp
webertj@25014
   836
webertj@25014
   837
lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
blanchet@46099
   838
refute [maxsize = 2, expect = none]
blanchet@46099
   839
by simp
webertj@25014
   840
webertj@25014
   841
lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
blanchet@46099
   842
refute [maxsize = 2, expect = none]
blanchet@46099
   843
by simp
webertj@25014
   844
webertj@25014
   845
lemma "P (BitList_rec nil bit0 bit1 x)"
blanchet@46099
   846
refute [expect = potential]
webertj@25014
   847
oops
webertj@25014
   848
webertj@14350
   849
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
webertj@14350
   850
webertj@14350
   851
lemma "P (x::'a BinTree)"
blanchet@46099
   852
refute [expect = potential]
webertj@14350
   853
oops
webertj@14350
   854
webertj@14350
   855
lemma "\<forall>x::'a BinTree. P x"
blanchet@46099
   856
refute [expect = potential]
webertj@14809
   857
oops
webertj@14809
   858
webertj@14809
   859
lemma "P (Node (Leaf x) (Leaf y))"
blanchet@46099
   860
refute [expect = potential]
webertj@14350
   861
oops
webertj@14350
   862
webertj@25014
   863
lemma "BinTree_rec l n (Leaf x) = l x"
blanchet@46099
   864
  refute [maxsize = 1, expect = none]
blanchet@46099
   865
  (* The "maxsize = 1" tests are a bit pointless: for some formulae
blanchet@46099
   866
     below, refute will find no countermodel simply because this
blanchet@46099
   867
     size makes involved terms undefined.  Unfortunately, any
blanchet@46099
   868
     larger size already takes too long. *)
blanchet@46099
   869
by simp
webertj@25014
   870
webertj@25014
   871
lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
blanchet@46099
   872
refute [maxsize = 1, expect = none]
blanchet@46099
   873
by simp
webertj@25014
   874
webertj@15547
   875
lemma "P (BinTree_rec l n x)"
blanchet@46099
   876
refute [expect = potential]
webertj@15547
   877
oops
webertj@15547
   878
webertj@15547
   879
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
blanchet@46099
   880
refute [expect = potential]
webertj@15547
   881
oops
webertj@15547
   882
wenzelm@23219
   883
text {* Mutually recursive datatypes *}
webertj@14350
   884
webertj@14350
   885
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
webertj@14350
   886
     and 'a bexp = Equal "'a aexp" "'a aexp"
webertj@14350
   887
webertj@14350
   888
lemma "P (x::'a aexp)"
blanchet@46099
   889
refute [expect = potential]
webertj@14350
   890
oops
webertj@14350
   891
webertj@14350
   892
lemma "\<forall>x::'a aexp. P x"
blanchet@46099
   893
refute [expect = potential]
webertj@14350
   894
oops
webertj@14350
   895
webertj@15547
   896
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
blanchet@46099
   897
refute [expect = potential]
webertj@15547
   898
oops
webertj@15547
   899
webertj@14350
   900
lemma "P (x::'a bexp)"
blanchet@46099
   901
refute [expect = potential]
webertj@14350
   902
oops
webertj@14350
   903
webertj@14350
   904
lemma "\<forall>x::'a bexp. P x"
blanchet@46099
   905
refute [expect = potential]
webertj@14350
   906
oops
webertj@14350
   907
webertj@25014
   908
lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
blanchet@46099
   909
refute [maxsize = 1, expect = none]
blanchet@46099
   910
by simp
webertj@25014
   911
webertj@25014
   912
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@46099
   913
refute [maxsize = 1, expect = none]
blanchet@46099
   914
by simp
webertj@25014
   915
webertj@15547
   916
lemma "P (aexp_bexp_rec_1 number ite equal x)"
blanchet@46099
   917
refute [expect = potential]
webertj@15547
   918
oops
webertj@15547
   919
webertj@15547
   920
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
blanchet@46099
   921
refute [expect = potential]
webertj@14350
   922
oops
webertj@14350
   923
webertj@25014
   924
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@46099
   925
refute [maxsize = 1, expect = none]
blanchet@46099
   926
by simp
webertj@25014
   927
webertj@15547
   928
lemma "P (aexp_bexp_rec_2 number ite equal x)"
blanchet@46099
   929
refute [expect = potential]
webertj@15547
   930
oops
webertj@15547
   931
webertj@15547
   932
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
blanchet@46099
   933
refute [expect = potential]
webertj@15547
   934
oops
webertj@15547
   935
webertj@25014
   936
datatype X = A | B X | C Y
webertj@25014
   937
     and Y = D X | E Y | F
webertj@25014
   938
webertj@25014
   939
lemma "P (x::X)"
blanchet@46099
   940
refute [expect = potential]
webertj@25014
   941
oops
webertj@25014
   942
webertj@25014
   943
lemma "P (y::Y)"
blanchet@46099
   944
refute [expect = potential]
webertj@25014
   945
oops
webertj@25014
   946
webertj@25014
   947
lemma "P (B (B A))"
blanchet@46099
   948
refute [expect = potential]
webertj@25014
   949
oops
webertj@25014
   950
webertj@25014
   951
lemma "P (B (C F))"
blanchet@46099
   952
refute [expect = potential]
webertj@25014
   953
oops
webertj@25014
   954
webertj@25014
   955
lemma "P (C (D A))"
blanchet@46099
   956
refute [expect = potential]
webertj@25014
   957
oops
webertj@25014
   958
webertj@25014
   959
lemma "P (C (E F))"
blanchet@46099
   960
refute [expect = potential]
webertj@25014
   961
oops
webertj@25014
   962
webertj@25014
   963
lemma "P (D (B A))"
blanchet@46099
   964
refute [expect = potential]
webertj@25014
   965
oops
webertj@25014
   966
webertj@25014
   967
lemma "P (D (C F))"
blanchet@46099
   968
refute [expect = potential]
webertj@25014
   969
oops
webertj@25014
   970
webertj@25014
   971
lemma "P (E (D A))"
blanchet@46099
   972
refute [expect = potential]
webertj@25014
   973
oops
webertj@25014
   974
webertj@25014
   975
lemma "P (E (E F))"
blanchet@46099
   976
refute [expect = potential]
webertj@25014
   977
oops
webertj@25014
   978
webertj@25014
   979
lemma "P (C (D (C F)))"
blanchet@46099
   980
refute [expect = potential]
webertj@25014
   981
oops
webertj@25014
   982
webertj@25014
   983
lemma "X_Y_rec_1 a b c d e f A = a"
blanchet@46099
   984
refute [maxsize = 3, expect = none]
blanchet@46099
   985
by simp
webertj@25014
   986
webertj@25014
   987
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@46099
   988
refute [maxsize = 1, expect = none]
blanchet@46099
   989
by simp
webertj@25014
   990
webertj@25014
   991
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@46099
   992
refute [maxsize = 1, expect = none]
blanchet@46099
   993
by simp
webertj@25014
   994
webertj@25014
   995
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@46099
   996
refute [maxsize = 1, expect = none]
blanchet@46099
   997
by simp
webertj@25014
   998
webertj@25014
   999
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@46099
  1000
refute [maxsize = 1, expect = none]
blanchet@46099
  1001
by simp
webertj@25014
  1002
webertj@25014
  1003
lemma "X_Y_rec_2 a b c d e f F = f"
blanchet@46099
  1004
refute [maxsize = 3, expect = none]
blanchet@46099
  1005
by simp
webertj@25014
  1006
webertj@25014
  1007
lemma "P (X_Y_rec_1 a b c d e f x)"
blanchet@46099
  1008
refute [expect = potential]
webertj@25014
  1009
oops
webertj@25014
  1010
webertj@25014
  1011
lemma "P (X_Y_rec_2 a b c d e f y)"
blanchet@46099
  1012
refute [expect = potential]
webertj@25014
  1013
oops
webertj@25014
  1014
wenzelm@23219
  1015
text {* Other datatype examples *}
webertj@14350
  1016
webertj@25014
  1017
text {* Indirect recursion is implemented via mutual recursion. *}
webertj@25014
  1018
webertj@25014
  1019
datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
webertj@25014
  1020
webertj@25014
  1021
lemma "P (x::XOpt)"
blanchet@46099
  1022
refute [expect = potential]
webertj@25014
  1023
oops
webertj@25014
  1024
webertj@25014
  1025
lemma "P (CX None)"
blanchet@46099
  1026
refute [expect = potential]
webertj@25014
  1027
oops
webertj@25014
  1028
webertj@25014
  1029
lemma "P (CX (Some (CX None)))"
blanchet@46099
  1030
refute [expect = potential]
webertj@25014
  1031
oops
webertj@25014
  1032
webertj@25014
  1033
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@46099
  1034
refute [maxsize = 1, expect = none]
blanchet@46099
  1035
by simp
webertj@25014
  1036
webertj@25014
  1037
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@46099
  1038
refute [maxsize = 1, expect = none]
blanchet@46099
  1039
by simp
webertj@25014
  1040
webertj@25014
  1041
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
blanchet@46099
  1042
refute [maxsize = 2, expect = none]
blanchet@46099
  1043
by simp
webertj@25014
  1044
webertj@25014
  1045
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@46099
  1046
refute [maxsize = 1, expect = none]
blanchet@46099
  1047
by simp
webertj@25014
  1048
webertj@25014
  1049
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
blanchet@46099
  1050
refute [maxsize = 2, expect = none]
blanchet@46099
  1051
by simp
webertj@25014
  1052
webertj@25014
  1053
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@46099
  1054
refute [maxsize = 1, expect = none]
blanchet@46099
  1055
by simp
webertj@25014
  1056
webertj@25014
  1057
lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1058
refute [expect = potential]
webertj@25014
  1059
oops
webertj@25014
  1060
webertj@25014
  1061
lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1062
refute [expect = potential]
webertj@25014
  1063
oops
webertj@25014
  1064
webertj@25014
  1065
lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1066
refute [expect = potential]
webertj@25014
  1067
oops
webertj@25014
  1068
webertj@25014
  1069
datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
webertj@25014
  1070
webertj@25014
  1071
lemma "P (x::'a YOpt)"
blanchet@46099
  1072
refute [expect = potential]
webertj@25014
  1073
oops
webertj@25014
  1074
webertj@25014
  1075
lemma "P (CY None)"
blanchet@46099
  1076
refute [expect = potential]
webertj@25014
  1077
oops
webertj@25014
  1078
webertj@25014
  1079
lemma "P (CY (Some (\<lambda>a. CY None)))"
blanchet@46099
  1080
refute [expect = potential]
webertj@25014
  1081
oops
webertj@25014
  1082
webertj@25014
  1083
lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
blanchet@46099
  1084
refute [maxsize = 1, expect = none]
blanchet@46099
  1085
by simp
webertj@25014
  1086
webertj@25014
  1087
lemma "YOpt_rec_2 cy n s None = n"
blanchet@46099
  1088
refute [maxsize = 2, expect = none]
blanchet@46099
  1089
by simp
webertj@25014
  1090
webertj@25014
  1091
lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
blanchet@46099
  1092
refute [maxsize = 1, expect = none]
blanchet@46099
  1093
by simp
webertj@25014
  1094
webertj@25014
  1095
lemma "P (YOpt_rec_1 cy n s x)"
blanchet@46099
  1096
refute [expect = potential]
webertj@25014
  1097
oops
webertj@25014
  1098
webertj@25014
  1099
lemma "P (YOpt_rec_2 cy n s x)"
blanchet@46099
  1100
refute [expect = potential]
webertj@25014
  1101
oops
webertj@25014
  1102
webertj@15547
  1103
datatype Trie = TR "Trie list"
webertj@15547
  1104
webertj@15547
  1105
lemma "P (x::Trie)"
blanchet@46099
  1106
refute [expect = potential]
webertj@15547
  1107
oops
webertj@15547
  1108
webertj@15547
  1109
lemma "\<forall>x::Trie. P x"
blanchet@46099
  1110
refute [expect = potential]
webertj@15547
  1111
oops
webertj@15547
  1112
webertj@15547
  1113
lemma "P (TR [TR []])"
blanchet@46099
  1114
refute [expect = potential]
webertj@15547
  1115
oops
webertj@15547
  1116
webertj@25014
  1117
lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
blanchet@46099
  1118
refute [maxsize = 1, expect = none]
blanchet@46099
  1119
by simp
webertj@25014
  1120
webertj@25014
  1121
lemma "Trie_rec_2 tr nil cons [] = nil"
blanchet@46099
  1122
refute [maxsize = 3, expect = none]
blanchet@46099
  1123
by simp
webertj@25014
  1124
webertj@25014
  1125
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@46099
  1126
refute [maxsize = 1, expect = none]
blanchet@46099
  1127
by simp
webertj@25014
  1128
webertj@25014
  1129
lemma "P (Trie_rec_1 tr nil cons x)"
blanchet@46099
  1130
refute [expect = potential]
webertj@15767
  1131
oops
webertj@15767
  1132
webertj@25014
  1133
lemma "P (Trie_rec_2 tr nil cons x)"
blanchet@46099
  1134
refute [expect = potential]
webertj@15547
  1135
oops
webertj@15547
  1136
webertj@14809
  1137
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
webertj@14350
  1138
webertj@14350
  1139
lemma "P (x::InfTree)"
blanchet@46099
  1140
refute [expect = potential]
webertj@14350
  1141
oops
webertj@14350
  1142
webertj@15547
  1143
lemma "\<forall>x::InfTree. P x"
blanchet@46099
  1144
refute [expect = potential]
webertj@15547
  1145
oops
webertj@15547
  1146
webertj@15547
  1147
lemma "P (Node (\<lambda>n. Leaf))"
blanchet@46099
  1148
refute [expect = potential]
webertj@15547
  1149
oops
webertj@15547
  1150
webertj@25014
  1151
lemma "InfTree_rec leaf node Leaf = leaf"
blanchet@46099
  1152
refute [maxsize = 2, expect = none]
blanchet@46099
  1153
by simp
webertj@25014
  1154
webertj@25014
  1155
lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
blanchet@46099
  1156
refute [maxsize = 1, expect = none]
blanchet@46099
  1157
by simp
webertj@25014
  1158
webertj@15547
  1159
lemma "P (InfTree_rec leaf node x)"
blanchet@46099
  1160
refute [expect = potential]
webertj@15547
  1161
oops
webertj@15547
  1162
webertj@14350
  1163
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
webertj@14350
  1164
webertj@15547
  1165
lemma "P (x::'a lambda)"
blanchet@46099
  1166
refute [expect = potential]
webertj@15547
  1167
oops
webertj@15547
  1168
webertj@15547
  1169
lemma "\<forall>x::'a lambda. P x"
blanchet@46099
  1170
refute [expect = potential]
webertj@15547
  1171
oops
webertj@15547
  1172
webertj@15547
  1173
lemma "P (Lam (\<lambda>a. Var a))"
blanchet@46099
  1174
refute [expect = potential]
webertj@15547
  1175
oops
webertj@15547
  1176
webertj@25014
  1177
lemma "lambda_rec var app lam (Var x) = var x"
blanchet@46099
  1178
refute [maxsize = 1, expect = none]
blanchet@46099
  1179
by simp
webertj@25014
  1180
webertj@25014
  1181
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@46099
  1182
refute [maxsize = 1, expect = none]
blanchet@46099
  1183
by simp
webertj@25014
  1184
webertj@25014
  1185
lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
blanchet@46099
  1186
refute [maxsize = 1, expect = none]
blanchet@46099
  1187
by simp
webertj@25014
  1188
webertj@15547
  1189
lemma "P (lambda_rec v a l x)"
blanchet@46099
  1190
refute [expect = potential]
webertj@15547
  1191
oops
webertj@15547
  1192
webertj@15767
  1193
text {* Taken from "Inductive datatypes in HOL", p.8: *}
webertj@15767
  1194
webertj@15767
  1195
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
webertj@15767
  1196
datatype 'c U = E "('c, 'c U) T"
webertj@15767
  1197
webertj@15767
  1198
lemma "P (x::'c U)"
blanchet@46099
  1199
refute [expect = potential]
webertj@15767
  1200
oops
webertj@15767
  1201
webertj@15767
  1202
lemma "\<forall>x::'c U. P x"
blanchet@46099
  1203
refute [expect = potential]
webertj@15767
  1204
oops
webertj@15767
  1205
webertj@15767
  1206
lemma "P (E (C (\<lambda>a. True)))"
blanchet@46099
  1207
refute [expect = potential]
webertj@15767
  1208
oops
webertj@15767
  1209
webertj@25014
  1210
lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
blanchet@46099
  1211
refute [maxsize = 1, expect = none]
blanchet@46099
  1212
by simp
webertj@25014
  1213
webertj@25014
  1214
lemma "U_rec_2 e c d nil cons (C x) = c x"
blanchet@46099
  1215
refute [maxsize = 1, expect = none]
blanchet@46099
  1216
by simp
webertj@25014
  1217
webertj@25014
  1218
lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
blanchet@46099
  1219
refute [maxsize = 1, expect = none]
blanchet@46099
  1220
by simp
webertj@25014
  1221
webertj@25014
  1222
lemma "U_rec_3 e c d nil cons [] = nil"
blanchet@46099
  1223
refute [maxsize = 2, expect = none]
blanchet@46099
  1224
by simp
webertj@25014
  1225
webertj@25014
  1226
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@46099
  1227
refute [maxsize = 1, expect = none]
blanchet@46099
  1228
by simp
webertj@25014
  1229
webertj@25014
  1230
lemma "P (U_rec_1 e c d nil cons x)"
blanchet@46099
  1231
refute [expect = potential]
webertj@15767
  1232
oops
webertj@15767
  1233
webertj@25014
  1234
lemma "P (U_rec_2 e c d nil cons x)"
blanchet@46099
  1235
refute [expect = potential]
webertj@15767
  1236
oops
webertj@15767
  1237
webertj@25014
  1238
lemma "P (U_rec_3 e c d nil cons x)"
blanchet@46099
  1239
refute [expect = potential]
webertj@15767
  1240
oops
webertj@15767
  1241
webertj@25014
  1242
(*****************************************************************************)
webertj@15767
  1243
wenzelm@23219
  1244
subsubsection {* Records *}
webertj@15767
  1245
webertj@15767
  1246
(*TODO: make use of pair types, rather than typedef, for record types*)
webertj@15767
  1247
webertj@15767
  1248
record ('a, 'b) point =
webertj@15767
  1249
  xpos :: 'a
webertj@15767
  1250
  ypos :: 'b
webertj@15767
  1251
webertj@15767
  1252
lemma "(x::('a, 'b) point) = y"
blanchet@46099
  1253
refute
webertj@15767
  1254
oops
webertj@15767
  1255
webertj@15767
  1256
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
webertj@15767
  1257
  ext :: 'c
webertj@15767
  1258
webertj@15767
  1259
lemma "(x::('a, 'b, 'c) extpoint) = y"
blanchet@46099
  1260
refute
webertj@15767
  1261
oops
webertj@15767
  1262
webertj@25014
  1263
(*****************************************************************************)
webertj@15767
  1264
wenzelm@23219
  1265
subsubsection {* Inductively defined sets *}
webertj@15767
  1266
berghofe@23778
  1267
inductive_set arbitrarySet :: "'a set"
berghofe@23778
  1268
where
haftmann@28524
  1269
  "undefined : arbitrarySet"
webertj@15767
  1270
webertj@15767
  1271
lemma "x : arbitrarySet"
blanchet@46099
  1272
refute
webertj@15767
  1273
oops
webertj@15767
  1274
berghofe@23778
  1275
inductive_set evenCard :: "'a set set"
berghofe@23778
  1276
where
webertj@15767
  1277
  "{} : evenCard"
berghofe@23778
  1278
| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
webertj@15767
  1279
webertj@15767
  1280
lemma "S : evenCard"
blanchet@46099
  1281
refute
webertj@15767
  1282
oops
webertj@15767
  1283
berghofe@23778
  1284
inductive_set
webertj@15767
  1285
  even :: "nat set"
berghofe@23778
  1286
  and odd  :: "nat set"
berghofe@23778
  1287
where
webertj@15767
  1288
  "0 : even"
berghofe@23778
  1289
| "n : even \<Longrightarrow> Suc n : odd"
berghofe@23778
  1290
| "n : odd \<Longrightarrow> Suc n : even"
webertj@15767
  1291
webertj@15767
  1292
lemma "n : odd"
blanchet@46099
  1293
(* refute *)  (* TODO: there seems to be an issue here with undefined terms
webertj@25014
  1294
                       because of the recursive datatype "nat" *)
webertj@15767
  1295
oops
webertj@15767
  1296
webertj@25014
  1297
consts f :: "'a \<Rightarrow> 'a"
webertj@25014
  1298
webertj@25014
  1299
inductive_set
webertj@25014
  1300
  a_even :: "'a set"
webertj@25014
  1301
  and a_odd :: "'a set"
webertj@25014
  1302
where
haftmann@28524
  1303
  "undefined : a_even"
webertj@25014
  1304
| "x : a_even \<Longrightarrow> f x : a_odd"
webertj@25014
  1305
| "x : a_odd \<Longrightarrow> f x : a_even"
webertj@25014
  1306
webertj@25014
  1307
lemma "x : a_odd"
blanchet@46099
  1308
(* refute [expect = genuine] -- {* finds a model of size 2 *}
blanchet@46099
  1309
   NO LONGER WORKS since "lfp"'s interpreter is disabled *)
webertj@25014
  1310
oops
webertj@25014
  1311
webertj@25014
  1312
(*****************************************************************************)
webertj@15767
  1313
wenzelm@23219
  1314
subsubsection {* Examples involving special functions *}
webertj@15547
  1315
webertj@15547
  1316
lemma "card x = 0"
blanchet@46099
  1317
refute
webertj@15547
  1318
oops
webertj@15547
  1319
webertj@15767
  1320
lemma "finite x"
blanchet@46099
  1321
refute -- {* no finite countermodel exists *}
webertj@15547
  1322
oops
webertj@15547
  1323
webertj@15547
  1324
lemma "(x::nat) + y = 0"
blanchet@46099
  1325
refute [expect = potential]
webertj@15547
  1326
oops
webertj@15547
  1327
webertj@15547
  1328
lemma "(x::nat) = x + x"
blanchet@46099
  1329
refute [expect = potential]
webertj@15547
  1330
oops
webertj@15547
  1331
webertj@15547
  1332
lemma "(x::nat) - y + y = x"
blanchet@46099
  1333
refute [expect = potential]
webertj@15547
  1334
oops
webertj@15547
  1335
webertj@15547
  1336
lemma "(x::nat) = x * x"
blanchet@46099
  1337
refute [expect = potential]
webertj@15547
  1338
oops
webertj@15547
  1339
webertj@15547
  1340
lemma "(x::nat) < x + y"
blanchet@46099
  1341
refute [expect = potential]
webertj@15547
  1342
oops
webertj@15547
  1343
webertj@21985
  1344
lemma "xs @ [] = ys @ []"
blanchet@46099
  1345
refute [expect = potential]
webertj@15547
  1346
oops
webertj@15547
  1347
webertj@21985
  1348
lemma "xs @ ys = ys @ xs"
blanchet@46099
  1349
refute [expect = potential]
webertj@15547
  1350
oops
webertj@15547
  1351
webertj@16050
  1352
lemma "f (lfp f) = lfp f"
blanchet@46099
  1353
refute
webertj@16050
  1354
oops
webertj@16050
  1355
webertj@16050
  1356
lemma "f (gfp f) = gfp f"
blanchet@46099
  1357
refute
webertj@16050
  1358
oops
webertj@16050
  1359
webertj@16050
  1360
lemma "lfp f = gfp f"
blanchet@46099
  1361
refute
webertj@16050
  1362
oops
webertj@16050
  1363
webertj@25014
  1364
(*****************************************************************************)
webertj@15547
  1365
haftmann@35315
  1366
subsubsection {* Type classes and overloading *}
webertj@15547
  1367
webertj@15547
  1368
text {* A type class without axioms: *}
webertj@15547
  1369
haftmann@35315
  1370
class classA
webertj@15547
  1371
webertj@15547
  1372
lemma "P (x::'a::classA)"
blanchet@46099
  1373
refute [expect = genuine]
webertj@14809
  1374
oops
webertj@14809
  1375
webertj@15547
  1376
text {* An axiom with a type variable (denoting types which have at least two elements): *}
webertj@15547
  1377
haftmann@35315
  1378
class classC =
haftmann@35315
  1379
  assumes classC_ax: "\<exists>x y. x \<noteq> y"
webertj@15547
  1380
webertj@15547
  1381
lemma "P (x::'a::classC)"
blanchet@46099
  1382
refute [expect = genuine]
webertj@15547
  1383
oops
webertj@15547
  1384
webertj@15547
  1385
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
blanchet@46099
  1386
(* refute [expect = none] FIXME *)
webertj@15547
  1387
oops
webertj@15547
  1388
webertj@15547
  1389
text {* A type class for which a constant is defined: *}
webertj@15547
  1390
haftmann@35315
  1391
class classD =
haftmann@35315
  1392
  fixes classD_const :: "'a \<Rightarrow> 'a"
haftmann@35315
  1393
  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
webertj@15547
  1394
webertj@15547
  1395
lemma "P (x::'a::classD)"
blanchet@46099
  1396
refute [expect = genuine]
webertj@15547
  1397
oops
webertj@15547
  1398
webertj@15547
  1399
text {* A type class with multiple superclasses: *}
webertj@15547
  1400
haftmann@35315
  1401
class classE = classC + classD
webertj@15547
  1402
webertj@15547
  1403
lemma "P (x::'a::classE)"
blanchet@46099
  1404
refute [expect = genuine]
webertj@14809
  1405
oops
webertj@14809
  1406
webertj@15547
  1407
text {* OFCLASS: *}
webertj@15547
  1408
webertj@15547
  1409
lemma "OFCLASS('a::type, type_class)"
blanchet@46099
  1410
refute [expect = none]
blanchet@46099
  1411
by intro_classes
webertj@15547
  1412
webertj@15547
  1413
lemma "OFCLASS('a::classC, type_class)"
blanchet@46099
  1414
refute [expect = none]
blanchet@46099
  1415
by intro_classes
webertj@15547
  1416
webertj@15547
  1417
lemma "OFCLASS('a::type, classC_class)"
blanchet@46099
  1418
refute [expect = genuine]
webertj@15547
  1419
oops
webertj@15547
  1420
webertj@15547
  1421
text {* Overloading: *}
webertj@15547
  1422
webertj@15547
  1423
consts inverse :: "'a \<Rightarrow> 'a"
webertj@15547
  1424
webertj@15547
  1425
defs (overloaded)
webertj@15547
  1426
  inverse_bool: "inverse (b::bool)   == ~ b"
webertj@15547
  1427
  inverse_set : "inverse (S::'a set) == -S"
webertj@15547
  1428
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
webertj@15547
  1429
webertj@15547
  1430
lemma "inverse b"
blanchet@46099
  1431
refute [expect = genuine]
webertj@15547
  1432
oops
webertj@15547
  1433
webertj@15547
  1434
lemma "P (inverse (S::'a set))"
blanchet@46099
  1435
refute [expect = genuine]
webertj@15547
  1436
oops
webertj@15547
  1437
webertj@15547
  1438
lemma "P (inverse (p::'a\<times>'b))"
blanchet@46099
  1439
refute [expect = genuine]
webertj@14350
  1440
oops
webertj@14350
  1441
blanchet@34120
  1442
text {* Structured proofs *}
blanchet@34120
  1443
blanchet@34120
  1444
lemma "x = y"
blanchet@34120
  1445
proof cases
blanchet@34120
  1446
  assume "x = y"
blanchet@34120
  1447
  show ?thesis
blanchet@46099
  1448
  refute [expect = none]
blanchet@46099
  1449
  refute [no_assms, expect = genuine]
blanchet@46099
  1450
  refute [no_assms = false, expect = none]
blanchet@34120
  1451
oops
blanchet@34120
  1452
blanchet@46099
  1453
refute_params [satsolver = "auto"]
webertj@18774
  1454
webertj@14350
  1455
end