src/FOL/ex/Intuitionistic.thy
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (21 months ago)
changeset 67087 733017b19de9
parent 62020 5d208fd2507d
child 67443 3abf6a722518
permissions -rw-r--r--
generalized more lemmas
wenzelm@31974
     1
(*  Title:      FOL/ex/Intuitionistic.thy
paulson@14239
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@14239
     3
    Copyright   1991  University of Cambridge
paulson@14239
     4
*)
paulson@14239
     5
wenzelm@60770
     6
section \<open>Intuitionistic First-Order Logic\<close>
paulson@14239
     7
wenzelm@31974
     8
theory Intuitionistic
wenzelm@31974
     9
imports IFOL
wenzelm@31974
    10
begin
paulson@14239
    11
paulson@14239
    12
(*
paulson@14239
    13
Single-step ML commands:
paulson@14239
    14
by (IntPr.step_tac 1)
paulson@14239
    15
by (biresolve_tac safe_brls 1);
paulson@14239
    16
by (biresolve_tac haz_brls 1);
paulson@14239
    17
by (assume_tac 1);
paulson@14239
    18
by (IntPr.safe_tac 1);
paulson@14239
    19
by (IntPr.mp_tac 1);
wenzelm@51798
    20
by (IntPr.fast_tac @{context} 1);
paulson@14239
    21
*)
paulson@14239
    22
paulson@14239
    23
wenzelm@60770
    24
text\<open>Metatheorem (for \emph{propositional} formulae):
paulson@14239
    25
  $P$ is classically provable iff $\neg\neg P$ is intuitionistically provable.
paulson@14239
    26
  Therefore $\neg P$ is classically provable iff it is intuitionistically
paulson@14239
    27
  provable.
paulson@14239
    28
paulson@14239
    29
Proof: Let $Q$ be the conjuction of the propositions $A\vee\neg A$, one for
paulson@14239
    30
each atom $A$ in $P$.  Now $\neg\neg Q$ is intuitionistically provable because
paulson@14239
    31
$\neg\neg(A\vee\neg A)$ is and because double-negation distributes over
paulson@14239
    32
conjunction.  If $P$ is provable classically, then clearly $Q\rightarrow P$ is
paulson@14239
    33
provable intuitionistically, so $\neg\neg(Q\rightarrow P)$ is also provable
paulson@14239
    34
intuitionistically.  The latter is intuitionistically equivalent to $\neg\neg
paulson@14239
    35
Q\rightarrow\neg\neg P$, hence to $\neg\neg P$, since $\neg\neg Q$ is
paulson@14239
    36
intuitionistically provable.  Finally, if $P$ is a negation then $\neg\neg P$
wenzelm@60770
    37
is intuitionstically equivalent to $P$.  [Andy Pitts]\<close>
paulson@14239
    38
wenzelm@61489
    39
lemma "\<not> \<not> (P \<and> Q) \<longleftrightarrow> \<not> \<not> P \<and> \<not> \<not> Q"
wenzelm@61489
    40
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    41
wenzelm@61489
    42
lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longrightarrow> (\<not> P \<longrightarrow> \<not> Q) \<longrightarrow> P)"
wenzelm@61489
    43
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    44
wenzelm@61489
    45
text \<open>Double-negation does NOT distribute over disjunction.\<close>
paulson@14239
    46
wenzelm@61489
    47
lemma "\<not> \<not> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> \<not> P \<longrightarrow> \<not> \<not> Q)"
wenzelm@61489
    48
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    49
wenzelm@61489
    50
lemma "\<not> \<not> \<not> P \<longleftrightarrow> \<not> P"
wenzelm@61489
    51
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    52
wenzelm@61489
    53
lemma "\<not> \<not> ((P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R))"
wenzelm@61489
    54
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    55
wenzelm@61489
    56
lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
wenzelm@61489
    57
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    58
wenzelm@61489
    59
lemma "((P \<longrightarrow> (Q \<or> (Q \<longrightarrow> R))) \<longrightarrow> R) \<longrightarrow> R"
wenzelm@61489
    60
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    61
wenzelm@61489
    62
lemma
wenzelm@61489
    63
  "(((G \<longrightarrow> A) \<longrightarrow> J) \<longrightarrow> D \<longrightarrow> E) \<longrightarrow> (((H \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> C \<longrightarrow> J)
wenzelm@61489
    64
    \<longrightarrow> (A \<longrightarrow> H) \<longrightarrow> F \<longrightarrow> G \<longrightarrow> (((C \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> D) \<longrightarrow> (A \<longrightarrow> C)
wenzelm@61489
    65
    \<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E"
wenzelm@61489
    66
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    67
paulson@14239
    68
wenzelm@61489
    69
subsection \<open>Lemmas for the propositional double-negation translation\<close>
paulson@14239
    70
wenzelm@61489
    71
lemma "P \<longrightarrow> \<not> \<not> P"
wenzelm@61489
    72
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    73
wenzelm@61489
    74
lemma "\<not> \<not> (\<not> \<not> P \<longrightarrow> P)"
wenzelm@61489
    75
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    76
wenzelm@61489
    77
lemma "\<not> \<not> P \<and> \<not> \<not> (P \<longrightarrow> Q) \<longrightarrow> \<not> \<not> Q"
wenzelm@61489
    78
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
    79
paulson@14239
    80
wenzelm@61489
    81
text \<open>The following are classically but not constructively valid.
wenzelm@61489
    82
  The attempt to prove them terminates quickly!\<close>
wenzelm@61489
    83
lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
wenzelm@61489
    84
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
    85
apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
paulson@14239
    86
oops
paulson@14239
    87
wenzelm@61489
    88
lemma "(P \<and> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R) \<or> (Q \<longrightarrow> R)"
wenzelm@61489
    89
apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
    90
apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
paulson@14239
    91
oops
paulson@14239
    92
paulson@14239
    93
wenzelm@61489
    94
subsection \<open>de Bruijn formulae\<close>
paulson@14239
    95
wenzelm@61489
    96
text \<open>de Bruijn formula with three predicates\<close>
wenzelm@61489
    97
lemma
wenzelm@61489
    98
  "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R) \<and>
wenzelm@61489
    99
    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R) \<and>
wenzelm@61489
   100
    ((R \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R) \<longrightarrow> P \<and> Q \<and> R"
wenzelm@61489
   101
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   102
paulson@14239
   103
wenzelm@61489
   104
text \<open>de Bruijn formula with five predicates\<close>
wenzelm@61489
   105
lemma
wenzelm@61489
   106
  "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
wenzelm@61489
   107
    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
wenzelm@61489
   108
    ((R \<longleftrightarrow> S) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
wenzelm@61489
   109
    ((S \<longleftrightarrow> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
wenzelm@61489
   110
    ((T \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T"
wenzelm@61489
   111
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   112
paulson@14239
   113
wenzelm@61489
   114
text \<open>
wenzelm@61489
   115
  Problems from of Sahlin, Franzen and Haridi,
wenzelm@61489
   116
  An Intuitionistic Predicate Logic Theorem Prover.
wenzelm@61489
   117
  J. Logic and Comp. 2 (5), October 1992, 619-656.
wenzelm@61489
   118
\<close>
paulson@14239
   119
wenzelm@60770
   120
text\<open>Problem 1.1\<close>
wenzelm@61489
   121
lemma
wenzelm@61489
   122
  "(\<forall>x. \<exists>y. \<forall>z. p(x) \<and> q(y) \<and> r(z)) \<longleftrightarrow>
wenzelm@61489
   123
    (\<forall>z. \<exists>y. \<forall>x. p(x) \<and> q(y) \<and> r(z))"
wenzelm@62020
   124
  by (tactic \<open>IntPr.best_dup_tac @{context} 1\<close>)  \<comment>\<open>SLOW\<close>
paulson@14239
   125
wenzelm@60770
   126
text\<open>Problem 3.1\<close>
wenzelm@61489
   127
lemma "\<not> (\<exists>x. \<forall>y. mem(y,x) \<longleftrightarrow> \<not> mem(x,x))"
wenzelm@61489
   128
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   129
wenzelm@60770
   130
text\<open>Problem 4.1: hopeless!\<close>
wenzelm@61489
   131
lemma
wenzelm@61489
   132
  "(\<forall>x. p(x) \<longrightarrow> p(h(x)) \<or> p(g(x))) \<and> (\<exists>x. p(x)) \<and> (\<forall>x. \<not> p(h(x)))
wenzelm@61489
   133
    \<longrightarrow> (\<exists>x. p(g(g(g(g(g(x)))))))"
wenzelm@61489
   134
  oops
paulson@14239
   135
paulson@14239
   136
wenzelm@61489
   137
subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
paulson@14239
   138
wenzelm@62020
   139
text\<open>\<open>\<not>\<not>\<close>1\<close>
wenzelm@61489
   140
lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P))"
wenzelm@61489
   141
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   142
wenzelm@62020
   143
text\<open>\<open>\<not>\<not>\<close>2\<close>
wenzelm@61489
   144
lemma "\<not> \<not> (\<not> \<not> P \<longleftrightarrow> P)"
wenzelm@61489
   145
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   146
wenzelm@60770
   147
text\<open>3\<close>
wenzelm@61489
   148
lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
wenzelm@61489
   149
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   150
wenzelm@62020
   151
text\<open>\<open>\<not>\<not>\<close>4\<close>
wenzelm@61489
   152
lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P))"
wenzelm@61489
   153
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   154
wenzelm@62020
   155
text\<open>\<open>\<not>\<not>\<close>5\<close>
wenzelm@61490
   156
lemma "\<not> \<not> ((P \<or> Q \<longrightarrow> P \<or> R) \<longrightarrow> P \<or> (Q \<longrightarrow> R))"
wenzelm@61489
   157
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   158
wenzelm@62020
   159
text\<open>\<open>\<not>\<not>\<close>6\<close>
wenzelm@61489
   160
lemma "\<not> \<not> (P \<or> \<not> P)"
wenzelm@61489
   161
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   162
wenzelm@62020
   163
text\<open>\<open>\<not>\<not>\<close>7\<close>
wenzelm@61489
   164
lemma "\<not> \<not> (P \<or> \<not> \<not> \<not> P)"
wenzelm@61489
   165
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   166
wenzelm@62020
   167
text\<open>\<open>\<not>\<not>\<close>8. Peirce's law\<close>
wenzelm@61489
   168
lemma "\<not> \<not> (((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P)"
wenzelm@61489
   169
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   170
wenzelm@60770
   171
text\<open>9\<close>
wenzelm@61489
   172
lemma "((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
wenzelm@61489
   173
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   174
wenzelm@60770
   175
text\<open>10\<close>
wenzelm@61489
   176
lemma "(Q \<longrightarrow> R) \<longrightarrow> (R \<longrightarrow> P \<and> Q) \<longrightarrow> (P \<longrightarrow> (Q \<or> R)) \<longrightarrow> (P \<longleftrightarrow> Q)"
wenzelm@61489
   177
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   178
paulson@14239
   179
wenzelm@61489
   180
subsection\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
wenzelm@61489
   181
wenzelm@61489
   182
lemma "P \<longleftrightarrow> P"
wenzelm@61489
   183
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   184
wenzelm@62020
   185
text\<open>\<open>\<not>\<not>\<close>12. Dijkstra's law\<close>
wenzelm@61489
   186
lemma "\<not> \<not> (((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R)))"
wenzelm@61489
   187
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   188
wenzelm@61489
   189
lemma "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longrightarrow> \<not> \<not> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
wenzelm@61489
   190
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   191
wenzelm@61489
   192
text\<open>13. Distributive law\<close>
wenzelm@61489
   193
lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
wenzelm@61489
   194
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   195
wenzelm@62020
   196
text\<open>\<open>\<not>\<not>\<close>14\<close>
wenzelm@61489
   197
lemma "\<not> \<not> ((P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P)))"
wenzelm@61489
   198
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   199
wenzelm@62020
   200
text\<open>\<open>\<not>\<not>\<close>15\<close>
wenzelm@61489
   201
lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q))"
wenzelm@61489
   202
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   203
wenzelm@62020
   204
text\<open>\<open>\<not>\<not>\<close>16\<close>
wenzelm@61489
   205
lemma "\<not> \<not> ((P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P))"
wenzelm@61489
   206
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   207
wenzelm@62020
   208
text\<open>\<open>\<not>\<not>\<close>17\<close>
wenzelm@61489
   209
lemma "\<not> \<not> (((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S)))"
wenzelm@61489
   210
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   211
wenzelm@61489
   212
text \<open>Dijkstra's ``Golden Rule''\<close>
wenzelm@61489
   213
lemma "(P \<and> Q) \<longleftrightarrow> P \<longleftrightarrow> Q \<longleftrightarrow> (P \<or> Q)"
wenzelm@61489
   214
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   215
wenzelm@61489
   216
wenzelm@61489
   217
section \<open>Examples with quantifiers\<close>
wenzelm@61489
   218
wenzelm@61489
   219
subsection \<open>The converse is classical in the following implications \dots\<close>
wenzelm@61489
   220
wenzelm@61489
   221
lemma "(\<exists>x. P(x) \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
wenzelm@61489
   222
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   223
wenzelm@61489
   224
lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. P(x) \<and> \<not> Q)"
wenzelm@61489
   225
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   226
wenzelm@61489
   227
lemma "((\<forall>x. \<not> P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. \<not> (P(x) \<or> Q))"
wenzelm@61489
   228
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   229
wenzelm@61489
   230
lemma "(\<forall>x. P(x)) \<or> Q \<longrightarrow> (\<forall>x. P(x) \<or> Q)"
wenzelm@61489
   231
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   232
wenzelm@61489
   233
lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<longrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
wenzelm@61489
   234
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   235
paulson@14239
   236
wenzelm@61489
   237
subsection \<open>The following are not constructively valid!\<close>
wenzelm@61489
   238
text \<open>The attempt to prove them terminates quickly!\<close>
paulson@14239
   239
wenzelm@61489
   240
lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)"
wenzelm@61489
   241
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
   242
  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
wenzelm@61489
   243
  oops
paulson@14239
   244
wenzelm@61489
   245
lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<longrightarrow> (\<exists>x. P \<longrightarrow> Q(x))"
wenzelm@61489
   246
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
   247
  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
wenzelm@61489
   248
  oops
paulson@14239
   249
wenzelm@61489
   250
lemma "(\<forall>x. P(x) \<or> Q) \<longrightarrow> ((\<forall>x. P(x)) \<or> Q)"
wenzelm@61489
   251
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
   252
  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
wenzelm@61489
   253
  oops
paulson@14239
   254
wenzelm@61489
   255
lemma "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"
wenzelm@61489
   256
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
   257
  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
wenzelm@61489
   258
  oops
paulson@14239
   259
wenzelm@61489
   260
text \<open>Classically but not intuitionistically valid.  Proved by a bug in 1986!\<close>
wenzelm@61489
   261
lemma "\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))"
wenzelm@61489
   262
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
wenzelm@62020
   263
  apply (rule asm_rl) \<comment>\<open>Checks that subgoals remain: proof failed.\<close>
wenzelm@61489
   264
  oops
paulson@14239
   265
paulson@14239
   266
wenzelm@61489
   267
subsection \<open>Hard examples with quantifiers\<close>
paulson@14239
   268
wenzelm@61489
   269
text \<open>
wenzelm@61489
   270
  The ones that have not been proved are not known to be valid! Some will
wenzelm@61489
   271
  require quantifier duplication -- not currently available.
wenzelm@61489
   272
\<close>
paulson@14239
   273
wenzelm@62020
   274
text\<open>\<open>\<not>\<not>\<close>18\<close>
wenzelm@61489
   275
lemma "\<not> \<not> (\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x))"
wenzelm@62020
   276
  oops  \<comment> \<open>NOT PROVED\<close>
paulson@14239
   277
wenzelm@62020
   278
text\<open>\<open>\<not>\<not>\<close>19\<close>
wenzelm@61489
   279
lemma "\<not> \<not> (\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x)))"
wenzelm@62020
   280
  oops  \<comment> \<open>NOT PROVED\<close>
paulson@14239
   281
wenzelm@60770
   282
text\<open>20\<close>
wenzelm@61489
   283
lemma
wenzelm@61489
   284
  "(\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y) \<longrightarrow> R(z) \<and> S(w)))
wenzelm@61489
   285
    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
wenzelm@61489
   286
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   287
wenzelm@60770
   288
text\<open>21\<close>
wenzelm@61489
   289
lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> \<not> \<not> (\<exists>x. P \<longleftrightarrow> Q(x))"
wenzelm@62020
   290
  oops \<comment> \<open>NOT PROVED; needs quantifier duplication\<close>
paulson@14239
   291
wenzelm@60770
   292
text\<open>22\<close>
wenzelm@61489
   293
lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
wenzelm@61489
   294
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   295
wenzelm@62020
   296
text\<open>\<open>\<not>\<not>\<close>23\<close>
wenzelm@61489
   297
lemma "\<not> \<not> ((\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x))))"
wenzelm@61489
   298
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   299
wenzelm@60770
   300
text\<open>24\<close>
wenzelm@61489
   301
lemma
wenzelm@61489
   302
  "\<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
wenzelm@61489
   303
    (\<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
wenzelm@61489
   304
    \<longrightarrow> \<not> \<not> (\<exists>x. P(x) \<and> R(x))"
wenzelm@61489
   305
text \<open>
wenzelm@62020
   306
  Not clear why \<open>fast_tac\<close>, \<open>best_tac\<close>, \<open>ASTAR\<close> and
wenzelm@62020
   307
  \<open>ITER_DEEPEN\<close> all take forever.
wenzelm@61489
   308
\<close>
wenzelm@61489
   309
  apply (tactic \<open>IntPr.safe_tac @{context}\<close>)
wenzelm@61489
   310
  apply (erule impE)
wenzelm@61489
   311
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   312
  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
wenzelm@61489
   313
  done
paulson@14239
   314
wenzelm@60770
   315
text\<open>25\<close>
wenzelm@61489
   316
lemma
wenzelm@61489
   317
  "(\<exists>x. P(x)) \<and>
wenzelm@61489
   318
      (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
wenzelm@61489
   319
      (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
wenzelm@61489
   320
      ((\<forall>x. P(x) \<longrightarrow> Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
wenzelm@61489
   321
    \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
wenzelm@61489
   322
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   323
wenzelm@62020
   324
text\<open>\<open>\<not>\<not>\<close>26\<close>
wenzelm@61489
   325
lemma
wenzelm@61489
   326
  "(\<not> \<not> (\<exists>x. p(x)) \<longleftrightarrow> \<not> \<not> (\<exists>x. q(x))) \<and>
wenzelm@61489
   327
    (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
wenzelm@61489
   328
  \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
wenzelm@62020
   329
  oops  \<comment>\<open>NOT PROVED\<close>
paulson@14239
   330
wenzelm@60770
   331
text\<open>27\<close>
wenzelm@61489
   332
lemma
wenzelm@61489
   333
  "(\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
wenzelm@61489
   334
    (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
wenzelm@61489
   335
    (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
wenzelm@61489
   336
    ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
wenzelm@61489
   337
  \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
wenzelm@61489
   338
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   339
wenzelm@62020
   340
text\<open>\<open>\<not>\<not>\<close>28. AMENDED\<close>
wenzelm@61489
   341
lemma
wenzelm@61489
   342
  "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
wenzelm@61489
   343
      (\<not> \<not> (\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
wenzelm@61489
   344
      (\<not> \<not> (\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
wenzelm@61489
   345
    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
wenzelm@61489
   346
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   347
wenzelm@61489
   348
text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
wenzelm@61489
   349
lemma
wenzelm@61489
   350
  "(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
wenzelm@61489
   351
    \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
wenzelm@61489
   352
      (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
wenzelm@61489
   353
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   354
wenzelm@62020
   355
text\<open>\<open>\<not>\<not>\<close>30\<close>
wenzelm@61489
   356
lemma
wenzelm@61489
   357
  "(\<forall>x. (P(x) \<or> Q(x)) \<longrightarrow> \<not> R(x)) \<and>
wenzelm@61489
   358
      (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
wenzelm@61489
   359
    \<longrightarrow> (\<forall>x. \<not> \<not> S(x))"
wenzelm@61489
   360
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   361
wenzelm@60770
   362
text\<open>31\<close>
wenzelm@61489
   363
lemma
wenzelm@61489
   364
  "\<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
wenzelm@61489
   365
      (\<exists>x. L(x) \<and> P(x)) \<and>
wenzelm@61489
   366
      (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
wenzelm@61489
   367
  \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
wenzelm@61489
   368
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   369
wenzelm@60770
   370
text\<open>32\<close>
wenzelm@61489
   371
lemma
wenzelm@61489
   372
  "(\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
wenzelm@61489
   373
    (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
wenzelm@61489
   374
    (\<forall>x. M(x) \<longrightarrow> R(x))
wenzelm@61489
   375
  \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
wenzelm@61489
   376
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   377
wenzelm@62020
   378
text\<open>\<open>\<not>\<not>\<close>33\<close>
wenzelm@61489
   379
lemma
wenzelm@61489
   380
  "(\<forall>x. \<not> \<not> (P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c))) \<longleftrightarrow>
wenzelm@61489
   381
    (\<forall>x. \<not> \<not> ((\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c))))"
wenzelm@61489
   382
  apply (tactic \<open>IntPr.best_tac @{context} 1\<close>)
wenzelm@61489
   383
  done
paulson@14239
   384
paulson@14239
   385
wenzelm@60770
   386
text\<open>36\<close>
wenzelm@61489
   387
lemma
wenzelm@61489
   388
  "(\<forall>x. \<exists>y. J(x,y)) \<and>
wenzelm@61489
   389
    (\<forall>x. \<exists>y. G(x,y)) \<and>
wenzelm@61489
   390
    (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow> (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
wenzelm@61489
   391
  \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))"
wenzelm@61489
   392
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   393
wenzelm@60770
   394
text\<open>37\<close>
wenzelm@61489
   395
lemma
wenzelm@61489
   396
  "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
wenzelm@61489
   397
      \<not> \<not> (P(x,z) \<longrightarrow> P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
wenzelm@61489
   398
        (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
wenzelm@61489
   399
        (\<not> \<not> (\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
wenzelm@61489
   400
    \<longrightarrow> \<not> \<not> (\<forall>x. \<exists>y. R(x,y))"
wenzelm@62020
   401
  oops  \<comment>\<open>NOT PROVED\<close>
paulson@14239
   402
wenzelm@60770
   403
text\<open>39\<close>
wenzelm@61489
   404
lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
wenzelm@61489
   405
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   406
wenzelm@61489
   407
text\<open>40. AMENDED\<close>
wenzelm@61489
   408
lemma
wenzelm@61489
   409
  "(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
wenzelm@61489
   410
    \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
wenzelm@61489
   411
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   412
wenzelm@60770
   413
text\<open>44\<close>
wenzelm@61489
   414
lemma
wenzelm@61489
   415
  "(\<forall>x. f(x) \<longrightarrow>
wenzelm@61489
   416
    (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
wenzelm@61489
   417
    (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
wenzelm@61489
   418
    \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))"
wenzelm@61489
   419
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   420
wenzelm@60770
   421
text\<open>48\<close>
wenzelm@61489
   422
lemma "(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
wenzelm@61489
   423
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   424
wenzelm@60770
   425
text\<open>51\<close>
wenzelm@61489
   426
lemma
wenzelm@61489
   427
  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
wenzelm@61489
   428
    (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)"
wenzelm@61489
   429
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   430
wenzelm@60770
   431
text\<open>52\<close>
wenzelm@61489
   432
text \<open>Almost the same as 51.\<close>
wenzelm@61489
   433
lemma
wenzelm@61489
   434
  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
wenzelm@61489
   435
    (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
wenzelm@61489
   436
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   437
wenzelm@60770
   438
text\<open>56\<close>
wenzelm@61489
   439
lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
wenzelm@61489
   440
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   441
wenzelm@60770
   442
text\<open>57\<close>
wenzelm@61489
   443
lemma
wenzelm@61489
   444
  "P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
wenzelm@61489
   445
    (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))"
wenzelm@61489
   446
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   447
wenzelm@60770
   448
text\<open>60\<close>
wenzelm@61489
   449
lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
wenzelm@61489
   450
  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
paulson@14239
   451
paulson@14239
   452
end