TFL/thms.sml
author paulson
Fri, 03 Nov 2000 10:23:24 +0100
changeset 10368 f7e8abd8ea15
parent 10212 33fe2d701ddd
permissions -rw-r--r--
replaced Acc.thy by Advanced.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9867
wenzelm
parents: 6498
diff changeset
     1
(*  Title:      TFL/thms.sml
3302
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
9867
wenzelm
parents: 6498
diff changeset
     7
signature Thms_sig =
wenzelm
parents: 6498
diff changeset
     8
sig
wenzelm
parents: 6498
diff changeset
     9
   val WF_INDUCTION_THM: thm
wenzelm
parents: 6498
diff changeset
    10
   val WFREC_COROLLARY: thm
wenzelm
parents: 6498
diff changeset
    11
   val CUT_DEF: thm
wenzelm
parents: 6498
diff changeset
    12
   val SELECT_AX: thm
wenzelm
parents: 6498
diff changeset
    13
   val eqT: thm
wenzelm
parents: 6498
diff changeset
    14
   val rev_eq_mp: thm
wenzelm
parents: 6498
diff changeset
    15
   val simp_thm: thm
wenzelm
parents: 6498
diff changeset
    16
end;
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
9867
wenzelm
parents: 6498
diff changeset
    18
structure Thms: Thms_sig =
wenzelm
parents: 6498
diff changeset
    19
struct
10212
33fe2d701ddd *** empty log message ***
nipkow
parents: 9971
diff changeset
    20
   val WFREC_COROLLARY = get_thm Wellfounded_Recursion.thy "tfl_wfrec";
33fe2d701ddd *** empty log message ***
nipkow
parents: 9971
diff changeset
    21
   val WF_INDUCTION_THM = get_thm Wellfounded_Recursion.thy "tfl_wf_induct";
33fe2d701ddd *** empty log message ***
nipkow
parents: 9971
diff changeset
    22
   val CUT_DEF = get_thm Wellfounded_Recursion.thy "cut_def";
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
9867
wenzelm
parents: 6498
diff changeset
    24
   val SELECT_AX = prove_goal HOL.thy "!P x. P x --> P (Eps P)"
9971
e0164f01d55a renamed the select rules
paulson
parents: 9867
diff changeset
    25
     (fn _ => [strip_tac 1, rtac someI 1, assume_tac 1]);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
3273
114704740c86 Code tidying: removal of C combinator
paulson
parents: 3245
diff changeset
    27
   fun prove s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
9867
wenzelm
parents: 6498
diff changeset
    29
   val eqT = prove"(x = True) --> x";
wenzelm
parents: 6498
diff changeset
    30
   val rev_eq_mp = prove"(x = y) --> y --> x";
wenzelm
parents: 6498
diff changeset
    31
   val simp_thm = prove"(x-->y) --> (x = x') --> (x' --> y)";
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
end;