164 fun cooper_tac elim add_ths del_ths ctxt = |
164 fun cooper_tac elim add_ths del_ths ctxt = |
165 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths |
165 let val ss = Simplifier.context ctxt (fst (CooperData.get ctxt)) delsimps del_ths addsimps add_ths |
166 val aprems = Arith_Data.get_arith_facts ctxt |
166 val aprems = Arith_Data.get_arith_facts ctxt |
167 in |
167 in |
168 Method.insert_tac aprems |
168 Method.insert_tac aprems |
169 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
169 THEN_ALL_NEW Object_Logic.full_atomize_tac |
170 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
170 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
171 THEN_ALL_NEW simp_tac ss |
171 THEN_ALL_NEW simp_tac ss |
172 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
172 THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
173 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
173 THEN_ALL_NEW Object_Logic.full_atomize_tac |
174 THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt)) |
174 THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt)) |
175 THEN_ALL_NEW ObjectLogic.full_atomize_tac |
175 THEN_ALL_NEW Object_Logic.full_atomize_tac |
176 THEN_ALL_NEW div_mod_tac ctxt |
176 THEN_ALL_NEW div_mod_tac ctxt |
177 THEN_ALL_NEW splits_tac ctxt |
177 THEN_ALL_NEW splits_tac ctxt |
178 THEN_ALL_NEW simp_tac ss |
178 THEN_ALL_NEW simp_tac ss |
179 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
179 THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
180 THEN_ALL_NEW nat_to_int_tac ctxt |
180 THEN_ALL_NEW nat_to_int_tac ctxt |