author  haftmann 
Thu, 18 Nov 2010 17:01:15 +0100  
changeset 40602  91e583511113 
parent 39782  f75381bc46d2 
child 42082  47f8bfe0f597 
permissions  rwrr 
9532  1 
(* Title: Provers/hypsubst.ML 
2 
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

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

4 

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

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

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

9 
version due to Martin Coen. 

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

10 

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

11 
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

12 

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

13 
Test data: 
0  14 

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

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

18 
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

19 

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

20 
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

21 

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

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

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

24 

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

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

27 

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

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

33 
signature HYPSUBST_DATA = 

21221  34 
sig 
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 
21221  36 
val dest_eq : term > term * term 
20974  37 
val dest_imp : term > term * term 
9532  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 *) 
21221  45 
end; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

46 

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

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

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

55 

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

59 
exception EQ_VAR; 

60 

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

16979  63 
(*Simplifier turns Bound variables to special Free variables: 
64 
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

65 
fun contract t = 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

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

69 

21221  70 
val has_vars = Term.exists_subterm Term.is_Var; 
71 
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

72 

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

73 
(*If novars then we forbid Vars in the equality. 
16979  74 
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

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

76 
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

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

80 
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

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

82 
Result: true = use as is, false = reorient first *) 
21221  83 
fun inspect_pair bnd novars (t, u) = 
84 
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

85 
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

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

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

90 
else true (*eliminates t*) 

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

92 
then raise Match 

93 
else false (*eliminates u*) 

39297
4f9e933a16e2
use etacontracted version for occurrence check (avoids possible nontermination)
krauss
parents:
36945
diff
changeset

94 
 (t' as Free _, _) => if bnd orelse Logic.occs(t',u) orelse 
9532  95 
novars andalso has_vars u 
96 
then raise Match 

97 
else true (*eliminates t*) 

39297
4f9e933a16e2
use etacontracted version for occurrence check (avoids possible nontermination)
krauss
parents:
36945
diff
changeset

98 
 (_, u' as Free _) => if bnd orelse Logic.occs(u',t) orelse 
9532  99 
novars andalso has_vars t 
100 
then raise Match 

101 
else false (*eliminates u*) 

0  102 
 _ => raise Match; 
103 

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

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

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

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

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

110 
(Data.dest_eq (Data.dest_Trueprop A))) 

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

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

114 
in eq_var_aux 0 end; 
0  115 

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

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

117 
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

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

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

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

124 

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

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

127 

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

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

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

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

35232
f588e1169c8b
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
wenzelm
parents:
35021
diff
changeset

134 
val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss 
36543
0e7fc5bf38de
proper context for mksimps etc.  via simpset of the running Simplifier;
wenzelm
parents:
35762
diff
changeset

135 
setmksimps (K (mk_eqs bnd)) 
13604  136 
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i, 
137 
etac thin_rl i, rotate_tac (~k) i] 

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

140 

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 

35021
c839a4c670c6
renamed oldstyle Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents:
32957
diff
changeset

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

144 

26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

145 
fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) => 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

146 
case try (Logic.strip_assums_hyp #> hd #> 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

147 
Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

148 
SOME (t, t') => 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

149 
let 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

150 
val Bi = Thm.term_of cBi; 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

151 
val ps = Logic.strip_params Bi; 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

152 
val U = Term.fastype_of1 (rev (map snd ps), t); 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

153 
val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi); 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

154 
val rl' = Thm.lift_rule cBi rl; 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

155 
val Var (ixn, T) = Term.head_of (Data.dest_Trueprop 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

156 
(Logic.strip_assums_concl (Thm.prop_of rl'))); 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

157 
val (v1, v2) = Data.dest_eq (Data.dest_Trueprop 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

158 
(Logic.strip_assums_concl (hd (Thm.prems_of rl')))); 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

159 
val (Ts, V) = split_last (Term.binder_types T); 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

160 
val u = list_abs (ps @ [("x", U)], case (if b then t else t') of 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

161 
Bound j => subst_bounds (map Bound 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

162 
((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

163 
 t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

164 
val thy = Thm.theory_of_thm rl'; 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

165 
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U)); 
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

166 
in compose_tac (true, Drule.instantiate (instT, 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

167 
map (pairself (cterm_of thy)) 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

168 
[(Var (ixn, Ts > U > body_type T), u), 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

169 
(Var (fst (dest_Var (head_of v1)), Ts > U), list_abs (ps, t)), 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

170 
(Var (fst (dest_Var (head_of v2)), Ts > U), list_abs (ps, t'))]) rl', 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

171 
nprems_of rl) i 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

172 
end 
26992
4508f20818af
inst_subst_tac: match types  no longer assume that subst rule has exactly one type argument;
wenzelm
parents:
26833
diff
changeset

173 
 NONE => no_tac); 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

174 

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

175 
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

176 

26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

177 
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

178 
(* premises containing metaimplications or quantifiers *) 
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

179 

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

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

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

9532  184 
val (k,symopt) = eq_var bnd false Bi 
185 
in 

186 
DETERM 

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

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

26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

190 
inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, 
9532  191 
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) 
0  192 
end 
3537  193 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  194 

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

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

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

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

201 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  202 

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

203 

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

205 
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

206 
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

207 

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

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

209 
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

210 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  211 
 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

212 
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

213 
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

214 

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

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

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

220 
Logic.strip_assums_concl > 

221 
Data.dest_Trueprop > Data.dest_imp 

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

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

224 
else (*leave affected hyps at end*) 

225 
(r+1, imp_intr_tac i) 

226 
in 

227 
case Seq.pull(tac st) of 

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

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

231 
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

232 

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

233 

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

234 
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

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

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

240 
in 

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

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

26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

246 
inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, 
9532  247 
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

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

249 
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

250 

9532  251 

252 
(*apply an equality or definition ONCE; 

253 
fails unless the substitution has an effect*) 

254 
fun stac th = 

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

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

257 

258 

9628  259 
(* theory setup *) 
260 

9532  261 
val hypsubst_setup = 
30515  262 
Method.setup @{binding hypsubst} 
263 
(Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)))) 

264 
"substitution using an assumption (improper)" #> 

265 
Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th)))) 

266 
"simple substitution"; 

9532  267 

0  268 
end; 