TFL/thms.sml
author wenzelm
Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434 5e4bba59bfaa
parent 6498 1ebbe18fe236
child 9867 bf8300fa4238
permissions -rw-r--r--
use HOLogic.Not; export indexify_names;
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
6498
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3458
diff changeset
     9
   val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
1ebbe18fe236 Now for recdefs that omit the WF relation;
paulson
parents: 3458
diff changeset
    10
   val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
   val CUT_DEF = cut_def
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
         val _ = by (strip_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
         val _ = by (rtac selectI 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
         val _ = by (assume_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
   in val SELECT_AX = result()
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
  (*-------------------------------------------------------------------------
3458
5ff4bfab859c Removal of COND_CONG, which is just if_cong RS eq_reflection
paulson
parents: 3302
diff changeset
    21
   *  Congruence rule needed for TFL, but not for general simplification
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
   *-------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
                          \ (Let M f = Let N g)";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
         val _ = by (rtac p2 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
         val _ = by (rtac refl 1);
3458
5ff4bfab859c Removal of COND_CONG, which is just if_cong RS eq_reflection
paulson
parents: 3302
diff changeset
    29
   in val LET_CONG = result() end;
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
3273
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    31
   fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
3273
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    33
   val eqT       = prove"(x = True) --> x"
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    34
   val rev_eq_mp = prove"(x = y) --> y --> x"
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    35
   val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
end;