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;
paulson@2112
     1
structure Thms : Thms_sig =
paulson@2112
     2
struct
paulson@2112
     3
   type Thm = Thm.thm
paulson@2112
     4
paulson@2112
     5
   val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
paulson@2112
     6
   val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
paulson@2112
     7
   val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
paulson@2112
     8
   val CUT_DEF = cut_def
paulson@2112
     9
paulson@2112
    10
   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
paulson@2112
    11
         val _ = by (strip_tac 1)
paulson@2112
    12
         val _ = by (rtac selectI 1)
paulson@2112
    13
         val _ = by (assume_tac 1)
paulson@2112
    14
   in val SELECT_AX = result()
paulson@2112
    15
   end;
paulson@2112
    16
paulson@2112
    17
  (*-------------------------------------------------------------------------
paulson@2112
    18
   *  A useful congruence rule
paulson@2112
    19
   *-------------------------------------------------------------------------*)
paulson@2112
    20
   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
paulson@2112
    21
                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
paulson@2112
    22
                          \ (Let M f = Let N g)";
paulson@2112
    23
         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
paulson@2112
    24
         val _ = by (rtac p2 1);
paulson@2112
    25
         val _ = by (rtac refl 1);
paulson@2112
    26
   in val LET_CONG = result() RS eq_reflection
paulson@2112
    27
   end;
paulson@2112
    28
paulson@2112
    29
   val COND_CONG = if_cong RS eq_reflection;
paulson@2112
    30
paulson@2112
    31
   fun C f x y = f y x;
paulson@2112
    32
   fun prover thl = [fast_tac HOL_cs 1];
paulson@2112
    33
   val P = C (prove_goal HOL.thy) prover;
paulson@2112
    34
paulson@2112
    35
   val eqT       = P"(x = True) --> x"
paulson@2112
    36
   val rev_eq_mp = P"(x = y) --> y --> x"
paulson@2112
    37
   val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
paulson@2112
    38
paulson@2112
    39
end;