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