787 fixes p q::"perm" |
787 fixes p q::"perm" |
788 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
788 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
789 unfolding permute_perm_def |
789 unfolding permute_perm_def |
790 by (simp add: diff_minus minus_add add_assoc) |
790 by (simp add: diff_minus minus_add add_assoc) |
791 |
791 |
792 |
|
793 subsubsection {* Equivariance of Logical Operators *} |
792 subsubsection {* Equivariance of Logical Operators *} |
794 |
793 |
795 lemma eq_eqvt [eqvt]: |
794 lemma eq_eqvt [eqvt]: |
796 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
795 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
797 unfolding permute_eq_iff permute_bool_def .. |
796 unfolding permute_eq_iff permute_bool_def .. |
949 lemma Union_eqvt [eqvt]: |
948 lemma Union_eqvt [eqvt]: |
950 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
949 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
951 unfolding Union_eq |
950 unfolding Union_eq |
952 by (perm_simp) (rule refl) |
951 by (perm_simp) (rule refl) |
953 |
952 |
|
953 lemma Inter_eqvt [eqvt]: |
|
954 shows "p \<bullet> (\<Inter> S) = \<Inter> (p \<bullet> S)" |
|
955 unfolding Inter_eq |
|
956 by (perm_simp) (rule refl) |
|
957 |
|
958 |
954 (* FIXME: eqvt attribute *) |
959 (* FIXME: eqvt attribute *) |
955 lemma Sigma_eqvt: |
960 lemma Sigma_eqvt: |
956 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
961 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
957 unfolding Sigma_def |
962 unfolding Sigma_def |
958 unfolding UNION_eq_Union_image |
963 unfolding UNION_eq_Union_image |
959 by (perm_simp) (rule refl) |
964 by (perm_simp) (rule refl) |
960 |
965 |
|
966 text {* |
|
967 In order to prove that lfp is equivariant we need two |
|
968 auxiliary classes which specify that (op <=) and |
|
969 Inf are equivariant. Instances for bool and fun are |
|
970 given. |
|
971 *} |
|
972 |
|
973 class le_eqvt = order + |
|
974 assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))" |
|
975 |
|
976 class inf_eqvt = complete_lattice + |
|
977 assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))" |
|
978 |
|
979 instantiation bool :: le_eqvt |
|
980 begin |
|
981 |
|
982 instance |
|
983 apply(default) |
|
984 unfolding le_bool_def |
|
985 apply(perm_simp) |
|
986 apply(rule refl) |
|
987 done |
|
988 |
|
989 end |
|
990 |
|
991 instantiation "fun" :: (pt, le_eqvt) le_eqvt |
|
992 begin |
|
993 |
|
994 instance |
|
995 apply(default) |
|
996 unfolding le_fun_def |
|
997 apply(perm_simp) |
|
998 apply(rule refl) |
|
999 done |
|
1000 |
|
1001 end |
|
1002 |
|
1003 instantiation bool :: inf_eqvt |
|
1004 begin |
|
1005 |
|
1006 instance |
|
1007 apply(default) |
|
1008 unfolding Inf_bool_def |
|
1009 apply(perm_simp) |
|
1010 apply(rule refl) |
|
1011 done |
|
1012 |
|
1013 end |
|
1014 |
|
1015 instantiation "fun" :: (pt, inf_eqvt) inf_eqvt |
|
1016 begin |
|
1017 |
|
1018 instance |
|
1019 apply(default) |
|
1020 unfolding Inf_fun_def |
|
1021 apply(perm_simp) |
|
1022 apply(rule refl) |
|
1023 done |
|
1024 |
|
1025 end |
|
1026 |
|
1027 lemma lfp_eqvt [eqvt]: |
|
1028 fixes F::"('a \<Rightarrow> 'b) \<Rightarrow> ('a::pt \<Rightarrow> 'b::{inf_eqvt, le_eqvt})" |
|
1029 shows "p \<bullet> (lfp F) = lfp (p \<bullet> F)" |
|
1030 unfolding lfp_def |
|
1031 by (perm_simp) (rule refl) |
|
1032 |
961 lemma finite_eqvt [eqvt]: |
1033 lemma finite_eqvt [eqvt]: |
962 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
1034 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
963 unfolding permute_finite permute_bool_def .. |
1035 unfolding finite_def |
|
1036 by (perm_simp) (rule refl) |
|
1037 |
964 |
1038 |
965 subsubsection {* Equivariance for product operations *} |
1039 subsubsection {* Equivariance for product operations *} |
966 |
1040 |
967 lemma fst_eqvt [eqvt]: |
1041 lemma fst_eqvt [eqvt]: |
968 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
1042 "p \<bullet> (fst x) = fst (p \<bullet> x)" |