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