equal
deleted
inserted
replaced
78 by (induct a, induct b, simp) |
78 by (induct a, induct b, simp) |
79 |
79 |
80 |
80 |
81 section {* Sort-Respecting Permutations *} |
81 section {* Sort-Respecting Permutations *} |
82 |
82 |
83 typedef perm = |
83 definition |
84 "{f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}" |
84 "perm \<equiv> {f. bij f \<and> finite {a. f a \<noteq> a} \<and> (\<forall>a. sort_of (f a) = sort_of a)}" |
|
85 |
|
86 typedef perm = "perm" |
85 proof |
87 proof |
86 show "id \<in> ?perm" by simp |
88 show "id \<in> perm" unfolding perm_def by simp |
87 qed |
89 qed |
88 |
90 |
89 lemma permI: |
91 lemma permI: |
90 assumes "bij f" and "MOST x. f x = x" and "\<And>a. sort_of (f a) = sort_of a" |
92 assumes "bij f" and "MOST x. f x = x" and "\<And>a. sort_of (f a) = sort_of a" |
91 shows "f \<in> perm" |
93 shows "f \<in> perm" |