equal
deleted
inserted
replaced
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 |
797 using `a \<in> S` `b \<notin> S` `sort_of a = sort_of b` |
806 using `a \<in> S` `b \<notin> S` `sort_of a = sort_of b` |
798 by (rule a3) |
807 by (rule a3) |
799 ultimately show "False" by simp |
808 ultimately show "False" by simp |
800 qed |
809 qed |
801 qed |
810 qed |
|
811 |
|
812 section {* Support for finite sets of atoms *} |
|
813 |
|
814 |
|
815 lemma supp_finite_atom_set: |
|
816 fixes S::"atom set" |
|
817 assumes "finite S" |
|
818 shows "supp S = S" |
|
819 apply(rule finite_supp_unique) |
|
820 apply(simp add: supports_def) |
|
821 apply(simp add: swap_set_not_in) |
|
822 apply(rule assms) |
|
823 apply(simp add: swap_set_in) |
|
824 done |
|
825 |
|
826 |
802 |
827 |
803 section {* Finitely-supported types *} |
828 section {* Finitely-supported types *} |
804 |
829 |
805 class fs = pt + |
830 class fs = pt + |
806 assumes finite_supp: "finite (supp x)" |
831 assumes finite_supp: "finite (supp x)" |