TFL/thms.sml
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 3458 5ff4bfab859c
child 6498 1ebbe18fe236
permissions -rw-r--r--
adapted extend_trfunsT;
     1 (*  Title:      TFL/thms
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 structure Thms : Thms_sig =
     8 struct
     9    val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
    10    val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
    11    val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
    12    val CUT_DEF = cut_def
    13 
    14    local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
    15          val _ = by (strip_tac 1)
    16          val _ = by (rtac selectI 1)
    17          val _ = by (assume_tac 1)
    18    in val SELECT_AX = result()
    19    end;
    20 
    21   (*-------------------------------------------------------------------------
    22    *  Congruence rule needed for TFL, but not for general simplification
    23    *-------------------------------------------------------------------------*)
    24    local val [p1,p2] = goal HOL.thy "(M = N) ==> \
    25                           \ (!!x. ((x = N) ==> (f x = g x))) ==> \
    26                           \ (Let M f = Let N g)";
    27          val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
    28          val _ = by (rtac p2 1);
    29          val _ = by (rtac refl 1);
    30    in val LET_CONG = result() end;
    31 
    32    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    33 
    34    val eqT       = prove"(x = True) --> x"
    35    val rev_eq_mp = prove"(x = y) --> y --> x"
    36    val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
    37 
    38 end;