8 imports Parity Fact |
8 imports Parity Fact |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Transpositions *} |
11 subsection {* Transpositions *} |
12 |
12 |
|
13 lemma swap_id_refl: "Fun.swap a a id = id" |
|
14 by (fact swap_self) |
|
15 |
|
16 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" |
|
17 by (fact swap_commute) |
|
18 |
13 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" |
19 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" |
14 by (auto simp add: fun_eq_iff swap_def fun_upd_def) |
20 by (fact swap_commute) |
15 |
|
16 lemma swap_id_refl: "Fun.swap a a id = id" |
|
17 by simp |
|
18 |
|
19 lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" |
|
20 by (rule ext, simp add: swap_def) |
|
21 |
21 |
22 lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id" |
22 lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id" |
23 by (rule ext, auto simp add: swap_def) |
23 by (rule ext, auto simp add: Fun.swap_def) |
24 |
24 |
25 lemma inv_unique_comp: |
25 lemma inv_unique_comp: |
26 assumes fg: "f \<circ> g = id" |
26 assumes fg: "f \<circ> g = id" |
27 and gf: "g \<circ> f = id" |
27 and gf: "g \<circ> f = id" |
28 shows "inv f = g" |
28 shows "inv f = g" |
30 |
30 |
31 lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" |
31 lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" |
32 by (rule inv_unique_comp) simp_all |
32 by (rule inv_unique_comp) simp_all |
33 |
33 |
34 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" |
34 lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" |
35 by (simp add: swap_def) |
35 by (simp add: Fun.swap_def) |
36 |
36 |
37 |
37 |
38 subsection {* Basic consequences of the definition *} |
38 subsection {* Basic consequences of the definition *} |
39 |
39 |
40 definition permutes (infixr "permutes" 41) |
40 definition permutes (infixr "permutes" 41) |
129 apply (rule permutes_superset[where S = "insert a S"]) |
129 apply (rule permutes_superset[where S = "insert a S"]) |
130 apply (rule permutes_compose[OF pS]) |
130 apply (rule permutes_compose[OF pS]) |
131 apply (rule permutes_swap_id, simp) |
131 apply (rule permutes_swap_id, simp) |
132 using permutes_in_image[OF pS, of a] |
132 using permutes_in_image[OF pS, of a] |
133 apply simp |
133 apply simp |
134 apply (auto simp add: Ball_def swap_def) |
134 apply (auto simp add: Ball_def Fun.swap_def) |
135 done |
135 done |
136 |
136 |
137 lemma permutes_insert: "{p. p permutes (insert a S)} = |
137 lemma permutes_insert: "{p. p permutes (insert a S)} = |
138 (\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" |
138 (\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" |
139 proof - |
139 proof - |
213 from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" |
213 from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" |
214 "p permutes F" "q permutes F" |
214 "p permutes F" "q permutes F" |
215 by auto |
215 by auto |
216 from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" |
216 from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" |
217 unfolding permutes_def |
217 unfolding permutes_def |
218 by (auto simp add: swap_def fun_upd_def fun_eq_iff) |
218 by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff) |
219 also have "\<dots> = ?g (c,q) x" |
219 also have "\<dots> = ?g (c,q) x" |
220 using ths(5) `x \<notin> F` eq |
220 using ths(5) `x \<notin> F` eq |
221 by (auto simp add: swap_def fun_upd_def fun_eq_iff) |
221 by (auto simp add: swap_def fun_upd_def fun_eq_iff) |
222 also have "\<dots> = c" |
222 also have "\<dots> = c" |
223 using ths(5) `x \<notin> F` |
223 using ths(5) `x \<notin> F` |
224 unfolding permutes_def |
224 unfolding permutes_def |
225 by (auto simp add: swap_def fun_upd_def fun_eq_iff) |
225 by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff) |
226 finally have bc: "b = c" . |
226 finally have bc: "b = c" . |
227 then have "Fun.swap x b id = Fun.swap x c id" |
227 then have "Fun.swap x b id = Fun.swap x c id" |
228 by simp |
228 by simp |
229 with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q" |
229 with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q" |
230 by simp |
230 by simp |
308 |
308 |
309 subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *} |
309 subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *} |
310 |
310 |
311 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> |
311 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> |
312 Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id" |
312 Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id" |
313 by (simp add: fun_eq_iff swap_def) |
313 by (simp add: fun_eq_iff Fun.swap_def) |
314 |
314 |
315 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> |
315 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> |
316 Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id" |
316 Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id" |
317 by (simp add: fun_eq_iff swap_def) |
317 by (simp add: fun_eq_iff Fun.swap_def) |
318 |
318 |
319 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> |
319 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> |
320 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id" |
320 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id" |
321 by (simp add: swap_def fun_eq_iff) |
321 by (simp add: fun_eq_iff Fun.swap_def) |
322 |
322 |
323 |
323 |
324 subsection {* Permutations as transposition sequences *} |
324 subsection {* Permutations as transposition sequences *} |
325 |
325 |
326 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
326 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
435 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> |
435 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> |
436 (Fun.swap a b id \<circ> Fun.swap c d id = id \<or> |
436 (Fun.swap a b id \<circ> Fun.swap c d id = id \<or> |
437 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
437 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
438 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))" |
438 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))" |
439 apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) |
439 apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) |
440 apply (simp_all only: swapid_sym) |
440 apply (simp_all only: swap_commute) |
441 apply (case_tac "a = c \<and> b = d") |
441 apply (case_tac "a = c \<and> b = d") |
442 apply (clarsimp simp only: swapid_sym swap_id_idempotent) |
442 apply (clarsimp simp only: swapid_sym swap_id_idempotent) |
443 apply (case_tac "a = c \<and> b \<noteq> d") |
443 apply (case_tac "a = c \<and> b \<noteq> d") |
444 apply (rule disjI2) |
444 apply (rule disjI2) |
445 apply (rule_tac x="b" in exI) |
445 apply (rule_tac x="b" in exI) |
446 apply (rule_tac x="d" in exI) |
446 apply (rule_tac x="d" in exI) |
447 apply (rule_tac x="b" in exI) |
447 apply (rule_tac x="b" in exI) |
448 apply (clarsimp simp add: fun_eq_iff swap_def) |
448 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
449 apply (case_tac "a \<noteq> c \<and> b = d") |
449 apply (case_tac "a \<noteq> c \<and> b = d") |
450 apply (rule disjI2) |
450 apply (rule disjI2) |
451 apply (rule_tac x="c" in exI) |
451 apply (rule_tac x="c" in exI) |
452 apply (rule_tac x="d" in exI) |
452 apply (rule_tac x="d" in exI) |
453 apply (rule_tac x="c" in exI) |
453 apply (rule_tac x="c" in exI) |
454 apply (clarsimp simp add: fun_eq_iff swap_def) |
454 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
455 apply (rule disjI2) |
455 apply (rule disjI2) |
456 apply (rule_tac x="c" in exI) |
456 apply (rule_tac x="c" in exI) |
457 apply (rule_tac x="d" in exI) |
457 apply (rule_tac x="d" in exI) |
458 apply (rule_tac x="b" in exI) |
458 apply (rule_tac x="b" in exI) |
459 apply (clarsimp simp add: fun_eq_iff swap_def) |
459 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
460 done |
460 done |
461 with H show ?thesis by metis |
461 with H show ?thesis by metis |
462 qed |
462 qed |
463 |
463 |
464 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id" |
464 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id" |
487 shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)" |
487 shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)" |
488 using spn ab pa |
488 using spn ab pa |
489 proof (induct n arbitrary: p a b) |
489 proof (induct n arbitrary: p a b) |
490 case 0 |
490 case 0 |
491 then show ?case |
491 then show ?case |
492 by (auto simp add: swap_def fun_upd_def) |
492 by (auto simp add: Fun.swap_def fun_upd_def) |
493 next |
493 next |
494 case (Suc n p a b) |
494 case (Suc n p a b) |
495 from Suc.prems(1) swapidseq_cases[of "Suc n" p] |
495 from Suc.prems(1) swapidseq_cases[of "Suc n" p] |
496 obtain c d q m where |
496 obtain c d q m where |
497 cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m" |
497 cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m" |
671 case (comp_Suc n p a b) |
671 case (comp_Suc n p a b) |
672 let ?S = "insert a (insert b {x. p x \<noteq> x})" |
672 let ?S = "insert a (insert b {x. p x \<noteq> x})" |
673 from comp_Suc.hyps(2) have fS: "finite ?S" |
673 from comp_Suc.hyps(2) have fS: "finite ?S" |
674 by simp |
674 by simp |
675 from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S" |
675 from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S" |
676 by (auto simp add: swap_def) |
676 by (auto simp add: Fun.swap_def) |
677 from finite_subset[OF th fS] show ?case . |
677 from finite_subset[OF th fS] show ?case . |
678 qed |
678 qed |
679 qed |
679 qed |
680 |
680 |
681 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" |
681 lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" |
707 next |
707 next |
708 case (insert a F p) |
708 case (insert a F p) |
709 let ?r = "Fun.swap a (p a) id \<circ> p" |
709 let ?r = "Fun.swap a (p a) id \<circ> p" |
710 let ?q = "Fun.swap a (p a) id \<circ> ?r" |
710 let ?q = "Fun.swap a (p a) id \<circ> ?r" |
711 have raa: "?r a = a" |
711 have raa: "?r a = a" |
712 by (simp add: swap_def) |
712 by (simp add: Fun.swap_def) |
713 from bij_swap_ompose_bij[OF insert(4)] |
713 from bij_swap_ompose_bij[OF insert(4)] |
714 have br: "bij ?r" . |
714 have br: "bij ?r" . |
715 |
715 |
716 from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" |
716 from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" |
717 apply (clarsimp simp add: swap_def) |
717 apply (clarsimp simp add: Fun.swap_def) |
718 apply (erule_tac x="x" in allE) |
718 apply (erule_tac x="x" in allE) |
719 apply auto |
719 apply auto |
720 unfolding bij_iff |
720 unfolding bij_iff |
721 apply metis |
721 apply metis |
722 done |
722 done |
1052 from p q aS have pa: "p a = a" and qa: "q a = a" |
1052 from p q aS have pa: "p a = a" and qa: "q a = a" |
1053 unfolding permutes_def by metis+ |
1053 unfolding permutes_def by metis+ |
1054 from eq have "(Fun.swap a b id \<circ> p) a = (Fun.swap a c id \<circ> q) a" |
1054 from eq have "(Fun.swap a b id \<circ> p) a = (Fun.swap a c id \<circ> q) a" |
1055 by simp |
1055 by simp |
1056 then have bc: "b = c" |
1056 then have bc: "b = c" |
1057 by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def |
1057 by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def |
1058 cong del: if_weak_cong split: split_if_asm) |
1058 cong del: if_weak_cong split: split_if_asm) |
1059 from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) = |
1059 from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) = |
1060 (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp |
1060 (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp |
1061 then have "p = q" |
1061 then have "p = q" |
1062 unfolding o_assoc swap_id_idempotent |
1062 unfolding o_assoc swap_id_idempotent |