0

1 
(* Title: Provers/hypsubst


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


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.


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


53 
but how could we check for this?*)


54 
fun inspect_pair bnd (t,u) =


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


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


57 
else (t, asm_rl)


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


59 
else (u, sym)


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


61 
else (t, asm_rl)


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


63 
else (u, sym)


64 
 _ => raise Match;


65 


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


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


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


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


70 
(inspect_pair bnd (dest_eq A)


71 
(*Match comes from inspect_pair or dest_eq*)


72 
handle Match => eq_var bnd B)


73 
 eq_var bnd _ = raise EQ_VAR;


74 


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


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


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


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


79 
val params = Logic.strip_params Bi


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


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


82 
and cterm = Sign.cterm_of sign


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


84 
end;


85 


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


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


88 
length(prems_of rule)) i);


89 


90 
val ssubst = sym RS subst;


91 


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


93 
Replaces only Bound variables if bnd is true*)


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


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


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


97 
val (t,symopt) = eq_var bnd Bi


98 
in eres_instpair_tac t (symopt RS rev_cut_eq) i THEN


99 
REPEATN n (etac rev_mp i) THEN


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


101 
end


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


103 


104 
(*Substitutes for Free or Bound variables*)


105 
val hyp_subst_tac = gen_hyp_subst_tac false;


106 


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


108 
val bound_hyp_subst_tac = gen_hyp_subst_tac true;


109 


110 
end


111 
end;


112 
