src/FOLP/hypsubst.ML
author haftmann
Thu Jul 08 16:19:24 2010 +0200 (2010-07-08)
changeset 37744 3daaf23b9ab4
parent 36692 54b64d4ad524
child 42125 a8cbb9371154
permissions -rw-r--r--
tuned titles
     1 (*  Title:      FOLP/hypsubst.ML
     2     Author:     Martin D Coen, Cambridge University Computer Laboratory
     3     Copyright   1995  University of Cambridge
     4 
     5 Original version of Provers/hypsubst.  Cannot use new version because it
     6 relies on the new simplifier!
     7 
     8 Martin Coen's tactic for substitution in the hypotheses
     9 *)
    10 
    11 signature HYPSUBST_DATA =
    12   sig
    13   val dest_eq   : term -> term*term
    14   val imp_intr  : thm           (* (P ==> Q) ==> P-->Q *)
    15   val rev_mp    : thm           (* [| P;  P-->Q |] ==> Q *)
    16   val subst     : thm           (* [| a=b;  P(a) |] ==> P(b) *)
    17   val sym       : thm           (* a=b ==> b=a *)
    18   end;
    19 
    20 signature HYPSUBST =
    21   sig
    22   val bound_hyp_subst_tac : int -> tactic
    23   val hyp_subst_tac       : int -> tactic
    24     (*exported purely for debugging purposes*)
    25   val eq_var              : bool -> term -> int * thm
    26   val inspect_pair        : bool -> term * term -> thm
    27   end;
    28 
    29 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    30 struct
    31 
    32 local open Data in
    33 
    34 exception EQ_VAR;
    35 
    36 fun loose (i, t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    37 
    38 (*It's not safe to substitute for a constant; consider 0=1.
    39   It's not safe to substitute for x=t[x] since x is not eliminated.
    40   It's not safe to substitute for a Var; what if it appears in other goals?
    41   It's not safe to substitute for a variable free in the premises,
    42     but how could we check for this?*)
    43 fun inspect_pair bnd (t,u) =
    44   case (Envir.eta_contract t, Envir.eta_contract u) of
    45        (Bound i, _) => if loose(i,u) then raise Match
    46                        else sym         (*eliminates t*)
    47      | (_, Bound i) => if loose(i,t) then raise Match
    48                        else asm_rl      (*eliminates u*)
    49      | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
    50                       else sym          (*eliminates t*)
    51      | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
    52                       else asm_rl       (*eliminates u*)
    53      | _ => raise Match;
    54 
    55 (*Locates a substitutable variable on the left (resp. right) of an equality
    56    assumption.  Returns the number of intervening assumptions, paried with
    57    the rule asm_rl (resp. sym). *)
    58 fun eq_var bnd =
    59   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    60         | eq_var_aux k (Const("==>",_) $ A $ B) =
    61               ((k, inspect_pair bnd (dest_eq A))
    62                       (*Exception Match comes from inspect_pair or dest_eq*)
    63                handle Match => eq_var_aux (k+1) B)
    64         | eq_var_aux k _ = raise EQ_VAR
    65   in  eq_var_aux 0  end;
    66 
    67 (*Select a suitable equality assumption and substitute throughout the subgoal
    68   Replaces only Bound variables if bnd is true*)
    69 fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    70       let val n = length(Logic.strip_assums_hyp Bi) - 1
    71           val (k,symopt) = eq_var bnd Bi
    72       in
    73          DETERM
    74            (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    75                    etac revcut_rl i,
    76                    REPEAT_DETERM_N (n-k) (etac rev_mp i),
    77                    etac (symopt RS subst) i,
    78                    REPEAT_DETERM_N n (rtac imp_intr i)])
    79       end
    80       handle THM _ => no_tac | EQ_VAR => no_tac);
    81 
    82 (*Substitutes for Free or Bound variables*)
    83 val hyp_subst_tac = gen_hyp_subst_tac false;
    84 
    85 (*Substitutes for Bound variables only -- this is always safe*)
    86 val bound_hyp_subst_tac = gen_hyp_subst_tac true;
    87 
    88 end
    89 end;
    90