TFL/thms.sml

--- a/TFL/thms.sml	Tue Sep 05 18:53:21 2000 +0200
+++ b/TFL/thms.sml	Tue Sep 05 18:53:42 2000 +0200
@@ -1,37 +1,32 @@
-(*  Title:      TFL/thms
+(*  Title:      TFL/thms.sml
     ID:         $Id$
     Author:     Konrad Slind, Cambridge University Computer Laboratory
     Copyright   1997  University of Cambridge
 *)
 
-structure Thms : Thms_sig =
-struct
-   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
-   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
-   val CUT_DEF = cut_def
+signature Thms_sig =
+sig
+   val WF_INDUCTION_THM: thm
+   val WFREC_COROLLARY: thm
+   val CUT_DEF: thm
+   val SELECT_AX: thm
+   val eqT: thm
+   val rev_eq_mp: thm
+   val simp_thm: thm
+end;
 
-   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
-         val _ = by (strip_tac 1)
-         val _ = by (rtac selectI 1)
-         val _ = by (assume_tac 1)
-   in val SELECT_AX = result()
-   end;
+structure Thms: Thms_sig =
+struct
+   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
+   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
+   val CUT_DEF = get_thm WF.thy "cut_def";
 
-  (*-------------------------------------------------------------------------
-   *  Congruence rule needed for TFL, but not for general simplification
-   *-------------------------------------------------------------------------*)
-   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
-                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
-                          \ (Let M f = Let N g)";
-         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
-         val _ = by (rtac p2 1);
-         val _ = by (rtac refl 1);
-   in val LET_CONG = result() end;
+   val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
+     (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
 
    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
 
-   val eqT       = prove"(x = True) --> x"
-   val rev_eq_mp = prove"(x = y) --> y --> x"
-   val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
-
+   val eqT = prove"(x = True) --> x";
+   val rev_eq_mp = prove"(x = y) --> y --> x";
+   val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
 end;