stac now handles definitions as well as equalities
authorpaulson
Thu Aug 13 17:28:52 1998 +0200 (1998-08-13)
changeset 530901c2b317da88
parent 5308 3ca4da83012c
child 5310 3e14d6d66dab
stac now handles definitions as well as equalities
src/FOL/IFOL.ML
src/HOL/HOL.ML
     1.1 --- a/src/FOL/IFOL.ML	Thu Aug 13 17:28:19 1998 +0200
     1.2 +++ b/src/FOL/IFOL.ML	Thu Aug 13 17:28:52 1998 +0200
     1.3 @@ -236,11 +236,29 @@
     1.4  (** ~ b=a ==> ~ a=b **)
     1.5  val [not_sym] = compose(sym,2,contrapos);
     1.6  
     1.7 +
     1.8 +(* Two theorms for rewriting only one instance of a definition:
     1.9 +   the first for definitions of formulae and the second for terms *)
    1.10 +
    1.11 +val prems = goal IFOL.thy "(A == B) ==> A <-> B";
    1.12 +by (rewrite_goals_tac prems);
    1.13 +by (rtac iff_refl 1);
    1.14 +qed "def_imp_iff";
    1.15 +
    1.16 +val prems = goal IFOL.thy "(A == B) ==> A = B";
    1.17 +by (rewrite_goals_tac prems);
    1.18 +by (rtac refl 1);
    1.19 +qed "def_imp_eq";
    1.20 +
    1.21  (*Substitution: rule and tactic*)
    1.22  bind_thm ("ssubst", sym RS subst);
    1.23  
    1.24 -(*Fails unless the substitution has an effect*)
    1.25 -fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
    1.26 +(*Apply an equality or definition ONCE.
    1.27 +  Fails unless the substitution has an effect*)
    1.28 +fun stac th = 
    1.29 +  let val th' = th RS def_imp_eq handle _ => th
    1.30 +  in  CHANGED_GOAL (rtac (th' RS ssubst))
    1.31 +  end;
    1.32  
    1.33  (*A special case of ex1E that would otherwise need quantifier expansion*)
    1.34  qed_goal "ex1_equalsE" IFOL.thy
    1.35 @@ -382,20 +400,6 @@
    1.36  by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
    1.37  qed "disj_imp_disj";
    1.38  
    1.39 -(* The following two theorms are useful when rewriting only one instance  *) 
    1.40 -(* of a definition                                                        *)
    1.41 -(* first one for definitions of formulae and the second for terms         *)
    1.42 -
    1.43 -val prems = goal IFOL.thy "(A == B) ==> A <-> B";
    1.44 -by (rewrite_goals_tac prems);
    1.45 -by (rtac iff_refl 1);
    1.46 -qed "def_imp_iff";
    1.47 -
    1.48 -val prems = goal IFOL.thy "(A == B) ==> A = B";
    1.49 -by (rewrite_goals_tac prems);
    1.50 -by (rtac refl 1);
    1.51 -qed "def_imp_eq";
    1.52 -
    1.53  
    1.54  (** strip ALL and --> from proved goal while preserving ALL-bound var names **)
    1.55  
     2.1 --- a/src/HOL/HOL.ML	Thu Aug 13 17:28:19 1998 +0200
     2.2 +++ b/src/HOL/HOL.ML	Thu Aug 13 17:28:52 1998 +0200
     2.3 @@ -23,6 +23,11 @@
     2.4   (fn prems =>
     2.5          [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
     2.6  
     2.7 +val prems = goal thy "(A == B) ==> A = B";
     2.8 +by (rewrite_goals_tac prems);
     2.9 +by (rtac refl 1);
    2.10 +qed "def_imp_eq";
    2.11 +
    2.12  (*Useful with eresolve_tac for proving equalties from known equalities.
    2.13          a = b
    2.14          |   |
    2.15 @@ -353,8 +358,12 @@
    2.16  
    2.17  (** Standard abbreviations **)
    2.18  
    2.19 -(*Fails unless the substitution has an effect*)
    2.20 -fun stac th = CHANGED_GOAL (rtac (th RS ssubst));
    2.21 +(*Apply an equality or definition ONCE.
    2.22 +  Fails unless the substitution has an effect*)
    2.23 +fun stac th = 
    2.24 +  let val th' = th RS def_imp_eq handle _ => th
    2.25 +  in  CHANGED_GOAL (rtac (th' RS ssubst))
    2.26 +  end;
    2.27  
    2.28  fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
    2.29