src/Provers/hypsubst.ML
author lcp
Tue Jan 18 16:37:12 1994 +0100 (1994-01-18 ago)
changeset 231 cb6a24451544
parent 0 a5a9c433f639
child 646 7928c9760667
permissions -rw-r--r--
Updated refs to old Sign functions
     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 (n-1) 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 = 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