src/HOL/ex/Refute_Examples.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 25032 f7095d7cb9a3
child 28524 644b62cf678f
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
webertj@14350
     1
(*  Title:      HOL/ex/Refute_Examples.thy
webertj@14350
     2
    ID:         $Id$
webertj@14350
     3
    Author:     Tjark Weber
webertj@21985
     4
    Copyright   2003-2007
webertj@14350
     5
*)
webertj@14350
     6
webertj@14350
     7
(* See 'HOL/Refute.thy' for help. *)
webertj@14350
     8
webertj@14350
     9
header {* Examples for the 'refute' command *}
webertj@14350
    10
webertj@15297
    11
theory Refute_Examples imports Main
webertj@15297
    12
begin
webertj@14350
    13
webertj@18774
    14
refute_params [satsolver="dpll"]
webertj@18774
    15
webertj@14350
    16
lemma "P \<and> Q"
webertj@14350
    17
  apply (rule conjI)
webertj@14350
    18
  refute 1  -- {* refutes @{term "P"} *}
webertj@14350
    19
  refute 2  -- {* refutes @{term "Q"} *}
webertj@14350
    20
  refute    -- {* equivalent to 'refute 1' *}
webertj@14455
    21
    -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
webertj@14465
    22
  refute [maxsize=5]           -- {* we can override parameters ... *}
webertj@14465
    23
  refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
webertj@14350
    24
oops
webertj@14350
    25
webertj@25014
    26
(*****************************************************************************)
webertj@21985
    27
wenzelm@23219
    28
subsection {* Examples and Test Cases *}
webertj@14350
    29
wenzelm@23219
    30
subsubsection {* Propositional logic *}
webertj@14350
    31
webertj@14350
    32
lemma "True"
webertj@14350
    33
  refute
webertj@14350
    34
  apply auto
webertj@14350
    35
done
webertj@14350
    36
webertj@14350
    37
lemma "False"
webertj@14350
    38
  refute
webertj@14350
    39
oops
webertj@14350
    40
webertj@14350
    41
lemma "P"
webertj@14350
    42
  refute
webertj@14350
    43
oops
webertj@14350
    44
webertj@14350
    45
lemma "~ P"
webertj@14350
    46
  refute
webertj@14350
    47
oops
webertj@14350
    48
webertj@14350
    49
lemma "P & Q"
webertj@14350
    50
  refute
webertj@14350
    51
oops
webertj@14350
    52
webertj@14350
    53
lemma "P | Q"
webertj@14350
    54
  refute
webertj@14350
    55
oops
webertj@14350
    56
webertj@14350
    57
lemma "P \<longrightarrow> Q"
webertj@14350
    58
  refute
webertj@14350
    59
oops
webertj@14350
    60
webertj@14350
    61
lemma "(P::bool) = Q"
webertj@14350
    62
  refute
webertj@14350
    63
oops
webertj@14350
    64
webertj@14350
    65
lemma "(P | Q) \<longrightarrow> (P & Q)"
webertj@14350
    66
  refute
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"
webertj@14350
    74
  refute
webertj@14350
    75
oops
webertj@14350
    76
webertj@14350
    77
lemma "P x y \<longrightarrow> P y x"
webertj@14350
    78
  refute
webertj@14350
    79
oops
webertj@14350
    80
webertj@14455
    81
lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
webertj@14455
    82
  refute
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"
webertj@14350
    90
  refute
webertj@14350
    91
oops
webertj@14350
    92
webertj@14350
    93
lemma "P = False"
webertj@14350
    94
  refute
webertj@14350
    95
oops
webertj@14350
    96
webertj@14350
    97
lemma "x = y"
webertj@14350
    98
  refute
webertj@14350
    99
oops
webertj@14350
   100
webertj@14350
   101
lemma "f x = g x"
webertj@14350
   102
  refute
webertj@14350
   103
oops
webertj@14350
   104
webertj@14350
   105
lemma "(f::'a\<Rightarrow>'b) = g"
webertj@14350
   106
  refute
webertj@14350
   107
oops
webertj@14350
   108
webertj@14350
   109
lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
webertj@14350
   110
  refute
webertj@14350
   111
oops
webertj@14350
   112
webertj@14350
   113
lemma "distinct [a,b]"
webertj@14809
   114
  refute
webertj@14350
   115
  apply simp
webertj@14350
   116
  refute
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"
webertj@14350
   124
  refute
webertj@14350
   125
oops
webertj@14350
   126
webertj@14350
   127
lemma "\<forall>x. P x"
webertj@14350
   128
  refute
webertj@14350
   129
oops
webertj@14350
   130
webertj@14350
   131
lemma "EX! x. P x"
webertj@14350
   132
  refute
webertj@14350
   133
oops
webertj@14350
   134
webertj@14350
   135
lemma "Ex P"
webertj@14350
   136
  refute
webertj@14350
   137
oops
webertj@14350
   138
webertj@14350
   139
lemma "All P"
webertj@14350
   140
  refute
webertj@14350
   141
oops
webertj@14350
   142
webertj@14350
   143
lemma "Ex1 P"
webertj@14350
   144
  refute
webertj@14350
   145
oops
webertj@14350
   146
webertj@14350
   147
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
webertj@14350
   148
  refute
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)"
webertj@14350
   152
  refute
webertj@14350
   153
oops
webertj@14350
   154
webertj@14350
   155
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
webertj@14350
   156
  refute
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"
webertj@18774
   162
  refute [maxsize=4]
webertj@14350
   163
  apply fast
webertj@14350
   164
done
webertj@14350
   165
webertj@18789
   166
text {* "A type has at most 4 elements." *}
webertj@14350
   167
webertj@18789
   168
lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
webertj@14455
   169
  refute
webertj@14455
   170
oops
webertj@14455
   171
webertj@18789
   172
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
   173
  refute
webertj@14350
   174
oops
webertj@14350
   175
webertj@14350
   176
text {* "Every reflexive and symmetric relation is transitive." *}
webertj@14350
   177
webertj@14350
   178
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
   179
  refute
webertj@14350
   180
oops
webertj@14350
   181
webertj@14465
   182
text {* The "Drinker's theorem" ... *}
webertj@14350
   183
webertj@14350
   184
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
webertj@14809
   185
  refute [maxsize=4]
webertj@14350
   186
  apply (auto simp add: ext)
webertj@14350
   187
done
webertj@14350
   188
webertj@14465
   189
text {* ... and an incorrect version of it *}
webertj@14350
   190
webertj@14350
   191
lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
webertj@14350
   192
  refute
webertj@14350
   193
oops
webertj@14350
   194
webertj@14350
   195
text {* "Every function has a fixed point." *}
webertj@14350
   196
webertj@14350
   197
lemma "\<exists>x. f x = x"
webertj@14350
   198
  refute
webertj@14350
   199
oops
webertj@14350
   200
webertj@14350
   201
text {* "Function composition is commutative." *}
webertj@14350
   202
webertj@14350
   203
lemma "f (g x) = g (f x)"
webertj@14350
   204
  refute
webertj@14350
   205
oops
webertj@14350
   206
webertj@14350
   207
text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
webertj@14350
   208
webertj@14350
   209
lemma "((P::('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
webertj@14350
   210
  refute
webertj@14350
   211
oops
webertj@14350
   212
webertj@25014
   213
(*****************************************************************************)
webertj@21985
   214
wenzelm@23219
   215
subsubsection {* Higher-Order Logic *}
webertj@14350
   216
webertj@14350
   217
lemma "\<exists>P. P"
webertj@14350
   218
  refute
webertj@14350
   219
  apply auto
webertj@14350
   220
done
webertj@14350
   221
webertj@14350
   222
lemma "\<forall>P. P"
webertj@14350
   223
  refute
webertj@14350
   224
oops
webertj@14350
   225
webertj@14350
   226
lemma "EX! P. P"
webertj@14350
   227
  refute
webertj@14350
   228
  apply auto
webertj@14350
   229
done
webertj@14350
   230
webertj@14350
   231
lemma "EX! P. P x"
webertj@14350
   232
  refute
webertj@14350
   233
oops
webertj@14350
   234
webertj@14350
   235
lemma "P Q | Q x"
webertj@14350
   236
  refute
webertj@14350
   237
oops
webertj@14350
   238
webertj@21985
   239
lemma "x \<noteq> All"
webertj@14455
   240
  refute
webertj@14455
   241
oops
webertj@14455
   242
webertj@21985
   243
lemma "x \<noteq> Ex"
webertj@14455
   244
  refute
webertj@14455
   245
oops
webertj@14455
   246
webertj@21985
   247
lemma "x \<noteq> Ex1"
webertj@14455
   248
  refute
webertj@14455
   249
oops
webertj@14455
   250
webertj@14350
   251
text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
webertj@14350
   252
webertj@14350
   253
constdefs
webertj@14350
   254
  "trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
webertj@14350
   255
  "trans P == (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
webertj@14350
   256
  "subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
webertj@14350
   257
  "subset P Q == (ALL x y. P x y \<longrightarrow> Q x y)"
webertj@14350
   258
  "trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
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
webertj@14350
   350
lemma "?P"
webertj@14350
   351
  refute
webertj@14350
   352
  apply auto
webertj@14350
   353
done
webertj@14350
   354
webertj@14350
   355
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
wenzelm@23219
   424
subsubsection {* arbitrary *}
webertj@14455
   425
webertj@14455
   426
lemma "arbitrary"
webertj@14455
   427
  refute
webertj@14455
   428
oops
webertj@14455
   429
webertj@14455
   430
lemma "P arbitrary"
webertj@14455
   431
  refute
webertj@14455
   432
oops
webertj@14455
   433
webertj@14455
   434
lemma "arbitrary x"
webertj@14455
   435
  refute
webertj@14455
   436
oops
webertj@14455
   437
webertj@14455
   438
lemma "arbitrary arbitrary"
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
webertj@14809
   497
typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'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
webertj@25031
   521
(*
webertj@25031
   522
ML {* reset quick_and_dirty; *}
webertj@25031
   523
*)
webertj@25014
   524
wenzelm@23219
   525
text {* unit *}
webertj@14350
   526
webertj@14350
   527
lemma "P (x::unit)"
webertj@14350
   528
  refute
webertj@14350
   529
oops
webertj@14350
   530
webertj@14350
   531
lemma "\<forall>x::unit. P x"
webertj@14350
   532
  refute
webertj@14350
   533
oops
webertj@14350
   534
webertj@14350
   535
lemma "P ()"
webertj@14350
   536
  refute
webertj@14350
   537
oops
webertj@14350
   538
webertj@25014
   539
lemma "unit_rec u x = u"
webertj@25014
   540
  refute
webertj@25014
   541
  apply simp
webertj@25014
   542
done
webertj@25014
   543
webertj@15547
   544
lemma "P (unit_rec u x)"
webertj@15547
   545
  refute
webertj@15547
   546
oops
webertj@15547
   547
webertj@15547
   548
lemma "P (case x of () \<Rightarrow> u)"
webertj@15547
   549
  refute
webertj@15547
   550
oops
webertj@15547
   551
wenzelm@23219
   552
text {* option *}
webertj@14455
   553
webertj@14455
   554
lemma "P (x::'a option)"
webertj@14455
   555
  refute
webertj@14455
   556
oops
webertj@14455
   557
webertj@14455
   558
lemma "\<forall>x::'a option. P x"
webertj@14455
   559
  refute
webertj@14455
   560
oops
webertj@14455
   561
webertj@14809
   562
lemma "P None"
webertj@14809
   563
  refute
webertj@14809
   564
oops
webertj@14809
   565
webertj@14455
   566
lemma "P (Some x)"
webertj@14455
   567
  refute
webertj@14455
   568
oops
webertj@14455
   569
webertj@25014
   570
lemma "option_rec n s None = n"
webertj@25014
   571
  refute
webertj@25014
   572
  apply simp
webertj@25014
   573
done
webertj@25014
   574
webertj@25014
   575
lemma "option_rec n s (Some x) = s x"
webertj@25014
   576
  refute [maxsize=4]
webertj@25014
   577
  apply simp
webertj@25014
   578
done
webertj@25014
   579
webertj@15547
   580
lemma "P (option_rec n s x)"
webertj@15547
   581
  refute
webertj@15547
   582
oops
webertj@15547
   583
webertj@15547
   584
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
webertj@15547
   585
  refute
webertj@15547
   586
oops
webertj@15547
   587
wenzelm@23219
   588
text {* * *}
webertj@14350
   589
webertj@14350
   590
lemma "P (x::'a*'b)"
webertj@14455
   591
  refute
webertj@14350
   592
oops
webertj@14350
   593
webertj@14350
   594
lemma "\<forall>x::'a*'b. P x"
webertj@14455
   595
  refute
webertj@14350
   596
oops
webertj@14350
   597
webertj@25014
   598
lemma "P (x, y)"
webertj@14455
   599
  refute
webertj@14350
   600
oops
webertj@14350
   601
webertj@14350
   602
lemma "P (fst x)"
webertj@14455
   603
  refute
webertj@14350
   604
oops
webertj@14350
   605
webertj@14350
   606
lemma "P (snd x)"
webertj@14455
   607
  refute
webertj@14455
   608
oops
webertj@14455
   609
webertj@14455
   610
lemma "P Pair"
webertj@14455
   611
  refute
webertj@14350
   612
oops
webertj@14350
   613
webertj@25014
   614
lemma "prod_rec p (a, b) = p a b"
webertj@25014
   615
  refute [maxsize=2]
webertj@25014
   616
  apply simp
webertj@25014
   617
oops
webertj@25014
   618
webertj@15547
   619
lemma "P (prod_rec p x)"
webertj@15547
   620
  refute
webertj@15547
   621
oops
webertj@15547
   622
webertj@15547
   623
lemma "P (case x of Pair a b \<Rightarrow> p a b)"
webertj@15547
   624
  refute
webertj@15547
   625
oops
webertj@15547
   626
wenzelm@23219
   627
text {* + *}
webertj@14350
   628
webertj@14350
   629
lemma "P (x::'a+'b)"
webertj@14455
   630
  refute
webertj@14350
   631
oops
webertj@14350
   632
webertj@14350
   633
lemma "\<forall>x::'a+'b. P x"
webertj@14455
   634
  refute
webertj@14350
   635
oops
webertj@14350
   636
webertj@14350
   637
lemma "P (Inl x)"
webertj@14455
   638
  refute
webertj@14350
   639
oops
webertj@14350
   640
webertj@14350
   641
lemma "P (Inr x)"
webertj@14455
   642
  refute
webertj@14455
   643
oops
webertj@14455
   644
webertj@14455
   645
lemma "P Inl"
webertj@14455
   646
  refute
webertj@14350
   647
oops
webertj@14350
   648
webertj@25014
   649
lemma "sum_rec l r (Inl x) = l x"
webertj@25014
   650
  refute [maxsize=3]
webertj@25014
   651
  apply simp
webertj@25014
   652
done
webertj@25014
   653
webertj@25014
   654
lemma "sum_rec l r (Inr x) = r x"
webertj@25014
   655
  refute [maxsize=3]
webertj@25014
   656
  apply simp
webertj@25014
   657
done
webertj@25014
   658
webertj@15547
   659
lemma "P (sum_rec l r x)"
webertj@15547
   660
  refute
webertj@15547
   661
oops
webertj@15547
   662
webertj@15547
   663
lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
webertj@15547
   664
  refute
webertj@15547
   665
oops
webertj@15547
   666
wenzelm@23219
   667
text {* Non-recursive datatypes *}
webertj@14350
   668
webertj@14455
   669
datatype T1 = A | B
webertj@14350
   670
webertj@14350
   671
lemma "P (x::T1)"
webertj@14350
   672
  refute
webertj@14350
   673
oops
webertj@14350
   674
webertj@14350
   675
lemma "\<forall>x::T1. P x"
webertj@14350
   676
  refute
webertj@14350
   677
oops
webertj@14350
   678
webertj@14455
   679
lemma "P A"
webertj@14350
   680
  refute
webertj@14350
   681
oops
webertj@14350
   682
webertj@25014
   683
lemma "P B"
webertj@25014
   684
  refute
webertj@25014
   685
oops
webertj@25014
   686
webertj@25014
   687
lemma "T1_rec a b A = a"
webertj@25014
   688
  refute
webertj@25014
   689
  apply simp
webertj@25014
   690
done
webertj@25014
   691
webertj@25014
   692
lemma "T1_rec a b B = b"
webertj@25014
   693
  refute
webertj@25014
   694
  apply simp
webertj@25014
   695
done
webertj@25014
   696
webertj@15547
   697
lemma "P (T1_rec a b x)"
webertj@15547
   698
  refute
webertj@15547
   699
oops
webertj@15547
   700
webertj@15547
   701
lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
webertj@15547
   702
  refute
webertj@15547
   703
oops
webertj@15547
   704
webertj@14455
   705
datatype 'a T2 = C T1 | D 'a
webertj@14455
   706
webertj@14455
   707
lemma "P (x::'a T2)"
webertj@14350
   708
  refute
webertj@14350
   709
oops
webertj@14350
   710
webertj@14455
   711
lemma "\<forall>x::'a T2. P x"
webertj@14350
   712
  refute
webertj@14350
   713
oops
webertj@14350
   714
webertj@14455
   715
lemma "P D"
webertj@14350
   716
  refute
webertj@14350
   717
oops
webertj@14350
   718
webertj@25014
   719
lemma "T2_rec c d (C x) = c x"
webertj@25014
   720
  refute [maxsize=4]
webertj@25014
   721
  apply simp
webertj@25014
   722
done
webertj@25014
   723
webertj@25014
   724
lemma "T2_rec c d (D x) = d x"
webertj@25014
   725
  refute [maxsize=4]
webertj@25014
   726
  apply simp
webertj@25014
   727
done
webertj@25014
   728
webertj@15547
   729
lemma "P (T2_rec c d x)"
webertj@15547
   730
  refute
webertj@15547
   731
oops
webertj@15547
   732
webertj@15547
   733
lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
webertj@15547
   734
  refute
webertj@15547
   735
oops
webertj@15547
   736
webertj@14455
   737
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
webertj@14455
   738
webertj@14809
   739
lemma "P (x::('a,'b) T3)"
webertj@14809
   740
  refute
webertj@14809
   741
oops
webertj@14809
   742
webertj@14809
   743
lemma "\<forall>x::('a,'b) T3. P x"
webertj@14809
   744
  refute
webertj@14809
   745
oops
webertj@14809
   746
webertj@14455
   747
lemma "P E"
webertj@14455
   748
  refute
webertj@14350
   749
oops
webertj@14350
   750
webertj@25014
   751
lemma "T3_rec e (E x) = e x"
webertj@25014
   752
  refute [maxsize=2]
webertj@25014
   753
  apply simp
webertj@25014
   754
done
webertj@25014
   755
webertj@15547
   756
lemma "P (T3_rec e x)"
webertj@15547
   757
  refute
webertj@15547
   758
oops
webertj@15547
   759
webertj@15547
   760
lemma "P (case x of E f \<Rightarrow> e f)"
webertj@15547
   761
  refute
webertj@15547
   762
oops
webertj@15547
   763
wenzelm@23219
   764
text {* Recursive datatypes *}
webertj@14350
   765
webertj@15547
   766
text {* nat *}
webertj@15547
   767
webertj@14809
   768
lemma "P (x::nat)"
webertj@14809
   769
  refute
webertj@14809
   770
oops
webertj@14350
   771
webertj@14809
   772
lemma "\<forall>x::nat. P x"
webertj@14809
   773
  refute
webertj@14350
   774
oops
webertj@14350
   775
webertj@14809
   776
lemma "P (Suc 0)"
webertj@14809
   777
  refute
webertj@14350
   778
oops
webertj@14350
   779
webertj@14809
   780
lemma "P Suc"
webertj@14809
   781
  refute  -- {* @{term "Suc"} is a partial function (regardless of the size
webertj@14809
   782
                of the model), hence @{term "P Suc"} is undefined, hence no
webertj@14809
   783
                model will be found *}
webertj@14350
   784
oops
webertj@14350
   785
webertj@25014
   786
lemma "nat_rec zero suc 0 = zero"
webertj@25014
   787
  refute
webertj@25014
   788
  apply simp
webertj@25014
   789
done
webertj@25014
   790
webertj@25014
   791
lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
webertj@25014
   792
  refute [maxsize=2]
webertj@25014
   793
  apply simp
webertj@25014
   794
done
webertj@25014
   795
webertj@15547
   796
lemma "P (nat_rec zero suc x)"
webertj@15547
   797
  refute
webertj@15547
   798
oops
webertj@15547
   799
webertj@15547
   800
lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
webertj@15547
   801
  refute
webertj@15547
   802
oops
webertj@15547
   803
webertj@15547
   804
text {* 'a list *}
webertj@15547
   805
webertj@15547
   806
lemma "P (xs::'a list)"
webertj@15547
   807
  refute
webertj@15547
   808
oops
webertj@15547
   809
webertj@15547
   810
lemma "\<forall>xs::'a list. P xs"
webertj@15547
   811
  refute
webertj@15547
   812
oops
webertj@15547
   813
webertj@15547
   814
lemma "P [x, y]"
webertj@15547
   815
  refute
webertj@15547
   816
oops
webertj@15547
   817
webertj@25014
   818
lemma "list_rec nil cons [] = nil"
webertj@25014
   819
  refute [maxsize=3]
webertj@25014
   820
  apply simp
webertj@25014
   821
done
webertj@25014
   822
webertj@25014
   823
lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
webertj@25014
   824
  refute [maxsize=2]
webertj@25014
   825
  apply simp
webertj@25014
   826
done
webertj@25014
   827
webertj@15547
   828
lemma "P (list_rec nil cons xs)"
webertj@15547
   829
  refute
webertj@15547
   830
oops
webertj@15547
   831
webertj@15547
   832
lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
webertj@15547
   833
  refute
webertj@15547
   834
oops
webertj@15547
   835
webertj@15547
   836
lemma "(xs::'a list) = ys"
webertj@15547
   837
  refute
webertj@15547
   838
oops
webertj@15547
   839
webertj@15547
   840
lemma "a # xs = b # xs"
webertj@15547
   841
  refute
webertj@15547
   842
oops
webertj@15547
   843
webertj@25014
   844
datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
webertj@25014
   845
webertj@25014
   846
lemma "P (x::BitList)"
webertj@25014
   847
  refute
webertj@25014
   848
oops
webertj@25014
   849
webertj@25014
   850
lemma "\<forall>x::BitList. P x"
webertj@25014
   851
  refute
webertj@25014
   852
oops
webertj@25014
   853
webertj@25014
   854
lemma "P (Bit0 (Bit1 BitListNil))"
webertj@25014
   855
  refute
webertj@25014
   856
oops
webertj@25014
   857
webertj@25014
   858
lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
webertj@25014
   859
  refute [maxsize=4]
webertj@25014
   860
  apply simp
webertj@25014
   861
done
webertj@25014
   862
webertj@25014
   863
lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
webertj@25014
   864
  refute [maxsize=2]
webertj@25014
   865
  apply simp
webertj@25014
   866
done
webertj@25014
   867
webertj@25014
   868
lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
webertj@25014
   869
  refute [maxsize=2]
webertj@25014
   870
  apply simp
webertj@25014
   871
done
webertj@25014
   872
webertj@25014
   873
lemma "P (BitList_rec nil bit0 bit1 x)"
webertj@25014
   874
  refute
webertj@25014
   875
oops
webertj@25014
   876
webertj@14350
   877
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
webertj@14350
   878
webertj@14350
   879
lemma "P (x::'a BinTree)"
webertj@14809
   880
  refute
webertj@14350
   881
oops
webertj@14350
   882
webertj@14350
   883
lemma "\<forall>x::'a BinTree. P x"
webertj@14809
   884
  refute
webertj@14809
   885
oops
webertj@14809
   886
webertj@14809
   887
lemma "P (Node (Leaf x) (Leaf y))"
webertj@14809
   888
  refute
webertj@14350
   889
oops
webertj@14350
   890
webertj@25014
   891
lemma "BinTree_rec l n (Leaf x) = l x"
webertj@25014
   892
  refute [maxsize=1]  (* The "maxsize=1" tests are a bit pointless: for some formulae
webertj@25014
   893
                         below, refute will find no countermodel simply because this
webertj@25014
   894
                         size makes involved terms undefined.  Unfortunately, any
webertj@25014
   895
                         larger size already takes too long. *)
webertj@25014
   896
  apply simp
webertj@25014
   897
done
webertj@25014
   898
webertj@25014
   899
lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
webertj@25014
   900
  refute [maxsize=1]
webertj@25014
   901
  apply simp
webertj@25014
   902
done
webertj@25014
   903
webertj@15547
   904
lemma "P (BinTree_rec l n x)"
webertj@15547
   905
  refute
webertj@15547
   906
oops
webertj@15547
   907
webertj@15547
   908
lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
webertj@15547
   909
  refute
webertj@15547
   910
oops
webertj@15547
   911
wenzelm@23219
   912
text {* Mutually recursive datatypes *}
webertj@14350
   913
webertj@14350
   914
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
webertj@14350
   915
     and 'a bexp = Equal "'a aexp" "'a aexp"
webertj@14350
   916
webertj@14350
   917
lemma "P (x::'a aexp)"
webertj@14809
   918
  refute
webertj@14350
   919
oops
webertj@14350
   920
webertj@14350
   921
lemma "\<forall>x::'a aexp. P x"
webertj@14809
   922
  refute
webertj@14350
   923
oops
webertj@14350
   924
webertj@15547
   925
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
webertj@15547
   926
  refute
webertj@15547
   927
oops
webertj@15547
   928
webertj@14350
   929
lemma "P (x::'a bexp)"
webertj@14809
   930
  refute
webertj@14350
   931
oops
webertj@14350
   932
webertj@14350
   933
lemma "\<forall>x::'a bexp. P x"
webertj@14809
   934
  refute
webertj@14350
   935
oops
webertj@14350
   936
webertj@25014
   937
lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
webertj@25014
   938
  refute [maxsize=1]
webertj@25014
   939
  apply simp
webertj@25014
   940
done
webertj@25014
   941
webertj@25014
   942
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
   943
  refute [maxsize=1]
webertj@25014
   944
  apply simp
webertj@25014
   945
done
webertj@25014
   946
webertj@15547
   947
lemma "P (aexp_bexp_rec_1 number ite equal x)"
webertj@15547
   948
  refute
webertj@15547
   949
oops
webertj@15547
   950
webertj@15547
   951
lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
webertj@14809
   952
  refute
webertj@14350
   953
oops
webertj@14350
   954
webertj@25014
   955
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
   956
  refute [maxsize=1]
webertj@25014
   957
  apply simp
webertj@25014
   958
done
webertj@25014
   959
webertj@15547
   960
lemma "P (aexp_bexp_rec_2 number ite equal x)"
webertj@15767
   961
  refute
webertj@15547
   962
oops
webertj@15547
   963
webertj@15547
   964
lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
webertj@15767
   965
  refute
webertj@15547
   966
oops
webertj@15547
   967
webertj@25014
   968
datatype X = A | B X | C Y
webertj@25014
   969
     and Y = D X | E Y | F
webertj@25014
   970
webertj@25014
   971
lemma "P (x::X)"
webertj@25014
   972
  refute
webertj@25014
   973
oops
webertj@25014
   974
webertj@25014
   975
lemma "P (y::Y)"
webertj@25014
   976
  refute
webertj@25014
   977
oops
webertj@25014
   978
webertj@25014
   979
lemma "P (B (B A))"
webertj@25014
   980
  refute
webertj@25014
   981
oops
webertj@25014
   982
webertj@25014
   983
lemma "P (B (C F))"
webertj@25014
   984
  refute
webertj@25014
   985
oops
webertj@25014
   986
webertj@25014
   987
lemma "P (C (D A))"
webertj@25014
   988
  refute
webertj@25014
   989
oops
webertj@25014
   990
webertj@25014
   991
lemma "P (C (E F))"
webertj@25014
   992
  refute
webertj@25014
   993
oops
webertj@25014
   994
webertj@25014
   995
lemma "P (D (B A))"
webertj@25014
   996
  refute
webertj@25014
   997
oops
webertj@25014
   998
webertj@25014
   999
lemma "P (D (C F))"
webertj@25014
  1000
  refute
webertj@25014
  1001
oops
webertj@25014
  1002
webertj@25014
  1003
lemma "P (E (D A))"
webertj@25014
  1004
  refute
webertj@25014
  1005
oops
webertj@25014
  1006
webertj@25014
  1007
lemma "P (E (E F))"
webertj@25014
  1008
  refute
webertj@25014
  1009
oops
webertj@25014
  1010
webertj@25014
  1011
lemma "P (C (D (C F)))"
webertj@25014
  1012
  refute
webertj@25014
  1013
oops
webertj@25014
  1014
webertj@25014
  1015
lemma "X_Y_rec_1 a b c d e f A = a"
webertj@25014
  1016
  refute [maxsize=3]
webertj@25014
  1017
  apply simp
webertj@25014
  1018
done
webertj@25014
  1019
webertj@25014
  1020
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
  1021
  refute [maxsize=1]
webertj@25014
  1022
  apply simp
webertj@25014
  1023
done
webertj@25014
  1024
webertj@25014
  1025
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
  1026
  refute [maxsize=1]
webertj@25014
  1027
  apply simp
webertj@25014
  1028
done
webertj@25014
  1029
webertj@25014
  1030
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
  1031
  refute [maxsize=1]
webertj@25014
  1032
  apply simp
webertj@25014
  1033
done
webertj@25014
  1034
webertj@25014
  1035
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
  1036
  refute [maxsize=1]
webertj@25014
  1037
  apply simp
webertj@25014
  1038
done
webertj@25014
  1039
webertj@25014
  1040
lemma "X_Y_rec_2 a b c d e f F = f"
webertj@25014
  1041
  refute [maxsize=3]
webertj@25014
  1042
  apply simp
webertj@25014
  1043
done
webertj@25014
  1044
webertj@25014
  1045
lemma "P (X_Y_rec_1 a b c d e f x)"
webertj@25014
  1046
  refute
webertj@25014
  1047
oops
webertj@25014
  1048
webertj@25014
  1049
lemma "P (X_Y_rec_2 a b c d e f y)"
webertj@25014
  1050
  refute
webertj@25014
  1051
oops
webertj@25014
  1052
wenzelm@23219
  1053
text {* Other datatype examples *}
webertj@14350
  1054
webertj@25014
  1055
text {* Indirect recursion is implemented via mutual recursion. *}
webertj@25014
  1056
webertj@25014
  1057
datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
webertj@25014
  1058
webertj@25014
  1059
lemma "P (x::XOpt)"
webertj@25014
  1060
  refute
webertj@25014
  1061
oops
webertj@25014
  1062
webertj@25014
  1063
lemma "P (CX None)"
webertj@25014
  1064
  refute
webertj@25014
  1065
oops
webertj@25014
  1066
webertj@25014
  1067
lemma "P (CX (Some (CX None)))"
webertj@25014
  1068
  refute
webertj@25014
  1069
oops
webertj@25014
  1070
webertj@25014
  1071
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
  1072
  refute [maxsize=1]
webertj@25014
  1073
  apply simp
webertj@25014
  1074
done
webertj@25014
  1075
webertj@25014
  1076
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
  1077
  refute [maxsize=1]
webertj@25014
  1078
  apply simp
webertj@25014
  1079
done
webertj@25014
  1080
webertj@25014
  1081
lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
webertj@25014
  1082
  refute [maxsize=2]
webertj@25014
  1083
  apply simp
webertj@25014
  1084
done
webertj@25014
  1085
webertj@25014
  1086
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
  1087
  refute [maxsize=1]
webertj@25014
  1088
  apply simp
webertj@25014
  1089
done
webertj@25014
  1090
webertj@25014
  1091
lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
webertj@25014
  1092
  refute [maxsize=2]
webertj@25014
  1093
  apply simp
webertj@25014
  1094
done
webertj@25014
  1095
webertj@25014
  1096
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
  1097
  refute [maxsize=1]
webertj@25014
  1098
  apply simp
webertj@25014
  1099
done
webertj@25014
  1100
webertj@25014
  1101
lemma "P (XOpt_rec_1 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_2 cx dx n1 s1 n2 s2 x)"
webertj@25014
  1106
  refute
webertj@25014
  1107
oops
webertj@25014
  1108
webertj@25014
  1109
lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
webertj@25014
  1110
  refute
webertj@25014
  1111
oops
webertj@25014
  1112
webertj@25014
  1113
datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
webertj@25014
  1114
webertj@25014
  1115
lemma "P (x::'a YOpt)"
webertj@25014
  1116
  refute
webertj@25014
  1117
oops
webertj@25014
  1118
webertj@25014
  1119
lemma "P (CY None)"
webertj@25014
  1120
  refute
webertj@25014
  1121
oops
webertj@25014
  1122
webertj@25014
  1123
lemma "P (CY (Some (\<lambda>a. CY None)))"
webertj@25014
  1124
  refute
webertj@25014
  1125
oops
webertj@25014
  1126
webertj@25014
  1127
lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
webertj@25014
  1128
  refute [maxsize=1]
webertj@25014
  1129
  apply simp
webertj@25014
  1130
done
webertj@25014
  1131
webertj@25014
  1132
lemma "YOpt_rec_2 cy n s None = n"
webertj@25014
  1133
  refute [maxsize=2]
webertj@25014
  1134
  apply simp
webertj@25014
  1135
done
webertj@25014
  1136
webertj@25014
  1137
lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
webertj@25014
  1138
  refute [maxsize=1]
webertj@25014
  1139
  apply simp
webertj@25014
  1140
done
webertj@25014
  1141
webertj@25014
  1142
lemma "P (YOpt_rec_1 cy n s x)"
webertj@25014
  1143
  refute
webertj@25014
  1144
oops
webertj@25014
  1145
webertj@25014
  1146
lemma "P (YOpt_rec_2 cy n s x)"
webertj@25014
  1147
  refute
webertj@25014
  1148
oops
webertj@25014
  1149
webertj@15547
  1150
datatype Trie = TR "Trie list"
webertj@15547
  1151
webertj@15547
  1152
lemma "P (x::Trie)"
webertj@15547
  1153
  refute
webertj@15547
  1154
oops
webertj@15547
  1155
webertj@15547
  1156
lemma "\<forall>x::Trie. P x"
webertj@15547
  1157
  refute
webertj@15547
  1158
oops
webertj@15547
  1159
webertj@15547
  1160
lemma "P (TR [TR []])"
webertj@15547
  1161
  refute
webertj@15547
  1162
oops
webertj@15547
  1163
webertj@25014
  1164
lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
webertj@25014
  1165
  refute [maxsize=1]
webertj@25014
  1166
  apply simp
webertj@25014
  1167
done
webertj@25014
  1168
webertj@25014
  1169
lemma "Trie_rec_2 tr nil cons [] = nil"
webertj@25014
  1170
  refute [maxsize=3]
webertj@25014
  1171
  apply simp
webertj@25014
  1172
done
webertj@25014
  1173
webertj@25014
  1174
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
  1175
  refute [maxsize=1]
webertj@25014
  1176
  apply simp
webertj@25014
  1177
done
webertj@25014
  1178
webertj@25014
  1179
lemma "P (Trie_rec_1 tr nil cons x)"
webertj@15767
  1180
  refute
webertj@15767
  1181
oops
webertj@15767
  1182
webertj@25014
  1183
lemma "P (Trie_rec_2 tr nil cons x)"
webertj@15547
  1184
  refute
webertj@15547
  1185
oops
webertj@15547
  1186
webertj@14809
  1187
datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
webertj@14350
  1188
webertj@14350
  1189
lemma "P (x::InfTree)"
webertj@14809
  1190
  refute
webertj@14350
  1191
oops
webertj@14350
  1192
webertj@15547
  1193
lemma "\<forall>x::InfTree. P x"
webertj@15547
  1194
  refute
webertj@15547
  1195
oops
webertj@15547
  1196
webertj@15547
  1197
lemma "P (Node (\<lambda>n. Leaf))"
webertj@15547
  1198
  refute
webertj@15547
  1199
oops
webertj@15547
  1200
webertj@25014
  1201
lemma "InfTree_rec leaf node Leaf = leaf"
webertj@25014
  1202
  refute [maxsize=2]
webertj@25014
  1203
  apply simp
webertj@25014
  1204
done
webertj@25014
  1205
webertj@25014
  1206
lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
webertj@25014
  1207
  refute [maxsize=1]
webertj@25014
  1208
  apply simp
webertj@25014
  1209
done
webertj@25014
  1210
webertj@15547
  1211
lemma "P (InfTree_rec leaf node x)"
webertj@15547
  1212
  refute
webertj@15547
  1213
oops
webertj@15547
  1214
webertj@14350
  1215
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
webertj@14350
  1216
webertj@15547
  1217
lemma "P (x::'a lambda)"
webertj@15547
  1218
  refute
webertj@15547
  1219
oops
webertj@15547
  1220
webertj@15547
  1221
lemma "\<forall>x::'a lambda. P x"
webertj@15547
  1222
  refute
webertj@15547
  1223
oops
webertj@15547
  1224
webertj@15547
  1225
lemma "P (Lam (\<lambda>a. Var a))"
webertj@15547
  1226
  refute
webertj@15547
  1227
oops
webertj@15547
  1228
webertj@25014
  1229
lemma "lambda_rec var app lam (Var x) = var x"
webertj@25014
  1230
  refute [maxsize=1]
webertj@25014
  1231
  apply simp
webertj@25014
  1232
done
webertj@25014
  1233
webertj@25014
  1234
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
  1235
  refute [maxsize=1]
webertj@25014
  1236
  apply simp
webertj@25014
  1237
done
webertj@25014
  1238
webertj@25014
  1239
lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
webertj@25014
  1240
  refute [maxsize=1]
webertj@25014
  1241
  apply simp
webertj@25014
  1242
done
webertj@25014
  1243
webertj@15547
  1244
lemma "P (lambda_rec v a l x)"
webertj@15547
  1245
  refute
webertj@15547
  1246
oops
webertj@15547
  1247
webertj@15767
  1248
text {* Taken from "Inductive datatypes in HOL", p.8: *}
webertj@15767
  1249
webertj@15767
  1250
datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
webertj@15767
  1251
datatype 'c U = E "('c, 'c U) T"
webertj@15767
  1252
webertj@15767
  1253
lemma "P (x::'c U)"
webertj@15767
  1254
  refute
webertj@15767
  1255
oops
webertj@15767
  1256
webertj@15767
  1257
lemma "\<forall>x::'c U. P x"
webertj@15767
  1258
  refute
webertj@15767
  1259
oops
webertj@15767
  1260
webertj@15767
  1261
lemma "P (E (C (\<lambda>a. True)))"
webertj@15767
  1262
  refute
webertj@15767
  1263
oops
webertj@15767
  1264
webertj@25014
  1265
lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
webertj@25014
  1266
  refute [maxsize=1]
webertj@25014
  1267
  apply simp
webertj@25014
  1268
done
webertj@25014
  1269
webertj@25014
  1270
lemma "U_rec_2 e c d nil cons (C x) = c x"
webertj@25014
  1271
  refute [maxsize=1]
webertj@25014
  1272
  apply simp
webertj@25014
  1273
done
webertj@25014
  1274
webertj@25014
  1275
lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
webertj@25014
  1276
  refute [maxsize=1]
webertj@25014
  1277
  apply simp
webertj@25014
  1278
done
webertj@25014
  1279
webertj@25014
  1280
lemma "U_rec_3 e c d nil cons [] = nil"
webertj@25014
  1281
  refute [maxsize=2]
webertj@25014
  1282
  apply simp
webertj@25014
  1283
done
webertj@25014
  1284
webertj@25014
  1285
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
  1286
  refute [maxsize=1]
webertj@25014
  1287
  apply simp
webertj@25014
  1288
done
webertj@25014
  1289
webertj@25014
  1290
lemma "P (U_rec_1 e c d nil cons x)"
webertj@15767
  1291
  refute
webertj@15767
  1292
oops
webertj@15767
  1293
webertj@25014
  1294
lemma "P (U_rec_2 e c d nil cons x)"
webertj@15767
  1295
  refute
webertj@15767
  1296
oops
webertj@15767
  1297
webertj@25014
  1298
lemma "P (U_rec_3 e c d nil cons x)"
webertj@15767
  1299
  refute
webertj@15767
  1300
oops
webertj@15767
  1301
webertj@25014
  1302
(*****************************************************************************)
webertj@15767
  1303
wenzelm@23219
  1304
subsubsection {* Records *}
webertj@15767
  1305
webertj@15767
  1306
(*TODO: make use of pair types, rather than typedef, for record types*)
webertj@15767
  1307
webertj@15767
  1308
record ('a, 'b) point =
webertj@15767
  1309
  xpos :: 'a
webertj@15767
  1310
  ypos :: 'b
webertj@15767
  1311
webertj@15767
  1312
lemma "(x::('a, 'b) point) = y"
webertj@15767
  1313
  refute
webertj@15767
  1314
oops
webertj@15767
  1315
webertj@15767
  1316
record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
webertj@15767
  1317
  ext :: 'c
webertj@15767
  1318
webertj@15767
  1319
lemma "(x::('a, 'b, 'c) extpoint) = y"
webertj@15767
  1320
  refute
webertj@15767
  1321
oops
webertj@15767
  1322
webertj@25014
  1323
(*****************************************************************************)
webertj@15767
  1324
wenzelm@23219
  1325
subsubsection {* Inductively defined sets *}
webertj@15767
  1326
berghofe@23778
  1327
inductive_set arbitrarySet :: "'a set"
berghofe@23778
  1328
where
webertj@15767
  1329
  "arbitrary : arbitrarySet"
webertj@15767
  1330
webertj@15767
  1331
lemma "x : arbitrarySet"
webertj@16050
  1332
  refute
webertj@15767
  1333
oops
webertj@15767
  1334
berghofe@23778
  1335
inductive_set evenCard :: "'a set set"
berghofe@23778
  1336
where
webertj@15767
  1337
  "{} : evenCard"
berghofe@23778
  1338
| "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
webertj@15767
  1339
webertj@15767
  1340
lemma "S : evenCard"
webertj@16050
  1341
  refute
webertj@15767
  1342
oops
webertj@15767
  1343
berghofe@23778
  1344
inductive_set
webertj@15767
  1345
  even :: "nat set"
berghofe@23778
  1346
  and odd  :: "nat set"
berghofe@23778
  1347
where
webertj@15767
  1348
  "0 : even"
berghofe@23778
  1349
| "n : even \<Longrightarrow> Suc n : odd"
berghofe@23778
  1350
| "n : odd \<Longrightarrow> Suc n : even"
webertj@15767
  1351
webertj@15767
  1352
lemma "n : odd"
webertj@25014
  1353
  (*refute*)  (* TODO: there seems to be an issue here with undefined terms
webertj@25014
  1354
                       because of the recursive datatype "nat" *)
webertj@15767
  1355
oops
webertj@15767
  1356
webertj@25014
  1357
consts f :: "'a \<Rightarrow> 'a"
webertj@25014
  1358
webertj@25014
  1359
inductive_set
webertj@25014
  1360
  a_even :: "'a set"
webertj@25014
  1361
  and a_odd :: "'a set"
webertj@25014
  1362
where
webertj@25014
  1363
  "arbitrary : a_even"
webertj@25014
  1364
| "x : a_even \<Longrightarrow> f x : a_odd"
webertj@25014
  1365
| "x : a_odd \<Longrightarrow> f x : a_even"
webertj@25014
  1366
webertj@25014
  1367
lemma "x : a_odd"
webertj@25014
  1368
  refute  -- {* finds a model of size 2, as expected *}
webertj@25014
  1369
oops
webertj@25014
  1370
webertj@25014
  1371
(*****************************************************************************)
webertj@15767
  1372
wenzelm@23219
  1373
subsubsection {* Examples involving special functions *}
webertj@15547
  1374
webertj@15547
  1375
lemma "card x = 0"
webertj@15547
  1376
  refute
webertj@15547
  1377
oops
webertj@15547
  1378
webertj@15767
  1379
lemma "finite x"
webertj@15767
  1380
  refute  -- {* no finite countermodel exists *}
webertj@15547
  1381
oops
webertj@15547
  1382
webertj@15547
  1383
lemma "(x::nat) + y = 0"
webertj@15547
  1384
  refute
webertj@15547
  1385
oops
webertj@15547
  1386
webertj@15547
  1387
lemma "(x::nat) = x + x"
webertj@15547
  1388
  refute
webertj@15547
  1389
oops
webertj@15547
  1390
webertj@15547
  1391
lemma "(x::nat) - y + y = x"
webertj@15547
  1392
  refute
webertj@15547
  1393
oops
webertj@15547
  1394
webertj@15547
  1395
lemma "(x::nat) = x * x"
webertj@15547
  1396
  refute
webertj@15547
  1397
oops
webertj@15547
  1398
webertj@15547
  1399
lemma "(x::nat) < x + y"
webertj@15547
  1400
  refute
webertj@15547
  1401
oops
webertj@15547
  1402
webertj@21985
  1403
lemma "xs @ [] = ys @ []"
webertj@15547
  1404
  refute
webertj@15547
  1405
oops
webertj@15547
  1406
webertj@21985
  1407
lemma "xs @ ys = ys @ xs"
webertj@15767
  1408
  refute
webertj@15547
  1409
oops
webertj@15547
  1410
webertj@16050
  1411
lemma "f (lfp f) = lfp f"
webertj@16050
  1412
  refute
webertj@16050
  1413
oops
webertj@16050
  1414
webertj@16050
  1415
lemma "f (gfp f) = gfp f"
webertj@16050
  1416
  refute
webertj@16050
  1417
oops
webertj@16050
  1418
webertj@16050
  1419
lemma "lfp f = gfp f"
webertj@16050
  1420
  refute
webertj@16050
  1421
oops
webertj@16050
  1422
webertj@25014
  1423
(*****************************************************************************)
webertj@15547
  1424
wenzelm@23219
  1425
subsubsection {* Axiomatic type classes and overloading *}
webertj@15547
  1426
webertj@15547
  1427
text {* A type class without axioms: *}
webertj@15547
  1428
webertj@15547
  1429
axclass classA
webertj@15547
  1430
webertj@15547
  1431
lemma "P (x::'a::classA)"
webertj@14809
  1432
  refute
webertj@14809
  1433
oops
webertj@14809
  1434
webertj@21985
  1435
text {* The axiom of this type class does not contain any type variables: *}
webertj@15547
  1436
webertj@15547
  1437
axclass classB
webertj@15547
  1438
  classB_ax: "P | ~ P"
webertj@15547
  1439
webertj@15547
  1440
lemma "P (x::'a::classB)"
webertj@15547
  1441
  refute
webertj@15547
  1442
oops
webertj@15547
  1443
webertj@15547
  1444
text {* An axiom with a type variable (denoting types which have at least two elements): *}
webertj@15547
  1445
webertj@15547
  1446
axclass classC < type
webertj@15547
  1447
  classC_ax: "\<exists>x y. x \<noteq> y"
webertj@15547
  1448
webertj@15547
  1449
lemma "P (x::'a::classC)"
webertj@15547
  1450
  refute
webertj@15547
  1451
oops
webertj@15547
  1452
webertj@15547
  1453
lemma "\<exists>x y. (x::'a::classC) \<noteq> y"
webertj@15547
  1454
  refute  -- {* no countermodel exists *}
webertj@15547
  1455
oops
webertj@15547
  1456
webertj@15547
  1457
text {* A type class for which a constant is defined: *}
webertj@15547
  1458
webertj@15547
  1459
consts
webertj@15547
  1460
  classD_const :: "'a \<Rightarrow> 'a"
webertj@15547
  1461
webertj@15547
  1462
axclass classD < type
webertj@15547
  1463
  classD_ax: "classD_const (classD_const x) = classD_const x"
webertj@15547
  1464
webertj@15547
  1465
lemma "P (x::'a::classD)"
webertj@15547
  1466
  refute
webertj@15547
  1467
oops
webertj@15547
  1468
webertj@15547
  1469
text {* A type class with multiple superclasses: *}
webertj@15547
  1470
webertj@15547
  1471
axclass classE < classC, classD
webertj@15547
  1472
webertj@15547
  1473
lemma "P (x::'a::classE)"
webertj@14809
  1474
  refute
webertj@14809
  1475
oops
webertj@14809
  1476
webertj@15547
  1477
lemma "P (x::'a::{classB, classE})"
webertj@14809
  1478
  refute
webertj@14809
  1479
oops
webertj@14809
  1480
webertj@15547
  1481
text {* OFCLASS: *}
webertj@15547
  1482
webertj@15547
  1483
lemma "OFCLASS('a::type, type_class)"
webertj@15547
  1484
  refute  -- {* no countermodel exists *}
webertj@15547
  1485
  apply intro_classes
webertj@15547
  1486
done
webertj@15547
  1487
webertj@15547
  1488
lemma "OFCLASS('a::classC, type_class)"
webertj@15547
  1489
  refute  -- {* no countermodel exists *}
webertj@15547
  1490
  apply intro_classes
webertj@15547
  1491
done
webertj@15547
  1492
webertj@15547
  1493
lemma "OFCLASS('a, classB_class)"
webertj@15547
  1494
  refute  -- {* no countermodel exists *}
webertj@15547
  1495
  apply intro_classes
webertj@15547
  1496
  apply simp
webertj@15547
  1497
done
webertj@15547
  1498
webertj@15547
  1499
lemma "OFCLASS('a::type, classC_class)"
webertj@15547
  1500
  refute
webertj@15547
  1501
oops
webertj@15547
  1502
webertj@15547
  1503
text {* Overloading: *}
webertj@15547
  1504
webertj@15547
  1505
consts inverse :: "'a \<Rightarrow> 'a"
webertj@15547
  1506
webertj@15547
  1507
defs (overloaded)
webertj@15547
  1508
  inverse_bool: "inverse (b::bool)   == ~ b"
webertj@15547
  1509
  inverse_set : "inverse (S::'a set) == -S"
webertj@15547
  1510
  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
webertj@15547
  1511
webertj@15547
  1512
lemma "inverse b"
webertj@15547
  1513
  refute
webertj@15547
  1514
oops
webertj@15547
  1515
webertj@15547
  1516
lemma "P (inverse (S::'a set))"
webertj@15547
  1517
  refute
webertj@15547
  1518
oops
webertj@15547
  1519
webertj@15547
  1520
lemma "P (inverse (p::'a\<times>'b))"
webertj@14809
  1521
  refute
webertj@14350
  1522
oops
webertj@14350
  1523
webertj@18774
  1524
refute_params [satsolver="auto"]
webertj@18774
  1525
webertj@14350
  1526
end