683 val fresh_iff = thm "Nominal.fresh_abs_fun_iff"; |
683 val fresh_iff = thm "Nominal.fresh_abs_fun_iff"; |
684 val fresh_iff_ineq = thm "Nominal.fresh_abs_fun_iff_ineq"; |
684 val fresh_iff_ineq = thm "Nominal.fresh_abs_fun_iff_ineq"; |
685 val abs_fun_supp = thm "Nominal.abs_fun_supp"; |
685 val abs_fun_supp = thm "Nominal.abs_fun_supp"; |
686 val abs_fun_supp_ineq = thm "Nominal.abs_fun_supp_ineq"; |
686 val abs_fun_supp_ineq = thm "Nominal.abs_fun_supp_ineq"; |
687 val pt_swap_bij = thm "Nominal.pt_swap_bij"; |
687 val pt_swap_bij = thm "Nominal.pt_swap_bij"; |
|
688 val pt_swap_bij' = thm "Nominal.pt_swap_bij'"; |
688 val pt_fresh_fresh = thm "Nominal.pt_fresh_fresh"; |
689 val pt_fresh_fresh = thm "Nominal.pt_fresh_fresh"; |
689 val pt_bij = thm "Nominal.pt_bij"; |
690 val pt_bij = thm "Nominal.pt_bij"; |
690 val pt_perm_compose = thm "Nominal.pt_perm_compose"; |
691 val pt_perm_compose = thm "Nominal.pt_perm_compose"; |
691 val pt_perm_compose' = thm "Nominal.pt_perm_compose'"; |
692 val pt_perm_compose' = thm "Nominal.pt_perm_compose'"; |
692 val perm_app = thm "Nominal.pt_fun_app_eq"; |
693 val perm_app = thm "Nominal.pt_fun_app_eq"; |
781 fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); |
782 fun inst_pt_pt_at_cp_dj thms = inst_zip djs (inst_pt_pt_at_cp thms); |
782 in |
783 in |
783 thy32 |
784 thy32 |
784 |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] |
785 |> PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])] |
785 ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] |
786 ||>> PureThy.add_thmss [(("alpha'", inst_pt_at [abs_fun_eq']),[])] |
786 ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])] |
787 ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij] @ inst_pt_at [pt_swap_bij']),[])] |
787 ||>> PureThy.add_thmss |
788 ||>> PureThy.add_thmss |
788 let val thms1 = inst_pt_at [pt_pi_rev]; |
789 let val thms1 = inst_pt_at [pt_pi_rev]; |
789 val thms2 = inst_pt_at [pt_rev_pi]; |
790 val thms2 = inst_pt_at [pt_rev_pi]; |
790 in [(("perm_pi_simp",thms1 @ thms2),[])] end |
791 in [(("perm_pi_simp",thms1 @ thms2),[])] end |
791 ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] |
792 ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])] |
811 (List.concat (List.concat perm_defs)) |
812 (List.concat (List.concat perm_defs)) |
812 in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end |
813 in [(("calc_atm", (inst_at at_calc) @ thms1),[])] end |
813 ||>> PureThy.add_thmss |
814 ||>> PureThy.add_thmss |
814 let val thms1 = inst_pt_at [abs_fun_pi] |
815 let val thms1 = inst_pt_at [abs_fun_pi] |
815 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
816 and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq] |
816 in [(("abs_perm", thms1 @ thms2),[])] end |
817 in [(("abs_perm", thms1 @ thms2),[NominalThmDecls.eqvt_add])] end |
817 ||>> PureThy.add_thmss |
818 ||>> PureThy.add_thmss |
818 let val thms1 = inst_dj [dj_perm_forget] |
819 let val thms1 = inst_dj [dj_perm_forget] |
819 and thms2 = inst_dj [dj_pp_forget] |
820 and thms2 = inst_dj [dj_pp_forget] |
820 in [(("perm_dj", thms1 @ thms2),[])] end |
821 in [(("perm_dj", thms1 @ thms2),[])] end |
821 ||>> PureThy.add_thmss |
822 ||>> PureThy.add_thmss |