TFL/thms.sml
author wenzelm
Mon Sep 11 18:00:47 2000 +0200 (2000-09-11)
changeset 9924 3370f6aa3200
parent 9867 bf8300fa4238
child 9971 e0164f01d55a
permissions -rw-r--r--
updated;
     1 (*  Title:      TFL/thms.sml
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 signature Thms_sig =
     8 sig
     9    val WF_INDUCTION_THM: thm
    10    val WFREC_COROLLARY: thm
    11    val CUT_DEF: thm
    12    val SELECT_AX: thm
    13    val eqT: thm
    14    val rev_eq_mp: thm
    15    val simp_thm: thm
    16 end;
    17 
    18 structure Thms: Thms_sig =
    19 struct
    20    val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
    21    val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
    22    val CUT_DEF = get_thm WF.thy "cut_def";
    23 
    24    val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
    25      (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
    26 
    27    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    28 
    29    val eqT = prove"(x = True) --> x";
    30    val rev_eq_mp = prove"(x = y) --> y --> x";
    31    val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
    32 end;