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