src/Provers/hypsubst.ML
author lcp
Fri Nov 11 10:42:55 1994 +0100 (1994-11-11 ago)
changeset 704 b71b6be59354
parent 680 f9e24455bbd1
child 1011 5c9654e2e3de
permissions -rw-r--r--
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
     1 (*  Title: 	Provers/hypsubst
     2     ID:         $Id$
     3     Author: 	Martin D Coen, 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_mp	: thm		(* [| P;  P-->Q |] ==> Q *)
    14   val subst	: thm		(* [| a=b;  P(a) |] ==> P(b) *)
    15   val sym	: thm		(* a=b ==> b=a *)
    16   end;
    17 
    18 signature HYPSUBST =
    19   sig
    20   val bound_hyp_subst_tac : int -> tactic
    21   val hyp_subst_tac       : int -> tactic
    22     (*exported purely for debugging purposes*)
    23   val eq_var              : bool -> term -> int * thm
    24   val inspect_pair        : bool -> term * term -> thm
    25   end;
    26 
    27 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
    28 struct
    29 
    30 local open Data in
    31 
    32 exception EQ_VAR;
    33 
    34 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
    35 
    36 (*It's not safe to substitute for a constant; consider 0=1.
    37   It's not safe to substitute for x=t[x] since x is not eliminated.
    38   It's not safe to substitute for a Var; what if it appears in other goals?
    39   It's not safe to substitute for a variable free in the premises,
    40     but how could we check for this?*)
    41 fun inspect_pair bnd (t,u) =
    42   case (Pattern.eta_contract t, Pattern.eta_contract u) of
    43        (Bound i, _) => if loose(i,u) then raise Match 
    44 		       else sym		(*eliminates t*)
    45      | (_, Bound i) => if loose(i,t) then raise Match 
    46 		       else asm_rl	(*eliminates u*)
    47      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
    48 		      else sym		(*eliminates t*)
    49      | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
    50 		      else asm_rl	(*eliminates u*)
    51      | _ => raise Match;
    52 
    53 (*Locates a substitutable variable on the left (resp. right) of an equality
    54    assumption.  Returns the number of intervening assumptions, paried with
    55    the rule asm_rl (resp. sym). *)
    56 fun eq_var bnd =
    57   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    58 	| eq_var_aux k (Const("==>",_) $ A $ B) = 
    59 	      ((k, inspect_pair bnd (dest_eq A))
    60 		      (*Exception Match comes from inspect_pair or dest_eq*)
    61 	       handle Match => eq_var_aux (k+1) B)
    62 	| eq_var_aux k _ = raise EQ_VAR
    63   in  eq_var_aux 0  end;
    64 
    65 (*Select a suitable equality assumption and substitute throughout the subgoal
    66   Replaces only Bound variables if bnd is true*)
    67 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    68       let val (_,_,Bi,_) = dest_state(state,i)
    69 	  val n = length(Logic.strip_assums_hyp Bi) - 1
    70 	  val (k,symopt) = eq_var bnd Bi
    71       in 
    72 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    73 		etac revcut_rl i,
    74 		REPEAT_DETERM_N (n-k) (etac rev_mp i),
    75 		etac (symopt RS subst) i,
    76 		REPEAT_DETERM_N n (rtac imp_intr i)]
    77       end
    78       handle THM _ => no_tac | EQ_VAR => no_tac));
    79 
    80 (*Substitutes for Free or Bound variables*)
    81 val hyp_subst_tac = gen_hyp_subst_tac false;
    82 
    83 (*Substitutes for Bound variables only -- this is always safe*)
    84 val bound_hyp_subst_tac = gen_hyp_subst_tac true;
    85 
    86 end
    87 end;
    88