author  paulson 
Thu, 16 Dec 2004 12:44:32 +0100  
changeset 15415  6e437e276ef5 
parent 13604  57bfacbbaeda 
child 15481  fc075ae929e4 
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 

9628  6 
Basic equational reasoning: (hyp_)subst method and symmetric attribute. 
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)"; 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

31 
by (blast_hyp_subst_tac (ref true) 1); 
0  32 
*) 
33 

34 
signature HYPSUBST_DATA = 

35 
sig 

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

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

37 
val dest_Trueprop : term > term 
9532  38 
val dest_eq : term > term*term*typ 
39 
val dest_imp : term > term*term 

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

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

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

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

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

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

4223  46 
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

47 
end; 
0  48 

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

49 

0  50 
signature HYPSUBST = 
51 
sig 

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

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

53 
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

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

56 
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

57 
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

58 
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

59 
val inspect_pair : bool > bool > term * term * typ > bool 
15415
6e437e276ef5
fix to bound_hyp_subst_tac, partially fixing a bug in inductive definitions
paulson
parents:
13604
diff
changeset

60 
val mk_eqs : bool > thm > thm list 
9532  61 
val stac : thm > int > tactic 
62 
val hypsubst_setup : (theory > theory) list 

0  63 
end; 
64 

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

65 

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

66 

9532  67 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
0  68 
struct 
69 

70 
exception EQ_VAR; 

71 

2174  72 
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); 
0  73 

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

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

75 
in 
9532  76 
(*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

77 
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

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

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

80 
case Pattern.eta_contract_atom t of 
9532  81 
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

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

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

84 

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

85 
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

86 

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

87 
(*If novars then we forbid Vars in the equality. 
9532  88 
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

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

90 
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

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

94 
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

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

96 
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

97 
fun inspect_pair bnd novars (t,u,T) = 
9532  98 
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

99 
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

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

101 
case (contract t, contract u) of 
9532  102 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
103 
then raise Match 

104 
else true (*eliminates t*) 

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

106 
then raise Match 

107 
else false (*eliminates u*) 

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

109 
novars andalso has_vars u 

110 
then raise Match 

111 
else true (*eliminates t*) 

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

113 
novars andalso has_vars t 

114 
then raise Match 

115 
else false (*eliminates u*) 

0  116 
 _ => raise Match; 
117 

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

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

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

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

121 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
9532  122 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
123 
((k, inspect_pair bnd novars 

124 
(Data.dest_eq (Data.dest_Trueprop A))) 

125 
(*Exception comes from inspect_pair or dest_eq*) 

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

127 
 eq_var_aux k _ = raise EQ_VAR 

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

128 
in eq_var_aux 0 end; 
0  129 

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

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

131 
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

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

133 
[ if inspect_pair bnd false (Data.dest_eq 
9532  134 
(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

135 
then th RS Data.eq_reflection 
9532  136 
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

137 
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

138 

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

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

141 

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

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

143 
If bnd is true, then it replaces Bound variables only. *) 
13604  144 
fun gen_hyp_subst_tac bnd = 
145 
let val tac = SUBGOAL (fn (Bi, i) => 

146 
let val (k, _) = eq_var bnd true Bi 

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

147 
val hyp_subst_ss = empty_ss setmksimps (mk_eqs bnd) 
13604  148 
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, 
149 
etac thin_rl i, rotate_tac (~k) i] 

150 
end handle THM _ => no_tac  EQ_VAR => no_tac) 

151 
in REPEAT_DETERM1 o tac end; 

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

152 

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

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

154 

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

155 
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

156 

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

157 
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

158 

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

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

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

9532  163 
val (k,symopt) = eq_var bnd false Bi 
164 
in 

165 
DETERM 

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

166 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  167 
rotate_tac 1 i, 
168 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

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

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

0  171 
end 
3537  172 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  173 

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

175 
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], 
4223  176 
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; 
0  177 

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

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

180 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  181 

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

182 

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

184 
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

185 
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

186 

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

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

188 
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

189 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  190 
 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

191 
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

192 
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

193 

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

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

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

199 
Logic.strip_assums_concl > 

200 
Data.dest_Trueprop > Data.dest_imp 

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

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

203 
else (*leave affected hyps at end*) 

204 
(r+1, imp_intr_tac i) 

205 
in 

206 
case Seq.pull(tac st) of 

207 
None => Seq.single(st) 

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

209 
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

210 
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

211 

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

212 

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

213 
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

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

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

219 
in 

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

222 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  223 
rotate_tac 1 i, 
224 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

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

226 
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

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

228 
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

229 

9532  230 

231 
(*apply an equality or definition ONCE; 

232 
fails unless the substitution has an effect*) 

233 
fun stac th = 

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

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

236 

237 

9628  238 
(* proof methods *) 
9532  239 

9705  240 
val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac); 
10821  241 
val hyp_subst_meth = 
242 
Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac)); 

9532  243 

9628  244 

245 
(* theory setup *) 

246 

9532  247 
val hypsubst_setup = 
248 
[Method.add_methods 

9628  249 
[("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"), 
12377
c1e3e7d3f469
'symmetric' attribute moved to Pure/calculation.ML;
wenzelm
parents:
12262
diff
changeset

250 
("subst", subst_meth, "substitution")]]; 
9532  251 

0  252 
end; 