# HG changeset patch
# User paulson
# Date 903022132 -7200
# Node ID 01c2b317da884a039d6495ce0ef56f3e91729a5e
# Parent  3ca4da83012c9359d2073c7e93687f1ce453573b
stac now handles definitions as well as equalities

diff -r 3ca4da83012c -r 01c2b317da88 src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Thu Aug 13 17:28:19 1998 +0200
+++ b/src/FOL/IFOL.ML	Thu Aug 13 17:28:52 1998 +0200
@@ -236,11 +236,29 @@
 (** ~ b=a ==> ~ a=b **)
 val [not_sym] = compose(sym,2,contrapos);
 
+
+(* Two theorms for rewriting only one instance of a definition:
+   the first for definitions of formulae and the second for terms *)
+
+val prems = goal IFOL.thy "(A == B) ==> A <-> B";
+by (rewrite_goals_tac prems);
+by (rtac iff_refl 1);
+qed "def_imp_iff";
+
+val prems = goal IFOL.thy "(A == B) ==> A = B";
+by (rewrite_goals_tac prems);
+by (rtac refl 1);
+qed "def_imp_eq";
+
 (*Substitution: rule and tactic*)
 bind_thm ("ssubst", sym RS subst);
 
-(*Fails unless the substitution has an effect*)
-fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
+(*Apply an equality or definition ONCE.
+  Fails unless the substitution has an effect*)
+fun stac th = 
+  let val th' = th RS def_imp_eq handle _ => th
+  in  CHANGED_GOAL (rtac (th' RS ssubst))
+  end;
 
 (*A special case of ex1E that would otherwise need quantifier expansion*)
 qed_goal "ex1_equalsE" IFOL.thy
@@ -382,20 +400,6 @@
 by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
 qed "disj_imp_disj";
 
-(* The following two theorms are useful when rewriting only one instance  *) 
-(* of a definition                                                        *)
-(* first one for definitions of formulae and the second for terms         *)
-
-val prems = goal IFOL.thy "(A == B) ==> A <-> B";
-by (rewrite_goals_tac prems);
-by (rtac iff_refl 1);
-qed "def_imp_iff";
-
-val prems = goal IFOL.thy "(A == B) ==> A = B";
-by (rewrite_goals_tac prems);
-by (rtac refl 1);
-qed "def_imp_eq";
-
 
 (** strip ALL and --> from proved goal while preserving ALL-bound var names **)
 
diff -r 3ca4da83012c -r 01c2b317da88 src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Thu Aug 13 17:28:19 1998 +0200
+++ b/src/HOL/HOL.ML	Thu Aug 13 17:28:52 1998 +0200
@@ -23,6 +23,11 @@
  (fn prems =>
         [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
 
+val prems = goal thy "(A == B) ==> A = B";
+by (rewrite_goals_tac prems);
+by (rtac refl 1);
+qed "def_imp_eq";
+
 (*Useful with eresolve_tac for proving equalties from known equalities.
         a = b
         |   |
@@ -353,8 +358,12 @@
 
 (** Standard abbreviations **)
 
-(*Fails unless the substitution has an effect*)
-fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
+(*Apply an equality or definition ONCE.
+  Fails unless the substitution has an effect*)
+fun stac th = 
+  let val th' = th RS def_imp_eq handle _ => th
+  in  CHANGED_GOAL (rtac (th' RS ssubst))
+  end;
 
 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);