1(* Title: FOLP/hypsubst.ML 2 Author: Martin D Coen, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4 5Original version of Provers/hypsubst. Cannot use new version because it 6relies on the new simplifier! 7 8Martin Coen's tactic for substitution in the hypotheses 9*) 10 11signature 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 20signature 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 29functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = 30struct 31 32local open Data in 33 34exception 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?*) 41fun 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). *) 60fun eq_var bnd = 61 let fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) = eq_var_aux k t 62 | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ 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*) 71fun 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*) 85val hyp_subst_tac = gen_hyp_subst_tac false; 86 87(*Substitutes for Bound variables only -- this is always safe*) 88val bound_hyp_subst_tac = gen_hyp_subst_tac true; 89 90end 91end; 92 93