author  wenzelm 
Fri, 04 Aug 2000 22:58:23 +0200  
changeset 9532  36b9bc6eb454 
parent 4466  305390f23734 
child 9592  abbd48606a0a 
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 

9532  6 
Tactic to substitute using (at least) the assumption x=t in the rest of the 
7 
subgoal, and to delete (at least) that assumption. 

4223  8 
Original version due to Martin Coen. 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

9 

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

10 
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

11 

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

12 
Test data: 
0  13 

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

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

17 
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

18 

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

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

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

21 

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

22 
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) 
9532  23 
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

24 

9532  25 
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

26 
\ P(x,h5); P(y,h6); K(x,h7) ] ==> Q(x,c)"; 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

27 
by (blast_hyp_subst_tac (ref true) 1); 
0  28 
*) 
29 

30 
signature HYPSUBST_DATA = 

31 
sig 

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

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

33 
val dest_Trueprop : term > term 
9532  34 
val dest_eq : term > term*term*typ 
35 
val dest_imp : term > term*term 

36 
val eq_reflection : thm (* a=b ==> a==b *) 

37 
val rev_eq_reflection: thm (* a==b ==> a=b *) 

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

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

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

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

4223  42 
val thin_refl : thm (* [x=x; PROP W] ==> PROP W *) 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

43 
end; 
0  44 

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

45 

0  46 
signature HYPSUBST = 
47 
sig 

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

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

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

50 
val blast_hyp_subst_tac : bool ref > int > tactic 
0  51 
(*exported purely for debugging purposes*) 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

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

54 
val eq_var : bool > bool > term > int * bool 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

55 
val inspect_pair : bool > bool > term * term * typ > bool 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

56 
val mk_eqs : thm > thm list 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

57 
val thin_leading_eqs_tac : bool > int > int > tactic 
9532  58 
val stac : thm > int > tactic 
59 
val hypsubst_setup : (theory > theory) list 

0  60 
end; 
61 

2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

62 

3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

63 

9532  64 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
0  65 
struct 
66 

67 
exception EQ_VAR; 

68 

2174  69 
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); 
0  70 

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

71 
local val odot = ord"." 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

72 
in 
9532  73 
(*Simplifier turns Bound variables to dotted Free variables: 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

74 
change it back (any Bound variable will do) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

76 
fun contract t = 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

77 
case Pattern.eta_contract_atom t of 
9532  78 
Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

79 
 t' => t' 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

81 

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

82 
fun has_vars t = maxidx_of_term t <> ~1; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

83 

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

84 
(*If novars then we forbid Vars in the equality. 
9532  85 
If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

87 
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

88 
Not if it resembles x=t[x], since substitution does not eliminate x. 
4299  89 
Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P 
9532  90 
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

91 
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

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

93 
Result: true = use as is, false = reorient first *) 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

94 
fun inspect_pair bnd novars (t,u,T) = 
9532  95 
if novars andalso maxidx_of_typ T <> ~1 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

96 
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

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

98 
case (contract t, contract u) of 
9532  99 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
100 
then raise Match 

101 
else true (*eliminates t*) 

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

103 
then raise Match 

104 
else false (*eliminates u*) 

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

106 
novars andalso has_vars u 

107 
then raise Match 

108 
else true (*eliminates t*) 

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

110 
novars andalso has_vars t 

111 
then raise Match 

112 
else false (*eliminates u*) 

0  113 
 _ => raise Match; 
114 

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

115 
(*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

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

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

118 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
9532  119 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
120 
((k, inspect_pair bnd novars 

121 
(Data.dest_eq (Data.dest_Trueprop A))) 

122 
(*Exception comes from inspect_pair or dest_eq*) 

123 
handle _ => eq_var_aux (k+1) B) 

124 
 eq_var_aux k _ = raise EQ_VAR 

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

125 
in eq_var_aux 0 end; 
0  126 

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

127 
(*We do not try to delete ALL equality assumptions at once. But 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

128 
it is easy to handle several consecutive equality assumptions in a row. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

129 
Note that we have to inspect the proof state after doing the rewriting, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

130 
since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

131 
must NOT be deleted. Tactic must rotate or delete m assumptions. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

132 
*) 
3537  133 
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

134 
let fun count [] = 0 
9532  135 
 count (A::Bs) = ((inspect_pair bnd true 
136 
(Data.dest_eq (Data.dest_Trueprop A)); 

137 
1 + count Bs) 

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

138 
handle _ => 0) 
2143  139 
val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

140 
in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (mj) i 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

142 

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

143 
(*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

144 
No vars are allowed here, as simpsets are built from metaassumptions*) 
9532  145 
fun mk_eqs th = 
146 
[ if inspect_pair false false (Data.dest_eq 

147 
(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

148 
then th RS Data.eq_reflection 
9532  149 
else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

150 
handle _ => []; (*Exception comes from inspect_pair or dest_eq*) 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

151 

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

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

154 

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

155 
val hyp_subst_ss = empty_ss setmksimps mk_eqs 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

156 

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

157 
(*Select a suitable equality assumption and substitute throughout the subgoal 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

158 
Replaces only Bound variables if bnd is true*) 
3537  159 
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
9532  160 
let val n = length(Logic.strip_assums_hyp Bi)  1 
161 
val (k,_) = eq_var bnd true Bi 

162 
in 

163 
DETERM (EVERY [rotate_tac k i, 

164 
asm_full_simp_tac hyp_subst_ss i, 

165 
etac thin_rl i, 

166 
thin_leading_eqs_tac bnd (nk) i]) 

167 
end 

168 
handle THM _ => no_tac  EQ_VAR => no_tac); 

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

169 

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

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

171 

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

172 
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

173 

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

174 
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

175 

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

176 
(*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

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

9532  180 
val (k,symopt) = eq_var bnd false Bi 
181 
in 

182 
DETERM 

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

183 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  184 
rotate_tac 1 i, 
185 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

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

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

0  188 
end 
3537  189 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  190 

191 
(*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

192 
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], 
4223  193 
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; 
0  194 

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

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

197 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  198 

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

199 

9532  200 
(** 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

201 
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

202 
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

203 

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

204 
(*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

205 
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

206 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  207 
 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

208 
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

209 
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

210 

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

211 
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 
9532  212 
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

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

216 
Logic.strip_assums_concl > 

217 
Data.dest_Trueprop > Data.dest_imp 

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

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

220 
else (*leave affected hyps at end*) 

221 
(r+1, imp_intr_tac i) 

222 
in 

223 
case Seq.pull(tac st) of 

224 
None => Seq.single(st) 

225 
 Some(st',_) => imptac (r',hyps) st' 

226 
end handle _ => error "?? in blast_hyp_subst_tac" 

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

227 
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

228 

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

229 

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

230 
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

231 
let val (k,symopt) = eq_var false false Bi 
9532  232 
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

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

236 
in 

237 
if !trace then writeln "Substituting an equality" else (); 

238 
DETERM 

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

239 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  240 
rotate_tac 1 i, 
241 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

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

243 
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

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

245 
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

246 

9532  247 

248 
(*apply an equality or definition ONCE; 

249 
fails unless the substitution has an effect*) 

250 
fun stac th = 

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

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

253 

254 

255 
(* proof method setup *) 

256 

257 
val subst_meth = Method.goal_args' Attrib.local_thm stac; 

258 
val hypsubst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac); 

259 

260 
val hypsubst_setup = 

261 
[Method.add_methods 

262 
[("hypsubst", hypsubst_meth, "substitution using an assumption (improper)"), 

263 
("subst", subst_meth, "substitution")]]; 

264 

0  265 
end; 