src/FOLP/hypsubst.ML
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (19 months ago)
changeset 67022 49309fe530fd
parent 60754 02924903a6fd
child 69593 3dda49e08b9d
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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 : Proof.context -> int -> tactic
    23   val hyp_subst_tac       : Proof.context -> 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 Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    30 struct
    31 
    32 local open Data in
    33 
    34 exception EQ_VAR;
    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 (Envir.eta_contract t, Envir.eta_contract u) of
    43     (Bound i, _) =>
    44       if loose_bvar1 (u, i) then raise Match
    45       else sym         (*eliminates t*)
    46    | (_, Bound i) =>
    47       if loose_bvar (t, i) then raise Match
    48       else asm_rl      (*eliminates u*)
    49    | (Free _, _) =>
    50       if bnd orelse Logic.occs (t, u) then raise Match
    51       else sym          (*eliminates t*)
    52    | (_, Free _) =>
    53       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(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
    62         | eq_var_aux k (Const(@{const_name Pure.imp},_) $ 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 ctxt = SUBGOAL(fn (Bi,i) =>
    72       let val n = length(Logic.strip_assums_hyp Bi) - 1
    73           val (k,symopt) = eq_var bnd Bi
    74       in
    75          DETERM
    76            (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [rev_mp] i),
    77                    eresolve_tac ctxt [revcut_rl] i,
    78                    REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [rev_mp] i),
    79                    eresolve_tac ctxt [symopt RS subst] i,
    80                    REPEAT_DETERM_N n (resolve_tac ctxt [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