24 subsection \<open>Syntax and axiomatic basis\<close> |
24 subsection \<open>Syntax and axiomatic basis\<close> |
25 |
25 |
26 setup Pure_Thy.old_appl_syntax_setup |
26 setup Pure_Thy.old_appl_syntax_setup |
27 |
27 |
28 class "term" |
28 class "term" |
29 default_sort "term" |
29 default_sort \<open>term\<close> |
30 |
30 |
31 typedecl o |
31 typedecl o |
32 |
32 |
33 judgment |
33 judgment |
34 Trueprop :: "o \<Rightarrow> prop" (\<open>(_)\<close> 5) |
34 Trueprop :: \<open>o \<Rightarrow> prop\<close> (\<open>(_)\<close> 5) |
35 |
35 |
36 |
36 |
37 subsubsection \<open>Equality\<close> |
37 subsubsection \<open>Equality\<close> |
38 |
38 |
39 axiomatization |
39 axiomatization |
40 eq :: "['a, 'a] \<Rightarrow> o" (infixl \<open>=\<close> 50) |
40 eq :: \<open>['a, 'a] \<Rightarrow> o\<close> (infixl \<open>=\<close> 50) |
41 where |
41 where |
42 refl: "a = a" and |
42 refl: \<open>a = a\<close> and |
43 subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)" |
43 subst: \<open>a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)\<close> |
44 |
44 |
45 |
45 |
46 subsubsection \<open>Propositional logic\<close> |
46 subsubsection \<open>Propositional logic\<close> |
47 |
47 |
48 axiomatization |
48 axiomatization |
49 False :: o and |
49 False :: \<open>o\<close> and |
50 conj :: "[o, o] => o" (infixr \<open>\<and>\<close> 35) and |
50 conj :: \<open>[o, o] => o\<close> (infixr \<open>\<and>\<close> 35) and |
51 disj :: "[o, o] => o" (infixr \<open>\<or>\<close> 30) and |
51 disj :: \<open>[o, o] => o\<close> (infixr \<open>\<or>\<close> 30) and |
52 imp :: "[o, o] => o" (infixr \<open>\<longrightarrow>\<close> 25) |
52 imp :: \<open>[o, o] => o\<close> (infixr \<open>\<longrightarrow>\<close> 25) |
53 where |
53 where |
54 conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" and |
54 conjI: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close> and |
55 conjunct1: "P \<and> Q \<Longrightarrow> P" and |
55 conjunct1: \<open>P \<and> Q \<Longrightarrow> P\<close> and |
56 conjunct2: "P \<and> Q \<Longrightarrow> Q" and |
56 conjunct2: \<open>P \<and> Q \<Longrightarrow> Q\<close> and |
57 |
57 |
58 disjI1: "P \<Longrightarrow> P \<or> Q" and |
58 disjI1: \<open>P \<Longrightarrow> P \<or> Q\<close> and |
59 disjI2: "Q \<Longrightarrow> P \<or> Q" and |
59 disjI2: \<open>Q \<Longrightarrow> P \<or> Q\<close> and |
60 disjE: "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" and |
60 disjE: \<open>\<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close> and |
61 |
61 |
62 impI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q" and |
62 impI: \<open>(P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q\<close> and |
63 mp: "\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" and |
63 mp: \<open>\<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q\<close> and |
64 |
64 |
65 FalseE: "False \<Longrightarrow> P" |
65 FalseE: \<open>False \<Longrightarrow> P\<close> |
66 |
66 |
67 |
67 |
68 subsubsection \<open>Quantifiers\<close> |
68 subsubsection \<open>Quantifiers\<close> |
69 |
69 |
70 axiomatization |
70 axiomatization |
71 All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<forall>\<close> 10) and |
71 All :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close> (binder \<open>\<forall>\<close> 10) and |
72 Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<exists>\<close> 10) |
72 Ex :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close> (binder \<open>\<exists>\<close> 10) |
73 where |
73 where |
74 allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and |
74 allI: \<open>(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))\<close> and |
75 spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and |
75 spec: \<open>(\<forall>x. P(x)) \<Longrightarrow> P(x)\<close> and |
76 exI: "P(x) \<Longrightarrow> (\<exists>x. P(x))" and |
76 exI: \<open>P(x) \<Longrightarrow> (\<exists>x. P(x))\<close> and |
77 exE: "\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
77 exE: \<open>\<lbrakk>\<exists>x. P(x); \<And>x. P(x) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close> |
78 |
78 |
79 |
79 |
80 subsubsection \<open>Definitions\<close> |
80 subsubsection \<open>Definitions\<close> |
81 |
81 |
82 definition "True \<equiv> False \<longrightarrow> False" |
82 definition \<open>True \<equiv> False \<longrightarrow> False\<close> |
83 |
83 |
84 definition Not (\<open>\<not> _\<close> [40] 40) |
84 definition Not (\<open>\<not> _\<close> [40] 40) |
85 where not_def: "\<not> P \<equiv> P \<longrightarrow> False" |
85 where not_def: \<open>\<not> P \<equiv> P \<longrightarrow> False\<close> |
86 |
86 |
87 definition iff (infixr \<open>\<longleftrightarrow>\<close> 25) |
87 definition iff (infixr \<open>\<longleftrightarrow>\<close> 25) |
88 where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)" |
88 where \<open>P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)\<close> |
89 |
89 |
90 definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<exists>!\<close> 10) |
90 definition Ex1 :: \<open>('a \<Rightarrow> o) \<Rightarrow> o\<close> (binder \<open>\<exists>!\<close> 10) |
91 where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)" |
91 where ex1_def: \<open>\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)\<close> |
92 |
92 |
93 axiomatization where \<comment> \<open>Reflection, admissible\<close> |
93 axiomatization where \<comment> \<open>Reflection, admissible\<close> |
94 eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and |
94 eq_reflection: \<open>(x = y) \<Longrightarrow> (x \<equiv> y)\<close> and |
95 iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)" |
95 iff_reflection: \<open>(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)\<close> |
96 |
96 |
97 abbreviation not_equal :: "['a, 'a] \<Rightarrow> o" (infixl \<open>\<noteq>\<close> 50) |
97 abbreviation not_equal :: \<open>['a, 'a] \<Rightarrow> o\<close> (infixl \<open>\<noteq>\<close> 50) |
98 where "x \<noteq> y \<equiv> \<not> (x = y)" |
98 where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close> |
99 |
99 |
100 |
100 |
101 subsubsection \<open>Old-style ASCII syntax\<close> |
101 subsubsection \<open>Old-style ASCII syntax\<close> |
102 |
102 |
103 notation (ASCII) |
103 notation (ASCII) |
114 |
114 |
115 subsection \<open>Lemmas and proof tools\<close> |
115 subsection \<open>Lemmas and proof tools\<close> |
116 |
116 |
117 lemmas strip = impI allI |
117 lemmas strip = impI allI |
118 |
118 |
119 lemma TrueI: True |
119 lemma TrueI: \<open>True\<close> |
120 unfolding True_def by (rule impI) |
120 unfolding True_def by (rule impI) |
121 |
121 |
122 |
122 |
123 subsubsection \<open>Sequent-style elimination rules for \<open>\<and>\<close> \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close>\<close> |
123 subsubsection \<open>Sequent-style elimination rules for \<open>\<and>\<close> \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close>\<close> |
124 |
124 |
125 lemma conjE: |
125 lemma conjE: |
126 assumes major: "P \<and> Q" |
126 assumes major: \<open>P \<and> Q\<close> |
127 and r: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R" |
127 and r: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close> |
128 shows R |
128 shows \<open>R\<close> |
129 apply (rule r) |
129 apply (rule r) |
130 apply (rule major [THEN conjunct1]) |
130 apply (rule major [THEN conjunct1]) |
131 apply (rule major [THEN conjunct2]) |
131 apply (rule major [THEN conjunct2]) |
132 done |
132 done |
133 |
133 |
134 lemma impE: |
134 lemma impE: |
135 assumes major: "P \<longrightarrow> Q" |
135 assumes major: \<open>P \<longrightarrow> Q\<close> |
136 and P |
136 and \<open>P\<close> |
137 and r: "Q \<Longrightarrow> R" |
137 and r: \<open>Q \<Longrightarrow> R\<close> |
138 shows R |
138 shows \<open>R\<close> |
139 apply (rule r) |
139 apply (rule r) |
140 apply (rule major [THEN mp]) |
140 apply (rule major [THEN mp]) |
141 apply (rule \<open>P\<close>) |
141 apply (rule \<open>P\<close>) |
142 done |
142 done |
143 |
143 |
144 lemma allE: |
144 lemma allE: |
145 assumes major: "\<forall>x. P(x)" |
145 assumes major: \<open>\<forall>x. P(x)\<close> |
146 and r: "P(x) \<Longrightarrow> R" |
146 and r: \<open>P(x) \<Longrightarrow> R\<close> |
147 shows R |
147 shows \<open>R\<close> |
148 apply (rule r) |
148 apply (rule r) |
149 apply (rule major [THEN spec]) |
149 apply (rule major [THEN spec]) |
150 done |
150 done |
151 |
151 |
152 text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close> |
152 text \<open>Duplicates the quantifier; for use with @{ML eresolve_tac}.\<close> |
153 lemma all_dupE: |
153 lemma all_dupE: |
154 assumes major: "\<forall>x. P(x)" |
154 assumes major: \<open>\<forall>x. P(x)\<close> |
155 and r: "\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R" |
155 and r: \<open>\<lbrakk>P(x); \<forall>x. P(x)\<rbrakk> \<Longrightarrow> R\<close> |
156 shows R |
156 shows \<open>R\<close> |
157 apply (rule r) |
157 apply (rule r) |
158 apply (rule major [THEN spec]) |
158 apply (rule major [THEN spec]) |
159 apply (rule major) |
159 apply (rule major) |
160 done |
160 done |
161 |
161 |
162 |
162 |
163 subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close> |
163 subsubsection \<open>Negation rules, which translate between \<open>\<not> P\<close> and \<open>P \<longrightarrow> False\<close>\<close> |
164 |
164 |
165 lemma notI: "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" |
165 lemma notI: \<open>(P \<Longrightarrow> False) \<Longrightarrow> \<not> P\<close> |
166 unfolding not_def by (erule impI) |
166 unfolding not_def by (erule impI) |
167 |
167 |
168 lemma notE: "\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R" |
168 lemma notE: \<open>\<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> R\<close> |
169 unfolding not_def by (erule mp [THEN FalseE]) |
169 unfolding not_def by (erule mp [THEN FalseE]) |
170 |
170 |
171 lemma rev_notE: "\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R" |
171 lemma rev_notE: \<open>\<lbrakk>P; \<not> P\<rbrakk> \<Longrightarrow> R\<close> |
172 by (erule notE) |
172 by (erule notE) |
173 |
173 |
174 text \<open>This is useful with the special implication rules for each kind of \<open>P\<close>.\<close> |
174 text \<open>This is useful with the special implication rules for each kind of \<open>P\<close>.\<close> |
175 lemma not_to_imp: |
175 lemma not_to_imp: |
176 assumes "\<not> P" |
176 assumes \<open>\<not> P\<close> |
177 and r: "P \<longrightarrow> False \<Longrightarrow> Q" |
177 and r: \<open>P \<longrightarrow> False \<Longrightarrow> Q\<close> |
178 shows Q |
178 shows \<open>Q\<close> |
179 apply (rule r) |
179 apply (rule r) |
180 apply (rule impI) |
180 apply (rule impI) |
181 apply (erule notE [OF \<open>\<not> P\<close>]) |
181 apply (erule notE [OF \<open>\<not> P\<close>]) |
182 done |
182 done |
183 |
183 |
184 text \<open> |
184 text \<open> |
185 For substitution into an assumption \<open>P\<close>, reduce \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, substitute into this implication, then apply \<open>impI\<close> to |
185 For substitution into an assumption \<open>P\<close>, reduce \<open>Q\<close> to \<open>P \<longrightarrow> Q\<close>, substitute into this implication, then apply \<open>impI\<close> to |
186 move \<open>P\<close> back into the assumptions. |
186 move \<open>P\<close> back into the assumptions. |
187 \<close> |
187 \<close> |
188 lemma rev_mp: "\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
188 lemma rev_mp: \<open>\<lbrakk>P; P \<longrightarrow> Q\<rbrakk> \<Longrightarrow> Q\<close> |
189 by (erule mp) |
189 by (erule mp) |
190 |
190 |
191 text \<open>Contrapositive of an inference rule.\<close> |
191 text \<open>Contrapositive of an inference rule.\<close> |
192 lemma contrapos: |
192 lemma contrapos: |
193 assumes major: "\<not> Q" |
193 assumes major: \<open>\<not> Q\<close> |
194 and minor: "P \<Longrightarrow> Q" |
194 and minor: \<open>P \<Longrightarrow> Q\<close> |
195 shows "\<not> P" |
195 shows \<open>\<not> P\<close> |
196 apply (rule major [THEN notE, THEN notI]) |
196 apply (rule major [THEN notE, THEN notI]) |
197 apply (erule minor) |
197 apply (erule minor) |
198 done |
198 done |
199 |
199 |
200 |
200 |
212 \<close> |
212 \<close> |
213 |
213 |
214 |
214 |
215 subsection \<open>If-and-only-if\<close> |
215 subsection \<open>If-and-only-if\<close> |
216 |
216 |
217 lemma iffI: "\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q" |
217 lemma iffI: \<open>\<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> Q\<close> |
218 apply (unfold iff_def) |
218 apply (unfold iff_def) |
219 apply (rule conjI) |
219 apply (rule conjI) |
220 apply (erule impI) |
220 apply (erule impI) |
221 apply (erule impI) |
221 apply (erule impI) |
222 done |
222 done |
223 |
223 |
224 lemma iffE: |
224 lemma iffE: |
225 assumes major: "P \<longleftrightarrow> Q" |
225 assumes major: \<open>P \<longleftrightarrow> Q\<close> |
226 and r: "P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R" |
226 and r: \<open>P \<longrightarrow> Q \<Longrightarrow> Q \<longrightarrow> P \<Longrightarrow> R\<close> |
227 shows R |
227 shows \<open>R\<close> |
228 apply (insert major, unfold iff_def) |
228 apply (insert major, unfold iff_def) |
229 apply (erule conjE) |
229 apply (erule conjE) |
230 apply (erule r) |
230 apply (erule r) |
231 apply assumption |
231 apply assumption |
232 done |
232 done |
233 |
233 |
234 |
234 |
235 subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close> |
235 subsubsection \<open>Destruct rules for \<open>\<longleftrightarrow>\<close> similar to Modus Ponens\<close> |
236 |
236 |
237 lemma iffD1: "\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q" |
237 lemma iffD1: \<open>\<lbrakk>P \<longleftrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q\<close> |
238 apply (unfold iff_def) |
238 apply (unfold iff_def) |
239 apply (erule conjunct1 [THEN mp]) |
239 apply (erule conjunct1 [THEN mp]) |
240 apply assumption |
240 apply assumption |
241 done |
241 done |
242 |
242 |
243 lemma iffD2: "\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P" |
243 lemma iffD2: \<open>\<lbrakk>P \<longleftrightarrow> Q; Q\<rbrakk> \<Longrightarrow> P\<close> |
244 apply (unfold iff_def) |
244 apply (unfold iff_def) |
245 apply (erule conjunct2 [THEN mp]) |
245 apply (erule conjunct2 [THEN mp]) |
246 apply assumption |
246 apply assumption |
247 done |
247 done |
248 |
248 |
249 lemma rev_iffD1: "\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
249 lemma rev_iffD1: \<open>\<lbrakk>P; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> Q\<close> |
250 apply (erule iffD1) |
250 apply (erule iffD1) |
251 apply assumption |
251 apply assumption |
252 done |
252 done |
253 |
253 |
254 lemma rev_iffD2: "\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P" |
254 lemma rev_iffD2: \<open>\<lbrakk>Q; P \<longleftrightarrow> Q\<rbrakk> \<Longrightarrow> P\<close> |
255 apply (erule iffD2) |
255 apply (erule iffD2) |
256 apply assumption |
256 apply assumption |
257 done |
257 done |
258 |
258 |
259 lemma iff_refl: "P \<longleftrightarrow> P" |
259 lemma iff_refl: \<open>P \<longleftrightarrow> P\<close> |
260 by (rule iffI) |
260 by (rule iffI) |
261 |
261 |
262 lemma iff_sym: "Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q" |
262 lemma iff_sym: \<open>Q \<longleftrightarrow> P \<Longrightarrow> P \<longleftrightarrow> Q\<close> |
263 apply (erule iffE) |
263 apply (erule iffE) |
264 apply (rule iffI) |
264 apply (rule iffI) |
265 apply (assumption | erule mp)+ |
265 apply (assumption | erule mp)+ |
266 done |
266 done |
267 |
267 |
268 lemma iff_trans: "\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R" |
268 lemma iff_trans: \<open>\<lbrakk>P \<longleftrightarrow> Q; Q \<longleftrightarrow> R\<rbrakk> \<Longrightarrow> P \<longleftrightarrow> R\<close> |
269 apply (rule iffI) |
269 apply (rule iffI) |
270 apply (assumption | erule iffE | erule (1) notE impE)+ |
270 apply (assumption | erule iffE | erule (1) notE impE)+ |
271 done |
271 done |
272 |
272 |
273 |
273 |
313 method_setup iff = |
313 method_setup iff = |
314 \<open>Attrib.thms >> |
314 \<open>Attrib.thms >> |
315 (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close> |
315 (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close> |
316 |
316 |
317 lemma conj_cong: |
317 lemma conj_cong: |
318 assumes "P \<longleftrightarrow> P'" |
318 assumes \<open>P \<longleftrightarrow> P'\<close> |
319 and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
319 and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close> |
320 shows "(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')" |
320 shows \<open>(P \<and> Q) \<longleftrightarrow> (P' \<and> Q')\<close> |
321 apply (insert assms) |
321 apply (insert assms) |
322 apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
322 apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
323 done |
323 done |
324 |
324 |
325 text \<open>Reversed congruence rule! Used in ZF/Order.\<close> |
325 text \<open>Reversed congruence rule! Used in ZF/Order.\<close> |
326 lemma conj_cong2: |
326 lemma conj_cong2: |
327 assumes "P \<longleftrightarrow> P'" |
327 assumes \<open>P \<longleftrightarrow> P'\<close> |
328 and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
328 and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close> |
329 shows "(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')" |
329 shows \<open>(Q \<and> P) \<longleftrightarrow> (Q' \<and> P')\<close> |
330 apply (insert assms) |
330 apply (insert assms) |
331 apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
331 apply (assumption | rule iffI conjI | erule iffE conjE mp | iff assms)+ |
332 done |
332 done |
333 |
333 |
334 lemma disj_cong: |
334 lemma disj_cong: |
335 assumes "P \<longleftrightarrow> P'" and "Q \<longleftrightarrow> Q'" |
335 assumes \<open>P \<longleftrightarrow> P'\<close> and \<open>Q \<longleftrightarrow> Q'\<close> |
336 shows "(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')" |
336 shows \<open>(P \<or> Q) \<longleftrightarrow> (P' \<or> Q')\<close> |
337 apply (insert assms) |
337 apply (insert assms) |
338 apply (erule iffE disjE disjI1 disjI2 | |
338 apply (erule iffE disjE disjI1 disjI2 | |
339 assumption | rule iffI | erule (1) notE impE)+ |
339 assumption | rule iffI | erule (1) notE impE)+ |
340 done |
340 done |
341 |
341 |
342 lemma imp_cong: |
342 lemma imp_cong: |
343 assumes "P \<longleftrightarrow> P'" |
343 assumes \<open>P \<longleftrightarrow> P'\<close> |
344 and "P' \<Longrightarrow> Q \<longleftrightarrow> Q'" |
344 and \<open>P' \<Longrightarrow> Q \<longleftrightarrow> Q'\<close> |
345 shows "(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')" |
345 shows \<open>(P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')\<close> |
346 apply (insert assms) |
346 apply (insert assms) |
347 apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+ |
347 apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | iff assms)+ |
348 done |
348 done |
349 |
349 |
350 lemma iff_cong: "\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')" |
350 lemma iff_cong: \<open>\<lbrakk>P \<longleftrightarrow> P'; Q \<longleftrightarrow> Q'\<rbrakk> \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P' \<longleftrightarrow> Q')\<close> |
351 apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ |
351 apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+ |
352 done |
352 done |
353 |
353 |
354 lemma not_cong: "P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'" |
354 lemma not_cong: \<open>P \<longleftrightarrow> P' \<Longrightarrow> \<not> P \<longleftrightarrow> \<not> P'\<close> |
355 apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ |
355 apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+ |
356 done |
356 done |
357 |
357 |
358 lemma all_cong: |
358 lemma all_cong: |
359 assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
359 assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close> |
360 shows "(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))" |
360 shows \<open>(\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close> |
361 apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+ |
361 apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | iff assms)+ |
362 done |
362 done |
363 |
363 |
364 lemma ex_cong: |
364 lemma ex_cong: |
365 assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
365 assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close> |
366 shows "(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))" |
366 shows \<open>(\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close> |
367 apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+ |
367 apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | iff assms)+ |
368 done |
368 done |
369 |
369 |
370 lemma ex1_cong: |
370 lemma ex1_cong: |
371 assumes "\<And>x. P(x) \<longleftrightarrow> Q(x)" |
371 assumes \<open>\<And>x. P(x) \<longleftrightarrow> Q(x)\<close> |
372 shows "(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))" |
372 shows \<open>(\<exists>!x. P(x)) \<longleftrightarrow> (\<exists>!x. Q(x))\<close> |
373 apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+ |
373 apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | iff assms)+ |
374 done |
374 done |
375 |
375 |
376 |
376 |
377 subsection \<open>Equality rules\<close> |
377 subsection \<open>Equality rules\<close> |
378 |
378 |
379 lemma sym: "a = b \<Longrightarrow> b = a" |
379 lemma sym: \<open>a = b \<Longrightarrow> b = a\<close> |
380 apply (erule subst) |
380 apply (erule subst) |
381 apply (rule refl) |
381 apply (rule refl) |
382 done |
382 done |
383 |
383 |
384 lemma trans: "\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c" |
384 lemma trans: \<open>\<lbrakk>a = b; b = c\<rbrakk> \<Longrightarrow> a = c\<close> |
385 apply (erule subst, assumption) |
385 apply (erule subst, assumption) |
386 done |
386 done |
387 |
387 |
388 lemma not_sym: "b \<noteq> a \<Longrightarrow> a \<noteq> b" |
388 lemma not_sym: \<open>b \<noteq> a \<Longrightarrow> a \<noteq> b\<close> |
389 apply (erule contrapos) |
389 apply (erule contrapos) |
390 apply (erule sym) |
390 apply (erule sym) |
391 done |
391 done |
392 |
392 |
393 text \<open> |
393 text \<open> |
394 Two theorems for rewriting only one instance of a definition: |
394 Two theorems for rewriting only one instance of a definition: |
395 the first for definitions of formulae and the second for terms. |
395 the first for definitions of formulae and the second for terms. |
396 \<close> |
396 \<close> |
397 |
397 |
398 lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B" |
398 lemma def_imp_iff: \<open>(A \<equiv> B) \<Longrightarrow> A \<longleftrightarrow> B\<close> |
399 apply unfold |
399 apply unfold |
400 apply (rule iff_refl) |
400 apply (rule iff_refl) |
401 done |
401 done |
402 |
402 |
403 lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> A = B" |
403 lemma meta_eq_to_obj_eq: \<open>(A \<equiv> B) \<Longrightarrow> A = B\<close> |
404 apply unfold |
404 apply unfold |
405 apply (rule refl) |
405 apply (rule refl) |
406 done |
406 done |
407 |
407 |
408 lemma meta_eq_to_iff: "x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y" |
408 lemma meta_eq_to_iff: \<open>x \<equiv> y \<Longrightarrow> x \<longleftrightarrow> y\<close> |
409 by unfold (rule iff_refl) |
409 by unfold (rule iff_refl) |
410 |
410 |
411 text \<open>Substitution.\<close> |
411 text \<open>Substitution.\<close> |
412 lemma ssubst: "\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)" |
412 lemma ssubst: \<open>\<lbrakk>b = a; P(a)\<rbrakk> \<Longrightarrow> P(b)\<close> |
413 apply (drule sym) |
413 apply (drule sym) |
414 apply (erule (1) subst) |
414 apply (erule (1) subst) |
415 done |
415 done |
416 |
416 |
417 text \<open>A special case of \<open>ex1E\<close> that would otherwise need quantifier |
417 text \<open>A special case of \<open>ex1E\<close> that would otherwise need quantifier |
418 expansion.\<close> |
418 expansion.\<close> |
419 lemma ex1_equalsE: "\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b" |
419 lemma ex1_equalsE: \<open>\<lbrakk>\<exists>!x. P(x); P(a); P(b)\<rbrakk> \<Longrightarrow> a = b\<close> |
420 apply (erule ex1E) |
420 apply (erule ex1E) |
421 apply (rule trans) |
421 apply (rule trans) |
422 apply (rule_tac [2] sym) |
422 apply (rule_tac [2] sym) |
423 apply (assumption | erule spec [THEN mp])+ |
423 apply (assumption | erule spec [THEN mp])+ |
424 done |
424 done |
425 |
425 |
426 |
426 |
427 subsubsection \<open>Polymorphic congruence rules\<close> |
427 subsubsection \<open>Polymorphic congruence rules\<close> |
428 |
428 |
429 lemma subst_context: "a = b \<Longrightarrow> t(a) = t(b)" |
429 lemma subst_context: \<open>a = b \<Longrightarrow> t(a) = t(b)\<close> |
430 apply (erule ssubst) |
430 apply (erule ssubst) |
431 apply (rule refl) |
431 apply (rule refl) |
432 done |
432 done |
433 |
433 |
434 lemma subst_context2: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)" |
434 lemma subst_context2: \<open>\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> t(a,c) = t(b,d)\<close> |
435 apply (erule ssubst)+ |
435 apply (erule ssubst)+ |
436 apply (rule refl) |
436 apply (rule refl) |
437 done |
437 done |
438 |
438 |
439 lemma subst_context3: "\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)" |
439 lemma subst_context3: \<open>\<lbrakk>a = b; c = d; e = f\<rbrakk> \<Longrightarrow> t(a,c,e) = t(b,d,f)\<close> |
440 apply (erule ssubst)+ |
440 apply (erule ssubst)+ |
441 apply (rule refl) |
441 apply (rule refl) |
442 done |
442 done |
443 |
443 |
444 text \<open> |
444 text \<open> |
505 See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
505 See R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
506 (preprint, University of St Andrews, 1991). |
506 (preprint, University of St Andrews, 1991). |
507 \<close> |
507 \<close> |
508 |
508 |
509 lemma conj_impE: |
509 lemma conj_impE: |
510 assumes major: "(P \<and> Q) \<longrightarrow> S" |
510 assumes major: \<open>(P \<and> Q) \<longrightarrow> S\<close> |
511 and r: "P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R" |
511 and r: \<open>P \<longrightarrow> (Q \<longrightarrow> S) \<Longrightarrow> R\<close> |
512 shows R |
512 shows \<open>R\<close> |
513 by (assumption | rule conjI impI major [THEN mp] r)+ |
513 by (assumption | rule conjI impI major [THEN mp] r)+ |
514 |
514 |
515 lemma disj_impE: |
515 lemma disj_impE: |
516 assumes major: "(P \<or> Q) \<longrightarrow> S" |
516 assumes major: \<open>(P \<or> Q) \<longrightarrow> S\<close> |
517 and r: "\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R" |
517 and r: \<open>\<lbrakk>P \<longrightarrow> S; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> R\<close> |
518 shows R |
518 shows \<open>R\<close> |
519 by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ |
519 by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+ |
520 |
520 |
521 text \<open>Simplifies the implication. Classical version is stronger. |
521 text \<open>Simplifies the implication. Classical version is stronger. |
522 Still UNSAFE since Q must be provable -- backtracking needed.\<close> |
522 Still UNSAFE since Q must be provable -- backtracking needed.\<close> |
523 lemma imp_impE: |
523 lemma imp_impE: |
524 assumes major: "(P \<longrightarrow> Q) \<longrightarrow> S" |
524 assumes major: \<open>(P \<longrightarrow> Q) \<longrightarrow> S\<close> |
525 and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q" |
525 and r1: \<open>\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q\<close> |
526 and r2: "S \<Longrightarrow> R" |
526 and r2: \<open>S \<Longrightarrow> R\<close> |
527 shows R |
527 shows \<open>R\<close> |
528 by (assumption | rule impI major [THEN mp] r1 r2)+ |
528 by (assumption | rule impI major [THEN mp] r1 r2)+ |
529 |
529 |
530 text \<open>Simplifies the implication. Classical version is stronger. |
530 text \<open>Simplifies the implication. Classical version is stronger. |
531 Still UNSAFE since ~P must be provable -- backtracking needed.\<close> |
531 Still UNSAFE since ~P must be provable -- backtracking needed.\<close> |
532 lemma not_impE: "\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R" |
532 lemma not_impE: \<open>\<not> P \<longrightarrow> S \<Longrightarrow> (P \<Longrightarrow> False) \<Longrightarrow> (S \<Longrightarrow> R) \<Longrightarrow> R\<close> |
533 apply (drule mp) |
533 apply (drule mp) |
534 apply (rule notI) |
534 apply (rule notI) |
535 apply assumption |
535 apply assumption |
536 apply assumption |
536 apply assumption |
537 done |
537 done |
538 |
538 |
539 text \<open>Simplifies the implication. UNSAFE.\<close> |
539 text \<open>Simplifies the implication. UNSAFE.\<close> |
540 lemma iff_impE: |
540 lemma iff_impE: |
541 assumes major: "(P \<longleftrightarrow> Q) \<longrightarrow> S" |
541 assumes major: \<open>(P \<longleftrightarrow> Q) \<longrightarrow> S\<close> |
542 and r1: "\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q" |
542 and r1: \<open>\<lbrakk>P; Q \<longrightarrow> S\<rbrakk> \<Longrightarrow> Q\<close> |
543 and r2: "\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P" |
543 and r2: \<open>\<lbrakk>Q; P \<longrightarrow> S\<rbrakk> \<Longrightarrow> P\<close> |
544 and r3: "S \<Longrightarrow> R" |
544 and r3: \<open>S \<Longrightarrow> R\<close> |
545 shows R |
545 shows \<open>R\<close> |
546 apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ |
546 apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+ |
547 done |
547 done |
548 |
548 |
549 text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption? |
549 text \<open>What if \<open>(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))\<close> is an assumption? |
550 UNSAFE.\<close> |
550 UNSAFE.\<close> |
551 lemma all_impE: |
551 lemma all_impE: |
552 assumes major: "(\<forall>x. P(x)) \<longrightarrow> S" |
552 assumes major: \<open>(\<forall>x. P(x)) \<longrightarrow> S\<close> |
553 and r1: "\<And>x. P(x)" |
553 and r1: \<open>\<And>x. P(x)\<close> |
554 and r2: "S \<Longrightarrow> R" |
554 and r2: \<open>S \<Longrightarrow> R\<close> |
555 shows R |
555 shows \<open>R\<close> |
556 apply (rule allI impI major [THEN mp] r1 r2)+ |
556 apply (rule allI impI major [THEN mp] r1 r2)+ |
557 done |
557 done |
558 |
558 |
559 text \<open> |
559 text \<open> |
560 Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent |
560 Unsafe: \<open>\<exists>x. P(x)) \<longrightarrow> S\<close> is equivalent |
561 to \<open>\<forall>x. P(x) \<longrightarrow> S\<close>.\<close> |
561 to \<open>\<forall>x. P(x) \<longrightarrow> S\<close>.\<close> |
562 lemma ex_impE: |
562 lemma ex_impE: |
563 assumes major: "(\<exists>x. P(x)) \<longrightarrow> S" |
563 assumes major: \<open>(\<exists>x. P(x)) \<longrightarrow> S\<close> |
564 and r: "P(x) \<longrightarrow> S \<Longrightarrow> R" |
564 and r: \<open>P(x) \<longrightarrow> S \<Longrightarrow> R\<close> |
565 shows R |
565 shows \<open>R\<close> |
566 apply (assumption | rule exI impI major [THEN mp] r)+ |
566 apply (assumption | rule exI impI major [THEN mp] r)+ |
567 done |
567 done |
568 |
568 |
569 text \<open>Courtesy of Krzysztof Grabczewski.\<close> |
569 text \<open>Courtesy of Krzysztof Grabczewski.\<close> |
570 lemma disj_imp_disj: "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S" |
570 lemma disj_imp_disj: \<open>P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> S) \<Longrightarrow> R \<or> S\<close> |
571 apply (erule disjE) |
571 apply (erule disjE) |
572 apply (rule disjI1) apply assumption |
572 apply (rule disjI1) apply assumption |
573 apply (rule disjI2) apply assumption |
573 apply (rule disjI2) apply assumption |
574 done |
574 done |
575 |
575 |
648 Context_Rules.addSWrapper |
648 Context_Rules.addSWrapper |
649 (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) |
649 (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) |
650 \<close> |
650 \<close> |
651 |
651 |
652 |
652 |
653 lemma iff_not_sym: "\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)" |
653 lemma iff_not_sym: \<open>\<not> (Q \<longleftrightarrow> P) \<Longrightarrow> \<not> (P \<longleftrightarrow> Q)\<close> |
654 by iprover |
654 by iprover |
655 |
655 |
656 lemmas [sym] = sym iff_sym not_sym iff_not_sym |
656 lemmas [sym] = sym iff_sym not_sym iff_not_sym |
657 and [Pure.elim?] = iffD1 iffD2 impE |
657 and [Pure.elim?] = iffD1 iffD2 impE |
658 |
658 |
659 |
659 |
660 lemma eq_commute: "a = b \<longleftrightarrow> b = a" |
660 lemma eq_commute: \<open>a = b \<longleftrightarrow> b = a\<close> |
661 apply (rule iffI) |
661 apply (rule iffI) |
662 apply (erule sym)+ |
662 apply (erule sym)+ |
663 done |
663 done |
664 |
664 |
665 |
665 |
666 subsection \<open>Atomizing meta-level rules\<close> |
666 subsection \<open>Atomizing meta-level rules\<close> |
667 |
667 |
668 lemma atomize_all [atomize]: "(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))" |
668 lemma atomize_all [atomize]: \<open>(\<And>x. P(x)) \<equiv> Trueprop (\<forall>x. P(x))\<close> |
669 proof |
669 proof |
670 assume "\<And>x. P(x)" |
670 assume \<open>\<And>x. P(x)\<close> |
671 then show "\<forall>x. P(x)" .. |
671 then show \<open>\<forall>x. P(x)\<close> .. |
672 next |
672 next |
673 assume "\<forall>x. P(x)" |
673 assume \<open>\<forall>x. P(x)\<close> |
674 then show "\<And>x. P(x)" .. |
674 then show \<open>\<And>x. P(x)\<close> .. |
675 qed |
675 qed |
676 |
676 |
677 lemma atomize_imp [atomize]: "(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)" |
677 lemma atomize_imp [atomize]: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop (A \<longrightarrow> B)\<close> |
678 proof |
678 proof |
679 assume "A \<Longrightarrow> B" |
679 assume \<open>A \<Longrightarrow> B\<close> |
680 then show "A \<longrightarrow> B" .. |
680 then show \<open>A \<longrightarrow> B\<close> .. |
681 next |
681 next |
682 assume "A \<longrightarrow> B" and A |
682 assume \<open>A \<longrightarrow> B\<close> and \<open>A\<close> |
683 then show B by (rule mp) |
683 then show \<open>B\<close> by (rule mp) |
684 qed |
684 qed |
685 |
685 |
686 lemma atomize_eq [atomize]: "(x \<equiv> y) \<equiv> Trueprop (x = y)" |
686 lemma atomize_eq [atomize]: \<open>(x \<equiv> y) \<equiv> Trueprop (x = y)\<close> |
687 proof |
687 proof |
688 assume "x \<equiv> y" |
688 assume \<open>x \<equiv> y\<close> |
689 show "x = y" unfolding \<open>x \<equiv> y\<close> by (rule refl) |
689 show \<open>x = y\<close> unfolding \<open>x \<equiv> y\<close> by (rule refl) |
690 next |
690 next |
691 assume "x = y" |
691 assume \<open>x = y\<close> |
692 then show "x \<equiv> y" by (rule eq_reflection) |
692 then show \<open>x \<equiv> y\<close> by (rule eq_reflection) |
693 qed |
693 qed |
694 |
694 |
695 lemma atomize_iff [atomize]: "(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)" |
695 lemma atomize_iff [atomize]: \<open>(A \<equiv> B) \<equiv> Trueprop (A \<longleftrightarrow> B)\<close> |
696 proof |
696 proof |
697 assume "A \<equiv> B" |
697 assume \<open>A \<equiv> B\<close> |
698 show "A \<longleftrightarrow> B" unfolding \<open>A \<equiv> B\<close> by (rule iff_refl) |
698 show \<open>A \<longleftrightarrow> B\<close> unfolding \<open>A \<equiv> B\<close> by (rule iff_refl) |
699 next |
699 next |
700 assume "A \<longleftrightarrow> B" |
700 assume \<open>A \<longleftrightarrow> B\<close> |
701 then show "A \<equiv> B" by (rule iff_reflection) |
701 then show \<open>A \<equiv> B\<close> by (rule iff_reflection) |
702 qed |
702 qed |
703 |
703 |
704 lemma atomize_conj [atomize]: "(A &&& B) \<equiv> Trueprop (A \<and> B)" |
704 lemma atomize_conj [atomize]: \<open>(A &&& B) \<equiv> Trueprop (A \<and> B)\<close> |
705 proof |
705 proof |
706 assume conj: "A &&& B" |
706 assume conj: \<open>A &&& B\<close> |
707 show "A \<and> B" |
707 show \<open>A \<and> B\<close> |
708 proof (rule conjI) |
708 proof (rule conjI) |
709 from conj show A by (rule conjunctionD1) |
709 from conj show \<open>A\<close> by (rule conjunctionD1) |
710 from conj show B by (rule conjunctionD2) |
710 from conj show \<open>B\<close> by (rule conjunctionD2) |
711 qed |
711 qed |
712 next |
712 next |
713 assume conj: "A \<and> B" |
713 assume conj: \<open>A \<and> B\<close> |
714 show "A &&& B" |
714 show \<open>A &&& B\<close> |
715 proof - |
715 proof - |
716 from conj show A .. |
716 from conj show \<open>A\<close> .. |
717 from conj show B .. |
717 from conj show \<open>B\<close> .. |
718 qed |
718 qed |
719 qed |
719 qed |
720 |
720 |
721 lemmas [symmetric, rulify] = atomize_all atomize_imp |
721 lemmas [symmetric, rulify] = atomize_all atomize_imp |
722 and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff |
722 and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff |
723 |
723 |
724 |
724 |
725 subsection \<open>Atomizing elimination rules\<close> |
725 subsection \<open>Atomizing elimination rules\<close> |
726 |
726 |
727 lemma atomize_exL[atomize_elim]: "(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)" |
727 lemma atomize_exL[atomize_elim]: \<open>(\<And>x. P(x) \<Longrightarrow> Q) \<equiv> ((\<exists>x. P(x)) \<Longrightarrow> Q)\<close> |
728 by rule iprover+ |
728 by rule iprover+ |
729 |
729 |
730 lemma atomize_conjL[atomize_elim]: "(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)" |
730 lemma atomize_conjL[atomize_elim]: \<open>(A \<Longrightarrow> B \<Longrightarrow> C) \<equiv> (A \<and> B \<Longrightarrow> C)\<close> |
731 by rule iprover+ |
731 by rule iprover+ |
732 |
732 |
733 lemma atomize_disjL[atomize_elim]: "((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)" |
733 lemma atomize_disjL[atomize_elim]: \<open>((A \<Longrightarrow> C) \<Longrightarrow> (B \<Longrightarrow> C) \<Longrightarrow> C) \<equiv> ((A \<or> B \<Longrightarrow> C) \<Longrightarrow> C)\<close> |
734 by rule iprover+ |
734 by rule iprover+ |
735 |
735 |
736 lemma atomize_elimL[atomize_elim]: "(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop(A)" .. |
736 lemma atomize_elimL[atomize_elim]: \<open>(\<And>B. (A \<Longrightarrow> B) \<Longrightarrow> B) \<equiv> Trueprop(A)\<close> .. |
737 |
737 |
738 |
738 |
739 subsection \<open>Calculational rules\<close> |
739 subsection \<open>Calculational rules\<close> |
740 |
740 |
741 lemma forw_subst: "a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)" |
741 lemma forw_subst: \<open>a = b \<Longrightarrow> P(b) \<Longrightarrow> P(a)\<close> |
742 by (rule ssubst) |
742 by (rule ssubst) |
743 |
743 |
744 lemma back_subst: "P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)" |
744 lemma back_subst: \<open>P(a) \<Longrightarrow> a = b \<Longrightarrow> P(b)\<close> |
745 by (rule subst) |
745 by (rule subst) |
746 |
746 |
747 text \<open> |
747 text \<open> |
748 Note that this list of rules is in reverse order of priorities. |
748 Note that this list of rules is in reverse order of priorities. |
749 \<close> |
749 \<close> |
758 |
758 |
759 subsection \<open>``Let'' declarations\<close> |
759 subsection \<open>``Let'' declarations\<close> |
760 |
760 |
761 nonterminal letbinds and letbind |
761 nonterminal letbinds and letbind |
762 |
762 |
763 definition Let :: "['a::{}, 'a => 'b] \<Rightarrow> ('b::{})" |
763 definition Let :: \<open>['a::{}, 'a => 'b] \<Rightarrow> ('b::{})\<close> |
764 where "Let(s, f) \<equiv> f(s)" |
764 where \<open>Let(s, f) \<equiv> f(s)\<close> |
765 |
765 |
766 syntax |
766 syntax |
767 "_bind" :: "[pttrn, 'a] => letbind" (\<open>(2_ =/ _)\<close> 10) |
767 "_bind" :: \<open>[pttrn, 'a] => letbind\<close> (\<open>(2_ =/ _)\<close> 10) |
768 "" :: "letbind => letbinds" (\<open>_\<close>) |
768 "" :: \<open>letbind => letbinds\<close> (\<open>_\<close>) |
769 "_binds" :: "[letbind, letbinds] => letbinds" (\<open>_;/ _\<close>) |
769 "_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>) |
770 "_Let" :: "[letbinds, 'a] => 'a" (\<open>(let (_)/ in (_))\<close> 10) |
770 "_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(let (_)/ in (_))\<close> 10) |
771 |
771 |
772 translations |
772 translations |
773 "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
773 "_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
774 "let x = a in e" == "CONST Let(a, \<lambda>x. e)" |
774 "let x = a in e" == "CONST Let(a, \<lambda>x. e)" |
775 |
775 |
776 lemma LetI: |
776 lemma LetI: |
777 assumes "\<And>x. x = t \<Longrightarrow> P(u(x))" |
777 assumes \<open>\<And>x. x = t \<Longrightarrow> P(u(x))\<close> |
778 shows "P(let x = t in u(x))" |
778 shows \<open>P(let x = t in u(x))\<close> |
779 apply (unfold Let_def) |
779 apply (unfold Let_def) |
780 apply (rule refl [THEN assms]) |
780 apply (rule refl [THEN assms]) |
781 done |
781 done |
782 |
782 |
783 |
783 |
784 subsection \<open>Intuitionistic simplification rules\<close> |
784 subsection \<open>Intuitionistic simplification rules\<close> |
785 |
785 |
786 lemma conj_simps: |
786 lemma conj_simps: |
787 "P \<and> True \<longleftrightarrow> P" |
787 \<open>P \<and> True \<longleftrightarrow> P\<close> |
788 "True \<and> P \<longleftrightarrow> P" |
788 \<open>True \<and> P \<longleftrightarrow> P\<close> |
789 "P \<and> False \<longleftrightarrow> False" |
789 \<open>P \<and> False \<longleftrightarrow> False\<close> |
790 "False \<and> P \<longleftrightarrow> False" |
790 \<open>False \<and> P \<longleftrightarrow> False\<close> |
791 "P \<and> P \<longleftrightarrow> P" |
791 \<open>P \<and> P \<longleftrightarrow> P\<close> |
792 "P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q" |
792 \<open>P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q\<close> |
793 "P \<and> \<not> P \<longleftrightarrow> False" |
793 \<open>P \<and> \<not> P \<longleftrightarrow> False\<close> |
794 "\<not> P \<and> P \<longleftrightarrow> False" |
794 \<open>\<not> P \<and> P \<longleftrightarrow> False\<close> |
795 "(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)" |
795 \<open>(P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)\<close> |
796 by iprover+ |
796 by iprover+ |
797 |
797 |
798 lemma disj_simps: |
798 lemma disj_simps: |
799 "P \<or> True \<longleftrightarrow> True" |
799 \<open>P \<or> True \<longleftrightarrow> True\<close> |
800 "True \<or> P \<longleftrightarrow> True" |
800 \<open>True \<or> P \<longleftrightarrow> True\<close> |
801 "P \<or> False \<longleftrightarrow> P" |
801 \<open>P \<or> False \<longleftrightarrow> P\<close> |
802 "False \<or> P \<longleftrightarrow> P" |
802 \<open>False \<or> P \<longleftrightarrow> P\<close> |
803 "P \<or> P \<longleftrightarrow> P" |
803 \<open>P \<or> P \<longleftrightarrow> P\<close> |
804 "P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q" |
804 \<open>P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q\<close> |
805 "(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)" |
805 \<open>(P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)\<close> |
806 by iprover+ |
806 by iprover+ |
807 |
807 |
808 lemma not_simps: |
808 lemma not_simps: |
809 "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q" |
809 \<open>\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q\<close> |
810 "\<not> False \<longleftrightarrow> True" |
810 \<open>\<not> False \<longleftrightarrow> True\<close> |
811 "\<not> True \<longleftrightarrow> False" |
811 \<open>\<not> True \<longleftrightarrow> False\<close> |
812 by iprover+ |
812 by iprover+ |
813 |
813 |
814 lemma imp_simps: |
814 lemma imp_simps: |
815 "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P" |
815 \<open>(P \<longrightarrow> False) \<longleftrightarrow> \<not> P\<close> |
816 "(P \<longrightarrow> True) \<longleftrightarrow> True" |
816 \<open>(P \<longrightarrow> True) \<longleftrightarrow> True\<close> |
817 "(False \<longrightarrow> P) \<longleftrightarrow> True" |
817 \<open>(False \<longrightarrow> P) \<longleftrightarrow> True\<close> |
818 "(True \<longrightarrow> P) \<longleftrightarrow> P" |
818 \<open>(True \<longrightarrow> P) \<longleftrightarrow> P\<close> |
819 "(P \<longrightarrow> P) \<longleftrightarrow> True" |
819 \<open>(P \<longrightarrow> P) \<longleftrightarrow> True\<close> |
820 "(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P" |
820 \<open>(P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P\<close> |
821 by iprover+ |
821 by iprover+ |
822 |
822 |
823 lemma iff_simps: |
823 lemma iff_simps: |
824 "(True \<longleftrightarrow> P) \<longleftrightarrow> P" |
824 \<open>(True \<longleftrightarrow> P) \<longleftrightarrow> P\<close> |
825 "(P \<longleftrightarrow> True) \<longleftrightarrow> P" |
825 \<open>(P \<longleftrightarrow> True) \<longleftrightarrow> P\<close> |
826 "(P \<longleftrightarrow> P) \<longleftrightarrow> True" |
826 \<open>(P \<longleftrightarrow> P) \<longleftrightarrow> True\<close> |
827 "(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P" |
827 \<open>(False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P\<close> |
828 "(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P" |
828 \<open>(P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P\<close> |
829 by iprover+ |
829 by iprover+ |
830 |
830 |
831 text \<open>The \<open>x = t\<close> versions are needed for the simplification |
831 text \<open>The \<open>x = t\<close> versions are needed for the simplification |
832 procedures.\<close> |
832 procedures.\<close> |
833 lemma quant_simps: |
833 lemma quant_simps: |
834 "\<And>P. (\<forall>x. P) \<longleftrightarrow> P" |
834 \<open>\<And>P. (\<forall>x. P) \<longleftrightarrow> P\<close> |
835 "(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)" |
835 \<open>(\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)\<close> |
836 "(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)" |
836 \<open>(\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)\<close> |
837 "\<And>P. (\<exists>x. P) \<longleftrightarrow> P" |
837 \<open>\<And>P. (\<exists>x. P) \<longleftrightarrow> P\<close> |
838 "\<exists>x. x = t" |
838 \<open>\<exists>x. x = t\<close> |
839 "\<exists>x. t = x" |
839 \<open>\<exists>x. t = x\<close> |
840 "(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)" |
840 \<open>(\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)\<close> |
841 "(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)" |
841 \<open>(\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)\<close> |
842 by iprover+ |
842 by iprover+ |
843 |
843 |
844 text \<open>These are NOT supplied by default!\<close> |
844 text \<open>These are NOT supplied by default!\<close> |
845 lemma distrib_simps: |
845 lemma distrib_simps: |
846 "P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R" |
846 \<open>P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R\<close> |
847 "(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P" |
847 \<open>(Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P\<close> |
848 "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" |
848 \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close> |
849 by iprover+ |
849 by iprover+ |
850 |
850 |
851 |
851 |
852 subsubsection \<open>Conversion into rewrite rules\<close> |
852 subsubsection \<open>Conversion into rewrite rules\<close> |
853 |
853 |
854 lemma P_iff_F: "\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)" |
854 lemma P_iff_F: \<open>\<not> P \<Longrightarrow> (P \<longleftrightarrow> False)\<close> |
855 by iprover |
855 by iprover |
856 lemma iff_reflection_F: "\<not> P \<Longrightarrow> (P \<equiv> False)" |
856 lemma iff_reflection_F: \<open>\<not> P \<Longrightarrow> (P \<equiv> False)\<close> |
857 by (rule P_iff_F [THEN iff_reflection]) |
857 by (rule P_iff_F [THEN iff_reflection]) |
858 |
858 |
859 lemma P_iff_T: "P \<Longrightarrow> (P \<longleftrightarrow> True)" |
859 lemma P_iff_T: \<open>P \<Longrightarrow> (P \<longleftrightarrow> True)\<close> |
860 by iprover |
860 by iprover |
861 lemma iff_reflection_T: "P \<Longrightarrow> (P \<equiv> True)" |
861 lemma iff_reflection_T: \<open>P \<Longrightarrow> (P \<equiv> True)\<close> |
862 by (rule P_iff_T [THEN iff_reflection]) |
862 by (rule P_iff_T [THEN iff_reflection]) |
863 |
863 |
864 |
864 |
865 subsubsection \<open>More rewrite rules\<close> |
865 subsubsection \<open>More rewrite rules\<close> |
866 |
866 |
867 lemma conj_commute: "P \<and> Q \<longleftrightarrow> Q \<and> P" by iprover |
867 lemma conj_commute: \<open>P \<and> Q \<longleftrightarrow> Q \<and> P\<close> by iprover |
868 lemma conj_left_commute: "P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)" by iprover |
868 lemma conj_left_commute: \<open>P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)\<close> by iprover |
869 lemmas conj_comms = conj_commute conj_left_commute |
869 lemmas conj_comms = conj_commute conj_left_commute |
870 |
870 |
871 lemma disj_commute: "P \<or> Q \<longleftrightarrow> Q \<or> P" by iprover |
871 lemma disj_commute: \<open>P \<or> Q \<longleftrightarrow> Q \<or> P\<close> by iprover |
872 lemma disj_left_commute: "P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)" by iprover |
872 lemma disj_left_commute: \<open>P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)\<close> by iprover |
873 lemmas disj_comms = disj_commute disj_left_commute |
873 lemmas disj_comms = disj_commute disj_left_commute |
874 |
874 |
875 lemma conj_disj_distribL: "P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)" by iprover |
875 lemma conj_disj_distribL: \<open>P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)\<close> by iprover |
876 lemma conj_disj_distribR: "(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)" by iprover |
876 lemma conj_disj_distribR: \<open>(P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)\<close> by iprover |
877 |
877 |
878 lemma disj_conj_distribL: "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)" by iprover |
878 lemma disj_conj_distribL: \<open>P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)\<close> by iprover |
879 lemma disj_conj_distribR: "(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)" by iprover |
879 lemma disj_conj_distribR: \<open>(P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)\<close> by iprover |
880 |
880 |
881 lemma imp_conj_distrib: "(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)" by iprover |
881 lemma imp_conj_distrib: \<open>(P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)\<close> by iprover |
882 lemma imp_conj: "((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))" by iprover |
882 lemma imp_conj: \<open>((P \<and> Q) \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))\<close> by iprover |
883 lemma imp_disj: "(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)" by iprover |
883 lemma imp_disj: \<open>(P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)\<close> by iprover |
884 |
884 |
885 lemma de_Morgan_disj: "(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)" by iprover |
885 lemma de_Morgan_disj: \<open>(\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)\<close> by iprover |
886 |
886 |
887 lemma not_ex: "(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))" by iprover |
887 lemma not_ex: \<open>(\<not> (\<exists>x. P(x))) \<longleftrightarrow> (\<forall>x. \<not> P(x))\<close> by iprover |
888 lemma imp_ex: "((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)" by iprover |
888 lemma imp_ex: \<open>((\<exists>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> Q)\<close> by iprover |
889 |
889 |
890 lemma ex_disj_distrib: "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))" |
890 lemma ex_disj_distrib: \<open>(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> ((\<exists>x. P(x)) \<or> (\<exists>x. Q(x)))\<close> |
891 by iprover |
891 by iprover |
892 |
892 |
893 lemma all_conj_distrib: "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))" |
893 lemma all_conj_distrib: \<open>(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> ((\<forall>x. P(x)) \<and> (\<forall>x. Q(x)))\<close> |
894 by iprover |
894 by iprover |
895 |
895 |
896 end |
896 end |