|
1 (* Title: ~/projects/isabelle/TLA/hypsubst.ML |
|
2 Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson |
|
3 Copyright 1995 University of Cambridge |
|
4 |
|
5 Tactic to substitute using the assumption x=t in the rest of the subgoal, |
|
6 and to delete that assumption. Original version due to Martin Coen. |
|
7 |
|
8 This version uses the simplifier, and requires it to be already present. |
|
9 |
|
10 Local changes for TLA (Stephan Merz): |
|
11 Simplify equations like f(x) = g(y) if x,y are bound variables. |
|
12 This is useful for TLA if f and g are state variables. f and g may be |
|
13 free or bound variables, or even constants. (This may be unsafe, but |
|
14 we do some type checking to restrict this to state variables!) |
|
15 |
|
16 |
|
17 |
|
18 Test data: |
|
19 |
|
20 goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; |
|
21 goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; |
|
22 goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a"; |
|
23 goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a"; |
|
24 |
|
25 by (hyp_subst_tac 1); |
|
26 by (bound_hyp_subst_tac 1); |
|
27 |
|
28 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) |
|
29 goal thy "P(a) --> (EX y. a=y --> P(f(a)))"; |
|
30 *) |
|
31 |
|
32 (*** Signatures unchanged (but renamed) from the original hypsubst.ML ***) |
|
33 |
|
34 signature ACTHYPSUBST_DATA = |
|
35 sig |
|
36 structure Simplifier : SIMPLIFIER |
|
37 val dest_eq : term -> term*term |
|
38 val eq_reflection : thm (* a=b ==> a==b *) |
|
39 val imp_intr : thm (* (P ==> Q) ==> P-->Q *) |
|
40 val rev_mp : thm (* [| P; P-->Q |] ==> Q *) |
|
41 val subst : thm (* [| a=b; P(a) |] ==> P(b) *) |
|
42 val sym : thm (* a=b ==> b=a *) |
|
43 end; |
|
44 |
|
45 |
|
46 signature ACTHYPSUBST = |
|
47 sig |
|
48 val action_bound_hyp_subst_tac : int -> tactic |
|
49 val action_hyp_subst_tac : int -> tactic |
|
50 (*exported purely for debugging purposes*) |
|
51 val gen_hyp_subst_tac : bool -> int -> tactic |
|
52 val vars_gen_hyp_subst_tac : bool -> int -> tactic |
|
53 val eq_var : bool -> bool -> term -> int * bool |
|
54 val inspect_pair : bool -> bool -> term * term -> bool |
|
55 val mk_eqs : thm -> thm list |
|
56 val thin_leading_eqs_tac : bool -> int -> int -> tactic |
|
57 end; |
|
58 |
|
59 |
|
60 functor ActHypsubstFun(Data: ACTHYPSUBST_DATA): ACTHYPSUBST = |
|
61 struct |
|
62 |
|
63 fun STATE tacfun st = tacfun st st; |
|
64 |
|
65 |
|
66 local open Data in |
|
67 |
|
68 exception EQ_VAR; |
|
69 |
|
70 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
|
71 |
|
72 local val odot = ord"." |
|
73 in |
|
74 (*Simplifier turns Bound variables to dotted Free variables: |
|
75 change it back (any Bound variable will do) |
|
76 *) |
|
77 fun contract t = |
|
78 case Pattern.eta_contract t of |
|
79 Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) |
|
80 | Free at $ Free(b,T) => Free at $ |
|
81 (if ord b = odot then Bound 0 else Free(b,T)) |
|
82 | t' => t' |
|
83 end; |
|
84 |
|
85 fun has_vars t = maxidx_of_term t <> ~1; |
|
86 |
|
87 (* Added for TLA version. |
|
88 Is type ty the type of a state variable? Only then do we substitute |
|
89 in applications. This function either returns true or raises Match. |
|
90 *) |
|
91 fun is_stvar (Type("fun", Type("state",[])::_)) = true; |
|
92 |
|
93 |
|
94 (*If novars then we forbid Vars in the equality. |
|
95 If bnd then we only look for Bound (or dotted Free) variables to eliminate. |
|
96 When can we safely delete the equality? |
|
97 Not if it equates two constants; consider 0=1. |
|
98 Not if it resembles x=t[x], since substitution does not eliminate x. |
|
99 Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) |
|
100 Not if it involves a variable free in the premises, |
|
101 but we can't check for this -- hence bnd and bound_hyp_subst_tac |
|
102 Prefer to eliminate Bound variables if possible. |
|
103 Result: true = use as is, false = reorient first *) |
|
104 fun inspect_pair bnd novars (t,u) = |
|
105 case (contract t, contract u) of |
|
106 (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u |
|
107 then raise Match |
|
108 else true (*eliminates t*) |
|
109 | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t |
|
110 then raise Match |
|
111 else false (*eliminates u*) |
|
112 | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse |
|
113 novars andalso has_vars u |
|
114 then raise Match |
|
115 else true (*eliminates t*) |
|
116 | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse |
|
117 novars andalso has_vars t |
|
118 then raise Match |
|
119 else false (*eliminates u*) |
|
120 | (Free(_,ty) $ (Bound _), _) => |
|
121 if bnd orelse |
|
122 novars andalso has_vars u |
|
123 then raise Match |
|
124 else is_stvar(ty) (* changed for TLA *) |
|
125 | (_, Free(_,ty) $ (Bound _)) => |
|
126 if bnd orelse |
|
127 novars andalso has_vars t |
|
128 then raise Match |
|
129 else not(is_stvar(ty)) (* changed for TLA *) |
|
130 | ((Bound _) $ (Bound _), _) => (* can't check for types here *) |
|
131 if bnd orelse |
|
132 novars andalso has_vars u |
|
133 then raise Match |
|
134 else true |
|
135 | (_, (Bound _) $ (Bound _)) => (* can't check for types here *) |
|
136 if bnd orelse |
|
137 novars andalso has_vars t |
|
138 then raise Match |
|
139 else false |
|
140 | (Const(_,ty) $ (Bound _), _) => |
|
141 if bnd orelse |
|
142 novars andalso has_vars u |
|
143 then raise Match |
|
144 else is_stvar(ty) (* changed for TLA *) |
|
145 | (_, Const(_,ty) $ (Bound _)) => |
|
146 if bnd orelse |
|
147 novars andalso has_vars t |
|
148 then raise Match |
|
149 else not(is_stvar(ty)) (* changed for TLA *) |
|
150 | _ => raise Match; |
|
151 |
|
152 (*Locates a substitutable variable on the left (resp. right) of an equality |
|
153 assumption. Returns the number of intervening assumptions. *) |
|
154 fun eq_var bnd novars = |
|
155 let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t |
|
156 | eq_var_aux k (Const("==>",_) $ A $ B) = |
|
157 ((k, inspect_pair bnd novars (dest_eq A)) |
|
158 (*Exception comes from inspect_pair or dest_eq*) |
|
159 handle Match => eq_var_aux (k+1) B) |
|
160 | eq_var_aux k _ = raise EQ_VAR |
|
161 in eq_var_aux 0 end; |
|
162 |
|
163 (*We do not try to delete ALL equality assumptions at once. But |
|
164 it is easy to handle several consecutive equality assumptions in a row. |
|
165 Note that we have to inspect the proof state after doing the rewriting, |
|
166 since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality |
|
167 must NOT be deleted. Tactic must rotate or delete m assumptions. |
|
168 *) |
|
169 fun thin_leading_eqs_tac bnd m i = STATE(fn state => |
|
170 let fun count [] = 0 |
|
171 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); |
|
172 1 + count Bs) |
|
173 handle Match => 0) |
|
174 val (_,_,Bi,_) = dest_state(state,i) |
|
175 val j = Int.min (m, count (Logic.strip_assums_hyp Bi)) |
|
176 in REPEAT_DETERM_N j (etac thin_rl i) THEN |
|
177 REPEAT_DETERM_N (m-j) (etac revcut_rl i) |
|
178 end); |
|
179 |
|
180 (*For the simpset. Adds ALL suitable equalities, even if not first! |
|
181 No vars are allowed here, as simpsets are built from meta-assumptions*) |
|
182 fun mk_eqs th = |
|
183 [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) |
|
184 then th RS Data.eq_reflection |
|
185 else symmetric(th RS Data.eq_reflection) (*reorient*) ] |
|
186 handle Match => []; (*Exception comes from inspect_pair or dest_eq*) |
|
187 |
|
188 local open Simplifier |
|
189 in |
|
190 |
|
191 val hyp_subst_ss = empty_ss setmksimps mk_eqs |
|
192 |
|
193 (*Select a suitable equality assumption and substitute throughout the subgoal |
|
194 Replaces only Bound variables if bnd is true*) |
|
195 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
|
196 let val (_,_,Bi,_) = dest_state(state,i) |
|
197 val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
198 val (k,_) = eq_var bnd true Bi |
|
199 in |
|
200 EVERY [REPEAT_DETERM_N k (etac revcut_rl i), |
|
201 asm_full_simp_tac hyp_subst_ss i, |
|
202 etac thin_rl i, |
|
203 thin_leading_eqs_tac bnd (n-k) i] |
|
204 end |
|
205 handle THM _ => no_tac | EQ_VAR => no_tac)); |
|
206 |
|
207 end; |
|
208 |
|
209 val ssubst = standard (sym RS subst); |
|
210 |
|
211 (*Old version of the tactic above -- slower but the only way |
|
212 to handle equalities containing Vars.*) |
|
213 fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
|
214 let val (_,_,Bi,_) = dest_state(state,i) |
|
215 val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
216 val (k,symopt) = eq_var bnd false Bi |
|
217 in |
|
218 EVERY [REPEAT_DETERM_N k (etac rev_mp i), |
|
219 etac revcut_rl i, |
|
220 REPEAT_DETERM_N (n-k) (etac rev_mp i), |
|
221 etac (if symopt then ssubst else subst) i, |
|
222 REPEAT_DETERM_N n (rtac imp_intr i)] |
|
223 end |
|
224 handle THM _ => no_tac | EQ_VAR => no_tac)); |
|
225 |
|
226 (*Substitutes for Free or Bound variables*) |
|
227 val action_hyp_subst_tac = |
|
228 (* gen_hyp_subst_tac false ORELSE' *) vars_gen_hyp_subst_tac false; |
|
229 |
|
230 (*Substitutes for Bound variables only -- this is always safe*) |
|
231 val action_bound_hyp_subst_tac = |
|
232 (* gen_hyp_subst_tac true ORELSE' *) vars_gen_hyp_subst_tac true; |
|
233 |
|
234 end |
|
235 end; |
|
236 |