26 |
26 |
27 primrec |
27 primrec |
28 sort_of :: "atom \<Rightarrow> atom_sort" |
28 sort_of :: "atom \<Rightarrow> atom_sort" |
29 where |
29 where |
30 "sort_of (Atom s i) = s" |
30 "sort_of (Atom s i) = s" |
|
31 |
|
32 primrec |
|
33 nat_of :: "atom \<Rightarrow> nat" |
|
34 where |
|
35 "nat_of (Atom s n) = n" |
31 |
36 |
32 |
37 |
33 text {* There are infinitely many atoms of each sort. *} |
38 text {* There are infinitely many atoms of each sort. *} |
34 lemma INFM_sort_of_eq: |
39 lemma INFM_sort_of_eq: |
35 shows "INFM a. sort_of a = s" |
40 shows "INFM a. sort_of a = s" |
61 then obtain a where "a \<notin> X" "sort_of a = s" |
66 then obtain a where "a \<notin> X" "sort_of a = s" |
62 by (auto elim: INFM_E) |
67 by (auto elim: INFM_E) |
63 then show ?thesis .. |
68 then show ?thesis .. |
64 qed |
69 qed |
65 |
70 |
|
71 lemma atom_components_eq_iff: |
|
72 fixes a b :: atom |
|
73 shows "a = b \<longleftrightarrow> sort_of a = sort_of b \<and> nat_of a = nat_of b" |
|
74 by (induct a, induct b, simp) |
|
75 |
66 section {* Sort-Respecting Permutations *} |
76 section {* Sort-Respecting Permutations *} |
67 |
77 |
68 typedef perm = |
78 typedef perm = |
69 "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}" |
79 "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}" |
70 proof |
80 proof |
456 lemma swap_set_in: |
466 lemma swap_set_in: |
457 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
467 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
458 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
468 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
459 unfolding permute_set_eq |
469 unfolding permute_set_eq |
460 using a by (auto simp add: swap_atom) |
470 using a by (auto simp add: swap_atom) |
461 |
|
462 |
471 |
463 subsection {* Permutations for units *} |
472 subsection {* Permutations for units *} |
464 |
473 |
465 instantiation unit :: pt |
474 instantiation unit :: pt |
466 begin |
475 begin |
833 unfolding fresh_def supp_atom by simp |
842 unfolding fresh_def supp_atom by simp |
834 |
843 |
835 instance atom :: fs |
844 instance atom :: fs |
836 by default (simp add: supp_atom) |
845 by default (simp add: supp_atom) |
837 |
846 |
|
847 section {* Support for finite sets of atoms *} |
|
848 |
|
849 lemma supp_finite_atom_set: |
|
850 fixes S::"atom set" |
|
851 assumes "finite S" |
|
852 shows "supp S = S" |
|
853 apply(rule finite_supp_unique) |
|
854 apply(simp add: supports_def) |
|
855 apply(simp add: swap_set_not_in) |
|
856 apply(rule assms) |
|
857 apply(simp add: swap_set_in) |
|
858 done |
|
859 |
|
860 lemma supp_atom_insert: |
|
861 fixes S::"atom set" |
|
862 assumes a: "finite S" |
|
863 shows "supp (insert a S) = supp a \<union> supp S" |
|
864 using a by (simp add: supp_finite_atom_set supp_atom) |
838 |
865 |
839 section {* Type @{typ perm} is finitely-supported. *} |
866 section {* Type @{typ perm} is finitely-supported. *} |
840 |
867 |
841 lemma perm_swap_eq: |
868 lemma perm_swap_eq: |
842 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
869 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
1052 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1079 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1053 using fresh_fun_app |
1080 using fresh_fun_app |
1054 unfolding fresh_def |
1081 unfolding fresh_def |
1055 by auto |
1082 by auto |
1056 |
1083 |
1057 (* alternative proof *) |
1084 lemma supp_fun_eqvt: |
1058 lemma |
1085 assumes a: "\<forall>p. p \<bullet> f = f" |
1059 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1086 shows "supp f = {}" |
1060 proof (rule subsetCI) |
1087 unfolding supp_def |
1061 fix a::"atom" |
1088 using a by simp |
1062 assume a: "a \<in> supp (f x)" |
1089 |
1063 assume b: "a \<notin> supp f \<union> supp x" |
1090 |
1064 then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" |
|
1065 unfolding supp_def by auto |
|
1066 then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp |
|
1067 moreover |
|
1068 have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" |
|
1069 by auto |
|
1070 ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}" |
|
1071 using finite_subset by auto |
|
1072 then have "a \<notin> supp (f x)" unfolding supp_def |
|
1073 by (simp add: permute_fun_app_eq) |
|
1074 with a show "False" by simp |
|
1075 qed |
|
1076 |
|
1077 lemma fresh_fun_eqvt_app: |
1091 lemma fresh_fun_eqvt_app: |
1078 assumes a: "\<forall>p. p \<bullet> f = f" |
1092 assumes a: "\<forall>p. p \<bullet> f = f" |
1079 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1093 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1080 proof - |
1094 proof - |
1081 from a have "supp f = {}" |
1095 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1082 unfolding supp_def by simp |
|
1083 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1096 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1084 unfolding fresh_def |
1097 unfolding fresh_def |
1085 using supp_fun_app |
1098 using supp_fun_app |
1086 by auto |
1099 by auto |
1087 qed |
1100 qed |