added thin_refl to hyp_subst_tac
authoroheimb
Wed Nov 12 18:58:50 1997 +0100 (1997-11-12)
changeset 4223f60e3d2c81d3
parent 4222 d7573d6d0513
child 4224 79e205c3a82c
added thin_refl to hyp_subst_tac
src/FOL/ROOT.ML
src/FOLP/ROOT.ML
src/HOL/cladata.ML
src/Provers/hypsubst.ML
     1.1 --- a/src/FOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     1.2 +++ b/src/FOL/ROOT.ML	Wed Nov 12 18:58:50 1997 +0100
     1.3 @@ -34,6 +34,8 @@
     1.4    val rev_mp = rev_mp
     1.5    val subst = subst
     1.6    val sym = sym
     1.7 +  val thin_refl = prove_goal IFOL.thy 
     1.8 +		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
     1.9    end;
    1.10  
    1.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     2.1 --- a/src/FOLP/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     2.2 +++ b/src/FOLP/ROOT.ML	Wed Nov 12 18:58:50 1997 +0100
     2.3 @@ -39,6 +39,8 @@
     2.4    val rev_mp = rev_mp
     2.5    val subst = subst
     2.6    val sym = sym
     2.7 +  val thin_refl = prove_goal IFOLP.thy 
     2.8 +		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
     2.9    end;
    2.10  
    2.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     3.1 --- a/src/HOL/cladata.ML	Wed Nov 12 16:28:53 1997 +0100
     3.2 +++ b/src/HOL/cladata.ML	Wed Nov 12 18:58:50 1997 +0100
     3.3 @@ -21,6 +21,8 @@
     3.4    val rev_mp = rev_mp
     3.5    val subst = subst
     3.6    val sym = sym
     3.7 +  val thin_refl = prove_goal HOL.thy 
     3.8 +		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
     3.9    end;
    3.10  
    3.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     4.1 --- a/src/Provers/hypsubst.ML	Wed Nov 12 16:28:53 1997 +0100
     4.2 +++ b/src/Provers/hypsubst.ML	Wed Nov 12 18:58:50 1997 +0100
     4.3 @@ -3,8 +3,9 @@
     4.4      Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     4.5      Copyright   1995  University of Cambridge
     4.6  
     4.7 -Tactic to substitute using the assumption x=t in the rest of the subgoal,
     4.8 -and to delete that assumption.  Original version due to Martin Coen.
     4.9 +Tactic to substitute using (at least) the assumption x=t in the rest of the 
    4.10 +subgoal, and to delete (at least) that assumption. 
    4.11 +Original version due to Martin Coen.
    4.12  
    4.13  This version uses the simplifier, and requires it to be already present.
    4.14  
    4.15 @@ -31,7 +32,8 @@
    4.16    val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    4.17    val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    4.18    val sym	       : thm		   (* a=b ==> b=a *)
    4.19 -  end;
    4.20 +  val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    4.21 +end;
    4.22  
    4.23  
    4.24  signature HYPSUBST =
    4.25 @@ -174,8 +176,8 @@
    4.26        handle THM _ => no_tac | EQ_VAR => no_tac);
    4.27  
    4.28  (*Substitutes for Free or Bound variables*)
    4.29 -val hyp_subst_tac = 
    4.30 -    gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;
    4.31 +val hyp_subst_tac = FIRST' [ematch_tac [thin_refl],
    4.32 +        gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
    4.33  
    4.34  (*Substitutes for Bound variables only -- this is always safe*)
    4.35  val bound_hyp_subst_tac =