--- a/src/Provers/hypsubst.ML Fri Aug 04 22:57:37 2000 +0200
+++ b/src/Provers/hypsubst.ML Fri Aug 04 22:58:23 2000 +0200
@@ -1,28 +1,28 @@
-(* Title: Provers/hypsubst
+(* Title: Provers/hypsubst.ML
ID: $Id$
- Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson
+ Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson
Copyright 1995 University of Cambridge
-Tactic to substitute using (at least) the assumption x=t in the rest of the
-subgoal, and to delete (at least) that assumption.
+Tactic to substitute using (at least) the assumption x=t in the rest of the
+subgoal, and to delete (at least) that assumption.
Original version due to Martin Coen.
This version uses the simplifier, and requires it to be already present.
Test data:
-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";
+Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
+Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
+Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
+Goal "!!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)))";
+Goal "P(a) --> (EX y. a=y --> P(f(a)))";
-goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
+Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
\ P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
by (blast_hyp_subst_tac (ref true) 1);
*)
@@ -31,13 +31,14 @@
sig
structure Simplifier : SIMPLIFIER
val dest_Trueprop : term -> term
- val dest_eq : term -> term*term*typ
- val dest_imp : 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 *)
+ val dest_eq : term -> term*term*typ
+ val dest_imp : term -> term*term
+ val eq_reflection : thm (* a=b ==> a==b *)
+ val rev_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 *)
val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *)
end;
@@ -54,11 +55,13 @@
val inspect_pair : bool -> bool -> term * term * typ -> bool
val mk_eqs : thm -> thm list
val thin_leading_eqs_tac : bool -> int -> int -> tactic
+ val stac : thm -> int -> tactic
+ val hypsubst_setup : (theory -> theory) list
end;
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
struct
exception EQ_VAR;
@@ -67,58 +70,58 @@
local val odot = ord"."
in
-(*Simplifier turns Bound variables to dotted Free variables:
+(*Simplifier turns Bound variables to dotted Free variables:
change it back (any Bound variable will do)
*)
fun contract t =
case Pattern.eta_contract_atom t of
- Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
+ 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.
+ 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; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
- Not if it involves a variable free in the premises,
+ 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,T) =
- if novars andalso maxidx_of_typ T <> ~1
+ if novars andalso maxidx_of_typ T <> ~1
then raise Match (*variables in the type!*)
else
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*)
+ (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. *)
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 novars
- (Data.dest_eq (Data.dest_Trueprop A)))
- (*Exception comes from inspect_pair or dest_eq*)
- handle _ => eq_var_aux (k+1) B)
- | eq_var_aux k _ = raise EQ_VAR
+ | eq_var_aux k (Const("==>",_) $ A $ B) =
+ ((k, inspect_pair bnd novars
+ (Data.dest_eq (Data.dest_Trueprop A)))
+ (*Exception comes from inspect_pair or dest_eq*)
+ handle _ => eq_var_aux (k+1) B)
+ | eq_var_aux k _ = raise EQ_VAR
in eq_var_aux 0 end;
(*We do not try to delete ALL equality assumptions at once. But
@@ -129,9 +132,9 @@
*)
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
let fun count [] = 0
- | count (A::Bs) = ((inspect_pair bnd true
- (Data.dest_eq (Data.dest_Trueprop A));
- 1 + count Bs)
+ | count (A::Bs) = ((inspect_pair bnd true
+ (Data.dest_eq (Data.dest_Trueprop A));
+ 1 + count Bs)
handle _ => 0)
val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i
@@ -139,14 +142,14 @@
(*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
- (Data.dest_Trueprop (#prop (rep_thm th))))
+fun mk_eqs th =
+ [ if inspect_pair false false (Data.dest_eq
+ (Data.dest_Trueprop (#prop (rep_thm th))))
then th RS Data.eq_reflection
- else symmetric(th RS Data.eq_reflection) (*reorient*) ]
+ else symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle _ => []; (*Exception comes from inspect_pair or dest_eq*)
-local open Simplifier
+local open Simplifier
in
val hyp_subst_ss = empty_ss setmksimps mk_eqs
@@ -154,15 +157,15 @@
(*Select a suitable equality assumption and substitute throughout the subgoal
Replaces only Bound variables if bnd is true*)
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
- let val n = length(Logic.strip_assums_hyp Bi) - 1
- val (k,_) = eq_var bnd true Bi
- in
- DETERM (EVERY [rotate_tac k 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);
+ let val n = length(Logic.strip_assums_hyp Bi) - 1
+ val (k,_) = eq_var bnd true Bi
+ in
+ DETERM (EVERY [rotate_tac k 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;
@@ -174,14 +177,14 @@
to handle equalities containing Vars.*)
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
let val n = length(Logic.strip_assums_hyp Bi) - 1
- val (k,symopt) = eq_var bnd false Bi
- in
- DETERM
+ val (k,symopt) = eq_var bnd false Bi
+ in
+ DETERM
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
- rotate_tac 1 i,
- REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
- etac (if symopt then ssubst else Data.subst) i,
- REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
+ rotate_tac 1 i,
+ REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
+ etac (if symopt then ssubst else Data.subst) i,
+ REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
@@ -190,56 +193,73 @@
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
(*Substitutes for Bound variables only -- this is always safe*)
-val bound_hyp_subst_tac =
+val bound_hyp_subst_tac =
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
-(** Version for Blast_tac. Hyps that are affected by the substitution are
+(** Version for Blast_tac. Hyps that are affected by the substitution are
moved to the front. Defect: even trivial changes are noticed, such as
substitutions in the arguments of a function Var. **)
(*final re-reversal of the changed assumptions*)
fun reverse_n_tac 0 i = all_tac
| reverse_n_tac 1 i = rotate_tac ~1 i
- | reverse_n_tac n i =
+ | reverse_n_tac n i =
REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
-fun all_imp_intr_tac hyps i =
+fun all_imp_intr_tac hyps i =
let fun imptac (r, []) st = reverse_n_tac r i st
- | imptac (r, hyp::hyps) st =
- let val (hyp',_) = List.nth (prems_of st, i-1) |>
- Logic.strip_assums_concl |>
- Data.dest_Trueprop |> Data.dest_imp
- val (r',tac) = if Pattern.aeconv (hyp,hyp')
- then (r, imp_intr_tac i THEN rotate_tac ~1 i)
- else (*leave affected hyps at end*)
- (r+1, imp_intr_tac i)
- in
- case Seq.pull(tac st) of
- None => Seq.single(st)
- | Some(st',_) => imptac (r',hyps) st'
- end handle _ => error "?? in blast_hyp_subst_tac"
+ | imptac (r, hyp::hyps) st =
+ let val (hyp',_) = List.nth (prems_of st, i-1) |>
+ Logic.strip_assums_concl |>
+ Data.dest_Trueprop |> Data.dest_imp
+ val (r',tac) = if Pattern.aeconv (hyp,hyp')
+ then (r, imp_intr_tac i THEN rotate_tac ~1 i)
+ else (*leave affected hyps at end*)
+ (r+1, imp_intr_tac i)
+ in
+ case Seq.pull(tac st) of
+ None => Seq.single(st)
+ | Some(st',_) => imptac (r',hyps) st'
+ end handle _ => error "?? in blast_hyp_subst_tac"
in imptac (0, rev hyps) end;
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
let val (k,symopt) = eq_var false false Bi
- val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
+ val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
(*omit selected equality, returning other hyps*)
- val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
- val n = length hyps
- in
- if !trace then writeln "Substituting an equality" else ();
- DETERM
+ val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
+ val n = length hyps
+ in
+ if !trace then writeln "Substituting an equality" else ();
+ DETERM
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
- rotate_tac 1 i,
- REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
- etac (if symopt then ssubst else Data.subst) i,
- all_imp_intr_tac hyps i])
+ rotate_tac 1 i,
+ REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
+ etac (if symopt then ssubst else Data.subst) i,
+ all_imp_intr_tac hyps i])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
+
+(*apply an equality or definition ONCE;
+ fails unless the substitution has an effect*)
+fun stac th =
+ let val th' = th RS Data.rev_eq_reflection handle THM _ => th
+ in CHANGED_GOAL (rtac (th' RS ssubst)) end;
+
+
+(* proof method setup *)
+
+val subst_meth = Method.goal_args' Attrib.local_thm stac;
+val hypsubst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
+
+val hypsubst_setup =
+ [Method.add_methods
+ [("hypsubst", hypsubst_meth, "substitution using an assumption (improper)"),
+ ("subst", subst_meth, "substitution")]];
+
end;
-