3 *) |
3 *) |
4 |
4 |
5 header {* Permutations, both general and specifically on finite sets.*} |
5 header {* Permutations, both general and specifically on finite sets.*} |
6 |
6 |
7 theory Permutations |
7 theory Permutations |
8 imports Finite_Cartesian_Product Parity Fact Main |
8 imports Finite_Cartesian_Product Parity Fact |
9 begin |
9 begin |
10 |
|
11 (* Why should I import Main just to solve the Typerep problem! *) |
|
12 |
10 |
13 definition permutes (infixr "permutes" 41) where |
11 definition permutes (infixr "permutes" 41) where |
14 "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" |
12 "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" |
15 |
13 |
16 (* ------------------------------------------------------------------------- *) |
14 (* ------------------------------------------------------------------------- *) |
83 |
81 |
84 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
82 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
85 unfolding permutes_def by simp |
83 unfolding permutes_def by simp |
86 |
84 |
87 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" |
85 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" |
88 unfolding permutes_def inv_def apply auto |
86 unfolding permutes_def inv_onto_def apply auto |
89 apply (erule allE[where x=y]) |
87 apply (erule allE[where x=y]) |
90 apply (erule allE[where x=y]) |
88 apply (erule allE[where x=y]) |
91 apply (rule someI_ex) apply blast |
89 apply (rule someI_ex) apply blast |
92 apply (rule some1_equality) |
90 apply (rule some1_equality) |
93 apply blast |
91 apply blast |
94 apply blast |
92 apply blast |
95 done |
93 done |
96 |
94 |
97 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S" |
95 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S" |
98 unfolding permutes_def swap_def fun_upd_def apply auto apply metis done |
96 unfolding permutes_def swap_def fun_upd_def by auto metis |
99 |
97 |
100 lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T" |
98 lemma permutes_superset: |
101 apply (simp add: Ball_def permutes_def Diff_iff) by metis |
99 "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T" |
|
100 by (simp add: Ball_def permutes_def Diff_iff) metis |
102 |
101 |
103 (* ------------------------------------------------------------------------- *) |
102 (* ------------------------------------------------------------------------- *) |
104 (* Group properties. *) |
103 (* Group properties. *) |
105 (* ------------------------------------------------------------------------- *) |
104 (* ------------------------------------------------------------------------- *) |
106 |
105 |