# HG changeset patch # User lcp # Date 797162374 -7200 # Node ID 5c9654e2e3de761f24bd8fc5e7e02a8f174ba22e # Parent a7693f30065dfe53123a73969c3ceaf6500d8936 Recoded with help from Toby to use rewriting instead of the subst rule -- the latter was too slow. But it must resort to the subst rule if the equality contains Vars. diff -r a7693f30065d -r 5c9654e2e3de src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Thu Apr 06 11:55:51 1995 +0200 +++ b/src/Provers/hypsubst.ML Thu Apr 06 11:59:34 1995 +0200 @@ -1,27 +1,50 @@ (* Title: Provers/hypsubst ID: $Id$ - Author: Martin D Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson + Copyright 1995 University of Cambridge + +Tactic to substitute using the assumption x=t in the rest of the subgoal, +and to delete that assumption. Original version due to Martin Coen. + +This version uses the simplifier, and requires it to be already present. + +Test data: -Martin Coen's tactic for substitution in the hypotheses +goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; +goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; +goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a"; +goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a"; + +by (hyp_subst_tac 1); +by (bound_hyp_subst_tac 1); + +Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) +goal thy "P(a) --> (EX y. a=y --> P(f(a)))"; *) signature HYPSUBST_DATA = sig - val dest_eq : term -> term*term - val imp_intr : thm (* (P ==> Q) ==> P-->Q *) - val rev_mp : thm (* [| P; P-->Q |] ==> Q *) - val subst : thm (* [| a=b; P(a) |] ==> P(b) *) - val sym : thm (* a=b ==> b=a *) + structure Simplifier : SIMPLIFIER + val dest_eq : term -> term*term + val eq_reflection : thm (* a=b ==> a==b *) + val imp_intr : thm (* (P ==> Q) ==> P-->Q *) + val rev_mp : thm (* [| P; P-->Q |] ==> Q *) + val subst : thm (* [| a=b; P(a) |] ==> P(b) *) + val sym : thm (* a=b ==> b=a *) end; + signature HYPSUBST = sig - val bound_hyp_subst_tac : int -> tactic - val hyp_subst_tac : int -> tactic + val bound_hyp_subst_tac : int -> tactic + val hyp_subst_tac : int -> tactic (*exported purely for debugging purposes*) - val eq_var : bool -> term -> int * thm - val inspect_pair : bool -> term * term -> thm + val gen_hyp_subst_tac : bool -> int -> tactic + val vars_gen_hyp_subst_tac : bool -> int -> tactic + val eq_var : bool -> bool -> term -> int * bool + val inspect_pair : bool -> bool -> term * term -> bool + val mk_eqs : thm -> thm list + val thin_leading_eqs_tac : bool -> int -> int -> tactic end; functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = @@ -33,55 +56,128 @@ fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); -(*It's not safe to substitute for a constant; consider 0=1. - It's not safe to substitute for x=t[x] since x is not eliminated. - It's not safe to substitute for a Var; what if it appears in other goals? - It's not safe to substitute for a variable free in the premises, - but how could we check for this?*) -fun inspect_pair bnd (t,u) = - case (Pattern.eta_contract t, Pattern.eta_contract u) of - (Bound i, _) => if loose(i,u) then raise Match - else sym (*eliminates t*) - | (_, Bound i) => if loose(i,t) then raise Match - else asm_rl (*eliminates u*) - | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match - else sym (*eliminates t*) - | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match - else asm_rl (*eliminates u*) +local val odot = ord"." +in +(*Simplifier turns Bound variables to dotted Free variables: + change it back (any Bound variable will do) +*) +fun contract t = + case Pattern.eta_contract t of + Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) + | t' => t' +end; + +fun has_vars t = maxidx_of_term t <> ~1; + +(*If novars then we forbid Vars in the equality. + If bnd then we only look for Bound (or dotted Free) variables to eliminate. + When can we safely delete the equality? + Not if it equates two constants; consider 0=1. + Not if it resembles x=t[x], since substitution does not eliminate x. + Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) + Not if it involves a variable free in the premises, + but we can't check for this -- hence bnd and bound_hyp_subst_tac + Prefer to eliminate Bound variables if possible. + Result: true = use as is, false = reorient first *) +fun inspect_pair bnd novars (t,u) = + case (contract t, contract u) of + (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u + then raise Match + else true (*eliminates t*) + | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t + then raise Match + else false (*eliminates u*) + | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse + novars andalso has_vars u + then raise Match + else true (*eliminates t*) + | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse + novars andalso has_vars t + then raise Match + else false (*eliminates u*) | _ => raise Match; (*Locates a substitutable variable on the left (resp. right) of an equality - assumption. Returns the number of intervening assumptions, paried with - the rule asm_rl (resp. sym). *) -fun eq_var bnd = + assumption. Returns the number of intervening assumptions. *) +fun eq_var bnd novars = let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t | eq_var_aux k (Const("==>",_) $ A $ B) = - ((k, inspect_pair bnd (dest_eq A)) - (*Exception Match comes from inspect_pair or dest_eq*) + ((k, inspect_pair bnd novars (dest_eq A)) + (*Exception comes from inspect_pair or dest_eq*) handle Match => eq_var_aux (k+1) B) | eq_var_aux k _ = raise EQ_VAR in eq_var_aux 0 end; -(*Select a suitable equality assumption and substitute throughout the subgoal - Replaces only Bound variables if bnd is true*) -fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => +(*We do not try to delete ALL equality assumptions at once. But + it is easy to handle several consecutive equality assumptions in a row. + Note that we have to inspect the proof state after doing the rewriting, + since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality + must NOT be deleted. Tactic must rotate or delete m assumptions. +*) +fun thin_leading_eqs_tac bnd m i = STATE(fn state => + let fun count [] = 0 + | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); + 1 + count Bs) + handle Match => 0) + val (_,_,Bi,_) = dest_state(state,i) + val j = min [m, count (Logic.strip_assums_hyp Bi)] + in REPEAT_DETERM_N j (etac thin_rl i) THEN + REPEAT_DETERM_N (m-j) (etac revcut_rl i) + end); + +(*For the simpset. Adds ALL suitable equalities, even if not first! + No vars are allowed here, as simpsets are built from meta-assumptions*) +fun mk_eqs th = + [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) + then th RS Data.eq_reflection + else symmetric(th RS Data.eq_reflection) (*reorient*) ] + handle Match => []; (*Exception comes from inspect_pair or dest_eq*) + +local open Simplifier +in + + val hyp_subst_ss = empty_ss setmksimps mk_eqs + + (*Select a suitable equality assumption and substitute throughout the subgoal + Replaces only Bound variables if bnd is true*) + fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => + let val (_,_,Bi,_) = dest_state(state,i) + val n = length(Logic.strip_assums_hyp Bi) - 1 + val (k,_) = eq_var bnd true Bi + in + EVERY [REPEAT_DETERM_N k (etac revcut_rl i), + asm_full_simp_tac hyp_subst_ss i, + etac thin_rl i, + thin_leading_eqs_tac bnd (n-k) i] + end + handle THM _ => no_tac | EQ_VAR => no_tac)); + +end; + +val ssubst = standard (sym RS subst); + +(*Old version of the tactic above -- slower but the only way + to handle equalities containing Vars.*) +fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => let val (_,_,Bi,_) = dest_state(state,i) val n = length(Logic.strip_assums_hyp Bi) - 1 - val (k,symopt) = eq_var bnd Bi + val (k,symopt) = eq_var bnd false Bi in EVERY [REPEAT_DETERM_N k (etac rev_mp i), etac revcut_rl i, REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (symopt RS subst) i, + etac (if symopt then ssubst else subst) i, REPEAT_DETERM_N n (rtac imp_intr i)] end handle THM _ => no_tac | EQ_VAR => no_tac)); (*Substitutes for Free or Bound variables*) -val hyp_subst_tac = gen_hyp_subst_tac false; +val hyp_subst_tac = + gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; (*Substitutes for Bound variables only -- this is always safe*) -val bound_hyp_subst_tac = gen_hyp_subst_tac true; +val bound_hyp_subst_tac = + gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; end end;