equal
deleted
inserted
replaced
256 (** equivarance proofs **) |
256 (** equivarance proofs **) |
257 |
257 |
258 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
258 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
259 |
259 |
260 fun subproof_tac const_names simps = |
260 fun subproof_tac const_names simps = |
261 Subgoal.FOCUS (fn {prems, context, ...} => |
261 SUBPROOF (fn {prems, context, ...} => |
262 HEADGOAL |
262 HEADGOAL |
263 (simp_tac (HOL_basic_ss addsimps simps) |
263 (simp_tac (HOL_basic_ss addsimps simps) |
264 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
264 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
265 THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems)))) |
265 THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym])))) |
266 |
266 |
267 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
267 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
268 HEADGOAL |
268 HEADGOAL |
269 (Object_Logic.full_atomize_tac |
269 (Object_Logic.full_atomize_tac |
270 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |
270 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |