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