Mercurial Mercurial > repos > Old_HOL / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
hol.ML
changeset 0 7949f97df77a
child 40 ac7b7003f177 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hol.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,334 @@
+(*  Title: 	HOL/hol.ML
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+For hol.thy
+Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
+*)
+
+open HOL;
+
+signature HOL_LEMMAS =
+  sig
+  val allE: thm
+  val all_dupE: thm
+  val allI: thm
+  val arg_cong: thm
+  val fun_cong: thm
+  val box_equals: thm
+  val ccontr: thm
+  val classical: thm
+  val cong: thm
+  val conjunct1: thm
+  val conjunct2: thm
+  val conjE: thm
+  val conjI: thm
+  val contrapos: thm
+  val disjCI: thm
+  val disjE: thm
+  val disjI1: thm
+  val disjI2: thm
+  val eqTrueI: thm
+  val eqTrueE: thm
+  val ex1E: thm
+  val ex1I: thm
+  val exCI: thm
+  val exI: thm
+  val exE: thm
+  val excluded_middle: thm
+  val FalseE: thm
+  val False_neq_True: thm
+  val iffCE : thm
+  val iffD1: thm
+  val iffD2: thm
+  val iffE: thm
+  val iffI: thm
+  val impCE: thm
+  val impE: thm
+  val not_sym: thm
+  val notE: thm
+  val notI: thm
+  val notnotD : thm
+  val rev_mp: thm
+  val select_equality: thm
+  val spec: thm
+  val sstac: thm list -> int -> tactic
+  val ssubst: thm
+  val stac: thm -> int -> tactic
+  val strip_tac: int -> tactic
+  val swap: thm
+  val sym: thm
+  val trans: thm
+  val TrueI: thm
+  end;
+
+structure HOL_Lemmas : HOL_LEMMAS =
+
+struct
+
+(** Equality **)
+
+val sym = prove_goal HOL.thy "s=t ==> t=s"
+ (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
+
+(*calling "standard" reduces maxidx to 0*)
+val ssubst = standard (sym RS subst);
+
+val trans = prove_goal HOL.thy "[| r=s; s=t |] ==> r=t"
+ (fn prems =>
+	[rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
+
+(*Useful with eresolve_tac for proving equalties from known equalities.
+	a = b
+	|   |
+	c = d	*)
+val box_equals = prove_goal HOL.thy
+    "[| a=b;  a=c;  b=d |] ==> c=d"  
+ (fn prems=>
+  [ (rtac trans 1),
+    (rtac trans 1),
+    (rtac sym 1),
+    (REPEAT (resolve_tac prems 1)) ]);
+
+(** Congruence rules for meta-application **)
+
+(*similar to AP_THM in Gordon's HOL*)
+val fun_cong = prove_goal HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
+  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
+
+(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
+val arg_cong = prove_goal HOL.thy "x=y ==> f(x)=f(y)"
+ (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
+
+val cong = prove_goal HOL.thy
+   "[| f = g; x::'a = y |] ==> f(x) = g(y)"
+ (fn [prem1,prem2] =>
+   [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
+
+(** Equality of booleans -- iff **)
+
+val iffI = prove_goal HOL.thy
+   "[| P ==> Q;  Q ==> P |] ==> P=Q"
+ (fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]);
+
+val iffD2 = prove_goal HOL.thy "[| P=Q; Q |] ==> P"
+ (fn prems =>
+	[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
+
+val iffD1 = sym RS iffD2;
+
+val iffE = prove_goal HOL.thy
+    "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
+ (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
+
+(** True **)
+
+val TrueI = refl RS (True_def RS iffD2);
+
+val eqTrueI  = prove_goal HOL.thy "P ==> P=True" 
+ (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
+
+val eqTrueE = prove_goal HOL.thy "P=True ==> P" 
+ (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
+
+(** Universal quantifier **)
+
+val allI = prove_goal HOL.thy "(!!x::'a. P(x)) ==> !x. P(x)"
+ (fn [asm] => [rtac (All_def RS ssubst) 1, rtac (asm RS (eqTrueI RS ext)) 1]);
+
+val spec = prove_goal HOL.thy "! x::'a.P(x) ==> P(x)"
+ (fn prems =>
+   [ rtac eqTrueE 1, 
+     resolve_tac (prems RL [All_def RS subst] RL [fun_cong]) 1 ]);
+
+val allE = prove_goal HOL.thy "[| !x.P(x);  P(x) ==> R |] ==> R"
+ (fn major::prems=>
+  [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
+
+val all_dupE = prove_goal HOL.thy 
+    "[| ! x.P(x);  [| P(x); ! x.P(x) |] ==> R |] ==> R"
+ (fn prems =>
+  [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
+
+
+(** False ** Depends upon spec; it is impossible to do propositional logic
+             before quantifiers! **)
+
+val FalseE = prove_goal HOL.thy "False ==> P"
+ (fn prems => [rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1]);
+
+val False_neq_True = prove_goal HOL.thy "False=True ==> P"
+ (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
+
+
+(** Negation **)
+
+val notI = prove_goal HOL.thy  "(P ==> False) ==> ~P"
+ (fn prems=> [rtac (not_def RS ssubst) 1, rtac impI 1, eresolve_tac prems 1]);
+
+val notE = prove_goal HOL.thy "[| ~P;  P |] ==> R"
+ (fn prems =>
+    [rtac (mp RS FalseE) 1, 
+     resolve_tac prems 2, rtac (not_def RS subst) 1,
+     resolve_tac prems 1]);
+
+(** Implication **)
+
+val impE = prove_goal HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
+ (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
+
+(* Reduces Q to P-->Q, allowing substitution in P. *)
+val rev_mp = prove_goal HOL.thy "[| P;  P --> Q |] ==> Q"
+ (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
+
+val contrapos = prove_goal HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
+ (fn [major,minor]=> 
+  [ (rtac (major RS notE RS notI) 1), 
+    (etac minor 1) ]);
+
+(* ~(?t = ?s) ==> ~(?s = ?t) *)
+val [not_sym] = compose(sym,2,contrapos);
+
+
+(** Existential quantifier **)
+
+val exI = prove_goal HOL.thy "P(x) ==> ? x::'a.P(x)"
+ (fn prems =>
+	[rtac (selectI RS (Ex_def RS ssubst)) 1,
+	 resolve_tac prems 1]);
+
+val exE = prove_goal HOL.thy "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+	(fn prems =>
+	[resolve_tac prems 1, res_inst_tac [("P","%C.C(P)")] subst 1,
+	 rtac Ex_def 1, resolve_tac prems 1]);
+
+
+(** Conjunction **)
+
+val conjI = prove_goal HOL.thy "[| P; Q |] ==> P&Q"
+ (fn prems =>
+  [ (rtac (and_def RS ssubst) 1), 
+    (REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)) ]);
+
+val conjunct1 = prove_goal HOL.thy "[| P & Q |] ==> P"
+ (fn prems =>
+   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
+     (REPEAT(ares_tac [impI] 1)) ]);
+
+val conjunct2 = prove_goal HOL.thy "[| P & Q |] ==> Q" 
+ (fn prems =>
+   [ (resolve_tac (prems RL [and_def RS subst] RL [spec] RL [mp]) 1),
+     (REPEAT(ares_tac [impI] 1)) ]);
+
+val conjE = prove_goal HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
+ (fn prems =>
+	 [cut_facts_tac prems 1, resolve_tac prems 1,
+	  etac conjunct1 1, etac conjunct2 1]);
+
+(** Disjunction *)
+
+val disjI1 = prove_goal HOL.thy "P ==> P|Q"
+ (fn [prem] =>
+	[rtac (or_def RS ssubst) 1,
+	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+
+val disjI2 = prove_goal HOL.thy "Q ==> P|Q"
+ (fn [prem] =>
+	[rtac (or_def RS ssubst) 1,
+	 REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
+
+val disjE = prove_goal HOL.thy "[| P | Q; P ==> R; Q ==> R |] ==> R"
+ (fn [a1,a2,a3] =>
+	[rtac (mp RS mp) 1, rtac spec 1, rtac (or_def RS subst) 1, rtac a1 1,
+	 rtac (a2 RS impI) 1, atac 1, rtac (a3 RS impI) 1, atac 1]);
+
+(** CCONTR -- classical logic **)
+
+val ccontr = prove_goal HOL.thy "(~P ==> False) ==> P"
+ (fn prems =>
+   [rtac (True_or_False RS (disjE RS eqTrueE)) 1, atac 1,
+    rtac spec 1, rtac (False_def RS subst) 1, resolve_tac prems 1,
+    rtac ssubst 1, atac 1, rtac (not_def RS ssubst) 1,
+    REPEAT (ares_tac [impI] 1) ]);
+
+val classical = prove_goal HOL.thy "(~P ==> P) ==> P"
+ (fn prems =>
+   [rtac ccontr 1,
+    REPEAT (ares_tac (prems@[notE]) 1)]);
+
+
+(*Double negation law*)
+val notnotD = prove_goal HOL.thy "~~P ==> P"
+ (fn [major]=>
+  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
+
+
+(** Unique existence **)
+
+val ex1I = prove_goal HOL.thy
+    "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
+ (fn prems =>
+  [ (rtac (Ex1_def RS ssubst) 1),
+    (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
+
+val ex1E = prove_goal HOL.thy
+    "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
+ (fn major::prems =>
+  [ (resolve_tac ([major] RL [Ex1_def RS subst] RL [exE]) 1),
+    (REPEAT (etac conjE 1 ORELSE ares_tac prems 1)) ]);
+
+
+(** Select: Hilbert's Epsilon-operator **)
+
+val select_equality = prove_goal HOL.thy
+    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
+ (fn prems => [ resolve_tac prems 1, 
+	        rtac selectI 1, 
+		resolve_tac prems 1 ]);
+
+(** Classical intro rules for disjunction and existential quantifiers *)
+
+val disjCI = prove_goal HOL.thy "(~Q ==> P) ==> P|Q"
+ (fn prems=>
+  [ (rtac classical 1),
+    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
+    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
+
+val excluded_middle = prove_goal HOL.thy "~P | P"
+ (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
+
+(*Classical implies (-->) elimination. *)
+val impCE = prove_goal HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
+ (fn major::prems=>
+  [ rtac (excluded_middle RS disjE) 1,
+    REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
+
+(*Classical <-> elimination. *)
+val iffCE = prove_goal HOL.thy
+    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
+ (fn major::prems =>
+  [ (rtac (major RS iffE) 1),
+    (REPEAT (DEPTH_SOLVE_1 
+	(eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
+
+val exCI = prove_goal HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)"
+ (fn prems=>
+  [ (rtac ccontr 1),
+    (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
+
+(*Required by the "classical" module*)
+val swap = prove_goal HOL.thy "~P ==> (~Q ==> P) ==> Q"
+ (fn major::prems=>
+  [ rtac ccontr 1, rtac (major RS notE) 1, REPEAT (ares_tac prems 1)]);
+
+(** Standard abbreviations **)
+
+fun stac th = rtac(th RS ssubst);
+fun sstac ths = EVERY' (map stac ths);
+fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
+
+end;
+
+open HOL_Lemmas;
+
Old_HOL