author  paulson 
Tue, 22 Jul 1997 11:12:55 +0200  
changeset 3537  79ac9b475621 
parent 2750  fe3799355b5e 
child 4179  cc4b6791d5dc 
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 
*) 
3537  119 
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => 
1011
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) 
2143  124 
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

125 
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

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

127 

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

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

129 
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

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

131 
[ 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

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

133 
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

134 
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

135 

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

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

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

138 

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

139 
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

140 

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

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

142 
Replaces only Bound variables if bnd is true*) 
3537  143 
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
144 
let 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

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

146 
in 
3537  147 
DETERM (EVERY [rotate_tac k i, 
148 
asm_full_simp_tac hyp_subst_ss i, 

149 
etac thin_rl i, 

150 
thin_leading_eqs_tac bnd (nk) i]) 

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

151 
end 
3537  152 
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

153 

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

154 
end; 
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 
val ssubst = standard (sym RS subst); 
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 
(*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

159 
to handle equalities containing Vars.*) 
3537  160 
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
161 
let 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

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

163 
in 
3537  164 
DETERM 
165 
(EVERY [REPEAT_DETERM_N k (etac rev_mp i), 

166 
etac revcut_rl i, 

167 
REPEAT_DETERM_N (nk) (etac rev_mp i), 

168 
etac (if symopt then ssubst else subst) i, 

169 
REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) 

0  170 
end 
3537  171 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  172 

173 
(*Substitutes for Free or Bound variables*) 

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

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

175 
gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; 
0  176 

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

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

179 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  180 

181 
end 

182 
end; 

183 