author  wenzelm 
Fri, 08 Jan 2021 22:30:32 +0100  
changeset 73110  c87ca43ebd3b 
parent 71406  3887432720a9 
child 74282  c2ee8d993d6a 
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 

48107
6cebeee3863e
Updated comment to reflect current state.
Rafal Kolanski <rafal.kolanski@nicta.com.au>
parents:
46219
diff
changeset

5 
Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst". 
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 
51798  49 
val bound_hyp_subst_tac : Proof.context > int > tactic 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

50 
val hyp_subst_tac_thin : bool > Proof.context > int > tactic 
57509  51 
val hyp_subst_thin : bool Config.T 
51798  52 
val hyp_subst_tac : Proof.context > int > tactic 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

53 
val blast_hyp_subst_tac : Proof.context > bool > int > tactic 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

54 
val stac : Proof.context > thm > int > tactic 
21221  55 
end; 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

56 

42799  57 
functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = 
0  58 
struct 
59 

60 
exception EQ_VAR; 

61 

16979  62 
(*Simplifier turns Bound variables to special Free variables: 
63 
change it back (any Bound variable will do)*) 

60706
03a6b1792cd8
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents:
60642
diff
changeset

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

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

68 

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

71 

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

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

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

75 
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

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

79 
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

80 
Prefer to eliminate Bound variables if possible. 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

81 
Result: true = use as is, false = reorient first 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

82 
also returns var to substitute, relevant if it is Free *) 
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 
60706
03a6b1792cd8
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents:
60642
diff
changeset

87 
(case apply2 inspect_contract (t, u) of 
42082  88 
(Bound i, _) => 
89 
if loose_bvar1 (u, i) orelse novars andalso has_vars u 

90 
then raise Match 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

91 
else (true, Bound i) (*eliminates t*) 
42082  92 
 (_, Bound i) => 
93 
if loose_bvar1 (t, i) orelse novars andalso has_vars t 

94 
then raise Match 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

95 
else (false, Bound i) (*eliminates u*) 
42082  96 
 (t' as Free _, _) => 
97 
if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u 

98 
then raise Match 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

99 
else (true, t') (*eliminates t*) 
42082  100 
 (_, u' as Free _) => 
101 
if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t 

102 
then raise Match 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

103 
else (false, u') (*eliminates u*) 
42082  104 
 _ => raise Match); 
0  105 

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

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

107 
assumption. Returns the number of intervening assumptions. *) 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

108 
fun eq_var bnd novars check_frees t = 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

109 
let 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

110 
fun check_free ts (orient, Free f) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

111 
= if not check_frees orelse not orient 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

112 
orelse exists (curry Logic.occs (Free f)) ts 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

113 
then (orient, true) else raise Match 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

114 
 check_free ts (orient, _) = (orient, false) 
69593  115 
fun eq_var_aux k (Const(\<^const_name>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs 
116 
 eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ A $ B) hs = 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

117 
((k, check_free (B :: hs) (inspect_pair bnd novars 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

118 
(Data.dest_eq (Data.dest_Trueprop A)))) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

119 
handle TERM _ => eq_var_aux (k+1) B (A :: hs) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

120 
 Match => eq_var_aux (k+1) B (A :: hs)) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

121 
 eq_var_aux k _ _ = raise EQ_VAR 
58826  122 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

123 
in eq_var_aux 0 t [] end; 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

124 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

125 
fun thin_free_eq_tac ctxt = SUBGOAL (fn (t, i) => 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

126 
let 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

127 
val (k, _) = eq_var false false false t 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

128 
val ok = (eq_var false false true t > fst) > k handle EQ_VAR => true 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

129 
in 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

130 
if ok then EVERY [rotate_tac k i, eresolve_tac ctxt [thin_rl] i, rotate_tac (~k) i] 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

131 
else no_tac 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

132 
end handle EQ_VAR => no_tac) 
0  133 

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

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

135 
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

136 
fun mk_eqs bnd th = 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

137 
[ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) > fst 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

141 

71406  142 
(*Select a suitable equality assumption; substitute throughout the subgoal 
143 
If bnd is true, then it replaces Bound variables only. *) 

144 
fun gen_hyp_subst_tac ctxt bnd = 

145 
SUBGOAL (fn (Bi, i) => 

146 
let 

147 
val (k, (orient, is_free)) = eq_var bnd true true Bi 

148 
val hyp_subst_ctxt = empty_simpset ctxt > Simplifier.set_mksimps (K (mk_eqs bnd)) 

149 
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, 

150 
if not is_free then eresolve_tac ctxt [thin_rl] i 

151 
else if orient then eresolve_tac ctxt [Data.rev_mp] i 

152 
else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i, 

153 
rotate_tac (~k) i, 

154 
if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac] 

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

156 

45659
09539cdffcd7
avoid stepping outside of context  plain zero_var_indexes should be sufficient;
wenzelm
parents:
45625
diff
changeset

157 
val ssubst = Drule.zero_var_indexes (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

158 

58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

159 
fun inst_subst_tac ctxt 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

160 
case try (Logic.strip_assums_hyp #> hd #> 
60706
03a6b1792cd8
clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e);
wenzelm
parents:
60642
diff
changeset

161 
Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_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

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

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

164 
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

165 
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

166 
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

167 
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

168 
val rl' = Thm.lift_rule cBi rl; 
71402  169 
val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop 
170 
(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

171 
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

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

173 
val (Ts, V) = split_last (Term.binder_types T); 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

174 
val u = 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

175 
fold_rev Term.abs (ps @ [("x", U)]) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

176 
(case (if b then t else t') of 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

177 
Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

178 
 t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); 
59642  179 
val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

180 
in 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

181 
compose_tac ctxt (true, Drule.instantiate_normalize (instT, 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset

182 
map (apsnd (Thm.cterm_of ctxt)) 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset

183 
[((ixn, Ts > U > body_type T), u), 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset

184 
((fst (dest_Var (head_of v1)), Ts > U), fold_rev Term.abs ps t), 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59642
diff
changeset

185 
((fst (dest_Var (head_of v2)), Ts > U), fold_rev Term.abs ps t')]) rl', 
59582  186 
Thm.nprems_of rl) i 
26833
7c3757fccf0e
Added function for computing instantiation for the subst rule, which is used
berghofe
parents:
23908
diff
changeset

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

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

189 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

190 
fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr]; 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

191 

58958  192 
fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) > Thm.assumption (SOME ctxt) 2 > Seq.hd; 
193 
fun dup_subst ctxt = rev_dup_elim ctxt ssubst 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

194 

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

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

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

197 

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

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

199 
to handle equalities containing Vars.*) 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

200 
fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) => 
3537  201 
let val n = length(Logic.strip_assums_hyp Bi)  1 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

202 
val (k, (orient, is_free)) = eq_var bnd false true Bi 
58958  203 
val rl = if is_free then dup_subst ctxt else ssubst 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

204 
val rl = if orient then rl else Data.sym RS rl 
9532  205 
in 
206 
DETERM 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

207 
(EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 
9532  208 
rotate_tac 1 i, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

209 
REPEAT_DETERM_N (nk) (eresolve_tac ctxt [Data.rev_mp] i), 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

210 
inst_subst_tac ctxt orient rl i, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

211 
REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)]) 
0  212 
end 
3537  213 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  214 

57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

215 
(*Substitutes for Free or Bound variables, 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

216 
discarding equalities on Bound variables 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

217 
and on Free variables if thin=true*) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

218 
fun hyp_subst_tac_thin thin ctxt = 
58957  219 
REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl], 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

220 
gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false, 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

221 
if thin then thin_free_eq_tac ctxt else K no_tac]; 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

222 

69593  223 
val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\<open>hypsubst_thin\<close> (K false); 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

224 

58826  225 
fun hyp_subst_tac ctxt = 
226 
hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt; 

0  227 

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

51798  229 
fun bound_hyp_subst_tac ctxt = 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

230 
REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true 
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
58950
diff
changeset

231 
ORELSE' vars_gen_hyp_subst_tac ctxt true); 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

232 

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

234 
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

235 
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

236 

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

237 
(*final rereversal of the changed assumptions*) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

238 
fun reverse_n_tac _ 0 i = all_tac 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

239 
 reverse_n_tac _ 1 i = rotate_tac ~1 i 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

240 
 reverse_n_tac ctxt n i = 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

241 
REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

242 
REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i); 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

243 

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

244 
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

245 
fun all_imp_intr_tac ctxt hyps i = 
42364  246 
let 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

247 
fun imptac (r, []) st = reverse_n_tac ctxt r i st 
42364  248 
 imptac (r, hyp::hyps) st = 
249 
let 

250 
val (hyp', _) = 

59582  251 
Thm.term_of (Thm.cprem_of st i) 
42364  252 
> Logic.strip_assums_concl 
253 
> Data.dest_Trueprop > Data.dest_imp; 

254 
val (r', tac) = 

52131  255 
if Envir.aeconv (hyp, hyp') 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

256 
then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

257 
else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i); 
42364  258 
in 
259 
(case Seq.pull (tac st) of 

260 
NONE => Seq.single st 

261 
 SOME (st', _) => imptac (r', hyps) st') 

262 
end 

263 
in imptac (0, rev hyps) end; 

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

264 

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

265 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

266 
fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) => 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

267 
let 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

268 
val (k, (symopt, _)) = eq_var false false false Bi 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

269 
val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

270 
(*omit selected equality, returning other hyps*) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

271 
val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

272 
val n = length hyps 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

273 
in 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

274 
if trace then tracing "Substituting an equality" else (); 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

275 
DETERM 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

276 
(EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

277 
rotate_tac 1 i, 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

278 
REPEAT_DETERM_N (nk) (eresolve_tac ctxt [Data.rev_mp] i), 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

279 
inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i, 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

280 
all_imp_intr_tac ctxt hyps i]) 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

281 
end 
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

282 
handle THM _ => no_tac  EQ_VAR => no_tac); 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4299
diff
changeset

283 

9532  284 
(*apply an equality or definition ONCE; 
285 
fails unless the substitution has an effect*) 

59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

286 
fun stac ctxt th = 
9532  287 
let val th' = th RS Data.rev_eq_reflection handle THM _ => th 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

288 
in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end; 
9532  289 

290 

58826  291 
(* method setup *) 
9628  292 

58826  293 
val _ = 
294 
Theory.setup 

69593  295 
(Method.setup \<^binding>\<open>hypsubst\<close> 
58826  296 
(Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) 
297 
"substitution using an assumption (improper)" #> 

69593  298 
Method.setup \<^binding>\<open>hypsubst_thin\<close> 
58826  299 
(Scan.succeed (fn ctxt => SIMPLE_METHOD' 
300 
(CHANGED_PROP o hyp_subst_tac_thin true ctxt))) 

301 
"substitution using an assumption, eliminating assumptions" #> 

69593  302 
Method.setup \<^binding>\<open>simplesubst\<close> 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59058
diff
changeset

303 
(Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th))) 
58826  304 
"simple substitution"); 
9532  305 

0  306 
end; 