src/HOL/HOL.ML
 author paulson Wed Nov 26 17:23:18 1997 +0100 (1997-11-26) changeset 4302 2c99775d953f parent 4131 916641b59219 child 4467 bd05e2a28602 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 val iffD1 = sym RS iffD2;
69 qed_goal "iffE" HOL.thy
70     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
71  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
74 (** True **)
75 section "True";
77 qed_goalw "TrueI" HOL.thy [True_def] "True"
78   (fn _ => [rtac refl 1]);
80 qed_goal "eqTrueI" HOL.thy "P ==> P=True"
81  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
83 qed_goal "eqTrueE" HOL.thy "P=True ==> P"
84  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
87 (** Universal quantifier **)
88 section "!";
90 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
91  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
93 qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
94  (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
96 qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
97  (fn major::prems=>
98   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
100 qed_goal "all_dupE" HOL.thy
101     "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
102  (fn prems =>
103   [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
106 (** False ** Depends upon spec; it is impossible to do propositional logic
107              before quantifiers! **)
108 section "False";
110 qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
111  (fn [major] => [rtac (major RS spec) 1]);
113 qed_goal "False_neq_True" HOL.thy "False=True ==> P"
114  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
117 (** Negation **)
118 section "~";
120 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
121  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
123 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
124  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
126 bind_thm ("classical2", notE RS notI);
128 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
129  (fn _ => [REPEAT (ares_tac [notE] 1)]);
132 (** Implication **)
133 section "-->";
135 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
136  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
138 (* Reduces Q to P-->Q, allowing substitution in P. *)
139 qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
140  (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
142 qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
143  (fn [major,minor]=>
144   [ (rtac (major RS notE RS notI) 1),
145     (etac minor 1) ]);
147 qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
148  (fn [major,minor]=>
149   [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
151 (* ~(?t = ?s) ==> ~(?s = ?t) *)
152 bind_thm("not_sym", sym COMP rev_contrapos);
155 (** Existential quantifier **)
156 section "?";
158 qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a. P(x)"
159  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
161 qed_goalw "exE" HOL.thy [Ex_def]
162   "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
163   (fn prems => [REPEAT(resolve_tac prems 1)]);
166 (** Conjunction **)
167 section "&";
169 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
170  (fn prems =>
171   [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
173 qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
174  (fn prems =>
175    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
177 qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
178  (fn prems =>
179    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
181 qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
182  (fn prems =>
183          [cut_facts_tac prems 1, resolve_tac prems 1,
184           etac conjunct1 1, etac conjunct2 1]);
187 (** Disjunction *)
188 section "|";
190 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
191  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
193 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
194  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
196 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
197  (fn [a1,a2,a3] =>
198         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
199          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
202 (** CCONTR -- classical logic **)
203 section "classical logic";
205 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
206  (fn [prem] =>
207    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
208     rtac (impI RS prem RS eqTrueI) 1,
209     etac subst 1,  assume_tac 1]);
211 val ccontr = FalseE RS classical;
213 (*Double negation law*)
214 qed_goal "notnotD" HOL.thy "~~P ==> P"
215  (fn [major]=>
216   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
218 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
219         rtac classical 1,
220         dtac p2 1,
221         etac notE 1,
222         rtac p1 1]);
224 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
225         rtac notI 1,
226         dtac p2 1,
227         etac notE 1,
228         rtac p1 1]);
230 (** Unique existence **)
231 section "?!";
233 qed_goalw "ex1I" HOL.thy [Ex1_def]
234             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
235  (fn prems =>
236   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
238 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
239 qed_goal "ex_ex1I" HOL.thy
240     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
241  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
242                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
244 qed_goalw "ex1E" HOL.thy [Ex1_def]
245     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
246  (fn major::prems =>
247   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
250 (** Select: Hilbert's Epsilon-operator **)
251 section "@";
253 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
254 qed_goal "selectI2" HOL.thy
255     "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x. P(x))"
256  (fn prems => [ resolve_tac prems 1,
257                 rtac selectI 1,
258                 resolve_tac prems 1 ]);
260 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
261 qed_goal "selectI2EX" HOL.thy
262   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
263 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
265 qed_goal "select_equality" HOL.thy
266     "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x. P(x)) = a"
267  (fn prems => [ rtac selectI2 1,
268                 REPEAT (ares_tac prems 1) ]);
270 qed_goalw "select1_equality" HOL.thy [Ex1_def]
271   "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a" (K [
272 	  rtac select_equality 1, atac 1,
273           etac exE 1, etac conjE 1,
274           rtac allE 1, atac 1,
275           etac impE 1, atac 1, etac ssubst 1,
276           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
277           rtac refl 1]);
279 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
280         rtac iffI 1,
281         etac exI 1,
282         etac exE 1,
283         etac selectI 1]);
285 val Eps_eq = prove_goal HOL.thy "Eps (op = x) = x" (K [
286 	rtac select_equality 1, rtac refl 1, etac sym 1]);
288 val ex1_Eps_eq = prove_goal HOL.thy "!!X. [|?!x. P x; P y|] ==> Eps P = y" (K [
289 	rtac select_equality 1,
290 	 atac 1,
291 	etac ex1E 1,
292 	etac all_dupE 1,
293 	etac impE 1,
294 	 atac 1,
295 	rtac trans 1,
296 	 etac sym 2,
297 	dtac spec 1,
298 	etac impE 1,
299 	 ALLGOALS atac]);
302 (** Classical intro rules for disjunction and existential quantifiers *)
303 section "classical intro rules";
305 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
306  (fn prems=>
307   [ (rtac classical 1),
308     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
309     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
311 qed_goal "excluded_middle" HOL.thy "~P | P"
312  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
314 (*For disjunctive case analysis*)
315 fun excluded_middle_tac sP =
316     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
318 (*Classical implies (-->) elimination. *)
319 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
320  (fn major::prems=>
321   [ rtac (excluded_middle RS disjE) 1,
322     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
324 (*This version of --> elimination works on Q before P.  It works best for
325   those cases in which P holds "almost everywhere".  Can't install as
326   default: would break old proofs.*)
327 qed_goal "impCE'" thy
328     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
329  (fn major::prems=>
330   [ (resolve_tac [excluded_middle RS disjE] 1),
331     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
333 (*Classical <-> elimination. *)
334 qed_goal "iffCE" HOL.thy
335     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
336  (fn major::prems =>
337   [ (rtac (major RS iffE) 1),
338     (REPEAT (DEPTH_SOLVE_1
339         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
341 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
342  (fn prems=>
343   [ (rtac ccontr 1),
344     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
347 (* case distinction *)
349 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
350   (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
351                   etac p2 1, etac p1 1]);
353 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
356 (** Standard abbreviations **)
358 fun stac th = CHANGED o 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;