179 qed |
179 qed |
180 |
180 |
181 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
181 lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" |
182 by (simp add: permutes_def) |
182 by (simp add: permutes_def) |
183 |
183 |
184 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S" |
184 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> transpose a b permutes S" |
185 by (rule bij_imp_permutes) (auto simp add: swap_id_eq) |
185 by (rule bij_imp_permutes) (auto intro: transpose_apply_other) |
186 |
186 |
187 lemma permutes_superset: |
187 lemma permutes_superset: |
188 \<open>p permutes T\<close> if \<open>p permutes S\<close> \<open>\<And>x. x \<in> S - T \<Longrightarrow> p x = x\<close> |
188 \<open>p permutes T\<close> if \<open>p permutes S\<close> \<open>\<And>x. x \<in> S - T \<Longrightarrow> p x = x\<close> |
189 proof - |
189 proof - |
190 define R U where \<open>R = T \<inter> S\<close> and \<open>U = S - T\<close> |
190 define R U where \<open>R = T \<inter> S\<close> and \<open>U = S - T\<close> |
374 |
374 |
375 subsection \<open>The number of permutations on a finite set\<close> |
375 subsection \<open>The number of permutations on a finite set\<close> |
376 |
376 |
377 lemma permutes_insert_lemma: |
377 lemma permutes_insert_lemma: |
378 assumes "p permutes (insert a S)" |
378 assumes "p permutes (insert a S)" |
379 shows "Fun.swap a (p a) id \<circ> p permutes S" |
379 shows "transpose a (p a) \<circ> p permutes S" |
380 apply (rule permutes_superset[where S = "insert a S"]) |
380 apply (rule permutes_superset[where S = "insert a S"]) |
381 apply (rule permutes_compose[OF assms]) |
381 apply (rule permutes_compose[OF assms]) |
382 apply (rule permutes_swap_id, simp) |
382 apply (rule permutes_swap_id, simp) |
383 using permutes_in_image[OF assms, of a] |
383 using permutes_in_image[OF assms, of a] |
384 apply simp |
384 apply simp |
385 apply (auto simp add: Ball_def Fun.swap_def) |
385 apply (auto simp add: Ball_def Fun.swap_def) |
386 done |
386 done |
387 |
387 |
388 lemma permutes_insert: "{p. p permutes (insert a S)} = |
388 lemma permutes_insert: "{p. p permutes (insert a S)} = |
389 (\<lambda>(b, p). Fun.swap a b id \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" |
389 (\<lambda>(b, p). transpose a b \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" |
390 proof - |
390 proof - |
391 have "p permutes insert a S \<longleftrightarrow> |
391 have "p permutes insert a S \<longleftrightarrow> |
392 (\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)" for p |
392 (\<exists>b q. p = transpose a b \<circ> q \<and> b \<in> insert a S \<and> q permutes S)" for p |
393 proof - |
393 proof - |
394 have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S" |
394 have "\<exists>b q. p = transpose a b \<circ> q \<and> b \<in> insert a S \<and> q permutes S" |
395 if p: "p permutes insert a S" |
395 if p: "p permutes insert a S" |
396 proof - |
396 proof - |
397 let ?b = "p a" |
397 let ?b = "p a" |
398 let ?q = "Fun.swap a (p a) id \<circ> p" |
398 let ?q = "transpose a (p a) \<circ> p" |
399 have *: "p = Fun.swap a ?b id \<circ> ?q" |
399 have *: "p = transpose a ?b \<circ> ?q" |
400 by (simp add: fun_eq_iff o_assoc) |
400 by (simp add: fun_eq_iff o_assoc) |
401 have **: "?b \<in> insert a S" |
401 have **: "?b \<in> insert a S" |
402 unfolding permutes_in_image[OF p] by simp |
402 unfolding permutes_in_image[OF p] by simp |
403 from permutes_insert_lemma[OF p] * ** show ?thesis |
403 from permutes_insert_lemma[OF p] * ** show ?thesis |
404 by blast |
404 by blast |
405 qed |
405 qed |
406 moreover have "p permutes insert a S" |
406 moreover have "p permutes insert a S" |
407 if bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S" for b q |
407 if bq: "p = transpose a b \<circ> q" "b \<in> insert a S" "q permutes S" for b q |
408 proof - |
408 proof - |
409 from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S" |
409 from permutes_subset[OF bq(3), of "insert a S"] have q: "q permutes insert a S" |
410 by auto |
410 by auto |
411 have a: "a \<in> insert a S" |
411 have a: "a \<in> insert a S" |
412 by simp |
412 by simp |
432 fix n |
432 fix n |
433 assume card_insert: "card (insert x F) = n" |
433 assume card_insert: "card (insert x F) = n" |
434 let ?xF = "{p. p permutes insert x F}" |
434 let ?xF = "{p. p permutes insert x F}" |
435 let ?pF = "{p. p permutes F}" |
435 let ?pF = "{p. p permutes F}" |
436 let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}" |
436 let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}" |
437 let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)" |
437 let ?g = "(\<lambda>(b, p). transpose x b \<circ> p)" |
438 have xfgpF': "?xF = ?g ` ?pF'" |
438 have xfgpF': "?xF = ?g ` ?pF'" |
439 by (rule permutes_insert[of x F]) |
439 by (rule permutes_insert[of x F]) |
440 from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1" |
440 from \<open>x \<notin> F\<close> \<open>finite F\<close> card_insert have Fs: "card F = n - 1" |
441 by auto |
441 by auto |
442 from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" |
442 from \<open>finite F\<close> insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" |
506 subsection \<open>Hence a sort of induction principle composing by swaps\<close> |
506 subsection \<open>Hence a sort of induction principle composing by swaps\<close> |
507 |
507 |
508 lemma permutes_induct [consumes 2, case_names id swap]: |
508 lemma permutes_induct [consumes 2, case_names id swap]: |
509 \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close> |
509 \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close> |
510 and id: \<open>P id\<close> |
510 and id: \<open>P id\<close> |
511 and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b id \<circ> p)\<close> |
511 and swap: \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (transpose a b \<circ> p)\<close> |
512 using \<open>finite S\<close> \<open>p permutes S\<close> swap proof (induction S arbitrary: p) |
512 using \<open>finite S\<close> \<open>p permutes S\<close> swap proof (induction S arbitrary: p) |
513 case empty |
513 case empty |
514 with id show ?case |
514 with id show ?case |
515 by (simp only: permutes_empty) |
515 by (simp only: permutes_empty) |
516 next |
516 next |
517 case (insert x S p) |
517 case (insert x S p) |
518 define q where \<open>q = Fun.swap x (p x) id \<circ> p\<close> |
518 define q where \<open>q = transpose x (p x) \<circ> p\<close> |
519 then have swap_q: \<open>Fun.swap x (p x) id \<circ> q = p\<close> |
519 then have swap_q: \<open>transpose x (p x) \<circ> q = p\<close> |
520 by (simp add: o_assoc) |
520 by (simp add: o_assoc) |
521 from \<open>p permutes insert x S\<close> have \<open>q permutes S\<close> |
521 from \<open>p permutes insert x S\<close> have \<open>q permutes S\<close> |
522 by (simp add: q_def permutes_insert_lemma) |
522 by (simp add: q_def permutes_insert_lemma) |
523 then have \<open>q permutes insert x S\<close> |
523 then have \<open>q permutes insert x S\<close> |
524 by (simp add: permutes_imp_permutes_insert) |
524 by (simp add: permutes_imp_permutes_insert) |
526 by (auto intro: insert.IH insert.prems(2) permutes_imp_permutes_insert) |
526 by (auto intro: insert.IH insert.prems(2) permutes_imp_permutes_insert) |
527 have \<open>x \<in> insert x S\<close> |
527 have \<open>x \<in> insert x S\<close> |
528 by simp |
528 by simp |
529 moreover from \<open>p permutes insert x S\<close> have \<open>p x \<in> insert x S\<close> |
529 moreover from \<open>p permutes insert x S\<close> have \<open>p x \<in> insert x S\<close> |
530 using permutes_in_image [of p \<open>insert x S\<close> x] by simp |
530 using permutes_in_image [of p \<open>insert x S\<close> x] by simp |
531 ultimately have \<open>P (Fun.swap x (p x) id \<circ> q)\<close> |
531 ultimately have \<open>P (transpose x (p x) \<circ> q)\<close> |
532 using \<open>q permutes insert x S\<close> \<open>P q\<close> |
532 using \<open>q permutes insert x S\<close> \<open>P q\<close> |
533 by (rule insert.prems(2)) |
533 by (rule insert.prems(2)) |
534 then show ?case |
534 then show ?case |
535 by (simp add: swap_q) |
535 by (simp add: swap_q) |
536 qed |
536 qed |
537 |
537 |
538 lemma permutes_rev_induct [consumes 2, case_names id swap]: |
538 lemma permutes_rev_induct [consumes 2, case_names id swap]: |
539 \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close> |
539 \<open>P p\<close> if \<open>p permutes S\<close> \<open>finite S\<close> |
540 and id': \<open>P id\<close> |
540 and id': \<open>P id\<close> |
541 and swap': \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (Fun.swap a b p)\<close> |
541 and swap': \<open>\<And>a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> p permutes S \<Longrightarrow> P p \<Longrightarrow> P (p \<circ> transpose a b)\<close> |
542 using \<open>p permutes S\<close> \<open>finite S\<close> proof (induction rule: permutes_induct) |
542 using \<open>p permutes S\<close> \<open>finite S\<close> proof (induction rule: permutes_induct) |
543 case id |
543 case id |
544 from id' show ?case . |
544 from id' show ?case . |
545 next |
545 next |
546 case (swap a b p) |
546 case (swap a b p) |
|
547 then have \<open>bij p\<close> |
|
548 using permutes_bij by blast |
547 have \<open>P (Fun.swap (inv p a) (inv p b) p)\<close> |
549 have \<open>P (Fun.swap (inv p a) (inv p b) p)\<close> |
548 by (rule swap') (auto simp add: swap permutes_in_image permutes_inv) |
550 by (rule swap') (auto simp add: swap permutes_in_image permutes_inv) |
549 also have \<open>Fun.swap (inv p a) (inv p b) p = Fun.swap a b id \<circ> p\<close> |
551 also have \<open>Fun.swap (inv p a) (inv p b) p = transpose a b \<circ> p\<close> |
550 by (rule bij_swap_comp [symmetric]) (rule permutes_bij, rule swap) |
552 using \<open>bij p\<close> by (rule transpose_comp_eq [symmetric]) |
551 finally show ?case . |
553 finally show ?case . |
552 qed |
554 qed |
553 |
555 |
554 |
556 |
555 subsection \<open>Permutations of index set for iterated operations\<close> |
557 subsection \<open>Permutations of index set for iterated operations\<close> |
574 subsection \<open>Permutations as transposition sequences\<close> |
576 subsection \<open>Permutations as transposition sequences\<close> |
575 |
577 |
576 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
578 inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" |
577 where |
579 where |
578 id[simp]: "swapidseq 0 id" |
580 id[simp]: "swapidseq 0 id" |
579 | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)" |
581 | comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (transpose a b \<circ> p)" |
580 |
582 |
581 declare id[unfolded id_def, simp] |
583 declare id[unfolded id_def, simp] |
582 |
584 |
583 definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)" |
585 definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)" |
584 |
586 |
588 lemma permutation_id[simp]: "permutation id" |
590 lemma permutation_id[simp]: "permutation id" |
589 unfolding permutation_def by (rule exI[where x=0]) simp |
591 unfolding permutation_def by (rule exI[where x=0]) simp |
590 |
592 |
591 declare permutation_id[unfolded id_def, simp] |
593 declare permutation_id[unfolded id_def, simp] |
592 |
594 |
593 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)" |
595 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (transpose a b)" |
594 apply clarsimp |
596 apply clarsimp |
595 using comp_Suc[of 0 id a b] |
597 using comp_Suc[of 0 id a b] |
596 apply simp |
598 apply simp |
597 done |
599 done |
598 |
600 |
599 lemma permutation_swap_id: "permutation (Fun.swap a b id)" |
601 lemma permutation_swap_id: "permutation (transpose a b)" |
600 proof (cases "a = b") |
602 proof (cases "a = b") |
601 case True |
603 case True |
602 then show ?thesis by simp |
604 then show ?thesis by simp |
603 next |
605 next |
604 case False |
606 case False |
625 qed |
627 qed |
626 |
628 |
627 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)" |
629 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)" |
628 unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis |
630 unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis |
629 |
631 |
630 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)" |
632 lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> transpose a b)" |
631 by (induct n p rule: swapidseq.induct) |
633 by (induct n p rule: swapidseq.induct) |
632 (use swapidseq_swap[of a b] in \<open>auto simp add: comp_assoc intro: swapidseq.comp_Suc\<close>) |
634 (use swapidseq_swap[of a b] in \<open>auto simp add: comp_assoc intro: swapidseq.comp_Suc\<close>) |
633 |
635 |
634 lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id" |
636 lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id" |
635 proof (induct n p rule: swapidseq.induct) |
637 proof (induct n p rule: swapidseq.induct) |
638 by (rule exI[where x=id]) simp |
640 by (rule exI[where x=id]) simp |
639 next |
641 next |
640 case (comp_Suc n p a b) |
642 case (comp_Suc n p a b) |
641 from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" |
643 from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" |
642 by blast |
644 by blast |
643 let ?q = "q \<circ> Fun.swap a b id" |
645 let ?q = "q \<circ> transpose a b" |
644 note H = comp_Suc.hyps |
646 note H = comp_Suc.hyps |
645 from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (Fun.swap a b id)" |
647 from swapidseq_swap[of a b] H(3) have *: "swapidseq 1 (transpose a b)" |
646 by simp |
648 by simp |
647 from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q" |
649 from swapidseq_comp_add[OF q(1) *] have **: "swapidseq (Suc n) ?q" |
648 by simp |
650 by simp |
649 have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id" |
651 have "transpose a b \<circ> p \<circ> ?q = transpose a b \<circ> (p \<circ> q) \<circ> transpose a b" |
650 by (simp add: o_assoc) |
652 by (simp add: o_assoc) |
651 also have "\<dots> = id" |
653 also have "\<dots> = id" |
652 by (simp add: q(2)) |
654 by (simp add: q(2)) |
653 finally have ***: "Fun.swap a b id \<circ> p \<circ> ?q = id" . |
655 finally have ***: "transpose a b \<circ> p \<circ> ?q = id" . |
654 have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p" |
656 have "?q \<circ> (transpose a b \<circ> p) = q \<circ> (transpose a b \<circ> transpose a b) \<circ> p" |
655 by (simp only: o_assoc) |
657 by (simp only: o_assoc) |
656 then have "?q \<circ> (Fun.swap a b id \<circ> p) = id" |
658 then have "?q \<circ> (transpose a b \<circ> p) = id" |
657 by (simp add: q(3)) |
659 by (simp add: q(3)) |
658 with ** *** show ?case |
660 with ** *** show ?case |
659 by blast |
661 by blast |
660 qed |
662 qed |
661 |
663 |
670 |
672 |
671 |
673 |
672 subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close> |
674 subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close> |
673 |
675 |
674 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> |
676 lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> |
675 Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id" |
677 transpose a b \<circ> transpose a c = Fun.swap b c id \<circ> transpose a b" |
676 by (simp add: fun_eq_iff Fun.swap_def) |
678 by (simp add: fun_eq_iff Fun.swap_def) |
677 |
679 |
678 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> |
680 lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> |
679 Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id" |
681 transpose a c \<circ> Fun.swap b c id = Fun.swap b c id \<circ> transpose a b" |
680 by (simp add: fun_eq_iff Fun.swap_def) |
682 by (simp add: fun_eq_iff Fun.swap_def) |
681 |
683 |
682 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> |
684 lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> |
683 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id" |
685 transpose a b \<circ> transpose c d = transpose c d \<circ> transpose a b" |
684 by (simp add: fun_eq_iff Fun.swap_def) |
686 by (simp add: fun_eq_iff Fun.swap_def) |
685 |
687 |
686 |
688 |
687 subsection \<open>The identity map only has even transposition sequences\<close> |
689 subsection \<open>The identity map only has even transposition sequences\<close> |
688 |
690 |
693 P a b c d" |
695 P a b c d" |
694 shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> P a b c d" |
696 shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> P a b c d" |
695 using assms by metis |
697 using assms by metis |
696 |
698 |
697 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> |
699 lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> |
698 Fun.swap a b id \<circ> Fun.swap c d id = id \<or> |
700 transpose a b \<circ> transpose c d = id \<or> |
699 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
701 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
700 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)" |
702 transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z)" |
701 proof - |
703 proof - |
702 assume neq: "a \<noteq> b" "c \<noteq> d" |
704 assume neq: "a \<noteq> b" "c \<noteq> d" |
703 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> |
705 have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> |
704 (Fun.swap a b id \<circ> Fun.swap c d id = id \<or> |
706 (transpose a b \<circ> transpose c d = id \<or> |
705 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
707 (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> |
706 Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))" |
708 transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z))" |
707 apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) |
709 apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) |
708 apply (simp_all only: swap_commute) |
710 apply (simp_all only: ac_simps) |
709 apply (case_tac "a = c \<and> b = d") |
711 apply (metis id_comp swap_id_common swap_id_common' swap_id_independent transpose_comp_involutory) |
710 apply (clarsimp simp only: swap_commute swap_id_idempotent) |
|
711 apply (case_tac "a = c \<and> b \<noteq> d") |
|
712 apply (rule disjI2) |
|
713 apply (rule_tac x="b" in exI) |
|
714 apply (rule_tac x="d" in exI) |
|
715 apply (rule_tac x="b" in exI) |
|
716 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
|
717 apply (case_tac "a \<noteq> c \<and> b = d") |
|
718 apply (rule disjI2) |
|
719 apply (rule_tac x="c" in exI) |
|
720 apply (rule_tac x="d" in exI) |
|
721 apply (rule_tac x="c" in exI) |
|
722 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
|
723 apply (rule disjI2) |
|
724 apply (rule_tac x="c" in exI) |
|
725 apply (rule_tac x="d" in exI) |
|
726 apply (rule_tac x="b" in exI) |
|
727 apply (clarsimp simp add: fun_eq_iff Fun.swap_def) |
|
728 done |
712 done |
729 with neq show ?thesis by metis |
713 with neq show ?thesis by metis |
730 qed |
714 qed |
731 |
715 |
732 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id" |
716 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id" |
733 using swapidseq.cases[of 0 p "p = id"] by auto |
717 using swapidseq.cases[of 0 p "p = id"] by auto |
734 |
718 |
735 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> |
719 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> |
736 n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)" |
720 n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = transpose a b \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)" |
737 apply (rule iffI) |
721 apply (rule iffI) |
738 apply (erule swapidseq.cases[of n p]) |
722 apply (erule swapidseq.cases[of n p]) |
739 apply simp |
723 apply simp |
740 apply (rule disjI2) |
724 apply (rule disjI2) |
741 apply (rule_tac x= "a" in exI) |
725 apply (rule_tac x= "a" in exI) |
748 done |
732 done |
749 |
733 |
750 lemma fixing_swapidseq_decrease: |
734 lemma fixing_swapidseq_decrease: |
751 assumes "swapidseq n p" |
735 assumes "swapidseq n p" |
752 and "a \<noteq> b" |
736 and "a \<noteq> b" |
753 and "(Fun.swap a b id \<circ> p) a = a" |
737 and "(transpose a b \<circ> p) a = a" |
754 shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)" |
738 shows "n \<noteq> 0 \<and> swapidseq (n - 1) (transpose a b \<circ> p)" |
755 using assms |
739 using assms |
756 proof (induct n arbitrary: p a b) |
740 proof (induct n arbitrary: p a b) |
757 case 0 |
741 case 0 |
758 then show ?case |
742 then show ?case |
759 by (auto simp add: Fun.swap_def fun_upd_def) |
743 by (auto simp add: Fun.swap_def fun_upd_def) |
760 next |
744 next |
761 case (Suc n p a b) |
745 case (Suc n p a b) |
762 from Suc.prems(1) swapidseq_cases[of "Suc n" p] |
746 from Suc.prems(1) swapidseq_cases[of "Suc n" p] |
763 obtain c d q m where |
747 obtain c d q m where |
764 cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m" |
748 cdqm: "Suc n = Suc m" "p = transpose c d \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m" |
765 by auto |
749 by auto |
766 consider "Fun.swap a b id \<circ> Fun.swap c d id = id" |
750 consider "transpose a b \<circ> transpose c d = id" |
767 | x y z where "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y" |
751 | x y z where "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y" |
768 "Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id" |
752 "transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z" |
769 using swap_general[OF Suc.prems(2) cdqm(4)] by metis |
753 using swap_general[OF Suc.prems(2) cdqm(4)] by metis |
770 then show ?case |
754 then show ?case |
771 proof cases |
755 proof cases |
772 case 1 |
756 case 1 |
773 then show ?thesis |
757 then show ?thesis |
774 by (simp only: cdqm o_assoc) (simp add: cdqm) |
758 by (simp only: cdqm o_assoc) (simp add: cdqm) |
775 next |
759 next |
776 case prems: 2 |
760 case prems: 2 |
777 then have az: "a \<noteq> z" |
761 then have az: "a \<noteq> z" |
778 by simp |
762 by simp |
779 from prems have *: "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a" for h |
763 from prems have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h |
780 by (simp add: Fun.swap_def) |
764 by (simp add: transpose_def) |
781 from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)" |
765 from cdqm(2) have "transpose a b \<circ> p = transpose a b \<circ> (transpose c d \<circ> q)" |
782 by simp |
766 by simp |
783 then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)" |
767 then have "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)" |
784 by (simp add: o_assoc prems) |
768 by (simp add: o_assoc prems) |
785 then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a" |
769 then have "(transpose a b \<circ> p) a = (transpose x y \<circ> (transpose a z \<circ> q)) a" |
786 by simp |
770 by simp |
787 then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a" |
771 then have "(transpose x y \<circ> (transpose a z \<circ> q)) a = a" |
788 unfolding Suc by metis |
772 unfolding Suc by metis |
789 then have "(Fun.swap a z id \<circ> q) a = a" |
773 then have "(transpose a z \<circ> q) a = a" |
790 by (simp only: *) |
774 by (simp only: *) |
791 from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this] |
775 from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this] |
792 have **: "swapidseq (n - 1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0" |
776 have **: "swapidseq (n - 1) (transpose a z \<circ> q)" "n \<noteq> 0" |
793 by blast+ |
777 by blast+ |
794 from \<open>n \<noteq> 0\<close> have ***: "Suc n - 1 = Suc (n - 1)" |
778 from \<open>n \<noteq> 0\<close> have ***: "Suc n - 1 = Suc (n - 1)" |
795 by auto |
779 by auto |
796 show ?thesis |
780 show ?thesis |
797 apply (simp only: cdqm(2) prems o_assoc ***) |
781 apply (simp only: cdqm(2) prems o_assoc ***) |
863 |
847 |
864 lemma evenperm_identity [simp]: |
848 lemma evenperm_identity [simp]: |
865 \<open>evenperm (\<lambda>x. x)\<close> |
849 \<open>evenperm (\<lambda>x. x)\<close> |
866 using evenperm_id by (simp add: id_def [abs_def]) |
850 using evenperm_id by (simp add: id_def [abs_def]) |
867 |
851 |
868 lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" |
852 lemma evenperm_swap: "evenperm (transpose a b) = (a = b)" |
869 by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap) |
853 by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap) |
870 |
854 |
871 lemma evenperm_comp: |
855 lemma evenperm_comp: |
872 assumes "permutation p" "permutation q" |
856 assumes "permutation p" "permutation q" |
873 shows "evenperm (p \<circ> q) \<longleftrightarrow> evenperm p = evenperm q" |
857 shows "evenperm (p \<circ> q) \<longleftrightarrow> evenperm p = evenperm q" |
922 next |
906 next |
923 case (comp_Suc n p a b) |
907 case (comp_Suc n p a b) |
924 let ?S = "insert a (insert b {x. p x \<noteq> x})" |
908 let ?S = "insert a (insert b {x. p x \<noteq> x})" |
925 from comp_Suc.hyps(2) have *: "finite ?S" |
909 from comp_Suc.hyps(2) have *: "finite ?S" |
926 by simp |
910 by simp |
927 from \<open>a \<noteq> b\<close> have **: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S" |
911 from \<open>a \<noteq> b\<close> have **: "{x. (transpose a b \<circ> p) x \<noteq> x} \<subseteq> ?S" |
928 by (auto simp: Fun.swap_def) |
912 by (auto simp: Fun.swap_def) |
929 show ?case |
913 show ?case |
930 by (rule finite_subset[OF ** *]) |
914 by (rule finite_subset[OF ** *]) |
931 qed |
915 qed |
932 qed |
916 qed |
1059 by (simp add: sign_def evenperm_inv) |
1043 by (simp add: sign_def evenperm_inv) |
1060 |
1044 |
1061 lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q" |
1045 lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q" |
1062 by (simp add: sign_def evenperm_comp) |
1046 by (simp add: sign_def evenperm_comp) |
1063 |
1047 |
1064 lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else - 1)" |
1048 lemma sign_swap_id: "sign (transpose a b) = (if a = b then 1 else - 1)" |
1065 by (simp add: sign_def evenperm_swap) |
1049 by (simp add: sign_def evenperm_swap) |
1066 |
1050 |
1067 lemma sign_idempotent [simp]: "sign p * sign p = 1" |
1051 lemma sign_idempotent [simp]: "sign p * sign p = 1" |
1068 by (simp add: sign_def) |
1052 by (simp add: sign_def) |
1069 |
1053 |
1587 |
1571 |
1588 lemma sum_over_permutations_insert: |
1572 lemma sum_over_permutations_insert: |
1589 assumes fS: "finite S" |
1573 assumes fS: "finite S" |
1590 and aS: "a \<notin> S" |
1574 and aS: "a \<notin> S" |
1591 shows "sum f {p. p permutes (insert a S)} = |
1575 shows "sum f {p. p permutes (insert a S)} = |
1592 sum (\<lambda>b. sum (\<lambda>q. f (Fun.swap a b id \<circ> q)) {p. p permutes S}) (insert a S)" |
1576 sum (\<lambda>b. sum (\<lambda>q. f (transpose a b \<circ> q)) {p. p permutes S}) (insert a S)" |
1593 proof - |
1577 proof - |
1594 have *: "\<And>f a b. (\<lambda>(b, p). f (Fun.swap a b id \<circ> p)) = f \<circ> (\<lambda>(b,p). Fun.swap a b id \<circ> p)" |
1578 have *: "\<And>f a b. (\<lambda>(b, p). f (transpose a b \<circ> p)) = f \<circ> (\<lambda>(b,p). transpose a b \<circ> p)" |
1595 by (simp add: fun_eq_iff) |
1579 by (simp add: fun_eq_iff) |
1596 have **: "\<And>P Q. {(a, b). a \<in> P \<and> b \<in> Q} = P \<times> Q" |
1580 have **: "\<And>P Q. {(a, b). a \<in> P \<and> b \<in> Q} = P \<times> Q" |
1597 by blast |
1581 by blast |
1598 show ?thesis |
1582 show ?thesis |
1599 unfolding * ** sum.cartesian_product permutes_insert |
1583 unfolding * ** sum.cartesian_product permutes_insert |
1600 proof (rule sum.reindex) |
1584 proof (rule sum.reindex) |
1601 let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)" |
1585 let ?f = "(\<lambda>(b, y). transpose a b \<circ> y)" |
1602 let ?P = "{p. p permutes S}" |
1586 let ?P = "{p. p permutes S}" |
1603 { |
1587 { |
1604 fix b c p q |
1588 fix b c p q |
1605 assume b: "b \<in> insert a S" |
1589 assume b: "b \<in> insert a S" |
1606 assume c: "c \<in> insert a S" |
1590 assume c: "c \<in> insert a S" |
1607 assume p: "p permutes S" |
1591 assume p: "p permutes S" |
1608 assume q: "q permutes S" |
1592 assume q: "q permutes S" |
1609 assume eq: "Fun.swap a b id \<circ> p = Fun.swap a c id \<circ> q" |
1593 assume eq: "transpose a b \<circ> p = transpose a c \<circ> q" |
1610 from p q aS have pa: "p a = a" and qa: "q a = a" |
1594 from p q aS have pa: "p a = a" and qa: "q a = a" |
1611 unfolding permutes_def by metis+ |
1595 unfolding permutes_def by metis+ |
1612 from eq have "(Fun.swap a b id \<circ> p) a = (Fun.swap a c id \<circ> q) a" |
1596 from eq have "(transpose a b \<circ> p) a = (transpose a c \<circ> q) a" |
1613 by simp |
1597 by simp |
1614 then have bc: "b = c" |
1598 then have bc: "b = c" |
1615 by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def |
1599 by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def |
1616 cong del: if_weak_cong split: if_split_asm) |
1600 cong del: if_weak_cong split: if_split_asm) |
1617 from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) = |
1601 from eq[unfolded bc] have "(\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> p) = |
1618 (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp |
1602 (\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> q)" by simp |
1619 then have "p = q" |
1603 then have "p = q" |
1620 unfolding o_assoc swap_id_idempotent by simp |
1604 unfolding o_assoc swap_id_idempotent by simp |
1621 with bc have "b = c \<and> p = q" |
1605 with bc have "b = c \<and> p = q" |
1622 by blast |
1606 by blast |
1623 } |
1607 } |