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;
```
(*  Title:      TFL/thms
ID:         \$Id\$
Author:     Konrad Slind, Cambridge University Computer Laboratory
*)

structure Thms : Thms_sig =
struct
val WFREC_COROLLARY = get_thm WF.thy "tfl_wfrec"
val WF_INDUCTION_THM = get_thm WF.thy "tfl_wf_induct"
val CUT_DEF = cut_def

local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
val _ = by (strip_tac 1)
val _ = by (rtac selectI 1)
val _ = by (assume_tac 1)
in val SELECT_AX = result()
end;

(*-------------------------------------------------------------------------
*  Congruence rule needed for TFL, but not for general simplification
*-------------------------------------------------------------------------*)
local val [p1,p2] = goal HOL.thy "(M = N) ==> \
\ (!!x. ((x = N) ==> (f x = g x))) ==> \
\ (Let M f = Let N g)";
val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
val _ = by (rtac p2 1);
val _ = by (rtac refl 1);
in val LET_CONG = result() end;

fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);

val eqT       = prove"(x = True) --> x"
val rev_eq_mp = prove"(x = y) --> y --> x"
val simp_thm  = prove"(x-->y) --> (x = x') --> (x' --> y)"

end;
```