114 it is easy to handle several consecutive equality assumptions in a row. |
114 it is easy to handle several consecutive equality assumptions in a row. |
115 Note that we have to inspect the proof state after doing the rewriting, |
115 Note that we have to inspect the proof state after doing the rewriting, |
116 since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality |
116 since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality |
117 must NOT be deleted. Tactic must rotate or delete m assumptions. |
117 must NOT be deleted. Tactic must rotate or delete m assumptions. |
118 *) |
118 *) |
119 fun thin_leading_eqs_tac bnd m i = STATE(fn state => |
119 fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => |
120 let fun count [] = 0 |
120 let fun count [] = 0 |
121 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); |
121 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); |
122 1 + count Bs) |
122 1 + count Bs) |
123 handle Match => 0) |
123 handle Match => 0) |
124 val (_,_,Bi,_) = dest_state(state,i) |
|
125 val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) |
124 val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) |
126 in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i |
125 in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i |
127 end); |
126 end); |
128 |
127 |
129 (*For the simpset. Adds ALL suitable equalities, even if not first! |
128 (*For the simpset. Adds ALL suitable equalities, even if not first! |
139 |
138 |
140 val hyp_subst_ss = empty_ss setmksimps mk_eqs |
139 val hyp_subst_ss = empty_ss setmksimps mk_eqs |
141 |
140 |
142 (*Select a suitable equality assumption and substitute throughout the subgoal |
141 (*Select a suitable equality assumption and substitute throughout the subgoal |
143 Replaces only Bound variables if bnd is true*) |
142 Replaces only Bound variables if bnd is true*) |
144 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
143 fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
145 let val (_,_,Bi,_) = dest_state(state,i) |
144 let val n = length(Logic.strip_assums_hyp Bi) - 1 |
146 val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
147 val (k,_) = eq_var bnd true Bi |
145 val (k,_) = eq_var bnd true Bi |
148 in |
146 in |
149 EVERY [rotate_tac k i, |
147 DETERM (EVERY [rotate_tac k i, |
150 asm_full_simp_tac hyp_subst_ss i, |
148 asm_full_simp_tac hyp_subst_ss i, |
151 etac thin_rl i, |
149 etac thin_rl i, |
152 thin_leading_eqs_tac bnd (n-k) i] |
150 thin_leading_eqs_tac bnd (n-k) i]) |
153 end |
151 end |
154 handle THM _ => no_tac | EQ_VAR => no_tac)); |
152 handle THM _ => no_tac | EQ_VAR => no_tac); |
155 |
153 |
156 end; |
154 end; |
157 |
155 |
158 val ssubst = standard (sym RS subst); |
156 val ssubst = standard (sym RS subst); |
159 |
157 |
160 (*Old version of the tactic above -- slower but the only way |
158 (*Old version of the tactic above -- slower but the only way |
161 to handle equalities containing Vars.*) |
159 to handle equalities containing Vars.*) |
162 fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
160 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => |
163 let val (_,_,Bi,_) = dest_state(state,i) |
161 let val n = length(Logic.strip_assums_hyp Bi) - 1 |
164 val n = length(Logic.strip_assums_hyp Bi) - 1 |
|
165 val (k,symopt) = eq_var bnd false Bi |
162 val (k,symopt) = eq_var bnd false Bi |
166 in |
163 in |
167 EVERY [REPEAT_DETERM_N k (etac rev_mp i), |
164 DETERM |
168 etac revcut_rl i, |
165 (EVERY [REPEAT_DETERM_N k (etac rev_mp i), |
169 REPEAT_DETERM_N (n-k) (etac rev_mp i), |
166 etac revcut_rl i, |
170 etac (if symopt then ssubst else subst) i, |
167 REPEAT_DETERM_N (n-k) (etac rev_mp i), |
171 REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)] |
168 etac (if symopt then ssubst else subst) i, |
|
169 REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) |
172 end |
170 end |
173 handle THM _ => no_tac | EQ_VAR => no_tac)); |
171 handle THM _ => no_tac | EQ_VAR => no_tac); |
174 |
172 |
175 (*Substitutes for Free or Bound variables*) |
173 (*Substitutes for Free or Bound variables*) |
176 val hyp_subst_tac = |
174 val hyp_subst_tac = |
177 gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; |
175 gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; |
178 |
176 |