src/Provers/hypsubst.ML
author lcp
Wed Nov 02 12:44:03 1994 +0100 (1994-11-02 ago)
changeset 680 f9e24455bbd1
parent 646 7928c9760667
child 704 b71b6be59354
permissions -rw-r--r--
Provers/hypsubst: greatly simplified! No longer simulates a
"eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen
equality to the end!
     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 fun REPEATN 0 tac = all_tac
    33   | REPEATN n tac = Tactic(fn state =>
    34                            tapply(tac THEN REPEATN (n-1) tac,  state));
    35 
    36 exception EQ_VAR;
    37 
    38 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
    39 
    40 (*It's not safe to substitute for a constant; consider 0=1.
    41   It's not safe to substitute for x=t[x] since x is not eliminated.
    42   It's not safe to substitute for a Var; what if it appears in other goals?
    43   It's not safe to substitute for a variable free in the premises,
    44     but how could we check for this?*)
    45 fun inspect_pair bnd (t,u) =
    46   case (Pattern.eta_contract t, Pattern.eta_contract u) of
    47        (Bound i, _) => if loose(i,u) then raise Match 
    48 		       else sym		(*eliminates t*)
    49      | (_, Bound i) => if loose(i,t) then raise Match 
    50 		       else asm_rl	(*eliminates u*)
    51      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
    52 		      else sym		(*eliminates t*)
    53      | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
    54 		      else asm_rl	(*eliminates u*)
    55      | _ => raise Match;
    56 
    57 (*Locates a substitutable variable on the left (resp. right) of an equality
    58    assumption.  Returns the number of intervening assumptions, paried with
    59    the rule asm_rl (resp. sym). *)
    60 fun eq_var bnd =
    61   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    62 	| eq_var_aux k (Const("==>",_) $ A $ B) = 
    63 	      ((k, inspect_pair bnd (dest_eq A))
    64 		      (*Exception Match comes from inspect_pair or dest_eq*)
    65 	       handle Match => eq_var_aux (k+1) B)
    66 	| eq_var_aux k _ = raise EQ_VAR
    67   in  eq_var_aux 0  end;
    68 
    69 (*Select a suitable equality assumption and substitute throughout the subgoal
    70   Replaces only Bound variables if bnd is true*)
    71 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    72       let val (_,_,Bi,_) = dest_state(state,i)
    73 	  val n = length(Logic.strip_assums_hyp Bi) - 1
    74 	  val (k,symopt) = eq_var bnd Bi
    75       in 
    76 	 EVERY [REPEATN k (etac rev_mp i),
    77 		etac revcut_rl i,
    78 		REPEATN (n-k) (etac rev_mp i),
    79 		etac (symopt RS subst) i,
    80 		REPEATN n (rtac imp_intr i)]
    81       end
    82       handle THM _ => no_tac | EQ_VAR => no_tac));
    83 
    84 (*Substitutes for Free or Bound variables*)
    85 val hyp_subst_tac = gen_hyp_subst_tac false;
    86 
    87 (*Substitutes for Bound variables only -- this is always safe*)
    88 val bound_hyp_subst_tac = gen_hyp_subst_tac true;
    89 
    90 end
    91 end;
    92