author  paulson 
Mon, 06 Aug 2001 12:42:43 +0200  
changeset 11461  ffeac9aa1967 
parent 10821  dcb75538f542 
child 12262  11ff5f47df6e 
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 

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

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

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

23 

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

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

26 

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

28 
\ 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

29 
by (blast_hyp_subst_tac (ref true) 1); 
0  30 
*) 
31 

32 
signature HYPSUBST_DATA = 

33 
sig 

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

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

35 
val dest_Trueprop : term > term 
9532  36 
val dest_eq : term > term*term*typ 
37 
val dest_imp : term > term*term 

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

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

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

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

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

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

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

45 
end; 
0  46 

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

47 

0  48 
signature HYPSUBST = 
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 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

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

54 
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

55 
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

56 
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

57 
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

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

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

0  62 
end; 
63 

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

64 

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

65 

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

69 
exception EQ_VAR; 

70 

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

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

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

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

76 
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

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

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

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

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

82 
end; 
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 
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

85 

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

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

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

89 
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

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

93 
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

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

95 
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

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

98 
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

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

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

103 
else true (*eliminates t*) 

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

105 
then raise Match 

106 
else false (*eliminates u*) 

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

108 
novars andalso has_vars u 

109 
then raise Match 

110 
else true (*eliminates t*) 

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

112 
novars andalso has_vars t 

113 
then raise Match 

114 
else false (*eliminates u*) 

0  115 
 _ => raise Match; 
116 

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

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

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

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

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

123 
(Data.dest_eq (Data.dest_Trueprop A))) 

124 
(*Exception comes from inspect_pair or dest_eq*) 

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

126 
 eq_var_aux k _ = raise EQ_VAR 

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

127 
in eq_var_aux 0 end; 
0  128 

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

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

130 
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

131 
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

132 
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

133 
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

134 
*) 
3537  135 
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

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

139 
1 + count Bs) 

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

140 
handle _ => 0) 
2143  141 
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

142 
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

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

144 

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

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

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

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

150 
then th RS Data.eq_reflection 
9532  151 
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

152 
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

153 

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

155 
in 
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 
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

158 

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

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

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

164 
in 

165 
DETERM (EVERY [rotate_tac k i, 

166 
asm_full_simp_tac hyp_subst_ss i, 

167 
etac thin_rl i, 

168 
thin_leading_eqs_tac bnd (nk) i]) 

169 
end 

170 
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

171 

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

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

173 

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

174 
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

175 

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

176 
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

177 

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

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

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

9532  182 
val (k,symopt) = eq_var bnd false Bi 
183 
in 

184 
DETERM 

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

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

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

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

0  190 
end 
3537  191 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  192 

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

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

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

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

199 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  200 

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

201 

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

203 
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

204 
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

205 

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

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

207 
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

208 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  209 
 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

210 
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

211 
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

212 

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

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

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

218 
Logic.strip_assums_concl > 

219 
Data.dest_Trueprop > Data.dest_imp 

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

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

222 
else (*leave affected hyps at end*) 

223 
(r+1, imp_intr_tac i) 

224 
in 

225 
case Seq.pull(tac st) of 

226 
None => Seq.single(st) 

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

228 
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

229 
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

230 

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

231 

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

232 
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

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

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

238 
in 

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

240 
DETERM 

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

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

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

245 
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

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

247 
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

248 

9532  249 

250 
(*apply an equality or definition ONCE; 

251 
fails unless the substitution has an effect*) 

252 
fun stac th = 

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

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

255 

256 

9628  257 
(* proof methods *) 
9532  258 

9705  259 
val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac); 
10821  260 
val hyp_subst_meth = 
261 
Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac)); 

9532  262 

9628  263 

264 
(* attributes *) 

265 

266 
fun symmetric_rule thm = 

267 
thm RS Drule.symmetric_thm handle THM _ => 

268 
thm RS Data.sym handle THM _ => error "Failed to apply symmetry of == or ="; 

269 

270 
fun gen_symmetric x = Drule.rule_attribute (K symmetric_rule); 

271 

272 

273 
(* theory setup *) 

274 

9532  275 
val hypsubst_setup = 
276 
[Method.add_methods 

9628  277 
[("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"), 
278 
("subst", subst_meth, "substitution")], 

279 
Attrib.add_attributes 

9893  280 
[("symmetric", (gen_symmetric, gen_symmetric), "resolution with symmetry of == or =")]]; 
9532  281 

0  282 
end; 