author  paulson 
Fri, 07 Mar 1997 10:22:54 +0100  
changeset 2750  fe3799355b5e 
parent 2722  3e07c20b967c 
child 3537  79ac9b475621 
permissions  rwrr 
0  1 
(* Title: Provers/hypsubst 
2 
ID: $Id$ 

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

3 
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson 
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 

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

6 
Tactic to substitute using the assumption x=t in the rest of the subgoal, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

7 
and to delete that assumption. Original version due to Martin Coen. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

8 

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

9 
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

10 

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

11 
Test data: 
0  12 

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

13 
goal thy "!!x.[ Q(x,y,z); y=x; a=x; z=y; P(y) ] ==> P(z)"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

14 
goal thy "!!x.[ Q(x,y,z); z=f(x); x=z ] ==> P(z)"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

15 
goal thy "!!y. [ ?x=y; P(?x) ] ==> y = a"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

16 
goal thy "!!z. [ ?x=y; P(?x) ] ==> y = a"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

17 

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

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

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

20 

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

21 
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

22 
goal thy "P(a) > (EX y. a=y > P(f(a)))"; 
0  23 
*) 
24 

25 
signature HYPSUBST_DATA = 

26 
sig 

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

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

28 
val dest_eq : term > term*term 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

29 
val eq_reflection : thm (* a=b ==> a==b *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

30 
val imp_intr : thm (* (P ==> Q) ==> P>Q *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

31 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

32 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

33 
val sym : thm (* a=b ==> b=a *) 
0  34 
end; 
35 

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

36 

0  37 
signature HYPSUBST = 
38 
sig 

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

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

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

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

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

44 
val eq_var : bool > bool > term > int * bool 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

45 
val inspect_pair : bool > bool > term * term > bool 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

47 
val thin_leading_eqs_tac : bool > int > int > tactic 
0  48 
end; 
49 

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

50 

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

51 

0  52 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
53 
struct 

54 

55 
local open Data in 

56 

57 
exception EQ_VAR; 

58 

2174  59 
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); 
0  60 

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

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

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

63 
(*Simplifier turns Bound variables to dotted Free variables: 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

64 
change it back (any Bound variable will do) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

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

67 
case Pattern.eta_contract_atom t of 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

68 
Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

70 
end; 
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 
fun has_vars t = maxidx_of_term t <> ~1; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

73 

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

74 
(*If novars then we forbid Vars in the equality. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

75 
If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

77 
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

78 
Not if it resembles x=t[x], since substitution does not eliminate x. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

79 
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

80 
Not if it involves a variable free in the premises, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

81 
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

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

83 
Result: true = use as is, false = reorient first *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

84 
fun inspect_pair bnd novars (t,u) = 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

85 
case (contract t, contract u) of 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

86 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

88 
else true (*eliminates t*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

89 
 (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

91 
else false (*eliminates u*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

92 
 (Free _, _) => if bnd orelse Logic.occs(t,u) orelse 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

93 
novars andalso has_vars u 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

95 
else true (*eliminates t*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

96 
 (_, Free _) => if bnd orelse Logic.occs(u,t) orelse 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

97 
novars andalso has_vars t 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

99 
else false (*eliminates u*) 
0  100 
 _ => raise Match; 
101 

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

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

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

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

105 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

106 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

107 
((k, inspect_pair bnd novars (dest_eq A)) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

108 
(*Exception comes from inspect_pair or dest_eq*) 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

109 
handle Match => eq_var_aux (k+1) B) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

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

111 
in eq_var_aux 0 end; 
0  112 

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

113 
(*We do not try to delete ALL equality assumptions at once. But 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

114 
it is easy to handle several consecutive equality assumptions in a row. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

115 
Note that we have to inspect the proof state after doing the rewriting, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

116 
since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

117 
must NOT be deleted. Tactic must rotate or delete m assumptions. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

119 
fun thin_leading_eqs_tac bnd m i = STATE(fn state => 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

120 
let fun count [] = 0 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

121 
 count (A::Bs) = ((inspect_pair bnd true (dest_eq A); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

122 
1 + count Bs) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

123 
handle Match => 0) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

124 
val (_,_,Bi,_) = dest_state(state,i) 
2143  125 
val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

126 
in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (mj) i 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

128 

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

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

130 
No vars are allowed here, as simpsets are built from metaassumptions*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

131 
fun mk_eqs th = 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

132 
[ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

133 
then th RS Data.eq_reflection 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

134 
else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

135 
handle Match => []; (*Exception comes from inspect_pair or dest_eq*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

136 

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

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

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

139 

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

140 
val hyp_subst_ss = empty_ss setmksimps mk_eqs 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

141 

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

142 
(*Select a suitable equality assumption and substitute throughout the subgoal 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

143 
Replaces only Bound variables if bnd is true*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

144 
fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

145 
let val (_,_,Bi,_) = dest_state(state,i) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

146 
val n = length(Logic.strip_assums_hyp Bi)  1 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

147 
val (k,_) = eq_var bnd true Bi 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

149 
EVERY [rotate_tac k i, 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

150 
asm_full_simp_tac hyp_subst_ss i, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

152 
thin_leading_eqs_tac bnd (nk) i] 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

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

154 
handle THM _ => no_tac  EQ_VAR => no_tac)); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

155 

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

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

157 

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

158 
val ssubst = standard (sym RS subst); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

159 

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

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

161 
to handle equalities containing Vars.*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

162 
fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => 
0  163 
let val (_,_,Bi,_) = dest_state(state,i) 
164 
val n = length(Logic.strip_assums_hyp Bi)  1 

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

165 
val (k,symopt) = eq_var bnd false Bi 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

166 
in 
704
b71b6be59354
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents:
680
diff
changeset

167 
EVERY [REPEAT_DETERM_N k (etac rev_mp i), 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

168 
etac revcut_rl i, 
704
b71b6be59354
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp
parents:
680
diff
changeset

169 
REPEAT_DETERM_N (nk) (etac rev_mp i), 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

170 
etac (if symopt then ssubst else subst) i, 
2750
fe3799355b5e
Prevent permutation of assumptions in hyp_subst_tac
paulson
parents:
2722
diff
changeset

171 
REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)] 
0  172 
end 
173 
handle THM _ => no_tac  EQ_VAR => no_tac)); 

174 

175 
(*Substitutes for Free or Bound variables*) 

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

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

177 
gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; 
0  178 

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

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

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

181 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  182 

183 
end 

184 
end; 

185 