author  wenzelm 
Sun, 22 Jul 2007 21:20:53 +0200  
changeset 23908  edca7f581c09 
parent 21588  cd0dc678a205 
child 26833  7c3757fccf0e 
permissions  rwrr 
9532  1 
(* Title: Provers/hypsubst.ML 
0  2 
ID: $Id$ 
9532  3 
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

4 
Copyright 1995 University of Cambridge 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

5 

15662  6 
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst". 
9628  7 

8 
Tactic to substitute using (at least) the assumption x=t in the rest 

9 
of the subgoal, and to delete (at least) that assumption. Original 

10 
version due to Martin Coen. 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

11 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

12 
This version uses the simplifier, and requires it to be already present. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

13 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

14 
Test data: 
0  15 

9532  16 
Goal "!!x.[ Q(x,y,z); y=x; a=x; z=y; P(y) ] ==> P(z)"; 
17 
Goal "!!x.[ Q(x,y,z); z=f(x); x=z ] ==> P(z)"; 

18 
Goal "!!y. [ ?x=y; P(?x) ] ==> y = a"; 

19 
Goal "!!z. [ ?x=y; P(?x) ] ==> y = a"; 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

20 

15415
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

21 
Goal "!!x a. [ x = f(b); g(a) = b ] ==> P(x)"; 
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

22 

6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

23 
by (bound_hyp_subst_tac 1); 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

24 
by (hyp_subst_tac 1); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

25 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

26 
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) 
9532  27 
Goal "P(a) > (EX y. a=y > P(f(a)))"; 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

28 

9532  29 
Goal "!!x. [ Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

30 
\ P(x,h5); P(y,h6); K(x,h7) ] ==> Q(x,c)"; 
23908  31 
by (blast_hyp_subst_tac true 1); 
0  32 
*) 
33 

34 
signature HYPSUBST_DATA = 

21221  35 
sig 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

36 
val dest_Trueprop : term > term 
21221  37 
val dest_eq : term > term * term 
20974  38 
val dest_imp : term > term * term 
9532  39 
val eq_reflection : thm (* a=b ==> a==b *) 
40 
val rev_eq_reflection: thm (* a==b ==> a=b *) 

41 
val imp_intr : thm (* (P ==> Q) ==> P>Q *) 

42 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 

43 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 

44 
val sym : thm (* a=b ==> b=a *) 

4223  45 
val thin_refl : thm (* [x=x; PROP W] ==> PROP W *) 
21221  46 
end; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

47 

0  48 
signature HYPSUBST = 
21221  49 
sig 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

50 
val bound_hyp_subst_tac : int > tactic 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

51 
val hyp_subst_tac : int > tactic 
23908  52 
val blast_hyp_subst_tac : bool > int > tactic 
20945  53 
val stac : thm > int > tactic 
18708  54 
val hypsubst_setup : theory > theory 
21221  55 
end; 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

56 

9532  57 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
0  58 
struct 
59 

60 
exception EQ_VAR; 

61 

17896  62 
fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0; 
0  63 

16979  64 
(*Simplifier turns Bound variables to special Free variables: 
65 
change it back (any Bound variable will do)*) 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

66 
fun contract t = 
16979  67 
(case Pattern.eta_contract_atom t of 
20074  68 
Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T) 
16979  69 
 t' => t'); 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

70 

21221  71 
val has_vars = Term.exists_subterm Term.is_Var; 
72 
val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar); 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

73 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

74 
(*If novars then we forbid Vars in the equality. 
16979  75 
If bnd then we only look for Bound variables to eliminate. 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

76 
When can we safely delete the equality? 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

77 
Not if it equates two constants; consider 0=1. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

78 
Not if it resembles x=t[x], since substitution does not eliminate x. 
4299  79 
Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P 
9532  80 
Not if it involves a variable free in the premises, 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

81 
but we can't check for this  hence bnd and bound_hyp_subst_tac 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

82 
Prefer to eliminate Bound variables if possible. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

83 
Result: true = use as is, false = reorient first *) 
21221  84 
fun inspect_pair bnd novars (t, u) = 
85 
if novars andalso (has_tvars t orelse has_tvars u) 

4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

86 
then raise Match (*variables in the type!*) 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

87 
else 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

88 
case (contract t, contract u) of 
9532  89 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
90 
then raise Match 

91 
else true (*eliminates t*) 

92 
 (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t 

93 
then raise Match 

94 
else false (*eliminates u*) 

95 
 (Free _, _) => if bnd orelse Logic.occs(t,u) orelse 

96 
novars andalso has_vars u 

97 
then raise Match 

98 
else true (*eliminates t*) 

99 
 (_, Free _) => if bnd orelse Logic.occs(u,t) orelse 

100 
novars andalso has_vars t 

101 
then raise Match 

102 
else false (*eliminates u*) 

0  103 
 _ => raise Match; 
104 

680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

105 
(*Locates a substitutable variable on the left (resp. right) of an equality 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

106 
assumption. Returns the number of intervening assumptions. *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

107 
fun eq_var bnd novars = 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

108 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
9532  109 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
110 
((k, inspect_pair bnd novars 

111 
(Data.dest_eq (Data.dest_Trueprop A))) 

21227  112 
handle TERM _ => eq_var_aux (k+1) B 
113 
 Match => eq_var_aux (k+1) B) 

9532  114 
 eq_var_aux k _ = raise EQ_VAR 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

115 
in eq_var_aux 0 end; 
0  116 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

117 
(*For the simpset. Adds ALL suitable equalities, even if not first! 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

118 
No vars are allowed here, as simpsets are built from metaassumptions*) 
15415
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

119 
fun mk_eqs bnd th = 
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

120 
[ if inspect_pair bnd false (Data.dest_eq 
9532  121 
(Data.dest_Trueprop (#prop (rep_thm th)))) 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

122 
then th RS Data.eq_reflection 
9532  123 
else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
21227  124 
handle TERM _ => []  Match => []; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

125 

17896  126 
local 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

127 
in 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

128 

15415
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

129 
(*Select a suitable equality assumption; substitute throughout the subgoal 
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

130 
If bnd is true, then it replaces Bound variables only. *) 
13604  131 
fun gen_hyp_subst_tac bnd = 
17896  132 
let fun tac i st = SUBGOAL (fn (Bi, _) => 
133 
let 

134 
val (k, _) = eq_var bnd true Bi 

135 
val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss 

136 
setmksimps (mk_eqs bnd) 

13604  137 
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, 
138 
etac thin_rl i, rotate_tac (~k) i] 

17896  139 
end handle THM _ => no_tac  EQ_VAR => no_tac) i st 
13604  140 
in REPEAT_DETERM1 o tac end; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

141 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

142 
end; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

143 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

144 
val ssubst = standard (Data.sym RS Data.subst); 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

145 

305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

146 
val imp_intr_tac = rtac Data.imp_intr; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

147 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

148 
(*Old version of the tactic above  slower but the only way 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

149 
to handle equalities containing Vars.*) 
3537  150 
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
151 
let val n = length(Logic.strip_assums_hyp Bi)  1 

9532  152 
val (k,symopt) = eq_var bnd false Bi 
153 
in 

154 
DETERM 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

155 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  156 
rotate_tac 1 i, 
157 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

158 
etac (if symopt then ssubst else Data.subst) i, 

159 
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) 

0  160 
end 
3537  161 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  162 

163 
(*Substitutes for Free or Bound variables*) 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

164 
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], 
4223  165 
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; 
0  166 

167 
(*Substitutes for Bound variables only  this is always safe*) 

9532  168 
val bound_hyp_subst_tac = 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

169 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  170 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

171 

9532  172 
(** Version for Blast_tac. Hyps that are affected by the substitution are 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

173 
moved to the front. Defect: even trivial changes are noticed, such as 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

174 
substitutions in the arguments of a function Var. **) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

175 

305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

176 
(*final rereversal of the changed assumptions*) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

177 
fun reverse_n_tac 0 i = all_tac 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

178 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  179 
 reverse_n_tac n i = 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

180 
REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

181 
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i); 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

182 

305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

183 
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 
9532  184 
fun all_imp_intr_tac hyps i = 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

185 
let fun imptac (r, []) st = reverse_n_tac r i st 
9532  186 
 imptac (r, hyp::hyps) st = 
187 
let val (hyp',_) = List.nth (prems_of st, i1) > 

188 
Logic.strip_assums_concl > 

189 
Data.dest_Trueprop > Data.dest_imp 

190 
val (r',tac) = if Pattern.aeconv (hyp,hyp') 

191 
then (r, imp_intr_tac i THEN rotate_tac ~1 i) 

192 
else (*leave affected hyps at end*) 

193 
(r+1, imp_intr_tac i) 

194 
in 

195 
case Seq.pull(tac st) of 

15531  196 
NONE => Seq.single(st) 
197 
 SOME(st',_) => imptac (r',hyps) st' 

21221  198 
end 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

199 
in imptac (0, rev hyps) end; 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

200 

305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

201 

305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

202 
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

203 
let val (k,symopt) = eq_var false false Bi 
9532  204 
val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

205 
(*omit selected equality, returning other hyps*) 
9532  206 
val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) 
207 
val n = length hyps 

208 
in 

23908  209 
if trace then tracing "Substituting an equality" else (); 
9532  210 
DETERM 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

211 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  212 
rotate_tac 1 i, 
213 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

214 
etac (if symopt then ssubst else Data.subst) i, 

215 
all_imp_intr_tac hyps i]) 

4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

216 
end 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

217 
handle THM _ => no_tac  EQ_VAR => no_tac); 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

218 

9532  219 

220 
(*apply an equality or definition ONCE; 

221 
fails unless the substitution has an effect*) 

222 
fun stac th = 

223 
let val th' = th RS Data.rev_eq_reflection handle THM _ => th 

224 
in CHANGED_GOAL (rtac (th' RS ssubst)) end; 

225 

226 

9628  227 
(* theory setup *) 
228 

9532  229 
val hypsubst_setup = 
18708  230 
Method.add_methods 
21588  231 
[("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)), 
232 
"substitution using an assumption (improper)"), 

233 
("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")]; 

9532  234 

0  235 
end; 