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