942 fun build_eqvt_gl pi frees fnctn ctxt = |
942 fun build_eqvt_gl pi frees fnctn ctxt = |
943 let |
943 let |
944 val typ = domain_type (fastype_of fnctn); |
944 val typ = domain_type (fastype_of fnctn); |
945 val arg = the (AList.lookup (op=) frees typ); |
945 val arg = the (AList.lookup (op=) frees typ); |
946 in |
946 in |
947 ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
947 ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
948 end |
948 end |
949 *} |
949 *} |
950 |
950 |
951 ML {* |
951 ML {* |
952 fun prove_eqvt tys ind simps funs ctxt = |
952 fun prove_eqvt tys ind simps funs ctxt = |
953 let |
953 let |
954 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
954 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
955 val pi = Free (pi, @{typ perm}); |
955 val pi = Free (pi, @{typ perm}); |
956 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt')) |
956 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thms atom_eqvt permute_list.simps} @ simps @ all_eqvts ctxt')) |
957 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
957 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
958 val ths = Variable.export ctxt' ctxt ths_loc |
958 val ths = Variable.export ctxt' ctxt ths_loc |
959 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
959 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
960 in |
960 in |
961 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
961 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |