author | skalberg |
Thu, 09 Oct 2003 18:13:32 +0200 | |
changeset 14223 | 0ee05eef881b |
parent 11973 | bd0111191d71 |
child 14430 | 5cb24165a2e1 |
permissions | -rw-r--r-- |
7357 | 1 |
(* Title: HOL/HOL_lemmas.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
6 |
Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68. |
|
7 |
*) |
|
8 |
||
11973 | 9 |
(* legacy ML bindings *) |
7357 | 10 |
|
11 |
val plusI = thm "plusI"; |
|
12 |
val minusI = thm "minusI"; |
|
13 |
val timesI = thm "timesI"; |
|
14 |
val eq_reflection = thm "eq_reflection"; |
|
15 |
val refl = thm "refl"; |
|
16 |
val subst = thm "subst"; |
|
17 |
val ext = thm "ext"; |
|
18 |
val impI = thm "impI"; |
|
19 |
val mp = thm "mp"; |
|
20 |
val True_def = thm "True_def"; |
|
21 |
val All_def = thm "All_def"; |
|
22 |
val Ex_def = thm "Ex_def"; |
|
23 |
val False_def = thm "False_def"; |
|
24 |
val not_def = thm "not_def"; |
|
25 |
val and_def = thm "and_def"; |
|
26 |
val or_def = thm "or_def"; |
|
27 |
val Ex1_def = thm "Ex1_def"; |
|
28 |
val iff = thm "iff"; |
|
29 |
val True_or_False = thm "True_or_False"; |
|
30 |
val Let_def = thm "Let_def"; |
|
31 |
val if_def = thm "if_def"; |
|
32 |
||
33 |
||
10063 | 34 |
section "Equality"; |
7357 | 35 |
|
7618 | 36 |
Goal "s=t ==> t=s"; |
37 |
by (etac subst 1); |
|
38 |
by (rtac refl 1); |
|
39 |
qed "sym"; |
|
7357 | 40 |
|
41 |
(*calling "standard" reduces maxidx to 0*) |
|
7618 | 42 |
bind_thm ("ssubst", sym RS subst); |
7357 | 43 |
|
7618 | 44 |
Goal "[| r=s; s=t |] ==> r=t"; |
45 |
by (etac subst 1 THEN assume_tac 1); |
|
46 |
qed "trans"; |
|
7357 | 47 |
|
9969 | 48 |
val prems = goal (the_context()) "(A == B) ==> A = B"; |
7357 | 49 |
by (rewrite_goals_tac prems); |
50 |
by (rtac refl 1); |
|
51 |
qed "def_imp_eq"; |
|
52 |
||
53 |
(*Useful with eresolve_tac for proving equalties from known equalities. |
|
54 |
a = b |
|
55 |
| | |
|
56 |
c = d *) |
|
57 |
Goal "[| a=b; a=c; b=d |] ==> c=d"; |
|
58 |
by (rtac trans 1); |
|
59 |
by (rtac trans 1); |
|
60 |
by (rtac sym 1); |
|
61 |
by (REPEAT (assume_tac 1)) ; |
|
62 |
qed "box_equals"; |
|
63 |
||
10063 | 64 |
|
65 |
section "Congruence rules for application"; |
|
7357 | 66 |
|
67 |
(*similar to AP_THM in Gordon's HOL*) |
|
7618 | 68 |
Goal "(f::'a=>'b) = g ==> f(x)=g(x)"; |
69 |
by (etac subst 1); |
|
70 |
by (rtac refl 1); |
|
71 |
qed "fun_cong"; |
|
7357 | 72 |
|
73 |
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*) |
|
7618 | 74 |
Goal "x=y ==> f(x)=f(y)"; |
75 |
by (etac subst 1); |
|
76 |
by (rtac refl 1); |
|
77 |
qed "arg_cong"; |
|
7357 | 78 |
|
7618 | 79 |
Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"; |
80 |
by (etac subst 1); |
|
81 |
by (etac subst 1); |
|
82 |
by (rtac refl 1); |
|
83 |
qed "cong"; |
|
7357 | 84 |
|
10063 | 85 |
|
86 |
section "Equality of booleans -- iff"; |
|
7357 | 87 |
|
7618 | 88 |
val prems = Goal "[| P ==> Q; Q ==> P |] ==> P=Q"; |
7357 | 89 |
by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)); |
90 |
qed "iffI"; |
|
91 |
||
7618 | 92 |
Goal "[| P=Q; Q |] ==> P"; |
93 |
by (etac ssubst 1); |
|
94 |
by (assume_tac 1); |
|
95 |
qed "iffD2"; |
|
7357 | 96 |
|
7618 | 97 |
Goal "[| Q; P=Q |] ==> P"; |
98 |
by (etac iffD2 1); |
|
99 |
by (assume_tac 1); |
|
100 |
qed "rev_iffD2"; |
|
7357 | 101 |
|
102 |
bind_thm ("iffD1", sym RS iffD2); |
|
103 |
bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2)); |
|
104 |
||
7618 | 105 |
val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"; |
106 |
by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1)); |
|
107 |
qed "iffE"; |
|
7357 | 108 |
|
109 |
||
110 |
section "True"; |
|
111 |
||
7618 | 112 |
Goalw [True_def] "True"; |
113 |
by (rtac refl 1); |
|
114 |
qed "TrueI"; |
|
7357 | 115 |
|
7618 | 116 |
Goal "P ==> P=True"; |
117 |
by (REPEAT (ares_tac [iffI,TrueI] 1)); |
|
118 |
qed "eqTrueI"; |
|
7357 | 119 |
|
7618 | 120 |
Goal "P=True ==> P"; |
121 |
by (etac iffD2 1); |
|
122 |
by (rtac TrueI 1); |
|
123 |
qed "eqTrueE"; |
|
7357 | 124 |
|
125 |
||
10063 | 126 |
section "Universal quantifier"; |
7357 | 127 |
|
9159 | 128 |
val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)"; |
8529 | 129 |
by (resolve_tac (prems RL [eqTrueI RS ext]) 1); |
130 |
qed "allI"; |
|
7357 | 131 |
|
9159 | 132 |
Goalw [All_def] "ALL x::'a. P(x) ==> P(x)"; |
8529 | 133 |
by (rtac eqTrueE 1); |
134 |
by (etac fun_cong 1); |
|
135 |
qed "spec"; |
|
7357 | 136 |
|
9969 | 137 |
val major::prems = Goal "[| ALL x. P(x); P(x) ==> R |] ==> R"; |
7357 | 138 |
by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ; |
139 |
qed "allE"; |
|
140 |
||
9969 | 141 |
val prems = Goal |
9159 | 142 |
"[| ALL x. P(x); [| P(x); ALL x. P(x) |] ==> R |] ==> R"; |
7357 | 143 |
by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ; |
144 |
qed "all_dupE"; |
|
145 |
||
146 |
||
147 |
section "False"; |
|
10063 | 148 |
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*) |
7357 | 149 |
|
8529 | 150 |
Goalw [False_def] "False ==> P"; |
151 |
by (etac spec 1); |
|
152 |
qed "FalseE"; |
|
7357 | 153 |
|
8529 | 154 |
Goal "False=True ==> P"; |
155 |
by (etac (eqTrueE RS FalseE) 1); |
|
156 |
qed "False_neq_True"; |
|
7357 | 157 |
|
158 |
||
10063 | 159 |
section "Negation"; |
7357 | 160 |
|
8529 | 161 |
val prems = Goalw [not_def] "(P ==> False) ==> ~P"; |
162 |
by (rtac impI 1); |
|
163 |
by (eresolve_tac prems 1); |
|
164 |
qed "notI"; |
|
7357 | 165 |
|
8529 | 166 |
Goal "False ~= True"; |
167 |
by (rtac notI 1); |
|
168 |
by (etac False_neq_True 1); |
|
169 |
qed "False_not_True"; |
|
7357 | 170 |
|
8529 | 171 |
Goal "True ~= False"; |
172 |
by (rtac notI 1); |
|
173 |
by (dtac sym 1); |
|
174 |
by (etac False_neq_True 1); |
|
175 |
qed "True_not_False"; |
|
7357 | 176 |
|
8529 | 177 |
Goalw [not_def] "[| ~P; P |] ==> R"; |
178 |
by (etac (mp RS FalseE) 1); |
|
179 |
by (assume_tac 1); |
|
180 |
qed "notE"; |
|
7357 | 181 |
|
9159 | 182 |
(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *) |
183 |
bind_thm ("notI2", notE RS notI); |
|
7357 | 184 |
|
185 |
||
10063 | 186 |
section "Implication"; |
7357 | 187 |
|
188 |
val prems = Goal "[| P-->Q; P; Q ==> R |] ==> R"; |
|
189 |
by (REPEAT (resolve_tac (prems@[mp]) 1)); |
|
190 |
qed "impE"; |
|
191 |
||
192 |
(* Reduces Q to P-->Q, allowing substitution in P. *) |
|
193 |
Goal "[| P; P --> Q |] ==> Q"; |
|
194 |
by (REPEAT (ares_tac [mp] 1)) ; |
|
195 |
qed "rev_mp"; |
|
196 |
||
197 |
val [major,minor] = Goal "[| ~Q; P==>Q |] ==> ~P"; |
|
198 |
by (rtac (major RS notE RS notI) 1); |
|
199 |
by (etac minor 1) ; |
|
10231 | 200 |
qed "contrapos_nn"; |
7357 | 201 |
|
11415 | 202 |
(*not used at all, but we already have the other 3 combinations *) |
203 |
val [major,minor] = Goal "[| Q; P ==> ~Q |] ==> ~P"; |
|
204 |
by (rtac (minor RS notE RS notI) 1); |
|
205 |
by (assume_tac 1); |
|
206 |
by (rtac major 1) ; |
|
207 |
qed "contrapos_pn"; |
|
208 |
||
10231 | 209 |
Goal "t ~= s ==> s ~= t"; |
210 |
by (etac contrapos_nn 1); |
|
211 |
by (etac sym 1); |
|
212 |
qed "not_sym"; |
|
213 |
||
214 |
(*still used in HOLCF*) |
|
7357 | 215 |
val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P"; |
10231 | 216 |
by (rtac (minor RS contrapos_nn) 1); |
7357 | 217 |
by (etac major 1) ; |
218 |
qed "rev_contrapos"; |
|
219 |
||
10063 | 220 |
section "Existential quantifier"; |
7357 | 221 |
|
9159 | 222 |
Goalw [Ex_def] "P x ==> EX x::'a. P x"; |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
223 |
by (rtac allI 1); |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
224 |
by (rtac impI 1); |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
225 |
by (etac allE 1); |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
226 |
by (etac mp 1) ; |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
227 |
by (assume_tac 1); |
8529 | 228 |
qed "exI"; |
7357 | 229 |
|
9869 | 230 |
val [major,minor] = |
9159 | 231 |
Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"; |
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
232 |
by (rtac (major RS spec RS mp) 1); |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
233 |
by (rtac (impI RS allI) 1); |
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11433
diff
changeset
|
234 |
by (etac minor 1); |
8529 | 235 |
qed "exE"; |
7357 | 236 |
|
237 |
||
10063 | 238 |
section "Conjunction"; |
7357 | 239 |
|
8529 | 240 |
Goalw [and_def] "[| P; Q |] ==> P&Q"; |
241 |
by (rtac (impI RS allI) 1); |
|
242 |
by (etac (mp RS mp) 1); |
|
243 |
by (REPEAT (assume_tac 1)); |
|
244 |
qed "conjI"; |
|
7357 | 245 |
|
8529 | 246 |
Goalw [and_def] "[| P & Q |] ==> P"; |
247 |
by (dtac spec 1) ; |
|
248 |
by (etac mp 1); |
|
249 |
by (REPEAT (ares_tac [impI] 1)); |
|
250 |
qed "conjunct1"; |
|
7357 | 251 |
|
8529 | 252 |
Goalw [and_def] "[| P & Q |] ==> Q"; |
253 |
by (dtac spec 1) ; |
|
254 |
by (etac mp 1); |
|
255 |
by (REPEAT (ares_tac [impI] 1)); |
|
256 |
qed "conjunct2"; |
|
7357 | 257 |
|
8529 | 258 |
val [major,minor] = |
259 |
Goal "[| P&Q; [| P; Q |] ==> R |] ==> R"; |
|
260 |
by (rtac minor 1); |
|
261 |
by (rtac (major RS conjunct1) 1); |
|
262 |
by (rtac (major RS conjunct2) 1); |
|
263 |
qed "conjE"; |
|
7357 | 264 |
|
8529 | 265 |
val prems = |
266 |
Goal "[| P; P ==> Q |] ==> P & Q"; |
|
267 |
by (REPEAT (resolve_tac (conjI::prems) 1)); |
|
268 |
qed "context_conjI"; |
|
7357 | 269 |
|
270 |
||
10063 | 271 |
section "Disjunction"; |
7357 | 272 |
|
8529 | 273 |
Goalw [or_def] "P ==> P|Q"; |
274 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
|
275 |
by (etac mp 1 THEN assume_tac 1); |
|
276 |
qed "disjI1"; |
|
7357 | 277 |
|
8529 | 278 |
Goalw [or_def] "Q ==> P|Q"; |
279 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
|
280 |
by (etac mp 1 THEN assume_tac 1); |
|
281 |
qed "disjI2"; |
|
7357 | 282 |
|
8529 | 283 |
val [major,minorP,minorQ] = |
284 |
Goalw [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"; |
|
285 |
by (rtac (major RS spec RS mp RS mp) 1); |
|
286 |
by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1)); |
|
287 |
qed "disjE"; |
|
7357 | 288 |
|
289 |
||
10063 | 290 |
section "Classical logic"; |
291 |
(*CCONTR -- classical logic*) |
|
7357 | 292 |
|
8529 | 293 |
val [prem] = Goal "(~P ==> P) ==> P"; |
294 |
by (rtac (True_or_False RS disjE RS eqTrueE) 1); |
|
295 |
by (assume_tac 1); |
|
296 |
by (rtac (notI RS prem RS eqTrueI) 1); |
|
297 |
by (etac subst 1); |
|
298 |
by (assume_tac 1); |
|
299 |
qed "classical"; |
|
7357 | 300 |
|
7832 | 301 |
bind_thm ("ccontr", FalseE RS classical); |
7357 | 302 |
|
9159 | 303 |
(*notE with premises exchanged; it discharges ~R so that it can be used to |
304 |
make elimination rules*) |
|
305 |
val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R"; |
|
306 |
by (rtac ccontr 1); |
|
307 |
by (etac ([premnot,premp] MRS notE) 1); |
|
308 |
qed "rev_notE"; |
|
309 |
||
7357 | 310 |
(*Double negation law*) |
311 |
Goal "~~P ==> P"; |
|
312 |
by (rtac classical 1); |
|
313 |
by (etac notE 1); |
|
314 |
by (assume_tac 1); |
|
315 |
qed "notnotD"; |
|
316 |
||
317 |
val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P"; |
|
318 |
by (rtac classical 1); |
|
319 |
by (dtac p2 1); |
|
320 |
by (etac notE 1); |
|
321 |
by (rtac p1 1); |
|
10231 | 322 |
qed "contrapos_pp"; |
7357 | 323 |
|
10063 | 324 |
|
325 |
section "Unique existence"; |
|
7357 | 326 |
|
9159 | 327 |
val prems = Goalw [Ex1_def] "[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"; |
8529 | 328 |
by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)); |
329 |
qed "ex1I"; |
|
7357 | 330 |
|
331 |
(*Sometimes easier to use: the premises have no shared variables. Safe!*) |
|
8529 | 332 |
val [ex_prem,eq] = Goal |
9159 | 333 |
"[| EX x. P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"; |
8529 | 334 |
by (rtac (ex_prem RS exE) 1); |
7357 | 335 |
by (REPEAT (ares_tac [ex1I,eq] 1)) ; |
336 |
qed "ex_ex1I"; |
|
337 |
||
8529 | 338 |
val major::prems = Goalw [Ex1_def] |
9159 | 339 |
"[| EX! x. P(x); !!x. [| P(x); ALL y. P(y) --> y=x |] ==> R |] ==> R"; |
8529 | 340 |
by (rtac (major RS exE) 1); |
341 |
by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)); |
|
342 |
qed "ex1E"; |
|
7357 | 343 |
|
9159 | 344 |
Goal "EX! x. P x ==> EX x. P x"; |
7357 | 345 |
by (etac ex1E 1); |
346 |
by (rtac exI 1); |
|
347 |
by (assume_tac 1); |
|
348 |
qed "ex1_implies_ex"; |
|
349 |
||
350 |
||
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
351 |
section "THE: definite description operator"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
352 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
353 |
val [prema,premx] = Goal "[| P a; !!x. P x ==> x=a |] ==> (THE x. P x) = a"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
354 |
by (rtac trans 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
355 |
by (rtac (thm "the_eq_trivial") 2); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
356 |
by (res_inst_tac [("f","The")] arg_cong 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
357 |
by (rtac ext 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
358 |
by (rtac iffI 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
359 |
by (etac premx 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
360 |
by (etac ssubst 1 THEN rtac prema 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
361 |
qed "the_equality"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
362 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
363 |
val [prema,premx] = Goal "[| P a; !!x. P x ==> x=a |] ==> P (THE x. P x)"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
364 |
by (rtac (the_equality RS ssubst) 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
365 |
by (REPEAT (ares_tac [prema,premx] 1)); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
366 |
qed "theI"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
367 |
|
11433 | 368 |
Goal "EX! x. P x ==> P (THE x. P x)"; |
11432
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
369 |
by (etac ex1E 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
370 |
by (etac theI 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
371 |
by (etac allE 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
372 |
by (etac mp 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
373 |
by (atac 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
374 |
qed "theI'"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
375 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
376 |
(*Easier to apply than theI: only one occurrence of P*) |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
377 |
val [prema,premx,premq] = Goal |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
378 |
"[| P a; !!x. P x ==> x=a; !!x. P x ==> Q x |] \ |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
379 |
\ ==> Q (THE x. P x)"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
380 |
by (rtac premq 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
381 |
by (rtac theI 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
382 |
by (REPEAT (ares_tac [prema,premx] 1)); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
383 |
qed "theI2"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
384 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
385 |
Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
386 |
by (rtac the_equality 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
387 |
by (atac 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
388 |
by (etac ex1E 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
389 |
by (etac all_dupE 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
390 |
by (dtac mp 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
391 |
by (atac 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
392 |
by (etac ssubst 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
393 |
by (etac allE 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
394 |
by (etac mp 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
395 |
by (atac 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
396 |
qed "the1_equality"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
397 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
398 |
Goal "(THE y. x=y) = x"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
399 |
by (rtac the_equality 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
400 |
by (rtac refl 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
401 |
by (etac sym 1); |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
402 |
qed "the_sym_eq_trivial"; |
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
403 |
|
8a203ae6efe3
added "The" (definite description operator) (by Larry);
wenzelm
parents:
11415
diff
changeset
|
404 |
|
10063 | 405 |
section "Classical intro rules for disjunction and existential quantifiers"; |
7357 | 406 |
|
9969 | 407 |
val prems = Goal "(~Q ==> P) ==> P|Q"; |
7357 | 408 |
by (rtac classical 1); |
409 |
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1)); |
|
410 |
by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ; |
|
411 |
qed "disjCI"; |
|
412 |
||
413 |
Goal "~P | P"; |
|
414 |
by (REPEAT (ares_tac [disjCI] 1)) ; |
|
415 |
qed "excluded_middle"; |
|
416 |
||
417 |
(*For disjunctive case analysis*) |
|
418 |
fun excluded_middle_tac sP = |
|
419 |
res_inst_tac [("Q",sP)] (excluded_middle RS disjE); |
|
420 |
||
421 |
(*Classical implies (-->) elimination. *) |
|
422 |
val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"; |
|
423 |
by (rtac (excluded_middle RS disjE) 1); |
|
424 |
by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))); |
|
425 |
qed "impCE"; |
|
426 |
||
427 |
(*This version of --> elimination works on Q before P. It works best for |
|
428 |
those cases in which P holds "almost everywhere". Can't install as |
|
429 |
default: would break old proofs.*) |
|
430 |
val major::prems = Goal |
|
431 |
"[| P-->Q; Q ==> R; ~P ==> R |] ==> R"; |
|
432 |
by (resolve_tac [excluded_middle RS disjE] 1); |
|
433 |
by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ; |
|
434 |
qed "impCE'"; |
|
435 |
||
436 |
(*Classical <-> elimination. *) |
|
437 |
val major::prems = Goal |
|
438 |
"[| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R"; |
|
439 |
by (rtac (major RS iffE) 1); |
|
9869 | 440 |
by (REPEAT (DEPTH_SOLVE_1 |
441 |
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))); |
|
7357 | 442 |
qed "iffCE"; |
443 |
||
9159 | 444 |
val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"; |
7357 | 445 |
by (rtac ccontr 1); |
446 |
by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ; |
|
447 |
qed "exCI"; |
|
448 |
||
8964 | 449 |
Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)"; |
450 |
by (rtac (thm"plus_ac0.commute" RS trans) 1); |
|
451 |
by (rtac (thm"plus_ac0.assoc" RS trans) 1); |
|
452 |
by (rtac (thm"plus_ac0.commute" RS arg_cong) 1); |
|
453 |
qed "plus_ac0_left_commute"; |
|
454 |
||
455 |
Goal "x + 0 = (x ::'a::plus_ac0)"; |
|
456 |
by (rtac (thm"plus_ac0.commute" RS trans) 1); |
|
457 |
by (rtac (thm"plus_ac0.zero") 1); |
|
458 |
qed "plus_ac0_zero_right"; |
|
459 |
||
9869 | 460 |
bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute", |
461 |
plus_ac0_left_commute, |
|
462 |
thm"plus_ac0.zero", plus_ac0_zero_right]); |
|
7357 | 463 |
|
464 |
(* case distinction *) |
|
465 |
||
8529 | 466 |
val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q"; |
467 |
by (rtac (excluded_middle RS disjE) 1); |
|
468 |
by (etac prem2 1); |
|
469 |
by (etac prem1 1); |
|
470 |
qed "case_split_thm"; |
|
7357 | 471 |
|
472 |
fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
|
473 |
||
474 |
||
475 |
(** Standard abbreviations **) |
|
476 |
||
10731 | 477 |
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *) |
7490 | 478 |
local |
479 |
fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t |
|
480 |
| wrong_prem (Bound _) = true |
|
481 |
| wrong_prem _ = false; |
|
7533 | 482 |
val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t))))); |
7490 | 483 |
in |
484 |
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]); |
|
485 |
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac] |
|
486 |
end; |
|
487 |
||
488 |
||
9869 | 489 |
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); |
11006 | 490 |