src/HOL/ex/Refute_Examples.thy
author blanchet
Mon Sep 01 17:34:03 2014 +0200 (2014-09-01)
changeset 58129 3ec65a7f2b50
parent 56851 35ff4ede3409
child 58143 7f7026ae9dc5
permissions -rw-r--r--
ported Refute to use new datatypes when possible
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@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 {* "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
wenzelm@56245
   328
lemma "(x == Pure.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@15547
   528
lemma "P (case x of () \<Rightarrow> u)"
blanchet@46099
   529
refute [expect = genuine]
webertj@15547
   530
oops
webertj@15547
   531
wenzelm@23219
   532
text {* option *}
webertj@14455
   533
webertj@14455
   534
lemma "P (x::'a option)"
blanchet@46099
   535
refute [expect = genuine]
webertj@14455
   536
oops
webertj@14455
   537
webertj@14455
   538
lemma "\<forall>x::'a option. P x"
blanchet@46099
   539
refute [expect = genuine]
webertj@14455
   540
oops
webertj@14455
   541
webertj@14809
   542
lemma "P None"
blanchet@46099
   543
refute [expect = genuine]
webertj@14809
   544
oops
webertj@14809
   545
webertj@14455
   546
lemma "P (Some x)"
blanchet@46099
   547
refute [expect = genuine]
webertj@14455
   548
oops
webertj@14455
   549
webertj@15547
   550
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
blanchet@46099
   551
refute [expect = genuine]
webertj@15547
   552
oops
webertj@15547
   553
wenzelm@23219
   554
text {* * *}
webertj@14350
   555
webertj@14350
   556
lemma "P (x::'a*'b)"
blanchet@46099
   557
refute [expect = genuine]
webertj@14350
   558
oops
webertj@14350
   559
webertj@14350
   560
lemma "\<forall>x::'a*'b. P x"
blanchet@46099
   561
refute [expect = genuine]
webertj@14350
   562
oops
webertj@14350
   563
webertj@25014
   564
lemma "P (x, y)"
blanchet@46099
   565
refute [expect = genuine]
webertj@14350
   566
oops
webertj@14350
   567
webertj@14350
   568
lemma "P (fst x)"
blanchet@46099
   569
refute [expect = genuine]
webertj@14350
   570
oops
webertj@14350
   571
webertj@14350
   572
lemma "P (snd x)"
blanchet@46099
   573
refute [expect = genuine]
webertj@14455
   574
oops
webertj@14455
   575
webertj@14455
   576
lemma "P Pair"
blanchet@46099
   577
refute [expect = genuine]
webertj@14350
   578
oops
webertj@14350
   579
webertj@15547
   580
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
blanchet@46099
   581
refute [expect = genuine]
webertj@15547
   582
oops
webertj@15547
   583
wenzelm@23219
   584
text {* + *}
webertj@14350
   585
webertj@14350
   586
lemma "P (x::'a+'b)"
blanchet@46099
   587
refute [expect = genuine]
webertj@14350
   588
oops
webertj@14350
   589
webertj@14350
   590
lemma "\<forall>x::'a+'b. P x"
blanchet@46099
   591
refute [expect = genuine]
webertj@14350
   592
oops
webertj@14350
   593
webertj@14350
   594
lemma "P (Inl x)"
blanchet@46099
   595
refute [expect = genuine]
webertj@14350
   596
oops
webertj@14350
   597
webertj@14350
   598
lemma "P (Inr x)"
blanchet@46099
   599
refute [expect = genuine]
webertj@14455
   600
oops
webertj@14455
   601
webertj@14455
   602
lemma "P Inl"
blanchet@46099
   603
refute [expect = genuine]
webertj@14350
   604
oops
webertj@14350
   605
webertj@15547
   606
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
blanchet@46099
   607
refute [expect = genuine]
webertj@15547
   608
oops
webertj@15547
   609
wenzelm@23219
   610
text {* Non-recursive datatypes *}
webertj@14350
   611
blanchet@58129
   612
datatype_new T1 = A | B
webertj@14350
   613
webertj@14350
   614
lemma "P (x::T1)"
blanchet@46099
   615
refute [expect = genuine]
webertj@14350
   616
oops
webertj@14350
   617
webertj@14350
   618
lemma "\<forall>x::T1. P x"
blanchet@46099
   619
refute [expect = genuine]
webertj@14350
   620
oops
webertj@14350
   621
webertj@14455
   622
lemma "P A"
blanchet@46099
   623
refute [expect = genuine]
webertj@14350
   624
oops
webertj@14350
   625
webertj@25014
   626
lemma "P B"
blanchet@46099
   627
refute [expect = genuine]
webertj@25014
   628
oops
webertj@25014
   629
blanchet@55416
   630
lemma "rec_T1 a b A = a"
blanchet@46099
   631
refute [expect = none]
blanchet@46099
   632
by simp
webertj@25014
   633
blanchet@55416
   634
lemma "rec_T1 a b B = b"
blanchet@46099
   635
refute [expect = none]
blanchet@46099
   636
by simp
webertj@25014
   637
blanchet@55416
   638
lemma "P (rec_T1 a b x)"
blanchet@46099
   639
refute [expect = genuine]
webertj@15547
   640
oops
webertj@15547
   641
webertj@15547
   642
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
blanchet@46099
   643
refute [expect = genuine]
webertj@15547
   644
oops
webertj@15547
   645
blanchet@58129
   646
datatype_new 'a T2 = C T1 | D 'a
webertj@14455
   647
webertj@14455
   648
lemma "P (x::'a T2)"
blanchet@46099
   649
refute [expect = genuine]
webertj@14350
   650
oops
webertj@14350
   651
webertj@14455
   652
lemma "\<forall>x::'a T2. P x"
blanchet@46099
   653
refute [expect = genuine]
webertj@14350
   654
oops
webertj@14350
   655
webertj@14455
   656
lemma "P D"
blanchet@46099
   657
refute [expect = genuine]
webertj@14350
   658
oops
webertj@14350
   659
blanchet@55416
   660
lemma "rec_T2 c d (C x) = c x"
blanchet@46099
   661
refute [maxsize = 4, expect = none]
blanchet@46099
   662
by simp
webertj@25014
   663
blanchet@55416
   664
lemma "rec_T2 c d (D x) = d x"
blanchet@46099
   665
refute [maxsize = 4, expect = none]
blanchet@46099
   666
by simp
webertj@25014
   667
blanchet@55416
   668
lemma "P (rec_T2 c d x)"
blanchet@46099
   669
refute [expect = genuine]
webertj@15547
   670
oops
webertj@15547
   671
webertj@15547
   672
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
blanchet@46099
   673
refute [expect = genuine]
webertj@15547
   674
oops
webertj@15547
   675
blanchet@58129
   676
datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
webertj@14455
   677
webertj@14809
   678
lemma "P (x::('a,'b) T3)"
blanchet@46099
   679
refute [expect = genuine]
webertj@14809
   680
oops
webertj@14809
   681
webertj@14809
   682
lemma "\<forall>x::('a,'b) T3. P x"
blanchet@46099
   683
refute [expect = genuine]
webertj@14809
   684
oops
webertj@14809
   685
webertj@14455
   686
lemma "P E"
blanchet@46099
   687
refute [expect = genuine]
webertj@14350
   688
oops
webertj@14350
   689
blanchet@55416
   690
lemma "rec_T3 e (E x) = e x"
blanchet@46099
   691
refute [maxsize = 2, expect = none]
blanchet@46099
   692
by simp
webertj@25014
   693
blanchet@55416
   694
lemma "P (rec_T3 e x)"
blanchet@46099
   695
refute [expect = genuine]
webertj@15547
   696
oops
webertj@15547
   697
webertj@15547
   698
lemma "P (case x of E f \<Rightarrow> e f)"
blanchet@46099
   699
refute [expect = genuine]
webertj@15547
   700
oops
webertj@15547
   701
wenzelm@23219
   702
text {* Recursive datatypes *}
webertj@14350
   703
webertj@15547
   704
text {* nat *}
webertj@15547
   705
webertj@14809
   706
lemma "P (x::nat)"
blanchet@46099
   707
refute [expect = potential]
webertj@14809
   708
oops
webertj@14350
   709
webertj@14809
   710
lemma "\<forall>x::nat. P x"
blanchet@46099
   711
refute [expect = potential]
webertj@14350
   712
oops
webertj@14350
   713
webertj@14809
   714
lemma "P (Suc 0)"
blanchet@46099
   715
refute [expect = potential]
webertj@14350
   716
oops
webertj@14350
   717
webertj@14809
   718
lemma "P Suc"
blanchet@46099
   719
refute [maxsize = 3, expect = none]
blanchet@46099
   720
-- {* @{term Suc} is a partial function (regardless of the size
blanchet@46099
   721
      of the model), hence @{term "P Suc"} is undefined and no
blanchet@46099
   722
      model will be found *}
webertj@14350
   723
oops
webertj@14350
   724
blanchet@55415
   725
lemma "rec_nat zero suc 0 = zero"
blanchet@46099
   726
refute [expect = none]
blanchet@46099
   727
by simp
webertj@25014
   728
blanchet@55415
   729
lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
blanchet@46099
   730
refute [maxsize = 2, expect = none]
blanchet@46099
   731
by simp
webertj@25014
   732
blanchet@55415
   733
lemma "P (rec_nat zero suc x)"
blanchet@46099
   734
refute [expect = potential]
webertj@15547
   735
oops
webertj@15547
   736
webertj@15547
   737
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
blanchet@46099
   738
refute [expect = potential]
webertj@15547
   739
oops
webertj@15547
   740
webertj@15547
   741
text {* 'a list *}
webertj@15547
   742
webertj@15547
   743
lemma "P (xs::'a list)"
blanchet@46099
   744
refute [expect = potential]
webertj@15547
   745
oops
webertj@15547
   746
webertj@15547
   747
lemma "\<forall>xs::'a list. P xs"
blanchet@46099
   748
refute [expect = potential]
webertj@15547
   749
oops
webertj@15547
   750
webertj@15547
   751
lemma "P [x, y]"
blanchet@46099
   752
refute [expect = potential]
webertj@15547
   753
oops
webertj@15547
   754
blanchet@55413
   755
lemma "rec_list nil cons [] = nil"
blanchet@46099
   756
refute [maxsize = 3, expect = none]
blanchet@46099
   757
by simp
webertj@25014
   758
blanchet@55413
   759
lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
blanchet@46099
   760
refute [maxsize = 2, expect = none]
blanchet@46099
   761
by simp
webertj@25014
   762
blanchet@55413
   763
lemma "P (rec_list nil cons xs)"
blanchet@46099
   764
refute [expect = potential]
webertj@15547
   765
oops
webertj@15547
   766
webertj@15547
   767
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
blanchet@46099
   768
refute [expect = potential]
webertj@15547
   769
oops
webertj@15547
   770
webertj@15547
   771
lemma "(xs::'a list) = ys"
blanchet@46099
   772
refute [expect = potential]
webertj@15547
   773
oops
webertj@15547
   774
webertj@15547
   775
lemma "a # xs = b # xs"
blanchet@46099
   776
refute [expect = potential]
webertj@15547
   777
oops
webertj@15547
   778
blanchet@58129
   779
datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
webertj@25014
   780
webertj@25014
   781
lemma "P (x::BitList)"
blanchet@46099
   782
refute [expect = potential]
webertj@25014
   783
oops
webertj@25014
   784
webertj@25014
   785
lemma "\<forall>x::BitList. P x"
blanchet@46099
   786
refute [expect = potential]
webertj@25014
   787
oops
webertj@25014
   788
webertj@25014
   789
lemma "P (Bit0 (Bit1 BitListNil))"
blanchet@46099
   790
refute [expect = potential]
webertj@25014
   791
oops
webertj@25014
   792
blanchet@55416
   793
lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
blanchet@46099
   794
refute [maxsize = 4, expect = none]
blanchet@46099
   795
by simp
webertj@25014
   796
blanchet@55416
   797
lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
blanchet@46099
   798
refute [maxsize = 2, expect = none]
blanchet@46099
   799
by simp
webertj@25014
   800
blanchet@55416
   801
lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
blanchet@46099
   802
refute [maxsize = 2, expect = none]
blanchet@46099
   803
by simp
webertj@25014
   804
blanchet@55416
   805
lemma "P (rec_BitList nil bit0 bit1 x)"
blanchet@46099
   806
refute [expect = potential]
webertj@25014
   807
oops
webertj@25014
   808
blanchet@58129
   809
datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
webertj@14350
   810
webertj@14350
   811
lemma "P (x::'a BinTree)"
blanchet@46099
   812
refute [expect = potential]
webertj@14350
   813
oops
webertj@14350
   814
webertj@14350
   815
lemma "\<forall>x::'a BinTree. P x"
blanchet@46099
   816
refute [expect = potential]
webertj@14809
   817
oops
webertj@14809
   818
webertj@14809
   819
lemma "P (Node (Leaf x) (Leaf y))"
blanchet@46099
   820
refute [expect = potential]
webertj@14350
   821
oops
webertj@14350
   822
blanchet@55416
   823
lemma "rec_BinTree l n (Leaf x) = l x"
blanchet@46099
   824
  refute [maxsize = 1, expect = none]
blanchet@46099
   825
  (* The "maxsize = 1" tests are a bit pointless: for some formulae
blanchet@46099
   826
     below, refute will find no countermodel simply because this
blanchet@46099
   827
     size makes involved terms undefined.  Unfortunately, any
blanchet@46099
   828
     larger size already takes too long. *)
blanchet@46099
   829
by simp
webertj@25014
   830
blanchet@55416
   831
lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
blanchet@46099
   832
refute [maxsize = 1, expect = none]
blanchet@46099
   833
by simp
webertj@25014
   834
blanchet@55416
   835
lemma "P (rec_BinTree l n x)"
blanchet@46099
   836
refute [expect = potential]
webertj@15547
   837
oops
webertj@15547
   838
webertj@15547
   839
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
blanchet@46099
   840
refute [expect = potential]
webertj@15547
   841
oops
webertj@15547
   842
wenzelm@23219
   843
text {* Mutually recursive datatypes *}
webertj@14350
   844
blanchet@58129
   845
datatype_new
blanchet@58129
   846
  'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and
blanchet@58129
   847
  'a bexp = Equal "'a aexp" "'a aexp"
webertj@14350
   848
webertj@14350
   849
lemma "P (x::'a aexp)"
blanchet@46099
   850
refute [expect = potential]
webertj@14350
   851
oops
webertj@14350
   852
webertj@14350
   853
lemma "\<forall>x::'a aexp. P x"
blanchet@46099
   854
refute [expect = potential]
webertj@14350
   855
oops
webertj@14350
   856
webertj@15547
   857
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
blanchet@46099
   858
refute [expect = potential]
webertj@15547
   859
oops
webertj@15547
   860
webertj@14350
   861
lemma "P (x::'a bexp)"
blanchet@46099
   862
refute [expect = potential]
webertj@14350
   863
oops
webertj@14350
   864
webertj@14350
   865
lemma "\<forall>x::'a bexp. P x"
blanchet@46099
   866
refute [expect = potential]
webertj@14350
   867
oops
webertj@14350
   868
blanchet@58129
   869
lemma "rec_aexp number ite equal (Number x) = number x"
blanchet@46099
   870
refute [maxsize = 1, expect = none]
blanchet@46099
   871
by simp
webertj@25014
   872
blanchet@58129
   873
lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
blanchet@46099
   874
refute [maxsize = 1, expect = none]
blanchet@46099
   875
by simp
webertj@25014
   876
blanchet@58129
   877
lemma "P (rec_aexp number ite equal x)"
blanchet@46099
   878
refute [expect = potential]
webertj@15547
   879
oops
webertj@15547
   880
webertj@15547
   881
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
blanchet@46099
   882
refute [expect = potential]
webertj@14350
   883
oops
webertj@14350
   884
blanchet@58129
   885
lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
blanchet@46099
   886
refute [maxsize = 1, expect = none]
blanchet@46099
   887
by simp
webertj@25014
   888
blanchet@58129
   889
lemma "P (rec_bexp number ite equal x)"
blanchet@46099
   890
refute [expect = potential]
webertj@15547
   891
oops
webertj@15547
   892
webertj@15547
   893
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
blanchet@46099
   894
refute [expect = potential]
webertj@15547
   895
oops
webertj@15547
   896
blanchet@58129
   897
datatype_new
blanchet@58129
   898
  X = A | B X | C Y and
blanchet@58129
   899
  Y = D X | E Y | F
webertj@25014
   900
webertj@25014
   901
lemma "P (x::X)"
blanchet@46099
   902
refute [expect = potential]
webertj@25014
   903
oops
webertj@25014
   904
webertj@25014
   905
lemma "P (y::Y)"
blanchet@46099
   906
refute [expect = potential]
webertj@25014
   907
oops
webertj@25014
   908
webertj@25014
   909
lemma "P (B (B A))"
blanchet@46099
   910
refute [expect = potential]
webertj@25014
   911
oops
webertj@25014
   912
webertj@25014
   913
lemma "P (B (C F))"
blanchet@46099
   914
refute [expect = potential]
webertj@25014
   915
oops
webertj@25014
   916
webertj@25014
   917
lemma "P (C (D A))"
blanchet@46099
   918
refute [expect = potential]
webertj@25014
   919
oops
webertj@25014
   920
webertj@25014
   921
lemma "P (C (E F))"
blanchet@46099
   922
refute [expect = potential]
webertj@25014
   923
oops
webertj@25014
   924
webertj@25014
   925
lemma "P (D (B A))"
blanchet@46099
   926
refute [expect = potential]
webertj@25014
   927
oops
webertj@25014
   928
webertj@25014
   929
lemma "P (D (C F))"
blanchet@46099
   930
refute [expect = potential]
webertj@25014
   931
oops
webertj@25014
   932
webertj@25014
   933
lemma "P (E (D A))"
blanchet@46099
   934
refute [expect = potential]
webertj@25014
   935
oops
webertj@25014
   936
webertj@25014
   937
lemma "P (E (E F))"
blanchet@46099
   938
refute [expect = potential]
webertj@25014
   939
oops
webertj@25014
   940
webertj@25014
   941
lemma "P (C (D (C F)))"
blanchet@46099
   942
refute [expect = potential]
webertj@25014
   943
oops
webertj@25014
   944
blanchet@58129
   945
lemma "rec_X a b c d e f A = a"
blanchet@46099
   946
refute [maxsize = 3, expect = none]
blanchet@46099
   947
by simp
webertj@25014
   948
blanchet@58129
   949
lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
blanchet@46099
   950
refute [maxsize = 1, expect = none]
blanchet@46099
   951
by simp
webertj@25014
   952
blanchet@58129
   953
lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
blanchet@46099
   954
refute [maxsize = 1, expect = none]
blanchet@46099
   955
by simp
webertj@25014
   956
blanchet@58129
   957
lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
blanchet@46099
   958
refute [maxsize = 1, expect = none]
blanchet@46099
   959
by simp
webertj@25014
   960
blanchet@58129
   961
lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
blanchet@46099
   962
refute [maxsize = 1, expect = none]
blanchet@46099
   963
by simp
webertj@25014
   964
blanchet@58129
   965
lemma "rec_Y a b c d e f F = f"
blanchet@46099
   966
refute [maxsize = 3, expect = none]
blanchet@46099
   967
by simp
webertj@25014
   968
blanchet@58129
   969
lemma "P (rec_X a b c d e f x)"
blanchet@46099
   970
refute [expect = potential]
webertj@25014
   971
oops
webertj@25014
   972
blanchet@58129
   973
lemma "P (rec_Y a b c d e f y)"
blanchet@46099
   974
refute [expect = potential]
webertj@25014
   975
oops
webertj@25014
   976
wenzelm@23219
   977
text {* Other datatype examples *}
webertj@14350
   978
webertj@25014
   979
text {* Indirect recursion is implemented via mutual recursion. *}
webertj@25014
   980
webertj@25014
   981
datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
webertj@25014
   982
webertj@25014
   983
lemma "P (x::XOpt)"
blanchet@46099
   984
refute [expect = potential]
webertj@25014
   985
oops
webertj@25014
   986
webertj@25014
   987
lemma "P (CX None)"
blanchet@46099
   988
refute [expect = potential]
webertj@25014
   989
oops
webertj@25014
   990
webertj@25014
   991
lemma "P (CX (Some (CX None)))"
blanchet@46099
   992
refute [expect = potential]
webertj@25014
   993
oops
webertj@25014
   994
blanchet@55416
   995
lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
blanchet@46099
   996
refute [maxsize = 1, expect = none]
blanchet@46099
   997
by simp
webertj@25014
   998
blanchet@55416
   999
lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
blanchet@46099
  1000
refute [maxsize = 1, expect = none]
blanchet@46099
  1001
by simp
webertj@25014
  1002
blanchet@55416
  1003
lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
blanchet@46099
  1004
refute [maxsize = 2, expect = none]
blanchet@46099
  1005
by simp
webertj@25014
  1006
blanchet@55416
  1007
lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1008
refute [maxsize = 1, expect = none]
blanchet@46099
  1009
by simp
webertj@25014
  1010
blanchet@55416
  1011
lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
blanchet@46099
  1012
refute [maxsize = 2, expect = none]
blanchet@46099
  1013
by simp
webertj@25014
  1014
blanchet@55416
  1015
lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1016
refute [maxsize = 1, expect = none]
blanchet@46099
  1017
by simp
webertj@25014
  1018
blanchet@55416
  1019
lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1020
refute [expect = potential]
webertj@25014
  1021
oops
webertj@25014
  1022
blanchet@55416
  1023
lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1024
refute [expect = potential]
webertj@25014
  1025
oops
webertj@25014
  1026
blanchet@55416
  1027
lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
blanchet@46099
  1028
refute [expect = potential]
webertj@25014
  1029
oops
webertj@25014
  1030
webertj@25014
  1031
datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
webertj@25014
  1032
webertj@25014
  1033
lemma "P (x::'a YOpt)"
blanchet@46099
  1034
refute [expect = potential]
webertj@25014
  1035
oops
webertj@25014
  1036
webertj@25014
  1037
lemma "P (CY None)"
blanchet@46099
  1038
refute [expect = potential]
webertj@25014
  1039
oops
webertj@25014
  1040
webertj@25014
  1041
lemma "P (CY (Some (\<lambda>a. CY None)))"
blanchet@46099
  1042
refute [expect = potential]
webertj@25014
  1043
oops
webertj@25014
  1044
blanchet@55416
  1045
lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
blanchet@46099
  1046
refute [maxsize = 1, expect = none]
blanchet@46099
  1047
by simp
webertj@25014
  1048
blanchet@55416
  1049
lemma "rec_YOpt_2 cy n s None = n"
blanchet@46099
  1050
refute [maxsize = 2, expect = none]
blanchet@46099
  1051
by simp
webertj@25014
  1052
blanchet@55416
  1053
lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
blanchet@46099
  1054
refute [maxsize = 1, expect = none]
blanchet@46099
  1055
by simp
webertj@25014
  1056
blanchet@55416
  1057
lemma "P (rec_YOpt_1 cy n s x)"
blanchet@46099
  1058
refute [expect = potential]
webertj@25014
  1059
oops
webertj@25014
  1060
blanchet@55416
  1061
lemma "P (rec_YOpt_2 cy n s x)"
blanchet@46099
  1062
refute [expect = potential]
webertj@25014
  1063
oops
webertj@25014
  1064
blanchet@58129
  1065
datatype_new Trie = TR "Trie list"
blanchet@58129
  1066
datatype_compat Trie
blanchet@58129
  1067
blanchet@58129
  1068
abbreviation "rec_Trie_1 \<equiv> compat_Trie.n2m_Trie_rec"
blanchet@58129
  1069
abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.n2m_Trie_list_rec"
webertj@15547
  1070
webertj@15547
  1071
lemma "P (x::Trie)"
blanchet@46099
  1072
refute [expect = potential]
webertj@15547
  1073
oops
webertj@15547
  1074
webertj@15547
  1075
lemma "\<forall>x::Trie. P x"
blanchet@46099
  1076
refute [expect = potential]
webertj@15547
  1077
oops
webertj@15547
  1078
webertj@15547
  1079
lemma "P (TR [TR []])"
blanchet@46099
  1080
refute [expect = potential]
webertj@15547
  1081
oops
webertj@15547
  1082
blanchet@55416
  1083
lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
blanchet@46099
  1084
refute [maxsize = 1, expect = none]
blanchet@46099
  1085
by simp
webertj@25014
  1086
blanchet@55416
  1087
lemma "rec_Trie_2 tr nil cons [] = nil"
blanchet@46099
  1088
refute [maxsize = 3, expect = none]
blanchet@46099
  1089
by simp
webertj@25014
  1090
blanchet@55416
  1091
lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
blanchet@46099
  1092
refute [maxsize = 1, expect = none]
blanchet@46099
  1093
by simp
webertj@25014
  1094
blanchet@55416
  1095
lemma "P (rec_Trie_1 tr nil cons x)"
blanchet@46099
  1096
refute [expect = potential]
webertj@15767
  1097
oops
webertj@15767
  1098
blanchet@55416
  1099
lemma "P (rec_Trie_2 tr nil cons x)"
blanchet@46099
  1100
refute [expect = potential]
webertj@15547
  1101
oops
webertj@15547
  1102
webertj@14809
  1103
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
webertj@14350
  1104
webertj@14350
  1105
lemma "P (x::InfTree)"
blanchet@46099
  1106
refute [expect = potential]
webertj@14350
  1107
oops
webertj@14350
  1108
webertj@15547
  1109
lemma "\<forall>x::InfTree. P x"
blanchet@46099
  1110
refute [expect = potential]
webertj@15547
  1111
oops
webertj@15547
  1112
webertj@15547
  1113
lemma "P (Node (\<lambda>n. Leaf))"
blanchet@46099
  1114
refute [expect = potential]
webertj@15547
  1115
oops
webertj@15547
  1116
blanchet@55416
  1117
lemma "rec_InfTree leaf node Leaf = leaf"
blanchet@46099
  1118
refute [maxsize = 2, expect = none]
blanchet@46099
  1119
by simp
webertj@25014
  1120
blanchet@55416
  1121
lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
blanchet@46099
  1122
refute [maxsize = 1, expect = none]
blanchet@46099
  1123
by simp
webertj@25014
  1124
blanchet@55416
  1125
lemma "P (rec_InfTree leaf node x)"
blanchet@46099
  1126
refute [expect = potential]
webertj@15547
  1127
oops
webertj@15547
  1128
webertj@14350
  1129
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
webertj@14350
  1130
webertj@15547
  1131
lemma "P (x::'a lambda)"
blanchet@46099
  1132
refute [expect = potential]
webertj@15547
  1133
oops
webertj@15547
  1134
webertj@15547
  1135
lemma "\<forall>x::'a lambda. P x"
blanchet@46099
  1136
refute [expect = potential]
webertj@15547
  1137
oops
webertj@15547
  1138
webertj@15547
  1139
lemma "P (Lam (\<lambda>a. Var a))"
blanchet@46099
  1140
refute [expect = potential]
webertj@15547
  1141
oops
webertj@15547
  1142
blanchet@55416
  1143
lemma "rec_lambda var app lam (Var x) = var x"
blanchet@46099
  1144
refute [maxsize = 1, expect = none]
blanchet@46099
  1145
by simp
webertj@25014
  1146
blanchet@55416
  1147
lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
blanchet@46099
  1148
refute [maxsize = 1, expect = none]
blanchet@46099
  1149
by simp
webertj@25014
  1150
blanchet@55416
  1151
lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
blanchet@46099
  1152
refute [maxsize = 1, expect = none]
blanchet@46099
  1153
by simp
webertj@25014
  1154
blanchet@55416
  1155
lemma "P (rec_lambda v a l x)"
blanchet@46099
  1156
refute [expect = potential]
webertj@15547
  1157
oops
webertj@15547
  1158
webertj@15767
  1159
text {* Taken from "Inductive datatypes in HOL", p.8: *}
webertj@15767
  1160
webertj@15767
  1161
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
webertj@15767
  1162
datatype 'c U = E "('c, 'c U) T"
webertj@15767
  1163
webertj@15767
  1164
lemma "P (x::'c U)"
blanchet@46099
  1165
refute [expect = potential]
webertj@15767
  1166
oops
webertj@15767
  1167
webertj@15767
  1168
lemma "\<forall>x::'c U. P x"
blanchet@46099
  1169
refute [expect = potential]
webertj@15767
  1170
oops
webertj@15767
  1171
webertj@15767
  1172
lemma "P (E (C (\<lambda>a. True)))"
blanchet@46099
  1173
refute [expect = potential]
webertj@15767
  1174
oops
webertj@15767
  1175
blanchet@55416
  1176
lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
blanchet@46099
  1177
refute [maxsize = 1, expect = none]
blanchet@46099
  1178
by simp
webertj@25014
  1179
blanchet@55416
  1180
lemma "rec_U_2 e c d nil cons (C x) = c x"
blanchet@46099
  1181
refute [maxsize = 1, expect = none]
blanchet@46099
  1182
by simp
webertj@25014
  1183
blanchet@55416
  1184
lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
blanchet@46099
  1185
refute [maxsize = 1, expect = none]
blanchet@46099
  1186
by simp
webertj@25014
  1187
blanchet@55416
  1188
lemma "rec_U_3 e c d nil cons [] = nil"
blanchet@46099
  1189
refute [maxsize = 2, expect = none]
blanchet@46099
  1190
by simp
webertj@25014
  1191
blanchet@55416
  1192
lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
blanchet@46099
  1193
refute [maxsize = 1, expect = none]
blanchet@46099
  1194
by simp
webertj@25014
  1195
blanchet@55416
  1196
lemma "P (rec_U_1 e c d nil cons x)"
blanchet@46099
  1197
refute [expect = potential]
webertj@15767
  1198
oops
webertj@15767
  1199
blanchet@55416
  1200
lemma "P (rec_U_2 e c d nil cons x)"
blanchet@46099
  1201
refute [expect = potential]
webertj@15767
  1202
oops
webertj@15767
  1203
blanchet@55416
  1204
lemma "P (rec_U_3 e c d nil cons x)"
blanchet@46099
  1205
refute [expect = potential]
webertj@15767
  1206
oops
webertj@15767
  1207
webertj@25014
  1208
(*****************************************************************************)
webertj@15767
  1209
wenzelm@23219
  1210
subsubsection {* Records *}
webertj@15767
  1211
webertj@15767
  1212
(*TODO: make use of pair types, rather than typedef, for record types*)
webertj@15767
  1213
webertj@15767
  1214
record ('a, 'b) point =
webertj@15767
  1215
  xpos :: 'a
webertj@15767
  1216
  ypos :: 'b
webertj@15767
  1217
webertj@15767
  1218
lemma "(x::('a, 'b) point) = y"
blanchet@46099
  1219
refute
webertj@15767
  1220
oops
webertj@15767
  1221
webertj@15767
  1222
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
webertj@15767
  1223
  ext :: 'c
webertj@15767
  1224
webertj@15767
  1225
lemma "(x::('a, 'b, 'c) extpoint) = y"
blanchet@46099
  1226
refute
webertj@15767
  1227
oops
webertj@15767
  1228
webertj@25014
  1229
(*****************************************************************************)
webertj@15767
  1230
wenzelm@23219
  1231
subsubsection {* Inductively defined sets *}
webertj@15767
  1232
berghofe@23778
  1233
inductive_set arbitrarySet :: "'a set"
berghofe@23778
  1234
where
haftmann@28524
  1235
  "undefined : arbitrarySet"
webertj@15767
  1236
webertj@15767
  1237
lemma "x : arbitrarySet"
blanchet@46099
  1238
refute
webertj@15767
  1239
oops
webertj@15767
  1240
berghofe@23778
  1241
inductive_set evenCard :: "'a set set"
berghofe@23778
  1242
where
webertj@15767
  1243
  "{} : evenCard"
berghofe@23778
  1244
| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
webertj@15767
  1245
webertj@15767
  1246
lemma "S : evenCard"
blanchet@46099
  1247
refute
webertj@15767
  1248
oops
webertj@15767
  1249
webertj@25014
  1250
consts f :: "'a \<Rightarrow> 'a"
webertj@25014
  1251
webertj@25014
  1252
inductive_set
webertj@25014
  1253
  a_even :: "'a set"
webertj@25014
  1254
  and a_odd :: "'a set"
webertj@25014
  1255
where
haftmann@28524
  1256
  "undefined : a_even"
webertj@25014
  1257
| "x : a_even \<Longrightarrow> f x : a_odd"
webertj@25014
  1258
| "x : a_odd \<Longrightarrow> f x : a_even"
webertj@25014
  1259
webertj@25014
  1260
lemma "x : a_odd"
blanchet@46099
  1261
(* refute [expect = genuine] -- {* finds a model of size 2 *}
blanchet@46099
  1262
   NO LONGER WORKS since "lfp"'s interpreter is disabled *)
webertj@25014
  1263
oops
webertj@25014
  1264
webertj@25014
  1265
(*****************************************************************************)
webertj@15767
  1266
wenzelm@23219
  1267
subsubsection {* Examples involving special functions *}
webertj@15547
  1268
webertj@15547
  1269
lemma "card x = 0"
blanchet@46099
  1270
refute
webertj@15547
  1271
oops
webertj@15547
  1272
webertj@15767
  1273
lemma "finite x"
blanchet@46099
  1274
refute -- {* no finite countermodel exists *}
webertj@15547
  1275
oops
webertj@15547
  1276
webertj@15547
  1277
lemma "(x::nat) + y = 0"
blanchet@46099
  1278
refute [expect = potential]
webertj@15547
  1279
oops
webertj@15547
  1280
webertj@15547
  1281
lemma "(x::nat) = x + x"
blanchet@46099
  1282
refute [expect = potential]
webertj@15547
  1283
oops
webertj@15547
  1284
webertj@15547
  1285
lemma "(x::nat) - y + y = x"
blanchet@46099
  1286
refute [expect = potential]
webertj@15547
  1287
oops
webertj@15547
  1288
webertj@15547
  1289
lemma "(x::nat) = x * x"
blanchet@46099
  1290
refute [expect = potential]
webertj@15547
  1291
oops
webertj@15547
  1292
webertj@15547
  1293
lemma "(x::nat) < x + y"
blanchet@46099
  1294
refute [expect = potential]
webertj@15547
  1295
oops
webertj@15547
  1296
webertj@21985
  1297
lemma "xs @ [] = ys @ []"
blanchet@46099
  1298
refute [expect = potential]
webertj@15547
  1299
oops
webertj@15547
  1300
webertj@21985
  1301
lemma "xs @ ys = ys @ xs"
blanchet@46099
  1302
refute [expect = potential]
webertj@15547
  1303
oops
webertj@15547
  1304
webertj@16050
  1305
lemma "f (lfp f) = lfp f"
blanchet@46099
  1306
refute
webertj@16050
  1307
oops
webertj@16050
  1308
webertj@16050
  1309
lemma "f (gfp f) = gfp f"
blanchet@46099
  1310
refute
webertj@16050
  1311
oops
webertj@16050
  1312
webertj@16050
  1313
lemma "lfp f = gfp f"
blanchet@46099
  1314
refute
webertj@16050
  1315
oops
webertj@16050
  1316
webertj@25014
  1317
(*****************************************************************************)
webertj@15547
  1318
haftmann@35315
  1319
subsubsection {* Type classes and overloading *}
webertj@15547
  1320
webertj@15547
  1321
text {* A type class without axioms: *}
webertj@15547
  1322
haftmann@35315
  1323
class classA
webertj@15547
  1324
webertj@15547
  1325
lemma "P (x::'a::classA)"
blanchet@46099
  1326
refute [expect = genuine]
webertj@14809
  1327
oops
webertj@14809
  1328
webertj@15547
  1329
text {* An axiom with a type variable (denoting types which have at least two elements): *}
webertj@15547
  1330
haftmann@35315
  1331
class classC =
haftmann@35315
  1332
  assumes classC_ax: "\<exists>x y. x \<noteq> y"
webertj@15547
  1333
webertj@15547
  1334
lemma "P (x::'a::classC)"
blanchet@46099
  1335
refute [expect = genuine]
webertj@15547
  1336
oops
webertj@15547
  1337
webertj@15547
  1338
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
blanchet@46099
  1339
(* refute [expect = none] FIXME *)
webertj@15547
  1340
oops
webertj@15547
  1341
webertj@15547
  1342
text {* A type class for which a constant is defined: *}
webertj@15547
  1343
haftmann@35315
  1344
class classD =
haftmann@35315
  1345
  fixes classD_const :: "'a \<Rightarrow> 'a"
haftmann@35315
  1346
  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
webertj@15547
  1347
webertj@15547
  1348
lemma "P (x::'a::classD)"
blanchet@46099
  1349
refute [expect = genuine]
webertj@15547
  1350
oops
webertj@15547
  1351
webertj@15547
  1352
text {* A type class with multiple superclasses: *}
webertj@15547
  1353
haftmann@35315
  1354
class classE = classC + classD
webertj@15547
  1355
webertj@15547
  1356
lemma "P (x::'a::classE)"
blanchet@46099
  1357
refute [expect = genuine]
webertj@14809
  1358
oops
webertj@14809
  1359
webertj@15547
  1360
text {* OFCLASS: *}
webertj@15547
  1361
webertj@15547
  1362
lemma "OFCLASS('a::type, type_class)"
blanchet@46099
  1363
refute [expect = none]
blanchet@46099
  1364
by intro_classes
webertj@15547
  1365
webertj@15547
  1366
lemma "OFCLASS('a::classC, type_class)"
blanchet@46099
  1367
refute [expect = none]
blanchet@46099
  1368
by intro_classes
webertj@15547
  1369
webertj@15547
  1370
lemma "OFCLASS('a::type, classC_class)"
blanchet@46099
  1371
refute [expect = genuine]
webertj@15547
  1372
oops
webertj@15547
  1373
webertj@15547
  1374
text {* Overloading: *}
webertj@15547
  1375
webertj@15547
  1376
consts inverse :: "'a \<Rightarrow> 'a"
webertj@15547
  1377
webertj@15547
  1378
defs (overloaded)
webertj@15547
  1379
  inverse_bool: "inverse (b::bool)   == ~ b"
webertj@15547
  1380
  inverse_set : "inverse (S::'a set) == -S"
webertj@15547
  1381
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
webertj@15547
  1382
webertj@15547
  1383
lemma "inverse b"
blanchet@46099
  1384
refute [expect = genuine]
webertj@15547
  1385
oops
webertj@15547
  1386
webertj@15547
  1387
lemma "P (inverse (S::'a set))"
blanchet@46099
  1388
refute [expect = genuine]
webertj@15547
  1389
oops
webertj@15547
  1390
webertj@15547
  1391
lemma "P (inverse (p::'a\<times>'b))"
blanchet@46099
  1392
refute [expect = genuine]
webertj@14350
  1393
oops
webertj@14350
  1394
blanchet@34120
  1395
text {* Structured proofs *}
blanchet@34120
  1396
blanchet@34120
  1397
lemma "x = y"
blanchet@34120
  1398
proof cases
blanchet@34120
  1399
  assume "x = y"
blanchet@34120
  1400
  show ?thesis
blanchet@46099
  1401
  refute [expect = none]
blanchet@46099
  1402
  refute [no_assms, expect = genuine]
blanchet@46099
  1403
  refute [no_assms = false, expect = none]
blanchet@34120
  1404
oops
blanchet@34120
  1405
blanchet@46099
  1406
refute_params [satsolver = "auto"]
webertj@18774
  1407
webertj@14350
  1408
end