src/Provers/hypsubst.ML
author lcp
Wed Oct 19 09:48:13 1994 +0100 (1994-10-19 ago)
changeset 646 7928c9760667
parent 231 cb6a24451544
child 680 f9e24455bbd1
permissions -rw-r--r--
new comments explaining abandoned change
     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_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 Var; what if it appears in other goals?
    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)
    83       and cterm = cterm_of sign
    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