TFL/thms.sml
author paulson
Fri, 18 Oct 1996 12:41:04 +0200
changeset 2112 3902e9af752f
child 3191 14bd6e5985f1
permissions -rw-r--r--
Konrad Slind's TFL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     1
structure Thms : Thms_sig =
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     2
struct
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     3
   type Thm = Thm.thm
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     4
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     5
   val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     6
   val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     7
   val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     8
   val CUT_DEF = cut_def
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
     9
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    10
   local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    11
         val _ = by (strip_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    12
         val _ = by (rtac selectI 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    13
         val _ = by (assume_tac 1)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    14
   in val SELECT_AX = result()
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    15
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    16
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    17
  (*-------------------------------------------------------------------------
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    18
   *  A useful congruence rule
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    19
   *-------------------------------------------------------------------------*)
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    20
   local val [p1,p2] = goal HOL.thy "(M = N) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    21
                          \ (!!x. ((x = N) ==> (f x = g x))) ==> \
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    22
                          \ (Let M f = Let N g)";
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    23
         val _ = by (simp_tac (HOL_ss addsimps[Let_def,p1]) 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    24
         val _ = by (rtac p2 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    25
         val _ = by (rtac refl 1);
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    26
   in val LET_CONG = result() RS eq_reflection
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    27
   end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    28
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    29
   val COND_CONG = if_cong RS eq_reflection;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    30
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    31
   fun C f x y = f y x;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    32
   fun prover thl = [fast_tac HOL_cs 1];
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    33
   val P = C (prove_goal HOL.thy) prover;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    34
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    35
   val eqT       = P"(x = True) --> x"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    36
   val rev_eq_mp = P"(x = y) --> y --> x"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    37
   val simp_thm  = P"(x-->y) --> (x = x') --> (x' --> y)"
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    38
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    39
end;