|
1 (* Title: Provers/hypsubst |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, 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 variable free in the premises, |
|
53 but how could we check for this?*) |
|
54 fun inspect_pair bnd (t,u) = |
|
55 case (Pattern.eta_contract t, Pattern.eta_contract u) of |
|
56 (Bound i, _) => if loose(i,u) then raise Match |
|
57 else (t, asm_rl) |
|
58 | (_, Bound i) => if loose(i,t) then raise Match |
|
59 else (u, sym) |
|
60 | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match |
|
61 else (t, asm_rl) |
|
62 | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match |
|
63 else (u, sym) |
|
64 | _ => raise Match; |
|
65 |
|
66 (* Extracts the name of the variable on the left (resp. right) of an equality |
|
67 assumption. Returns the rule asm_rl (resp. sym). *) |
|
68 fun eq_var bnd (Const("all",_) $ Abs(_,_,t)) = eq_var bnd t |
|
69 | eq_var bnd (Const("==>",_) $ A $ B) = |
|
70 (inspect_pair bnd (dest_eq A) |
|
71 (*Match comes from inspect_pair or dest_eq*) |
|
72 handle Match => eq_var bnd B) |
|
73 | eq_var bnd _ = raise EQ_VAR; |
|
74 |
|
75 (*Lift and instantiate a rule wrt the given state and subgoal number *) |
|
76 fun lift_instpair (state, i, t, rule) = |
|
77 let val {maxidx,sign,...} = rep_thm state |
|
78 val (_, _, Bi, _) = dest_state(state,i) |
|
79 val params = Logic.strip_params Bi |
|
80 val var = liftvar (maxidx+1) (map #2 params) |
|
81 and u = Unify.rlist_abs(rev params, t) |
|
82 and cterm = Sign.cterm_of sign |
|
83 in cterm_instantiate [(cterm var, cterm u)] (lift_rule (state,i) rule) |
|
84 end; |
|
85 |
|
86 fun eres_instpair_tac t rule i = STATE (fn state => |
|
87 compose_tac (true, lift_instpair (state, i, t, rule), |
|
88 length(prems_of rule)) i); |
|
89 |
|
90 val ssubst = sym RS subst; |
|
91 |
|
92 (*Select a suitable equality assumption and substitute throughout the subgoal |
|
93 Replaces only Bound variables if bnd is true*) |
|
94 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
|
95 let val (_,_,Bi,_) = dest_state(state,i) |
|
96 val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
97 val (t,symopt) = eq_var bnd Bi |
|
98 in eres_instpair_tac t (symopt RS rev_cut_eq) i THEN |
|
99 REPEATN n (etac rev_mp i) THEN |
|
100 etac ssubst i THEN REPEATN n (rtac imp_intr i) |
|
101 end |
|
102 handle THM _ => no_tac | EQ_VAR => no_tac)); |
|
103 |
|
104 (*Substitutes for Free or Bound variables*) |
|
105 val hyp_subst_tac = gen_hyp_subst_tac false; |
|
106 |
|
107 (*Substitutes for Bound variables only -- this is always safe*) |
|
108 val bound_hyp_subst_tac = gen_hyp_subst_tac true; |
|
109 |
|
110 end |
|
111 end; |
|
112 |