src/Pure/drule.ML
 changeset 4016 90aebb69c04e parent 3991 4cb2f2422695 child 4057 edd8cb346109
```--- 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;```