0

1 
(* Title: Provers/hypsubst


2 
ID: $Id$

646

3 
Author: Martin D Coen, Cambridge University Computer Laboratory

0

4 
Copyright 1993 University of Cambridge


5 


6 
Martin Coen's tactic for substitution in the hypotheses


7 
*)


8 


9 
signature HYPSUBST_DATA =


10 
sig


11 
val dest_eq: term > term*term


12 
val imp_intr: thm (* (P ==> Q) ==> P>Q *)


13 
val rev_cut_eq: thm (* [ a=b; a=b ==> R ] ==> R *)


14 
val rev_mp: thm (* [ P; P>Q ] ==> Q *)


15 
val subst: thm (* [ a=b; P(a) ] ==> P(b) *)


16 
val sym: thm (* a=b ==> b=a *)


17 
end;


18 


19 
signature HYPSUBST =


20 
sig


21 
val bound_hyp_subst_tac : int > tactic


22 
val hyp_subst_tac : int > tactic


23 
(*exported purely for debugging purposes*)


24 
val eq_var : bool > term > term * thm


25 
val inspect_pair : bool > term * term > term * thm


26 
val liftvar : int > typ list > term


27 
end;


28 


29 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =


30 
struct


31 


32 
local open Data in


33 


34 
fun REPEATN 0 tac = all_tac


35 
 REPEATN n tac = Tactic(fn state =>


36 
tapply(tac THEN REPEATN (n1) tac, state));


37 


38 
local


39 
val T = case #1 (types_sorts rev_cut_eq) ("a",0) of


40 
Some T => T


41 
 None => error"No such variable in rev_cut_eq"


42 
in


43 
fun liftvar inc paramTs = Var(("a",inc), paramTs > incr_tvar inc T);


44 
end;


45 


46 
exception EQ_VAR;


47 


48 
fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);


49 


50 
(*It's not safe to substitute for a constant; consider 0=1.


51 
It's not safe to substitute for x=t[x] since x is not eliminated.

646

52 
It's not safe to substitute for a Var; what if it appears in other goals?

0

53 
It's not safe to substitute for a variable free in the premises,


54 
but how could we check for this?*)


55 
fun inspect_pair bnd (t,u) =


56 
case (Pattern.eta_contract t, Pattern.eta_contract u) of


57 
(Bound i, _) => if loose(i,u) then raise Match


58 
else (t, asm_rl)


59 
 (_, Bound i) => if loose(i,t) then raise Match


60 
else (u, sym)


61 
 (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match


62 
else (t, asm_rl)


63 
 (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match


64 
else (u, sym)


65 
 _ => raise Match;


66 


67 
(* Extracts the name of the variable on the left (resp. right) of an equality


68 
assumption. Returns the rule asm_rl (resp. sym). *)


69 
fun eq_var bnd (Const("all",_) $ Abs(_,_,t)) = eq_var bnd t


70 
 eq_var bnd (Const("==>",_) $ A $ B) =


71 
(inspect_pair bnd (dest_eq A)


72 
(*Match comes from inspect_pair or dest_eq*)


73 
handle Match => eq_var bnd B)


74 
 eq_var bnd _ = raise EQ_VAR;


75 


76 
(*Lift and instantiate a rule wrt the given state and subgoal number *)


77 
fun lift_instpair (state, i, t, rule) =


78 
let val {maxidx,sign,...} = rep_thm state


79 
val (_, _, Bi, _) = dest_state(state,i)


80 
val params = Logic.strip_params Bi


81 
val var = liftvar (maxidx+1) (map #2 params)


82 
and u = Unify.rlist_abs(rev params, t)

231

83 
and cterm = cterm_of sign

0

84 
in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule)


85 
end;


86 


87 
fun eres_instpair_tac t rule i = STATE (fn state =>


88 
compose_tac (true, lift_instpair (state, i, t, rule),


89 
length(prems_of rule)) i);


90 


91 
val ssubst = sym RS subst;


92 


93 
(*Select a suitable equality assumption and substitute throughout the subgoal


94 
Replaces only Bound variables if bnd is true*)


95 
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>


96 
let val (_,_,Bi,_) = dest_state(state,i)


97 
val n = length(Logic.strip_assums_hyp Bi)  1


98 
val (t,symopt) = eq_var bnd Bi


99 
in eres_instpair_tac t (symopt RS rev_cut_eq) i THEN


100 
REPEATN n (etac rev_mp i) THEN


101 
etac ssubst i THEN REPEATN n (rtac imp_intr i)


102 
end


103 
handle THM _ => no_tac  EQ_VAR => no_tac));


104 


105 
(*Substitutes for Free or Bound variables*)


106 
val hyp_subst_tac = gen_hyp_subst_tac false;


107 


108 
(*Substitutes for Bound variables only  this is always safe*)


109 
val bound_hyp_subst_tac = gen_hyp_subst_tac true;


110 


111 
end


112 
end;


113 
