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