3807
|
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 |
*)
|
3945
|
91 |
fun is_stvar (Type("fun", Type("Stfun.state",[])::_)) = true;
|
3807
|
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 |
|