TFL/thms.sml
author wenzelm
Wed, 26 Aug 1998 16:33:29 +0200
changeset 5374 6ef3742b6153
parent 3458 5ff4bfab859c
child 6498 1ebbe18fe236
permissions -rw-r--r--
moved images to gfx dir;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3302
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     1
(*  Title:      TFL/thms
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     2
    ID:         $Id$
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     4
    Copyright   1997  University of Cambridge
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     5
*)
404fe31fd8d2 New headers and other minor changes
paulson
parents: 3273
diff changeset
     6
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
structure Thms : Thms_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
struct
3191
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
     9
   val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    10
   val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
14bd6e5985f1 TFL now integrated with HOL (more work needed)
paulson
parents: 2112
diff changeset
    11
   val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
   val CUT_DEF = cut_def
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
         val _ = by (strip_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
         val _ = by (rtac selectI 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
         val _ = by (assume_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
   in val SELECT_AX = result()
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
  (*-------------------------------------------------------------------------
3458
5ff4bfab859c Removal of COND_CONG, which is just if_cong RS eq_reflection
paulson
parents: 3302
diff changeset
    22
   *  Congruence rule needed for TFL, but not for general simplification
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
   *-------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
                          \ (Let M f = Let N g)";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
         val _ = by (rtac p2 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
         val _ = by (rtac refl 1);
3458
5ff4bfab859c Removal of COND_CONG, which is just if_cong RS eq_reflection
paulson
parents: 3302
diff changeset
    30
   in val LET_CONG = result() end;
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
3273
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    32
   fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
3273
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    34
   val eqT       = prove"(x = True) --> x"
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    35
   val rev_eq_mp = prove"(x = y) --> y --> x"
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    36
   val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
end;