244 end |
244 end |
245 |
245 |
246 |
246 |
247 (** equivarance proofs **) |
247 (** equivarance proofs **) |
248 |
248 |
249 fun mk_eqvt_goal pi const arg = |
249 val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} |
250 let |
250 |
251 val lhs = mk_perm pi (const $ arg) |
251 fun subproof_tac const_names simps = |
252 val rhs = const $ (mk_perm pi arg) |
|
253 in |
|
254 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
255 end |
|
256 |
|
257 fun subproof_tac const_names simps ctxt = |
|
258 Subgoal.FOCUS (fn {prems, context, ...} => |
252 Subgoal.FOCUS (fn {prems, context, ...} => |
259 HEADGOAL |
253 HEADGOAL |
260 (simp_tac (HOL_basic_ss addsimps simps) |
254 (simp_tac (HOL_basic_ss addsimps simps) |
261 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
255 THEN' Nominal_Permeq.eqvt_tac context [] const_names |
262 THEN' simp_tac (HOL_basic_ss addsimps (@{thms eqvt_apply[symmetric]} @ prems)))) ctxt |
256 THEN' simp_tac (HOL_basic_ss addsimps (eqvt_apply_sym :: prems)))) |
|
257 |
|
258 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = |
|
259 HEADGOAL |
|
260 (Object_Logic.full_atomize_tac |
|
261 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |
|
262 THEN_ALL_NEW subproof_tac const_names simps ctxt) |
|
263 |
|
264 fun mk_eqvt_goal pi const arg = |
|
265 let |
|
266 val lhs = mk_perm pi (const $ arg) |
|
267 val rhs = const $ (mk_perm pi arg) |
|
268 in |
|
269 HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
270 end |
263 |
271 |
264 fun raw_prove_eqvt consts ind_thms simps ctxt = |
272 fun raw_prove_eqvt consts ind_thms simps ctxt = |
265 if null consts then [] |
273 if null consts then [] |
266 else |
274 else |
267 let |
275 let |
269 val p = Free (p, @{typ perm}) |
277 val p = Free (p, @{typ perm}) |
270 val arg_tys = |
278 val arg_tys = |
271 consts |
279 consts |
272 |> map fastype_of |
280 |> map fastype_of |
273 |> map domain_type |
281 |> map domain_type |
274 val (arg_names, ctxt'') = Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' |
282 val (arg_names, ctxt'') = |
|
283 Variable.variant_fixes (Datatype_Prop.make_tnames arg_tys) ctxt' |
275 val args = map Free (arg_names ~~ arg_tys) |
284 val args = map Free (arg_names ~~ arg_tys) |
276 val goals = map2 (mk_eqvt_goal p) consts args |
285 val goals = map2 (mk_eqvt_goal p) consts args |
277 val insts = map (single o SOME) arg_names |
286 val insts = map (single o SOME) arg_names |
278 val const_names = map (fst o dest_Const) consts |
287 val const_names = map (fst o dest_Const) consts |
279 |
|
280 fun tac ctxt = |
|
281 Object_Logic.full_atomize_tac |
|
282 THEN' (DETERM o (InductTacs.induct_rules_tac ctxt insts ind_thms)) |
|
283 THEN_ALL_NEW subproof_tac const_names simps ctxt |
|
284 in |
288 in |
285 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => (HEADGOAL (tac context))) |
289 Goal.prove_multi ctxt'' [] [] goals (fn {context, ...} => |
|
290 prove_eqvt_tac insts ind_thms const_names simps context) |
286 |> ProofContext.export ctxt'' ctxt |
291 |> ProofContext.export ctxt'' ctxt |
287 end |
292 end |
288 |
293 |
289 end (* structure *) |
294 end (* structure *) |
290 |
295 |