equal
deleted
inserted
replaced
9 "~~/src/HOL/Library/Infinite_Set" |
9 "~~/src/HOL/Library/Infinite_Set" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
11 "~~/src/HOL/Library/FinFun" |
11 "~~/src/HOL/Library/FinFun" |
12 keywords |
12 keywords |
13 "atom_decl" "equivariance" :: thy_decl |
13 "atom_decl" "equivariance" :: thy_decl |
14 uses ("nominal_basics.ML") |
|
15 ("nominal_thmdecls.ML") |
|
16 ("nominal_permeq.ML") |
|
17 ("nominal_library.ML") |
|
18 ("nominal_atoms.ML") |
|
19 ("nominal_eqvt.ML") |
|
20 begin |
14 begin |
21 |
15 |
22 section {* Atoms and Sorts *} |
16 section {* Atoms and Sorts *} |
23 |
17 |
24 text {* A simple implementation for atom_sorts is strings. *} |
18 text {* A simple implementation for atom_sorts is strings. *} |
766 |
760 |
767 section {* Infrastructure for Equivariance and Perm_simp *} |
761 section {* Infrastructure for Equivariance and Perm_simp *} |
768 |
762 |
769 subsection {* Basic functions about permutations *} |
763 subsection {* Basic functions about permutations *} |
770 |
764 |
771 use "nominal_basics.ML" |
765 ML_file "nominal_basics.ML" |
772 |
766 |
773 |
767 |
774 subsection {* Eqvt infrastructure *} |
768 subsection {* Eqvt infrastructure *} |
775 |
769 |
776 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
770 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
777 |
771 |
778 use "nominal_thmdecls.ML" |
772 ML_file "nominal_thmdecls.ML" |
779 setup "Nominal_ThmDecls.setup" |
773 setup "Nominal_ThmDecls.setup" |
780 |
774 |
781 |
775 |
782 lemmas [eqvt] = |
776 lemmas [eqvt] = |
783 (* pt types *) |
777 (* pt types *) |
815 shows "p \<bullet> unpermute p x \<equiv> x" |
809 shows "p \<bullet> unpermute p x \<equiv> x" |
816 unfolding unpermute_def by simp |
810 unfolding unpermute_def by simp |
817 |
811 |
818 text {* provides perm_simp methods *} |
812 text {* provides perm_simp methods *} |
819 |
813 |
820 use "nominal_permeq.ML" |
814 ML_file "nominal_permeq.ML" |
821 |
815 |
822 method_setup perm_simp = |
816 method_setup perm_simp = |
823 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
817 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
824 {* pushes permutations inside. *} |
818 {* pushes permutations inside. *} |
825 |
819 |
3233 |
3227 |
3234 |
3228 |
3235 |
3229 |
3236 section {* Library functions for the nominal infrastructure *} |
3230 section {* Library functions for the nominal infrastructure *} |
3237 |
3231 |
3238 use "nominal_library.ML" |
3232 ML_file "nominal_library.ML" |
3239 |
3233 |
3240 |
3234 |
3241 |
3235 |
3242 section {* The freshness lemma according to Andy Pitts *} |
3236 section {* The freshness lemma according to Andy Pitts *} |
3243 |
3237 |
3423 |
3417 |
3424 section {* Automation for creating concrete atom types *} |
3418 section {* Automation for creating concrete atom types *} |
3425 |
3419 |
3426 text {* at the moment only single-sort concrete atoms are supported *} |
3420 text {* at the moment only single-sort concrete atoms are supported *} |
3427 |
3421 |
3428 use "nominal_atoms.ML" |
3422 ML_file "nominal_atoms.ML" |
3429 |
3423 |
3430 |
3424 |
3431 section {* automatic equivariance procedure for inductive definitions *} |
3425 section {* automatic equivariance procedure for inductive definitions *} |
3432 |
3426 |
3433 use "nominal_eqvt.ML" |
3427 ML_file "nominal_eqvt.ML" |
3434 |
3428 |
3435 |
3429 |
3436 |
3430 |
3437 |
3431 |
3438 end |
3432 end |