src/HOL/HOL.ML
 author wenzelm Tue Jan 12 13:54:51 1999 +0100 (1999-01-12) changeset 6092 d9db67970c73 parent 5888 d8e51792ca85 child 6214 0513cfd1a598 permissions -rw-r--r--
eliminated tthm type and Attribute structure;
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]);
199 (** Disjunction *)
200 section "|";
202 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
203  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
205 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
206  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
208 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
209  (fn [a1,a2,a3] =>
210         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
211          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
214 (** CCONTR -- classical logic **)
215 section "classical logic";
217 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
218  (fn [prem] =>
219    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
220     rtac (impI RS prem RS eqTrueI) 1,
221     etac subst 1,  assume_tac 1]);
223 val ccontr = FalseE RS classical;
225 (*Double negation law*)
226 qed_goal "notnotD" HOL.thy "~~P ==> P"
227  (fn [major]=>
228   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
230 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
231         rtac classical 1,
232         dtac p2 1,
233         etac notE 1,
234         rtac p1 1]);
236 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
237         rtac notI 1,
238         dtac p2 1,
239         etac notE 1,
240         rtac p1 1]);
242 (** Unique existence **)
243 section "?!";
245 qed_goalw "ex1I" HOL.thy [Ex1_def]
246             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
247  (fn prems =>
248   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
250 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
251 qed_goal "ex_ex1I" HOL.thy
252     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
253  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
254                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
256 qed_goalw "ex1E" HOL.thy [Ex1_def]
257     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
258  (fn major::prems =>
259   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
261 Goal "?! x. P x ==> ? x. P x";
262 by (etac ex1E 1);
263 by (rtac exI 1);
264 by (assume_tac 1);
265 qed "ex1_implies_ex";
268 (** Select: Hilbert's Epsilon-operator **)
269 section "@";
271 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
272 qed_goal "selectI2" HOL.thy
273     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
274  (fn prems => [ resolve_tac prems 1,
275                 rtac selectI 1,
276                 resolve_tac prems 1 ]);
278 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
279 qed_goal "selectI2EX" HOL.thy
280   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
281 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
283 qed_goal "select_equality" HOL.thy
284     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
285  (fn prems => [ rtac selectI2 1,
286                 REPEAT (ares_tac prems 1) ]);
288 qed_goalw "select1_equality" HOL.thy [Ex1_def]
289   "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
290 	  rtac select_equality 1, atac 1,
291           etac exE 1, etac conjE 1,
292           rtac allE 1, atac 1,
293           etac impE 1, atac 1, etac ssubst 1,
294           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
295           rtac refl 1]);
297 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
298         rtac iffI 1,
299         etac exI 1,
300         etac exE 1,
301         etac selectI 1]);
303 qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
304 	rtac select_equality 1,
305 	rtac refl 1,
306 	atac 1]);
308 qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
309 	rtac select_equality 1,
310 	rtac refl 1,
311 	etac sym 1]);
313 (** Classical intro rules for disjunction and existential quantifiers *)
314 section "classical intro rules";
316 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
317  (fn prems=>
318   [ (rtac classical 1),
319     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
320     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
322 qed_goal "excluded_middle" HOL.thy "~P | P"
323  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
325 (*For disjunctive case analysis*)
326 fun excluded_middle_tac sP =
327     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
329 (*Classical implies (-->) elimination. *)
330 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R"
331  (fn major::prems=>
332   [ rtac (excluded_middle RS disjE) 1,
333     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
335 (*This version of --> elimination works on Q before P.  It works best for
336   those cases in which P holds "almost everywhere".  Can't install as
337   default: would break old proofs.*)
338 qed_goal "impCE'" thy
339     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
340  (fn major::prems=>
341   [ (resolve_tac [excluded_middle RS disjE] 1),
342     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
344 (*Classical <-> elimination. *)
345 qed_goal "iffCE" HOL.thy
346     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
347  (fn major::prems =>
348   [ (rtac (major RS iffE) 1),
349     (REPEAT (DEPTH_SOLVE_1
350         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
352 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
353  (fn prems=>
354   [ (rtac ccontr 1),
355     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
358 (* case distinction *)
360 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
361   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
362                   etac p2 1, etac p1 1]);
364 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
367 (** Standard abbreviations **)
369 (*Apply an equality or definition ONCE.
370   Fails unless the substitution has an effect*)
371 fun stac th =
372   let val th' = th RS def_imp_eq handle _ => th
373   in  CHANGED_GOAL (rtac (th' RS ssubst))
374   end;
376 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
379 (** strip ! and --> from proved goal while preserving !-bound var names **)
381 local
383 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
384 val myspec = read_instantiate [("P","?XXX")] spec;
385 val _ \$ (_ \$ (vx as Var(_,vxT))) = concl_of myspec;
386 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
387 val aspec = forall_intr cvx myspec;
389 in
391 fun RSspec th =
392   (case concl_of th of
393      _ \$ (Const("All",_) \$ Abs(a,_,_)) =>
394          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
395          in th RS forall_elim ca aspec end
396   | _ => raise THM("RSspec",0,[th]));
398 fun RSmp th =
399   (case concl_of th of
400      _ \$ (Const("op -->",_)\$_\$_) => th RS mp
401   | _ => raise THM("RSmp",0,[th]));
403 fun normalize_thm funs =
404   let fun trans [] th = th
405 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
406   in zero_var_indexes o trans funs end;
408 fun qed_spec_mp name =
409   let val thm = normalize_thm [RSspec,RSmp] (result())
410   in ml_store_thm(name, thm) end;
412 fun qed_goal_spec_mp name thy s p =
413 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
415 fun qed_goalw_spec_mp name thy defs s p =
416 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
418 end;
421 (* attributes *)
423 local
425 fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
427 in
429 val attrib_setup =