equal
deleted
inserted
replaced
767 ML_file "nominal_basics.ML" |
767 ML_file "nominal_basics.ML" |
768 |
768 |
769 |
769 |
770 subsection {* Eqvt infrastructure *} |
770 subsection {* Eqvt infrastructure *} |
771 |
771 |
772 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
772 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw}. *} |
773 |
773 |
774 ML_file "nominal_thmdecls.ML" |
774 ML_file "nominal_thmdecls.ML" |
775 setup "Nominal_ThmDecls.setup" |
775 setup "Nominal_ThmDecls.setup" |
776 |
776 |
777 |
777 |
1054 auxiliary classes which specify that (op <=) and |
1054 auxiliary classes which specify that (op <=) and |
1055 Inf are equivariant. Instances for bool and fun are |
1055 Inf are equivariant. Instances for bool and fun are |
1056 given. |
1056 given. |
1057 *} |
1057 *} |
1058 |
1058 |
1059 class le_eqvt = ord + |
1059 class le_eqvt = order + |
1060 assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{order, pt}))))" |
1060 assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))" |
1061 |
1061 |
1062 class inf_eqvt = Inf + |
1062 class inf_eqvt = Inf + |
1063 assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::'a::{complete_lattice, pt} set))" |
1063 assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, complete_lattice}) set))" |
1064 |
1064 |
1065 instantiation bool :: le_eqvt |
1065 instantiation bool :: le_eqvt |
1066 begin |
1066 begin |
1067 |
1067 |
1068 instance |
1068 instance |
3226 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
3226 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
3227 setup {* Sign.add_const_constraint |
3227 setup {* Sign.add_const_constraint |
3228 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
3228 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
3229 |
3229 |
3230 |
3230 |
3231 |
|
3232 section {* Library functions for the nominal infrastructure *} |
3231 section {* Library functions for the nominal infrastructure *} |
3233 |
3232 |
3234 ML_file "nominal_library.ML" |
3233 ML_file "nominal_library.ML" |
3235 |
|
3236 |
3234 |
3237 |
3235 |
3238 section {* The freshness lemma according to Andy Pitts *} |
3236 section {* The freshness lemma according to Andy Pitts *} |
3239 |
3237 |
3240 lemma freshness_lemma: |
3238 lemma freshness_lemma: |
3415 fixes P Q :: "'a::at \<Rightarrow> bool" |
3413 fixes P Q :: "'a::at \<Rightarrow> bool" |
3416 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3414 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3417 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
3415 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
3418 using P Q by (rule FRESH_binop_iff) |
3416 using P Q by (rule FRESH_binop_iff) |
3419 |
3417 |
|
3418 |
3420 section {* Automation for creating concrete atom types *} |
3419 section {* Automation for creating concrete atom types *} |
3421 |
3420 |
3422 text {* at the moment only single-sort concrete atoms are supported *} |
3421 text {* At the moment only single-sort concrete atoms are supported. *} |
3423 |
3422 |
3424 ML_file "nominal_atoms.ML" |
3423 ML_file "nominal_atoms.ML" |
3425 |
3424 |
3426 |
3425 |
3427 section {* automatic equivariance procedure for inductive definitions *} |
3426 section {* Automatic equivariance procedure for inductive definitions *} |
3428 |
3427 |
3429 ML_file "nominal_eqvt.ML" |
3428 ML_file "nominal_eqvt.ML" |
3430 |
3429 |
3431 |
|
3432 |
|
3433 |
|
3434 end |
3430 end |