30 val eq_reflection = thm "eq_reflection"; |
30 val eq_reflection = thm "eq_reflection"; |
31 val iff_reflection = thm "iff_reflection"; |
31 val iff_reflection = thm "iff_reflection"; |
32 |
32 |
33 |
33 |
34 |
34 |
35 qed_goalw "TrueI" (the_context ()) [True_def] "True" |
35 Goalw [True_def] "True"; |
36 (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); |
36 by (REPEAT (ares_tac [impI] 1)) ; |
|
37 qed "TrueI"; |
37 |
38 |
38 (*** Sequent-style elimination rules for & --> and ALL ***) |
39 (*** Sequent-style elimination rules for & --> and ALL ***) |
39 |
40 |
40 qed_goal "conjE" (the_context ()) |
41 val major::prems = Goal |
41 "[| P&Q; [| P; Q |] ==> R |] ==> R" |
42 "[| P&Q; [| P; Q |] ==> R |] ==> R"; |
42 (fn prems=> |
43 by (resolve_tac prems 1); |
43 [ (REPEAT (resolve_tac prems 1 |
44 by (rtac (major RS conjunct1) 1); |
44 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN |
45 by (rtac (major RS conjunct2) 1); |
45 resolve_tac prems 1))) ]); |
46 qed "conjE"; |
46 |
47 |
47 qed_goal "impE" (the_context ()) |
48 val major::prems = Goal |
48 "[| P-->Q; P; Q ==> R |] ==> R" |
49 "[| P-->Q; P; Q ==> R |] ==> R"; |
49 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
50 by (resolve_tac prems 1); |
50 |
51 by (rtac (major RS mp) 1); |
51 qed_goal "allE" (the_context ()) |
52 by (resolve_tac prems 1); |
52 "[| ALL x. P(x); P(x) ==> R |] ==> R" |
53 qed "impE"; |
53 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
54 |
|
55 val major::prems = Goal |
|
56 "[| ALL x. P(x); P(x) ==> R |] ==> R"; |
|
57 by (resolve_tac prems 1); |
|
58 by (rtac (major RS spec) 1); |
|
59 qed "allE"; |
54 |
60 |
55 (*Duplicates the quantifier; for use with eresolve_tac*) |
61 (*Duplicates the quantifier; for use with eresolve_tac*) |
56 qed_goal "all_dupE" (the_context ()) |
62 val major::prems = Goal |
57 "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \ |
63 "[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R \ |
58 \ |] ==> R" |
64 \ |] ==> R"; |
59 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
65 by (resolve_tac prems 1); |
|
66 by (rtac (major RS spec) 1); |
|
67 by (rtac major 1); |
|
68 qed "all_dupE"; |
60 |
69 |
61 |
70 |
62 (*** Negation rules, which translate between ~P and P-->False ***) |
71 (*** Negation rules, which translate between ~P and P-->False ***) |
63 |
72 |
64 qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P" |
73 val prems = Goalw [not_def] "(P ==> False) ==> ~P"; |
65 (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); |
74 by (REPEAT (ares_tac (prems@[impI]) 1)) ; |
66 |
75 qed "notI"; |
67 qed_goalw "notE" (the_context ()) [not_def] "[| ~P; P |] ==> R" |
76 |
68 (fn prems=> |
77 Goalw [not_def] "[| ~P; P |] ==> R"; |
69 [ (resolve_tac [mp RS FalseE] 1), |
78 by (etac (mp RS FalseE) 1); |
70 (REPEAT (resolve_tac prems 1)) ]); |
79 by (assume_tac 1); |
71 |
80 qed "notE"; |
72 qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R" |
81 |
73 (fn _ => [REPEAT (ares_tac [notE] 1)]); |
82 Goal "[| P; ~P |] ==> R"; |
|
83 by (etac notE 1); |
|
84 by (assume_tac 1); |
|
85 qed "rev_notE"; |
74 |
86 |
75 (*This is useful with the special implication rules for each kind of P. *) |
87 (*This is useful with the special implication rules for each kind of P. *) |
76 qed_goal "not_to_imp" (the_context ()) |
88 val prems = Goal |
77 "[| ~P; (P-->False) ==> Q |] ==> Q" |
89 "[| ~P; (P-->False) ==> Q |] ==> Q"; |
78 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
90 by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ; |
|
91 qed "not_to_imp"; |
79 |
92 |
80 (* For substitution into an assumption P, reduce Q to P-->Q, substitute into |
93 (* For substitution into an assumption P, reduce Q to P-->Q, substitute into |
81 this implication, then apply impI to move P back into the assumptions. |
94 this implication, then apply impI to move P back into the assumptions. |
82 To specify P use something like |
95 To specify P use something like |
83 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
96 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
84 qed_goal "rev_mp" (the_context ()) "[| P; P --> Q |] ==> Q" |
97 Goal "[| P; P --> Q |] ==> Q"; |
85 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
98 by (etac mp 1); |
|
99 by (assume_tac 1); |
|
100 qed "rev_mp"; |
86 |
101 |
87 (*Contrapositive of an inference rule*) |
102 (*Contrapositive of an inference rule*) |
88 qed_goal "contrapos" (the_context ()) "[| ~Q; P==>Q |] ==> ~P" |
103 val [major,minor]= Goal "[| ~Q; P==>Q |] ==> ~P"; |
89 (fn [major,minor]=> |
104 by (rtac (major RS notE RS notI) 1); |
90 [ (rtac (major RS notE RS notI) 1), |
105 by (etac minor 1) ; |
91 (etac minor 1) ]); |
106 qed "contrapos"; |
92 |
107 |
93 |
108 |
94 (*** Modus Ponens Tactics ***) |
109 (*** Modus Ponens Tactics ***) |
95 |
110 |
96 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
111 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
100 fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; |
115 fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; |
101 |
116 |
102 |
117 |
103 (*** If-and-only-if ***) |
118 (*** If-and-only-if ***) |
104 |
119 |
105 qed_goalw "iffI" (the_context ()) [iff_def] |
120 val prems = Goalw [iff_def] |
106 "[| P ==> Q; Q ==> P |] ==> P<->Q" |
121 "[| P ==> Q; Q ==> P |] ==> P<->Q"; |
107 (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); |
122 by (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ; |
|
123 qed "iffI"; |
108 |
124 |
109 |
125 |
110 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
126 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
111 qed_goalw "iffE" (the_context ()) [iff_def] |
127 val prems = Goalw [iff_def] |
112 "[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R" |
128 "[| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R"; |
113 (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); |
129 by (rtac conjE 1); |
|
130 by (REPEAT (ares_tac prems 1)) ; |
|
131 qed "iffE"; |
114 |
132 |
115 (* Destruct rules for <-> similar to Modus Ponens *) |
133 (* Destruct rules for <-> similar to Modus Ponens *) |
116 |
134 |
117 qed_goalw "iffD1" (the_context ()) [iff_def] "[| P <-> Q; P |] ==> Q" |
135 Goalw [iff_def] "[| P <-> Q; P |] ==> Q"; |
118 (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
136 by (etac (conjunct1 RS mp) 1); |
119 |
137 by (assume_tac 1); |
120 qed_goalw "iffD2" (the_context ()) [iff_def] "[| P <-> Q; Q |] ==> P" |
138 qed "iffD1"; |
121 (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
139 |
122 |
140 val prems = Goalw [iff_def] "[| P <-> Q; Q |] ==> P"; |
123 qed_goal "rev_iffD1" (the_context ()) "!!P. [| P; P <-> Q |] ==> Q" |
141 by (etac (conjunct2 RS mp) 1); |
124 (fn _ => [etac iffD1 1, assume_tac 1]); |
142 by (assume_tac 1); |
125 |
143 qed "iffD2"; |
126 qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P <-> Q |] ==> P" |
144 |
127 (fn _ => [etac iffD2 1, assume_tac 1]); |
145 Goal "[| P; P <-> Q |] ==> Q"; |
128 |
146 by (etac iffD1 1); |
129 qed_goal "iff_refl" (the_context ()) "P <-> P" |
147 by (assume_tac 1); |
130 (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); |
148 qed "rev_iffD1"; |
131 |
149 |
132 qed_goal "iff_sym" (the_context ()) "Q <-> P ==> P <-> Q" |
150 Goal "[| Q; P <-> Q |] ==> P"; |
133 (fn [major] => |
151 by (etac iffD2 1); |
134 [ (rtac (major RS iffE) 1), |
152 by (assume_tac 1); |
135 (rtac iffI 1), |
153 qed "rev_iffD2"; |
136 (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); |
154 |
137 |
155 Goal "P <-> P"; |
138 qed_goal "iff_trans" (the_context ()) |
156 by (REPEAT (ares_tac [iffI] 1)) ; |
139 "!!P Q R. [| P <-> Q; Q<-> R |] ==> P <-> R" |
157 qed "iff_refl"; |
140 (fn _ => |
158 |
141 [ (rtac iffI 1), |
159 Goal "Q <-> P ==> P <-> Q"; |
142 (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); |
160 by (etac iffE 1); |
|
161 by (rtac iffI 1); |
|
162 by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ; |
|
163 qed "iff_sym"; |
|
164 |
|
165 Goal "[| P <-> Q; Q<-> R |] ==> P <-> R"; |
|
166 by (rtac iffI 1); |
|
167 by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ; |
|
168 qed "iff_trans"; |
143 |
169 |
144 |
170 |
145 (*** Unique existence. NOTE THAT the following 2 quantifications |
171 (*** Unique existence. NOTE THAT the following 2 quantifications |
146 EX!x such that [EX!y such that P(x,y)] (sequential) |
172 EX!x such that [EX!y such that P(x,y)] (sequential) |
147 EX!x,y such that P(x,y) (simultaneous) |
173 EX!x,y such that P(x,y) (simultaneous) |
148 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
174 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
149 ***) |
175 ***) |
150 |
176 |
151 qed_goalw "ex1I" (the_context ()) [ex1_def] |
177 val prems = Goalw [ex1_def] |
152 "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)" |
178 "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"; |
153 (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); |
179 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; |
|
180 qed "ex1I"; |
154 |
181 |
155 (*Sometimes easier to use: the premises have no shared variables. Safe!*) |
182 (*Sometimes easier to use: the premises have no shared variables. Safe!*) |
156 qed_goal "ex_ex1I" (the_context ()) |
183 val [ex,eq] = Goal |
157 "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)" |
184 "[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"; |
158 (fn [ex,eq] => [ (rtac (ex RS exE) 1), |
185 by (rtac (ex RS exE) 1); |
159 (REPEAT (ares_tac [ex1I,eq] 1)) ]); |
186 by (REPEAT (ares_tac [ex1I,eq] 1)) ; |
160 |
187 qed "ex_ex1I"; |
161 qed_goalw "ex1E" (the_context ()) [ex1_def] |
188 |
162 "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R" |
189 val prems = Goalw [ex1_def] |
163 (fn prems => |
190 "[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"; |
164 [ (cut_facts_tac prems 1), |
191 by (cut_facts_tac prems 1); |
165 (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); |
192 by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ; |
|
193 qed "ex1E"; |
166 |
194 |
167 |
195 |
168 (*** <-> congruence rules for simplification ***) |
196 (*** <-> congruence rules for simplification ***) |
169 |
197 |
170 (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
198 (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
171 fun iff_tac prems i = |
199 fun iff_tac prems i = |
172 resolve_tac (prems RL [iffE]) i THEN |
200 resolve_tac (prems RL [iffE]) i THEN |
173 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
201 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
174 |
202 |
175 qed_goal "conj_cong" (the_context ()) |
203 val prems = Goal |
176 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')" |
204 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')"; |
177 (fn prems => |
205 by (cut_facts_tac prems 1); |
178 [ (cut_facts_tac prems 1), |
206 by (REPEAT (ares_tac [iffI,conjI] 1 |
179 (REPEAT (ares_tac [iffI,conjI] 1 |
207 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
180 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
208 ORELSE iff_tac prems 1)) ; |
181 ORELSE iff_tac prems 1)) ]); |
209 qed "conj_cong"; |
182 |
210 |
183 (*Reversed congruence rule! Used in ZF/Order*) |
211 (*Reversed congruence rule! Used in ZF/Order*) |
184 qed_goal "conj_cong2" (the_context ()) |
212 val prems = Goal |
185 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')" |
213 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"; |
186 (fn prems => |
214 by (cut_facts_tac prems 1); |
187 [ (cut_facts_tac prems 1), |
215 by (REPEAT (ares_tac [iffI,conjI] 1 |
188 (REPEAT (ares_tac [iffI,conjI] 1 |
216 ORELSE eresolve_tac [iffE,conjE,mp] 1 ORELSE iff_tac prems 1)) ; |
189 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
217 qed "conj_cong2"; |
190 ORELSE iff_tac prems 1)) ]); |
218 |
191 |
219 val prems = Goal |
192 qed_goal "disj_cong" (the_context ()) |
220 "[| P <-> P'; Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"; |
193 "[| P <-> P'; Q <-> Q' |] ==> (P|Q) <-> (P'|Q')" |
221 by (cut_facts_tac prems 1); |
194 (fn prems => |
222 by (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
195 [ (cut_facts_tac prems 1), |
223 ORELSE ares_tac [iffI] 1 ORELSE mp_tac 1)) ; |
196 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
224 qed "disj_cong"; |
197 ORELSE ares_tac [iffI] 1 |
225 |
198 ORELSE mp_tac 1)) ]); |
226 val prems = Goal |
199 |
227 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')"; |
200 qed_goal "imp_cong" (the_context ()) |
228 by (cut_facts_tac prems 1); |
201 "[| P <-> P'; P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')" |
229 by (REPEAT (ares_tac [iffI,impI] 1 |
202 (fn prems => |
230 ORELSE etac iffE 1 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ; |
203 [ (cut_facts_tac prems 1), |
231 qed "imp_cong"; |
204 (REPEAT (ares_tac [iffI,impI] 1 |
232 |
205 ORELSE etac iffE 1 |
233 val prems = Goal |
206 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
234 "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"; |
207 |
235 by (cut_facts_tac prems 1); |
208 qed_goal "iff_cong" (the_context ()) |
236 by (REPEAT (etac iffE 1 ORELSE ares_tac [iffI] 1 ORELSE mp_tac 1)) ; |
209 "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" |
237 qed "iff_cong"; |
210 (fn prems => |
238 |
211 [ (cut_facts_tac prems 1), |
239 val prems = Goal |
212 (REPEAT (etac iffE 1 |
240 "P <-> P' ==> ~P <-> ~P'"; |
213 ORELSE ares_tac [iffI] 1 |
241 by (cut_facts_tac prems 1); |
214 ORELSE mp_tac 1)) ]); |
242 by (REPEAT (ares_tac [iffI,notI] 1 |
215 |
243 ORELSE mp_tac 1 ORELSE eresolve_tac [iffE,notE] 1)) ; |
216 qed_goal "not_cong" (the_context ()) |
244 qed "not_cong"; |
217 "P <-> P' ==> ~P <-> ~P'" |
245 |
218 (fn prems => |
246 val prems = Goal |
219 [ (cut_facts_tac prems 1), |
247 "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"; |
220 (REPEAT (ares_tac [iffI,notI] 1 |
248 by (REPEAT (ares_tac [iffI,allI] 1 |
221 ORELSE mp_tac 1 |
249 ORELSE mp_tac 1 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ; |
222 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
250 qed "all_cong"; |
223 |
251 |
224 qed_goal "all_cong" (the_context ()) |
252 val prems = Goal |
225 "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))" |
253 "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"; |
226 (fn prems => |
254 by (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
227 [ (REPEAT (ares_tac [iffI,allI] 1 |
255 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ; |
228 ORELSE mp_tac 1 |
256 qed "ex_cong"; |
229 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); |
257 |
230 |
258 val prems = Goal |
231 qed_goal "ex_cong" (the_context ()) |
259 "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"; |
232 "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))" |
260 by (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 |
233 (fn prems => |
261 ORELSE ares_tac [iffI,ex1I] 1 ORELSE mp_tac 1 |
234 [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
262 ORELSE iff_tac prems 1)) ; |
235 ORELSE mp_tac 1 |
263 qed "ex1_cong"; |
236 ORELSE iff_tac prems 1)) ]); |
|
237 |
|
238 qed_goal "ex1_cong" (the_context ()) |
|
239 "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))" |
|
240 (fn prems => |
|
241 [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 |
|
242 ORELSE mp_tac 1 |
|
243 ORELSE iff_tac prems 1)) ]); |
|
244 |
264 |
245 (*** Equality rules ***) |
265 (*** Equality rules ***) |
246 |
266 |
247 qed_goal "sym" (the_context ()) "a=b ==> b=a" |
267 Goal "a=b ==> b=a"; |
248 (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); |
268 by (etac subst 1); |
249 |
269 by (rtac refl 1) ; |
250 qed_goal "trans" (the_context ()) "[| a=b; b=c |] ==> a=c" |
270 qed "sym"; |
251 (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); |
271 |
|
272 Goal "[| a=b; b=c |] ==> a=c"; |
|
273 by (etac subst 1 THEN assume_tac 1) ; |
|
274 qed "trans"; |
252 |
275 |
253 (** ~ b=a ==> ~ a=b **) |
276 (** ~ b=a ==> ~ a=b **) |
254 bind_thm ("not_sym", hd (compose(sym,2,contrapos))); |
277 bind_thm ("not_sym", hd (compose(sym,2,contrapos))); |
255 |
278 |
256 |
279 |
257 (* Two theorms for rewriting only one instance of a definition: |
280 (* Two theorms for rewriting only one instance of a definition: |
258 the first for definitions of formulae and the second for terms *) |
281 the first for definitions of formulae and the second for terms *) |
259 |
282 |
260 val prems = goal (the_context ()) "(A == B) ==> A <-> B"; |
283 val prems = goal (the_context()) "(A == B) ==> A <-> B"; |
261 by (rewrite_goals_tac prems); |
284 by (rewrite_goals_tac prems); |
262 by (rtac iff_refl 1); |
285 by (rtac iff_refl 1); |
263 qed "def_imp_iff"; |
286 qed "def_imp_iff"; |
264 |
287 |
265 val prems = goal (the_context ()) "(A == B) ==> A = B"; |
288 val prems = goal (the_context()) "(A == B) ==> A = B"; |
266 by (rewrite_goals_tac prems); |
289 by (rewrite_goals_tac prems); |
267 by (rtac refl 1); |
290 by (rtac refl 1); |
268 qed "meta_eq_to_obj_eq"; |
291 qed "meta_eq_to_obj_eq"; |
269 |
292 |
270 |
293 |
277 let val th' = th RS meta_eq_to_obj_eq handle THM _ => th |
300 let val th' = th RS meta_eq_to_obj_eq handle THM _ => th |
278 in CHANGED_GOAL (rtac (th' RS ssubst)) |
301 in CHANGED_GOAL (rtac (th' RS ssubst)) |
279 end; |
302 end; |
280 |
303 |
281 (*A special case of ex1E that would otherwise need quantifier expansion*) |
304 (*A special case of ex1E that would otherwise need quantifier expansion*) |
282 qed_goal "ex1_equalsE" (the_context ()) |
305 val prems = Goal |
283 "[| EX! x. P(x); P(a); P(b) |] ==> a=b" |
306 "[| EX! x. P(x); P(a); P(b) |] ==> a=b"; |
284 (fn prems => |
307 by (cut_facts_tac prems 1); |
285 [ (cut_facts_tac prems 1), |
308 by (etac ex1E 1); |
286 (etac ex1E 1), |
309 by (rtac trans 1); |
287 (rtac trans 1), |
310 by (rtac sym 2); |
288 (rtac sym 2), |
311 by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ; |
289 (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); |
312 qed "ex1_equalsE"; |
290 |
313 |
291 (** Polymorphic congruence rules **) |
314 (** Polymorphic congruence rules **) |
292 |
315 |
293 qed_goal "subst_context" (the_context ()) |
316 Goal "[| a=b |] ==> t(a)=t(b)"; |
294 "[| a=b |] ==> t(a)=t(b)" |
317 by (etac ssubst 1); |
295 (fn prems=> |
318 by (rtac refl 1) ; |
296 [ (resolve_tac (prems RL [ssubst]) 1), |
319 qed "subst_context"; |
297 (rtac refl 1) ]); |
320 |
298 |
321 Goal "[| a=b; c=d |] ==> t(a,c)=t(b,d)"; |
299 qed_goal "subst_context2" (the_context ()) |
322 by (REPEAT (etac ssubst 1)); |
300 "[| a=b; c=d |] ==> t(a,c)=t(b,d)" |
323 by (rtac refl 1) ; |
301 (fn prems=> |
324 qed "subst_context2"; |
302 [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); |
325 |
303 |
326 Goal "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)"; |
304 qed_goal "subst_context3" (the_context ()) |
327 by (REPEAT (etac ssubst 1)); |
305 "[| a=b; c=d; e=f |] ==> t(a,c,e)=t(b,d,f)" |
328 by (rtac refl 1) ; |
306 (fn prems=> |
329 qed "subst_context3"; |
307 [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); |
|
308 |
330 |
309 (*Useful with eresolve_tac for proving equalties from known equalities. |
331 (*Useful with eresolve_tac for proving equalties from known equalities. |
310 a = b |
332 a = b |
311 | | |
333 | | |
312 c = d *) |
334 c = d *) |
313 qed_goal "box_equals" (the_context ()) |
335 Goal "[| a=b; a=c; b=d |] ==> c=d"; |
314 "[| a=b; a=c; b=d |] ==> c=d" |
336 by (rtac trans 1); |
315 (fn prems=> |
337 by (rtac trans 1); |
316 [ (rtac trans 1), |
338 by (rtac sym 1); |
317 (rtac trans 1), |
339 by (REPEAT (assume_tac 1)); |
318 (rtac sym 1), |
340 qed "box_equals"; |
319 (REPEAT (resolve_tac prems 1)) ]); |
|
320 |
341 |
321 (*Dual of box_equals: for proving equalities backwards*) |
342 (*Dual of box_equals: for proving equalities backwards*) |
322 qed_goal "simp_equals" (the_context ()) |
343 Goal "[| a=c; b=d; c=d |] ==> a=b"; |
323 "[| a=c; b=d; c=d |] ==> a=b" |
344 by (rtac trans 1); |
324 (fn prems=> |
345 by (rtac trans 1); |
325 [ (rtac trans 1), |
346 by (REPEAT (assume_tac 1)); |
326 (rtac trans 1), |
347 by (etac sym 1); |
327 (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); |
348 qed "simp_equals"; |
328 |
349 |
329 (** Congruence rules for predicate letters **) |
350 (** Congruence rules for predicate letters **) |
330 |
351 |
331 qed_goal "pred1_cong" (the_context ()) |
352 Goal "a=a' ==> P(a) <-> P(a')"; |
332 "a=a' ==> P(a) <-> P(a')" |
353 by (rtac iffI 1); |
333 (fn prems => |
354 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; |
334 [ (cut_facts_tac prems 1), |
355 qed "pred1_cong"; |
335 (rtac iffI 1), |
356 |
336 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
357 Goal "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')"; |
337 |
358 by (rtac iffI 1); |
338 qed_goal "pred2_cong" (the_context ()) |
359 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; |
339 "[| a=a'; b=b' |] ==> P(a,b) <-> P(a',b')" |
360 qed "pred2_cong"; |
340 (fn prems => |
361 |
341 [ (cut_facts_tac prems 1), |
362 Goal "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')"; |
342 (rtac iffI 1), |
363 by (rtac iffI 1); |
343 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
364 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; |
344 |
365 qed "pred3_cong"; |
345 qed_goal "pred3_cong" (the_context ()) |
|
346 "[| a=a'; b=b'; c=c' |] ==> P(a,b,c) <-> P(a',b',c')" |
|
347 (fn prems => |
|
348 [ (cut_facts_tac prems 1), |
|
349 (rtac iffI 1), |
|
350 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
|
351 |
366 |
352 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
367 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
353 |
368 |
354 val pred_congs = |
369 val pred_congs = |
355 flat (map (fn c => |
370 flat (map (fn c => |
366 used with mp_tac (restricted to atomic formulae) is COMPLETE for |
381 used with mp_tac (restricted to atomic formulae) is COMPLETE for |
367 intuitionistic propositional logic. See |
382 intuitionistic propositional logic. See |
368 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
383 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
369 (preprint, University of St Andrews, 1991) ***) |
384 (preprint, University of St Andrews, 1991) ***) |
370 |
385 |
371 qed_goal "conj_impE" (the_context ()) |
386 val major::prems= Goal |
372 "[| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R" |
387 "[| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R"; |
373 (fn major::prems=> |
388 by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ; |
374 [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); |
389 qed "conj_impE"; |
375 |
390 |
376 qed_goal "disj_impE" (the_context ()) |
391 val major::prems= Goal |
377 "[| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R" |
392 "[| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R"; |
378 (fn major::prems=> |
393 by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ; |
379 [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); |
394 qed "disj_impE"; |
380 |
395 |
381 (*Simplifies the implication. Classical version is stronger. |
396 (*Simplifies the implication. Classical version is stronger. |
382 Still UNSAFE since Q must be provable -- backtracking needed. *) |
397 Still UNSAFE since Q must be provable -- backtracking needed. *) |
383 qed_goal "imp_impE" (the_context ()) |
398 val major::prems= Goal |
384 "[| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R" |
399 "[| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R"; |
385 (fn major::prems=> |
400 by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ; |
386 [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); |
401 qed "imp_impE"; |
387 |
402 |
388 (*Simplifies the implication. Classical version is stronger. |
403 (*Simplifies the implication. Classical version is stronger. |
389 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
404 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
390 qed_goal "not_impE" (the_context ()) |
405 val major::prems= Goal |
391 "[| ~P --> S; P ==> False; S ==> R |] ==> R" |
406 "[| ~P --> S; P ==> False; S ==> R |] ==> R"; |
392 (fn major::prems=> |
407 by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ; |
393 [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); |
408 qed "not_impE"; |
394 |
409 |
395 (*Simplifies the implication. UNSAFE. *) |
410 (*Simplifies the implication. UNSAFE. *) |
396 qed_goal "iff_impE" (the_context ()) |
411 val major::prems= Goal |
397 "[| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; \ |
412 "[| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; \ |
398 \ S ==> R |] ==> R" |
413 \ S ==> R |] ==> R"; |
399 (fn major::prems=> |
414 by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ; |
400 [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); |
415 qed "iff_impE"; |
401 |
416 |
402 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
417 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
403 qed_goal "all_impE" (the_context ()) |
418 val major::prems= Goal |
404 "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> R" |
419 "[| (ALL x. P(x))-->S; !!x. P(x); S ==> R |] ==> R"; |
405 (fn major::prems=> |
420 by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ; |
406 [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); |
421 qed "all_impE"; |
407 |
422 |
408 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
423 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
409 qed_goal "ex_impE" (the_context ()) |
424 val major::prems= Goal |
410 "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R" |
425 "[| (EX x. P(x))-->S; P(x)-->S ==> R |] ==> R"; |
411 (fn major::prems=> |
426 by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ; |
412 [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); |
427 qed "ex_impE"; |
413 |
428 |
414 (*** Courtesy of Krzysztof Grabczewski ***) |
429 (*** Courtesy of Krzysztof Grabczewski ***) |
415 |
430 |
416 val major::prems = goal (the_context ()) "[| P|Q; P==>R; Q==>S |] ==> R|S"; |
431 val major::prems = Goal "[| P|Q; P==>R; Q==>S |] ==> R|S"; |
417 by (rtac (major RS disjE) 1); |
432 by (rtac (major RS disjE) 1); |
418 by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); |
433 by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); |
419 qed "disj_imp_disj"; |
434 qed "disj_imp_disj"; |
420 |
435 |
421 |
436 |