# HG changeset patch
# User wenzelm
# Date 878056091 -3600
# Node ID 90aebb69c04ecc1c0467bb94c6101b08a3ebd38f
# Parent  92874142156b1692946a2580a9a099770ad75eed
eq_thm moved to thm.ML;
store ProtoPure lemmas;

diff -r 92874142156b -r 90aebb69c04e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Oct 28 17:27:10 1997 +0100
+++ b/src/Pure/drule.ML	Tue Oct 28 17:28:11 1997 +0100
@@ -333,18 +333,9 @@
 end;
 
 
-(** theorem equality test is exported and used by BEST_FIRST **)
+(** theorem equality **)
 
-(*equality of theorems uses equality of signatures and
-  the a-convertible test for terms*)
-fun eq_thm (th1,th2) =
-    let val {sign=sg1, shyps=shyps1, hyps=hyps1, prop=prop1, ...} = rep_thm th1
-        and {sign=sg2, shyps=shyps2, hyps=hyps2, prop=prop2, ...} = rep_thm th2
-    in  Sign.eq_sg (sg1,sg2) andalso
-        eq_set_sort (shyps1, shyps2) andalso
-        aconvs(hyps1,hyps2) andalso
-        prop1 aconv prop2
-    end;
+val eq_thm = Thm.eq_thm;
 
 (*equality of theorems using similarity of signatures,
   i.e. the theorems belong to the same theory but not necessarily to the same
@@ -388,19 +379,21 @@
 
 (*** Meta-Rewriting Rules ***)
 
+fun store_thm name thm = PureThy.smart_store_thm (name, standard thm);
+
 val reflexive_thm =
   let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS)))
-  in Thm.reflexive cx end;
+  in store_thm "reflexive" (Thm.reflexive cx) end;
 
 val symmetric_thm =
   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
-  in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
+  in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end;
 
 val transitive_thm =
   let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT)
       val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT)
       val xythm = Thm.assume xy and yzthm = Thm.assume yz
-  in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
+  in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end;
 
 (** Below, a "conversion" has type cterm -> thm **)
 
@@ -486,27 +479,29 @@
 (*** Some useful meta-theorems ***)
 
 (*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT));
+val asm_rl =
+  store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT)));
 
 (*Meta-level cut rule: [| V==>W; V |] ==> W *)
-val cut_rl = trivial(read_cterm (sign_of ProtoPure.thy)
-        ("PROP ?psi ==> PROP ?theta", propT));
+val cut_rl =
+  store_thm "cut_rl"
+    (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT)));
 
 (*Generalized elim rule for one conclusion; cut_rl with reversed premises:
      [| PROP V;  PROP V ==> PROP W |] ==> PROP W *)
 val revcut_rl =
   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
       and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT);
-  in  standard (implies_intr V
-                (implies_intr VW
-                 (implies_elim (assume VW) (assume V))))
+  in
+    store_thm "revcut_rl"
+      (implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V))))
   end;
 
 (*for deleting an unwanted assumption*)
 val thin_rl =
   let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
       and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT);
-  in  standard (implies_intr V (implies_intr W (assume W)))
+  in  store_thm "thin_rl" (implies_intr V (implies_intr W (assume W)))
   end;
 
 (* (!!x. PROP ?V) == PROP ?V       Allows removal of redundant parameters*)
@@ -514,8 +509,10 @@
   let val V  = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT)
       and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT)
       and x  = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS));
-  in  standard (equal_intr (implies_intr QV (forall_elim x (assume QV)))
-                           (implies_intr V  (forall_intr x (assume V))))
+  in
+    store_thm "triv_forall_equality"
+      (equal_intr (implies_intr QV (forall_elim x (assume QV)))
+        (implies_intr V  (forall_intr x (assume V))))
   end;
 
 (* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
@@ -530,7 +527,7 @@
       val minor1 = assume cminor1;
       val cminor2 = read_cterm (sign_of ProtoPure.thy)  ("PROP PhiB", propT);
       val minor2 = assume cminor2;
-  in standard
+  in store_thm "swap_prems_rl"
        (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
          (implies_elim (implies_elim major minor1) minor2))))
   end;
@@ -542,10 +539,9 @@
 val equal_intr_rule =
   let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT)
       and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT)
-  in  equal_intr (assume PQ) (assume QP)
-      |> implies_intr QP
-      |> implies_intr PQ
-      |> standard
+  in
+    store_thm "equal_intr_rule"
+      (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   end;
 
 end;