author  wenzelm 
Mon, 04 Aug 2008 22:55:00 +0200  
changeset 27734  dcec1c564f05 
parent 27572  67cd6ed76446 
child 30510  4120fc59dd85 
permissions  rwrr 
9532  1 
(* Title: Provers/hypsubst.ML 
0  2 
ID: $Id$ 
9532  3 
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

5 

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

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

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

10 
version due to Martin Coen. 

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

11 

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

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

13 

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

14 
Test data: 
0  15 

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

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

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

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

20 

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

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

22 

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

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

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

25 

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

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

28 

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

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

34 
signature HYPSUBST_DATA = 

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

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

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

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

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

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

4223  45 
val thin_refl : thm (* [x=x; PROP W] ==> PROP W *) 
27572
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

46 
val prop_subst : thm (* PROP P t ==> PROP prop (x = t ==> PROP P x) *) 
21221  47 
end; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

48 

0  49 
signature HYPSUBST = 
21221  50 
sig 
27572
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

51 
val single_hyp_subst_tac : int > int > tactic 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

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

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

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

59 

9532  60 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
0  61 
struct 
62 

63 
exception EQ_VAR; 

64 

27734
dcec1c564f05
meta_subst: xsymbols make it work with clean Pure;
wenzelm
parents:
27572
diff
changeset

65 
val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)" 
27572
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

66 
by (unfold prop_def)} 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

67 

67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

68 
(** Simple version: Just subtitute one hypothesis, specified by index k **) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

69 
fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) => 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

70 
let 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

71 
val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

72 
> cterm_of (theory_of_cterm csubg) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

73 

67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

74 
val rule = 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

75 
Thm.lift_rule pat subst_rule (* lift just over parameters *) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

76 
> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}]) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

77 
in 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

78 
rotate_tac k i 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

79 
THEN Thm.compose_no_flatten false (rule, 1) i 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

80 
THEN rotate_tac (~k) i 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

81 
end) 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

82 

67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

83 
val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

84 
val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst 
67cd6ed76446
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
krauss
parents:
26992
diff
changeset

85 

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

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

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

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

94 

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

97 

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

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

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

101 
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

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

105 
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

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

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

110 
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

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

112 
case (contract t, contract u) of 
9532  113 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
114 
then raise Match 

115 
else true (*eliminates t*) 

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

117 
then raise Match 

118 
else false (*eliminates u*) 

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

120 
novars andalso has_vars u 

121 
then raise Match 

122 
else true (*eliminates t*) 

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

124 
novars andalso has_vars t 

125 
then raise Match 

126 
else false (*eliminates u*) 

0  127 
 _ => raise Match; 
128 

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

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

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

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

132 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
9532  133 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
134 
((k, inspect_pair bnd novars 

135 
(Data.dest_eq (Data.dest_Trueprop A))) 

21227  136 
handle TERM _ => eq_var_aux (k+1) B 
137 
 Match => eq_var_aux (k+1) B) 

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

139 
in eq_var_aux 0 end; 
0  140 

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

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

142 
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

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

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

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

149 

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

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

152 

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

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

154 
If bnd is true, then it replaces Bound variables only. *) 
13604  155 
fun gen_hyp_subst_tac bnd = 
17896  156 
let fun tac i st = SUBGOAL (fn (Bi, _) => 
157 
let 

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

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

160 
setmksimps (mk_eqs bnd) 

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

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

165 

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

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

167 

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

168 
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

169 

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

170 
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

171 
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

172 
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

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

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

175 
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

176 
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

177 
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

178 
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

179 
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

180 
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

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

182 
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

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

184 
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

185 
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

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

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

188 
 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

189 
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

190 
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

191 
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

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

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

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

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

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

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

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

199 

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

200 
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

201 

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

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

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

204 

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

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

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

9532  209 
val (k,symopt) = eq_var bnd false Bi 
210 
in 

211 
DETERM 

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

212 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  213 
rotate_tac 1 i, 
214 
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

215 
inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, 
9532  216 
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) 
0  217 
end 
3537  218 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  219 

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

221 
val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl], 
4223  222 
gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false]; 
0  223 

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

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

226 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  227 

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

228 

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

230 
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

231 
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

232 

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

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

234 
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

235 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  236 
 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

237 
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

238 
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

239 

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

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

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

245 
Logic.strip_assums_concl > 

246 
Data.dest_Trueprop > Data.dest_imp 

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

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

249 
else (*leave affected hyps at end*) 

250 
(r+1, imp_intr_tac i) 

251 
in 

252 
case Seq.pull(tac st) of 

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

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

256 
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

257 

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

258 

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

259 
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

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

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

265 
in 

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

268 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  269 
rotate_tac 1 i, 
270 
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

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

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

274 
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

275 

9532  276 

277 
(*apply an equality or definition ONCE; 

278 
fails unless the substitution has an effect*) 

279 
fun stac th = 

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

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

282 

283 

9628  284 
(* theory setup *) 
285 

9532  286 
val hypsubst_setup = 
18708  287 
Method.add_methods 
21588  288 
[("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)), 
289 
"substitution using an assumption (improper)"), 

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

9532  291 

0  292 
end; 