src/HOL/HOL.ML
 author oheimb Wed Aug 12 15:40:47 1998 +0200 (1998-08-12) changeset 5299 d15a4155b96b parent 5228 66925577cefe child 5309 01c2b317da88 permissions -rw-r--r--
1 (*  Title:      HOL/HOL.ML
2     ID:         \$Id\$
3     Author:     Tobias Nipkow
4     Copyright   1991  University of Cambridge
6 For HOL.thy
7 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68
8 *)
10 open HOL;
13 (** Equality **)
14 section "=";
16 qed_goal "sym" HOL.thy "s=t ==> t=s"
17  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
19 (*calling "standard" reduces maxidx to 0*)
20 bind_thm ("ssubst", (sym RS subst));
22 qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
23  (fn prems =>
24         [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
26 (*Useful with eresolve_tac for proving equalties from known equalities.
27         a = b
28         |   |
29         c = d   *)
30 qed_goal "box_equals" HOL.thy
31     "[| a=b;  a=c;  b=d |] ==> c=d"
32  (fn prems=>
33   [ (rtac trans 1),
34     (rtac trans 1),
35     (rtac sym 1),
36     (REPEAT (resolve_tac prems 1)) ]);
39 (** Congruence rules for meta-application **)
40 section "Congruence";
42 (*similar to AP_THM in Gordon's HOL*)
43 qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
44   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
46 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
47 qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)"
48  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
50 qed_goal "cong" HOL.thy
51    "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
52  (fn [prem1,prem2] =>
53    [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
56 (** Equality of booleans -- iff **)
57 section "iff";
59 qed_goal "iffI" HOL.thy
60    "[| P ==> Q;  Q ==> P |] ==> P=Q"
61  (fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]);
63 qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
64  (fn prems =>
65         [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
67 qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
68  (fn _ => [etac iffD2 1, assume_tac 1]);
70 bind_thm ("iffD1", sym RS iffD2);
71 bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
73 qed_goal "iffE" HOL.thy
74     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
75  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
78 (** True **)
79 section "True";
81 qed_goalw "TrueI" HOL.thy [True_def] "True"
82   (fn _ => [rtac refl 1]);
84 qed_goal "eqTrueI" HOL.thy "P ==> P=True"
85  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
87 qed_goal "eqTrueE" HOL.thy "P=True ==> P"
88  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
91 (** Universal quantifier **)
92 section "!";
94 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
95  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
97 qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
98  (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
100 qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
101  (fn major::prems=>
102   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
104 qed_goal "all_dupE" HOL.thy
105     "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
106  (fn prems =>
107   [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
110 (** False ** Depends upon spec; it is impossible to do propositional logic
111              before quantifiers! **)
112 section "False";
114 qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
115  (fn [major] => [rtac (major RS spec) 1]);
117 qed_goal "False_neq_True" HOL.thy "False=True ==> P"
118  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
121 (** Negation **)
122 section "~";
124 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
125  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
127 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
128  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
130 bind_thm ("classical2", notE RS notI);
132 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
133  (fn _ => [REPEAT (ares_tac [notE] 1)]);
136 (** Implication **)
137 section "-->";
139 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
140  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
142 (* Reduces Q to P-->Q, allowing substitution in P. *)
143 qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
144  (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
146 qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
147  (fn [major,minor]=>
148   [ (rtac (major RS notE RS notI) 1),
149     (etac minor 1) ]);
151 qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
152  (fn [major,minor]=>
153   [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
155 (* ~(?t = ?s) ==> ~(?s = ?t) *)
156 bind_thm("not_sym", sym COMP rev_contrapos);
159 (** Existential quantifier **)
160 section "?";
162 qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
163  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
165 qed_goalw "exE" HOL.thy [Ex_def]
166   "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
167   (fn prems => [REPEAT(resolve_tac prems 1)]);
170 (** Conjunction **)
171 section "&";
173 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
174  (fn prems =>
175   [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
177 qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
178  (fn prems =>
179    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
181 qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
182  (fn prems =>
183    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
185 qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
186  (fn prems =>
187          [cut_facts_tac prems 1, resolve_tac prems 1,
188           etac conjunct1 1, etac conjunct2 1]);
191 (** Disjunction *)
192 section "|";
194 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
195  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
197 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
198  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
200 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
201  (fn [a1,a2,a3] =>
202         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
203          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
206 (** CCONTR -- classical logic **)
207 section "classical logic";
209 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
210  (fn [prem] =>
211    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
212     rtac (impI RS prem RS eqTrueI) 1,
213     etac subst 1,  assume_tac 1]);
215 val ccontr = FalseE RS classical;
217 (*Double negation law*)
218 qed_goal "notnotD" HOL.thy "~~P ==> P"
219  (fn [major]=>
220   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
222 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
223         rtac classical 1,
224         dtac p2 1,
225         etac notE 1,
226         rtac p1 1]);
228 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
229         rtac notI 1,
230         dtac p2 1,
231         etac notE 1,
232         rtac p1 1]);
234 (** Unique existence **)
235 section "?!";
237 qed_goalw "ex1I" HOL.thy [Ex1_def]
238             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
239  (fn prems =>
240   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
242 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
243 qed_goal "ex_ex1I" HOL.thy
244     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
245  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
246                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
248 qed_goalw "ex1E" HOL.thy [Ex1_def]
249     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
250  (fn major::prems =>
251   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
253 Goal "?! x. P x ==> ? x. P x";
254 by (etac ex1E 1);
255 by (rtac exI 1);
256 by (assume_tac 1);
257 qed "ex1_implies_ex";
260 (** Select: Hilbert's Epsilon-operator **)
261 section "@";
263 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
264 qed_goal "selectI2" HOL.thy
265     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
266  (fn prems => [ resolve_tac prems 1,
267                 rtac selectI 1,
268                 resolve_tac prems 1 ]);
270 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
271 qed_goal "selectI2EX" HOL.thy
272   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
273 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
275 qed_goal "select_equality" HOL.thy
276     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
277  (fn prems => [ rtac selectI2 1,
278                 REPEAT (ares_tac prems 1) ]);
280 qed_goalw "select1_equality" HOL.thy [Ex1_def]
281   "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
282 	  rtac select_equality 1, atac 1,
283           etac exE 1, etac conjE 1,
284           rtac allE 1, atac 1,
285           etac impE 1, atac 1, etac ssubst 1,
286           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
287           rtac refl 1]);
289 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
290         rtac iffI 1,
291         etac exI 1,
292         etac exE 1,
293         etac selectI 1]);
295 qed_goal "Eps_eq" HOL.thy "(Eps (op = x)) = x" (K [
296 	rtac select_equality 1,
297 	rtac refl 1,
298 	etac sym 1]);
300 (** Classical intro rules for disjunction and existential quantifiers *)
301 section "classical intro rules";
303 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
304  (fn prems=>
305   [ (rtac classical 1),
306     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
307     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
309 qed_goal "excluded_middle" HOL.thy "~P | P"
310  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
312 (*For disjunctive case analysis*)
313 fun excluded_middle_tac sP =
314     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
316 (*Classical implies (-->) elimination. *)
317 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
318  (fn major::prems=>
319   [ rtac (excluded_middle RS disjE) 1,
320     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
322 (*This version of --> elimination works on Q before P.  It works best for
323   those cases in which P holds "almost everywhere".  Can't install as
324   default: would break old proofs.*)
325 qed_goal "impCE'" thy
326     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
327  (fn major::prems=>
328   [ (resolve_tac [excluded_middle RS disjE] 1),
329     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
331 (*Classical <-> elimination. *)
332 qed_goal "iffCE" HOL.thy
333     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
334  (fn major::prems =>
335   [ (rtac (major RS iffE) 1),
336     (REPEAT (DEPTH_SOLVE_1
337         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
339 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
340  (fn prems=>
341   [ (rtac ccontr 1),
342     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
345 (* case distinction *)
347 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
348   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
349                   etac p2 1, etac p1 1]);
351 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
354 (** Standard abbreviations **)
356 (*Fails unless the substitution has an effect*)
357 fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
359 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
362 (** strip ! and --> from proved goal while preserving !-bound var names **)
364 local
366 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
367 val myspec = read_instantiate [("P","?XXX")] spec;
368 val _ \$ (_ \$ (vx as Var(_,vxT))) = concl_of myspec;
369 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
370 val aspec = forall_intr cvx myspec;
372 in
374 fun RSspec th =
375   (case concl_of th of
376      _ \$ (Const("All",_) \$ Abs(a,_,_)) =>
377          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
378          in th RS forall_elim ca aspec end
379   | _ => raise THM("RSspec",0,[th]));
381 fun RSmp th =
382   (case concl_of th of
383      _ \$ (Const("op -->",_)\$_\$_) => th RS mp
384   | _ => raise THM("RSmp",0,[th]));
386 fun normalize_thm funs =
387 let fun trans [] th = th
388       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
389 in trans funs end;
391 fun qed_spec_mp name =
392   let val thm = normalize_thm [RSspec,RSmp] (result())
393   in bind_thm(name, thm) end;
395 fun qed_goal_spec_mp name thy s p =
396 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
398 fun qed_goalw_spec_mp name thy defs s p =
399 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
401 end;