author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 57509  cca0db87b653 
child 58826  2ed2eaabe3df 
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 
23908  53 
val blast_hyp_subst_tac : bool > int > tactic 
20945  54 
val stac : thm > int > tactic 
18708  55 
val hypsubst_setup : theory > theory 
21221  56 
end; 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

57 

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

61 
exception EQ_VAR; 

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. 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

83 
also returns var to substitute, relevant if it is Free *) 
21221  84 
fun inspect_pair bnd novars (t, u) = 
85 
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

86 
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

87 
else 
42082  88 
(case (contract t, contract u) of 
89 
(Bound i, _) => 

90 
if loose_bvar1 (u, i) orelse novars andalso has_vars u 

91 
then raise Match 

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

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

95 
then raise Match 

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

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

99 
then raise Match 

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

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

103 
then raise Match 

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

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

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

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

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

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

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

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

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

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

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

115 
 check_free ts (orient, _) = (orient, false) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

116 
fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

117 
 eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs = 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

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

120 
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

121 
 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

122 
 eq_var_aux k _ _ = raise EQ_VAR 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

123 

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

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

125 

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

126 
val thin_free_eq_tac = SUBGOAL (fn (t, i) => let 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

127 
val (k, _) = eq_var false false false t 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

128 
val ok = (eq_var false false true t > fst) > k 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

129 
handle EQ_VAR => true 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

131 
else no_tac 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
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 

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

142 
fun bool2s true = "true"  bool2s false = "false" 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

143 

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

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

146 

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

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

148 
If bnd is true, then it replaces Bound variables only. *) 
51798  149 
fun gen_hyp_subst_tac ctxt bnd = 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

150 
SUBGOAL (fn (Bi, i) => 
17896  151 
let 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

152 
val (k, (orient, is_free)) = eq_var bnd true true Bi 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50035
diff
changeset

153 
val hyp_subst_ctxt = empty_simpset ctxt > Simplifier.set_mksimps (K (mk_eqs bnd)) 
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50035
diff
changeset

154 
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

155 
if not is_free then etac thin_rl i 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

156 
else if orient then etac Data.rev_mp i 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

157 
else etac (Data.sym RS Data.rev_mp) i, 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

158 
rotate_tac (~k) i, 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

159 
if is_free then rtac Data.imp_intr i else all_tac] 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

160 
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

161 

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

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

163 

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

164 
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

165 

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

166 
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

167 
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

168 
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

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

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

171 
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

172 
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

173 
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

174 
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

175 
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

176 
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

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

178 
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

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

180 
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

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

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

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

184 
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

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

186 
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

187 
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U)); 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

188 
in 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

189 
compose_tac (true, Drule.instantiate_normalize (instT, 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

190 
map (pairself (cterm_of thy)) 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

191 
[(Var (ixn, Ts > U > body_type T), u), 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

192 
(Var (fst (dest_Var (head_of v1)), Ts > U), fold_rev Term.abs ps t), 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

193 
(Var (fst (dest_Var (head_of v2)), Ts > U), fold_rev Term.abs ps t')]) rl', 
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
45659
diff
changeset

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

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

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

197 

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

198 
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

199 

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

200 
fun rev_dup_elim th = (th RSN (2, revcut_rl)) > Thm.assumption 2 > Seq.hd; 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

201 
val dup_subst = rev_dup_elim ssubst 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

202 

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

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

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

205 

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

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

207 
to handle equalities containing Vars.*) 
3537  208 
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
209 
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

210 
val (k, (orient, is_free)) = eq_var bnd false true Bi 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

211 
val rl = if is_free then dup_subst else ssubst 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

212 
val rl = if orient then rl else Data.sym RS rl 
9532  213 
in 
214 
DETERM 

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

215 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  216 
rotate_tac 1 i, 
217 
REPEAT_DETERM_N (nk) (etac Data.rev_mp i), 

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

218 
inst_subst_tac orient rl i, 
9532  219 
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) 
0  220 
end 
3537  221 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  222 

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

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

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

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

226 
fun hyp_subst_tac_thin thin ctxt = 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

227 
REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl], 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

228 
gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false, 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

230 

57509  231 
val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

232 
@{binding hypsubst_thin} (K false); 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

233 

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

234 
fun hyp_subst_tac ctxt = hyp_subst_tac_thin 
57509  235 
(Config.get ctxt hyp_subst_thin) ctxt 
0  236 

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

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

239 
REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

241 

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

243 
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

244 
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

245 

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

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

247 
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

248 
 reverse_n_tac 1 i = rotate_tac ~1 i 
9532  249 
 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

250 
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

251 
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

252 

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

253 
(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 
9532  254 
fun all_imp_intr_tac hyps i = 
42364  255 
let 
256 
fun imptac (r, []) st = reverse_n_tac r i st 

257 
 imptac (r, hyp::hyps) st = 

258 
let 

259 
val (hyp', _) = 

42366
2305c70ec9b1
more direct Thm.cprem_of (with exception THM instead of Subscript);
wenzelm
parents:
42364
diff
changeset

260 
term_of (Thm.cprem_of st i) 
42364  261 
> Logic.strip_assums_concl 
262 
> Data.dest_Trueprop > Data.dest_imp; 

263 
val (r', tac) = 

52131  264 
if Envir.aeconv (hyp, hyp') 
42364  265 
then (r, imp_intr_tac i THEN rotate_tac ~1 i) 
266 
else (*leave affected hyps at end*) (r + 1, imp_intr_tac i); 

267 
in 

268 
(case Seq.pull (tac st) of 

269 
NONE => Seq.single st 

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

271 
end 

272 
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

273 

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

274 

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

275 
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

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

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

281 
in 

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

284 
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), 
9532  285 
rotate_tac 1 i, 
286 
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

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

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

290 
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

291 

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

294 
fun stac th = 

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

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

297 

298 

9628  299 
(* theory setup *) 
300 

9532  301 
val hypsubst_setup = 
30515  302 
Method.setup @{binding hypsubst} 
51798  303 
(Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) 
30515  304 
"substitution using an assumption (improper)" #> 
57492
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

305 
Method.setup @{binding hypsubst_thin} 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

306 
(Scan.succeed (fn ctxt => SIMPLE_METHOD' 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

307 
(CHANGED_PROP o hyp_subst_tac_thin true ctxt))) 
74bf65a1910a
Hypsubst preserves equality hypotheses
Thomas Sewell <thomas.sewell@nicta.com.au>
parents:
56245
diff
changeset

308 
"substitution using an assumption, eliminating assumptions" #> 
57509  309 
hyp_subst_thin_setup #> 
30515  310 
Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th)))) 
311 
"simple substitution"; 

9532  312 

0  313 
end; 