TFL/thms.sml
changeset 9867 bf8300fa4238
parent 6498 1ebbe18fe236
child 9971 e0164f01d55a
equal deleted inserted replaced
9866:90cbf68b9227 9867:bf8300fa4238
     1 (*  Title:      TFL/thms
     1 (*  Title:      TFL/thms.sml
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     4     Copyright   1997  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 structure Thms : Thms_sig =
     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 =
     8 struct
    19 struct
     9    val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
    20    val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec";
    10    val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
    21    val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct";
    11    val CUT_DEF = cut_def
    22    val CUT_DEF = get_thm WF.thy "cut_def";
    12 
    23 
    13    local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
    24    val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
    14          val _ = by (strip_tac 1)
    25      (fn _ => [strip_tac 1, rtac selectI 1, assume_tac 1]);
    15          val _ = by (rtac selectI 1)
       
    16          val _ = by (assume_tac 1)
       
    17    in val SELECT_AX = result()
       
    18    end;
       
    19 
       
    20   (*-------------------------------------------------------------------------
       
    21    *  Congruence rule needed for TFL, but not for general simplification
       
    22    *-------------------------------------------------------------------------*)
       
    23    local val [p1,p2] = goal HOL.thy "(M = N) ==> \
       
    24                           \ (!!x. ((x = N) ==> (f x = g x))) ==> \
       
    25                           \ (Let M f = Let N g)";
       
    26          val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
       
    27          val _ = by (rtac p2 1);
       
    28          val _ = by (rtac refl 1);
       
    29    in val LET_CONG = result() end;
       
    30 
    26 
    31    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    27    fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
    32 
    28 
    33    val eqT       = prove"(x = True) --> x"
    29    val eqT = prove"(x = True) --> x";
    34    val rev_eq_mp = prove"(x = y) --> y --> x"
    30    val rev_eq_mp = prove"(x = y) --> y --> x";
    35    val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
    31    val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
    36 
       
    37 end;
    32 end;