equal
deleted
inserted
replaced
675 val fresh_left = thm "Nominal.pt_fresh_left"; |
675 val fresh_left = thm "Nominal.pt_fresh_left"; |
676 val fresh_right_ineq = thm "Nominal.pt_fresh_right_ineq"; |
676 val fresh_right_ineq = thm "Nominal.pt_fresh_right_ineq"; |
677 val fresh_right = thm "Nominal.pt_fresh_right"; |
677 val fresh_right = thm "Nominal.pt_fresh_right"; |
678 val fresh_bij_ineq = thm "Nominal.pt_fresh_bij_ineq"; |
678 val fresh_bij_ineq = thm "Nominal.pt_fresh_bij_ineq"; |
679 val fresh_bij = thm "Nominal.pt_fresh_bij"; |
679 val fresh_bij = thm "Nominal.pt_fresh_bij"; |
|
680 val fresh_aux_ineq = thm "Nominal.pt_fresh_aux_ineq"; |
|
681 val fresh_aux = thm "Nominal.pt_fresh_aux"; |
680 val pt_pi_rev = thm "Nominal.pt_pi_rev"; |
682 val pt_pi_rev = thm "Nominal.pt_pi_rev"; |
681 val pt_rev_pi = thm "Nominal.pt_rev_pi"; |
683 val pt_rev_pi = thm "Nominal.pt_rev_pi"; |
682 val fresh_fun_eqvt = thm "Nominal.fresh_fun_equiv"; |
684 |
683 |
685 |
684 (* Now we collect and instantiate some lemmas w.r.t. all atom *) |
686 (* Now we collect and instantiate some lemmas w.r.t. all atom *) |
685 (* types; this allows for example to use abs_perm (which is a *) |
687 (* types; this allows for example to use abs_perm (which is a *) |
686 (* collection of theorems) instead of thm abs_fun_pi with explicit *) |
688 (* collection of theorems) instead of thm abs_fun_pi with explicit *) |
687 (* instantiations. *) |
689 (* instantiations. *) |
789 in [(("fresh_right", thms1 @ thms2),[])] end |
791 in [(("fresh_right", thms1 @ thms2),[])] end |
790 ||>> PureThy.add_thmss |
792 ||>> PureThy.add_thmss |
791 let val thms1 = inst_pt_at [fresh_bij] |
793 let val thms1 = inst_pt_at [fresh_bij] |
792 and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] |
794 and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq] |
793 in [(("fresh_eqvt", thms1 @ thms2),[])] end |
795 in [(("fresh_eqvt", thms1 @ thms2),[])] end |
794 ||>> PureThy.add_thmss [(("fresh_fun_eqvt",inst_pt_at [fresh_fun_eqvt]),[])] |
796 ||>> PureThy.add_thmss |
|
797 let val thms1 = inst_pt_at [fresh_aux] |
|
798 and thms2 = inst_pt_pt_at_cp_dj [fresh_aux_ineq] |
|
799 in [(("fresh_aux", thms1 @ thms2),[])] end |
795 end; |
800 end; |
796 |
801 |
797 in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names) |
802 in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names) |
798 (NominalData.get thy11)) thy33 |
803 (NominalData.get thy11)) thy33 |
799 end; |
804 end; |