summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 10 May 2021 19:45:54 +0000 | |

changeset 73919 | 7734c442802f |

parent 73918 | fecfb96474ca |

child 73920 | 6e26d06b24b1 |

avoid Fun.swap

src/HOL/Combinatorics/Cycles.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Combinatorics/Permutations.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Combinatorics/Cycles.thy Mon May 10 19:45:51 2021 +0000 +++ b/src/HOL/Combinatorics/Cycles.thy Mon May 10 19:45:54 2021 +0000 @@ -43,20 +43,25 @@ proof - { have "map (cycle_of_list cs) cs = rotate1 cs" using assms(1) proof (induction cs rule: cycle_of_list.induct) - case (1 i j cs) thus ?case + case (1 i j cs) + then have \<open>i \<notin> set cs\<close> \<open>j \<notin> set cs\<close> + by auto + then have \<open>map (Transposition.transpose i j) cs = cs\<close> + by (auto intro: map_idI simp add: transpose_eq_iff) + show ?case proof (cases) assume "cs = Nil" thus ?thesis by simp next assume "cs \<noteq> Nil" hence ge_two: "length (j # cs) \<ge> 2" using not_less by auto have "map (cycle_of_list (i # j # cs)) (i # j # cs) = - map (Fun.swap i j id) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp - also have " ... = map (Fun.swap i j id) (i # (rotate1 (j # cs)))" + map (transpose i j) (map (cycle_of_list (j # cs)) (i # j # cs))" by simp + also have " ... = map (transpose i j) (i # (rotate1 (j # cs)))" by (metis "1.IH" "1.prems" distinct.simps(2) id_outside_supp list.simps(9)) - also have " ... = map (Fun.swap i j id) (i # (cs @ [j]))" by simp - also have " ... = j # (map (Fun.swap i j id) cs) @ [i]" by simp + also have " ... = map (transpose i j) (i # (cs @ [j]))" by simp + also have " ... = j # (map (transpose i j) cs) @ [i]" by simp also have " ... = j # cs @ [i]" - by (metis "1.prems" distinct.simps(2) list.set_intros(2) map_idI swap_id_eq) + using \<open>map (Transposition.transpose i j) cs = cs\<close> by simp also have " ... = rotate1 (i # j # cs)" by simp finally show ?thesis . qed @@ -118,7 +123,7 @@ proof (induction cs rule: cycle_of_list.induct) case (1 i j cs) have "p \<circ> cycle_of_list (i # j # cs) \<circ> inv p = - (p \<circ> (Fun.swap i j id) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" + (p \<circ> (transpose i j) \<circ> inv p) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" by (simp add: assms(2) bij_is_inj fun.map_comp) also have " ... = (transpose (p i) (p j)) \<circ> (p \<circ> cycle_of_list (j # cs) \<circ> inv p)" using "1.prems"(2) by (simp add: bij_inv_eq_iff transpose_apply_commute fun_eq_iff bij_betw_inv_into_left)

--- a/src/HOL/Combinatorics/Permutations.thy Mon May 10 19:45:51 2021 +0000 +++ b/src/HOL/Combinatorics/Permutations.thy Mon May 10 19:45:54 2021 +0000 @@ -382,7 +382,7 @@ apply (rule permutes_swap_id, simp) using permutes_in_image[OF assms, of a] apply simp - apply (auto simp add: Ball_def Fun.swap_def) + apply (auto simp add: Ball_def) done lemma permutes_insert: "{p. p permutes (insert a S)} = @@ -459,17 +459,17 @@ from bp cq have pF: "p permutes F" and qF: "q permutes F" by auto from pF \<open>x \<notin> F\<close> eq have "b = ?g (b, p) x" - by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) + by (auto simp: permutes_def fun_upd_def fun_eq_iff) also from qF \<open>x \<notin> F\<close> eq have "\<dots> = ?g (c, q) x" by (auto simp: fun_upd_def fun_eq_iff) also from qF \<open>x \<notin> F\<close> have "\<dots> = c" - by (auto simp: permutes_def Fun.swap_def fun_upd_def fun_eq_iff) + by (auto simp: permutes_def fun_upd_def fun_eq_iff) finally have "b = c" . - then have "Fun.swap x b id = Fun.swap x c id" + then have "transpose x b = transpose x c" by simp - with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q" + with eq have "transpose x b \<circ> p = transpose x b \<circ> q" by simp - then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) = Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)" + then have "transpose x b \<circ> (transpose x b \<circ> p) = transpose x b \<circ> (transpose x b \<circ> q)" by simp then have "p = q" by (simp add: o_assoc) @@ -545,10 +545,10 @@ next case (swap a b p) then have \<open>bij p\<close> - using permutes_bij by blast - have \<open>P (Fun.swap (inv p a) (inv p b) p)\<close> + using permutes_bij by blast + have \<open>P (p \<circ> transpose (inv p a) (inv p b))\<close> by (rule swap') (auto simp add: swap permutes_in_image permutes_inv) - also have \<open>Fun.swap (inv p a) (inv p b) p = transpose a b \<circ> p\<close> + also have \<open>p \<circ> transpose (inv p a) (inv p b) = transpose a b \<circ> p\<close> using \<open>bij p\<close> by (rule transpose_comp_eq [symmetric]) finally show ?case . qed @@ -674,16 +674,16 @@ subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close> lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> - transpose a b \<circ> transpose a c = Fun.swap b c id \<circ> transpose a b" - by (simp add: fun_eq_iff Fun.swap_def) + transpose a b \<circ> transpose a c = transpose b c \<circ> transpose a b" + by (simp add: fun_eq_iff transpose_def) lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> - transpose a c \<circ> Fun.swap b c id = Fun.swap b c id \<circ> transpose a b" - by (simp add: fun_eq_iff Fun.swap_def) + transpose a c \<circ> transpose b c = transpose b c \<circ> transpose a b" + by (simp add: fun_eq_iff transpose_def) lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> transpose a b \<circ> transpose c d = transpose c d \<circ> transpose a b" - by (simp add: fun_eq_iff Fun.swap_def) + by (simp add: fun_eq_iff transpose_def) subsection \<open>The identity map only has even transposition sequences\<close> @@ -740,7 +740,7 @@ proof (induct n arbitrary: p a b) case 0 then show ?case - by (auto simp add: Fun.swap_def fun_upd_def) + by (auto simp add: fun_upd_def) next case (Suc n p a b) from Suc.prems(1) swapidseq_cases[of "Suc n" p] @@ -909,7 +909,7 @@ from comp_Suc.hyps(2) have *: "finite ?S" by simp from \<open>a \<noteq> b\<close> have **: "{x. (transpose a b \<circ> p) x \<noteq> x} \<subseteq> ?S" - by (auto simp: Fun.swap_def) + by auto show ?case by (rule finite_subset[OF ** *]) qed @@ -927,14 +927,14 @@ by simp next case (insert a F p) - let ?r = "Fun.swap a (p a) id \<circ> p" - let ?q = "Fun.swap a (p a) id \<circ> ?r" + let ?r = "transpose a (p a) \<circ> p" + let ?q = "transpose a (p a) \<circ> ?r" have *: "?r a = a" - by (simp add: Fun.swap_def) + by simp from insert * have **: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) have "bij ?r" - by (rule bij_swap_compose_bij[OF insert(4)]) + using insert by (simp add: bij_comp) have "permutation ?r" by (rule insert(3)[OF \<open>bij ?r\<close> **]) then have "permutation ?q" @@ -1596,7 +1596,7 @@ from eq have "(transpose a b \<circ> p) a = (transpose a c \<circ> q) a" by simp then have bc: "b = c" - by (simp add: permutes_def pa qa o_def fun_upd_def Fun.swap_def id_def + by (simp add: permutes_def pa qa o_def fun_upd_def id_def cong del: if_weak_cong split: if_split_asm) from eq[unfolded bc] have "(\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> p) = (\<lambda>p. transpose a c \<circ> p) (transpose a c \<circ> q)" by simp