src/HOL/HOL.ML
 author wenzelm Tue Apr 27 10:43:52 1999 +0200 (1999-04-27) changeset 6513 e0a9459e99fc parent 6433 228237ec56e5 child 6968 7f2977e96a5c permissions -rw-r--r--
hol_setup;
1 (*  Title:      HOL/HOL.ML
2     ID:         \$Id\$
3     Author:     Tobias Nipkow
4     Copyright   1991  University of Cambridge
6 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68
7 *)
10 (** Equality **)
11 section "=";
13 qed_goal "sym" HOL.thy "s=t ==> t=s"
14  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
16 (*calling "standard" reduces maxidx to 0*)
17 bind_thm ("ssubst", (sym RS subst));
19 qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
20  (fn prems =>
21         [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
23 val prems = goal thy "(A == B) ==> A = B";
24 by (rewrite_goals_tac prems);
25 by (rtac refl 1);
26 qed "def_imp_eq";
28 (*Useful with eresolve_tac for proving equalties from known equalities.
29         a = b
30         |   |
31         c = d   *)
32 qed_goal "box_equals" HOL.thy
33     "[| a=b;  a=c;  b=d |] ==> c=d"
34  (fn prems=>
35   [ (rtac trans 1),
36     (rtac trans 1),
37     (rtac sym 1),
38     (REPEAT (resolve_tac prems 1)) ]);
41 (** Congruence rules for meta-application **)
42 section "Congruence";
44 (*similar to AP_THM in Gordon's HOL*)
45 qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
46   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
48 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
49 qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)"
50  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
52 qed_goal "cong" HOL.thy
53    "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
54  (fn [prem1,prem2] =>
55    [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
58 (** Equality of booleans -- iff **)
59 section "iff";
61 qed_goal "iffI" HOL.thy
62    "[| P ==> Q;  Q ==> P |] ==> P=Q"
63  (fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]);
65 qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
66  (fn prems =>
67         [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
69 qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
70  (fn _ => [etac iffD2 1, assume_tac 1]);
72 bind_thm ("iffD1", sym RS iffD2);
73 bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
75 qed_goal "iffE" HOL.thy
76     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
77  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
80 (** True **)
81 section "True";
83 qed_goalw "TrueI" HOL.thy [True_def] "True"
84   (fn _ => [rtac refl 1]);
86 qed_goal "eqTrueI" HOL.thy "P ==> P=True"
87  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
89 qed_goal "eqTrueE" HOL.thy "P=True ==> P"
90  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
93 (** Universal quantifier **)
94 section "!";
96 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
97  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
99 qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
100  (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
102 qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
103  (fn major::prems=>
104   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
106 qed_goal "all_dupE" HOL.thy
107     "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
108  (fn prems =>
109   [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
112 (** False ** Depends upon spec; it is impossible to do propositional logic
113              before quantifiers! **)
114 section "False";
116 qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
117  (fn [major] => [rtac (major RS spec) 1]);
119 qed_goal "False_neq_True" HOL.thy "False=True ==> P"
120  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
123 (** Negation **)
124 section "~";
126 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
127  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
129 qed_goal "False_not_True" HOL.thy "False ~= True"
130   (K [rtac notI 1, etac False_neq_True 1]);
132 qed_goal "True_not_False" HOL.thy "True ~= False"
133   (K [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
135 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
136  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
138 bind_thm ("classical2", notE RS notI);
140 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
141  (fn _ => [REPEAT (ares_tac [notE] 1)]);
144 (** Implication **)
145 section "-->";
147 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
148  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
150 (* Reduces Q to P-->Q, allowing substitution in P. *)
151 qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
152  (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
154 qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
155  (fn [major,minor]=>
156   [ (rtac (major RS notE RS notI) 1),
157     (etac minor 1) ]);
159 qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
160  (fn [major,minor]=>
161   [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
163 (* ~(?t = ?s) ==> ~(?s = ?t) *)
164 bind_thm("not_sym", sym COMP rev_contrapos);
167 (** Existential quantifier **)
168 section "?";
170 qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
171  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
173 qed_goalw "exE" HOL.thy [Ex_def]
174   "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
175   (fn prems => [REPEAT(resolve_tac prems 1)]);
178 (** Conjunction **)
179 section "&";
181 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
182  (fn prems =>
183   [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
185 qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
186  (fn prems =>
187    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
189 qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
190  (fn prems =>
191    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
193 qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
194  (fn prems =>
195          [cut_facts_tac prems 1, resolve_tac prems 1,
196           etac conjunct1 1, etac conjunct2 1]);
198 qed_goal "context_conjI" HOL.thy  "[| P; P ==> Q |] ==> P & Q"
199  (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
202 (** Disjunction *)
203 section "|";
205 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
206  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
208 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
209  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
211 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
212  (fn [a1,a2,a3] =>
213         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
214          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
217 (** CCONTR -- classical logic **)
218 section "classical logic";
220 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
221  (fn [prem] =>
222    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
223     rtac (impI RS prem RS eqTrueI) 1,
224     etac subst 1,  assume_tac 1]);
226 val ccontr = FalseE RS classical;
228 (*Double negation law*)
229 qed_goal "notnotD" HOL.thy "~~P ==> P"
230  (fn [major]=>
231   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
233 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
234         rtac classical 1,
235         dtac p2 1,
236         etac notE 1,
237         rtac p1 1]);
239 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
240         rtac notI 1,
241         dtac p2 1,
242         etac notE 1,
243         rtac p1 1]);
245 (** Unique existence **)
246 section "?!";
248 qed_goalw "ex1I" HOL.thy [Ex1_def]
249             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
250  (fn prems =>
251   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
253 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
254 qed_goal "ex_ex1I" HOL.thy
255     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
256  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
257                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
259 qed_goalw "ex1E" HOL.thy [Ex1_def]
260     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
261  (fn major::prems =>
262   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
264 Goal "?! x. P x ==> ? x. P x";
265 by (etac ex1E 1);
266 by (rtac exI 1);
267 by (assume_tac 1);
268 qed "ex1_implies_ex";
271 (** Select: Hilbert's Epsilon-operator **)
272 section "@";
274 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
275 qed_goal "selectI2" HOL.thy
276     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
277  (fn prems => [ resolve_tac prems 1,
278                 rtac selectI 1,
279                 resolve_tac prems 1 ]);
281 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
282 qed_goal "selectI2EX" HOL.thy
283   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
284 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
286 qed_goal "select_equality" HOL.thy
287     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
288  (fn prems => [ rtac selectI2 1,
289                 REPEAT (ares_tac prems 1) ]);
291 qed_goalw "select1_equality" HOL.thy [Ex1_def]
292   "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
293 	  rtac select_equality 1, atac 1,
294           etac exE 1, etac conjE 1,
295           rtac allE 1, atac 1,
296           etac impE 1, atac 1, etac ssubst 1,
297           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
298           rtac refl 1]);
300 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
301         rtac iffI 1,
302         etac exI 1,
303         etac exE 1,
304         etac selectI 1]);
306 qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
307 	rtac select_equality 1,
308 	rtac refl 1,
309 	atac 1]);
311 qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
312 	rtac select_equality 1,
313 	rtac refl 1,
314 	etac sym 1]);
316 (** Classical intro rules for disjunction and existential quantifiers *)
317 section "classical intro rules";
319 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
320  (fn prems=>
321   [ (rtac classical 1),
322     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
323     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
325 qed_goal "excluded_middle" HOL.thy "~P | P"
326  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
328 (*For disjunctive case analysis*)
329 fun excluded_middle_tac sP =
330     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
332 (*Classical implies (-->) elimination. *)
333 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
334  (fn major::prems=>
335   [ rtac (excluded_middle RS disjE) 1,
336     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
338 (*This version of --> elimination works on Q before P.  It works best for
339   those cases in which P holds "almost everywhere".  Can't install as
340   default: would break old proofs.*)
341 qed_goal "impCE'" thy
342     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
343  (fn major::prems=>
344   [ (resolve_tac [excluded_middle RS disjE] 1),
345     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
347 (*Classical <-> elimination. *)
348 qed_goal "iffCE" HOL.thy
349     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
350  (fn major::prems =>
351   [ (rtac (major RS iffE) 1),
352     (REPEAT (DEPTH_SOLVE_1
353         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
355 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
356  (fn prems=>
357   [ (rtac ccontr 1),
358     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
361 (* case distinction *)
363 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
364   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
365                   etac p2 1, etac p1 1]);
367 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
370 (** Standard abbreviations **)
372 (*Apply an equality or definition ONCE.
373   Fails unless the substitution has an effect*)
374 fun stac th =
375   let val th' = th RS def_imp_eq handle _ => th
376   in  CHANGED_GOAL (rtac (th' RS ssubst))
377   end;
379 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
382 (** strip ! and --> from proved goal while preserving !-bound var names **)
384 local
386 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
387 val myspec = read_instantiate [("P","?XXX")] spec;
388 val _ \$ (_ \$ (vx as Var(_,vxT))) = concl_of myspec;
389 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
390 val aspec = forall_intr cvx myspec;
392 in
394 fun RSspec th =
395   (case concl_of th of
396      _ \$ (Const("All",_) \$ Abs(a,_,_)) =>
397          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
398          in th RS forall_elim ca aspec end
399   | _ => raise THM("RSspec",0,[th]));
401 fun RSmp th =
402   (case concl_of th of
403      _ \$ (Const("op -->",_)\$_\$_) => th RS mp
404   | _ => raise THM("RSmp",0,[th]));
406 fun normalize_thm funs =
407   let fun trans [] th = th
408 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
409   in zero_var_indexes o trans funs end;
411 fun qed_spec_mp name =
412   let val thm = normalize_thm [RSspec,RSmp] (result())
413   in ThmDatabase.ml_store_thm(name, thm) end;
415 fun qed_goal_spec_mp name thy s p =
416 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
418 fun qed_goalw_spec_mp name thy defs s p =
419 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
421 end;
424 (* attributes *)
426 local
428 fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
430 in
432 val hol_setup =