TFL/thms.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
     1 structure Thms : Thms_sig =
     2 struct
     3    type Thm = Thm.thm
     4 
     5    val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
     6    val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
     7    val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
     8    val CUT_DEF = cut_def
     9 
    10    local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
    11          val _ = by (strip_tac 1)
    12          val _ = by (rtac selectI 1)
    13          val _ = by (assume_tac 1)
    14    in val SELECT_AX = result()
    15    end;
    16 
    17   (*-------------------------------------------------------------------------
    18    *  A useful congruence rule
    19    *-------------------------------------------------------------------------*)
    20    local val [p1,p2] = goal HOL.thy "(M = N) ==> \
    21                           \ (!!x. ((x = N) ==> (f x = g x))) ==> \
    22                           \ (Let M f = Let N g)";
    23          val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
    24          val _ = by (rtac p2 1);
    25          val _ = by (rtac refl 1);
    26    in val LET_CONG = result() RS eq_reflection
    27    end;
    28 
    29    val COND_CONG = if_cong RS eq_reflection;
    30 
    31    fun C f x y = f y x;
    32    fun prover thl = [fast_tac HOL_cs 1];
    33    val P = C (prove_goal HOL.thy) prover;
    34 
    35    val eqT       = P"(x = True) --> x"
    36    val rev_eq_mp = P"(x = y) --> y --> x"
    37    val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
    38 
    39 end;