src/HOL/Combinatorics/Transposition.thy
 author haftmann Mon, 10 May 2021 19:46:01 +0000 changeset 73664 6e26d06b24b1 parent 73648 1bd3463e30b8 permissions -rw-r--r--
centralized more lemmas
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 1` ```section \Transposition function\ ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 2` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 3` ```theory Transposition ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 4` ``` imports Main ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 5` ```begin ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 6` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 7` ```definition transpose :: \'a \ 'a \ 'a \ 'a\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 8` ``` where \transpose a b c = (if c = a then b else if c = b then a else c)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 9` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 10` ```lemma transpose_apply_first [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 11` ``` \transpose a b a = b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 12` ``` by (simp add: transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 13` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 14` ```lemma transpose_apply_second [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 15` ``` \transpose a b b = a\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 16` ``` by (simp add: transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 17` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 18` ```lemma transpose_apply_other [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 19` ``` \transpose a b c = c\ if \c \ a\ \c \ b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 20` ``` using that by (simp add: transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 21` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 22` ```lemma transpose_same [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 23` ``` \transpose a a = id\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 24` ``` by (simp add: fun_eq_iff transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 25` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 26` ```lemma transpose_eq_iff: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 27` ``` \transpose a b c = d \ (c \ a \ c \ b \ d = c) \ (c = a \ d = b) \ (c = b \ d = a)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 28` ``` by (auto simp add: transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 29` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 30` ```lemma transpose_eq_imp_eq: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 31` ``` \c = d\ if \transpose a b c = transpose a b d\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 32` ``` using that by (auto simp add: transpose_eq_iff) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 33` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 34` ```lemma transpose_commute [ac_simps]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 35` ``` \transpose b a = transpose a b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 36` ``` by (auto simp add: fun_eq_iff transpose_eq_iff) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 37` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 38` ```lemma transpose_involutory [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 39` ``` \transpose a b (transpose a b c) = c\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 40` ``` by (auto simp add: transpose_eq_iff) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 41` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 42` ```lemma transpose_comp_involutory [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 43` ``` \transpose a b \ transpose a b = id\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 44` ``` by (rule ext) simp ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 45` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 46` ```lemma transpose_triple: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 47` ``` \transpose a b (transpose b c (transpose a b d)) = transpose a c d\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 48` ``` if \a \ c\ and \b \ c\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 49` ``` using that by (simp add: transpose_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 50` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 51` ```lemma transpose_comp_triple: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 52` ``` \transpose a b \ transpose b c \ transpose a b = transpose a c\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 53` ``` if \a \ c\ and \b \ c\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 54` ``` using that by (simp add: fun_eq_iff transpose_triple) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 55` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 56` ```lemma transpose_image_eq [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 57` ``` \transpose a b ` A = A\ if \a \ A \ b \ A\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 58` ``` using that by (auto simp add: transpose_def [abs_def]) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 59` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 60` ```lemma inj_on_transpose [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 61` ``` \inj_on (transpose a b) A\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 62` ``` by rule (drule transpose_eq_imp_eq) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 63` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 64` ```lemma inj_transpose: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 65` ``` \inj (transpose a b)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 66` ``` by (fact inj_on_transpose) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 67` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 68` ```lemma surj_transpose: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 69` ``` \surj (transpose a b)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 70` ``` by simp ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 71` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 72` ```lemma bij_betw_transpose_iff [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 73` ``` \bij_betw (transpose a b) A A\ if \a \ A \ b \ A\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 74` ``` using that by (auto simp: bij_betw_def) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 75` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 76` ```lemma bij_transpose [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 77` ``` \bij (transpose a b)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 78` ``` by (rule bij_betw_transpose_iff) simp ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 79` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 80` ```lemma bijection_transpose: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 81` ``` \bijection (transpose a b)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 82` ``` by standard (fact bij_transpose) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 83` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 84` ```lemma inv_transpose_eq [simp]: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 85` ``` \inv (transpose a b) = transpose a b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 86` ``` by (rule inv_unique_comp) simp_all ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 87` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 88` ```lemma transpose_apply_commute: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 89` ``` \transpose a b (f c) = f (transpose (inv f a) (inv f b) c)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 90` ``` if \bij f\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 91` ```proof - ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 92` ``` from that have \surj f\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 93` ``` by (rule bij_is_surj) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 94` ``` with that show ?thesis ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 95` ``` by (simp add: transpose_def bij_inv_eq_iff surj_f_inv_f) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 96` ```qed ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 97` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 98` ```lemma transpose_comp_eq: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 99` ``` \transpose a b \ f = f \ transpose (inv f a) (inv f b)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 100` ``` if \bij f\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 101` ``` using that by (simp add: fun_eq_iff transpose_apply_commute) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 102` 73664 6e26d06b24b1 centralized more lemmas haftmann parents: 73648 diff changeset ` 103` ```lemma in_transpose_image_iff: ``` 6e26d06b24b1 centralized more lemmas haftmann parents: 73648 diff changeset ` 104` ``` \x \ transpose a b ` S \ transpose a b x \ S\ ``` 6e26d06b24b1 centralized more lemmas haftmann parents: 73648 diff changeset ` 105` ``` by (auto intro!: image_eqI) ``` 6e26d06b24b1 centralized more lemmas haftmann parents: 73648 diff changeset ` 106` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 107` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 108` ```text \Legacy input alias\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 109` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 110` ```setup \Context.theory_map (Name_Space.map_naming (Name_Space.qualified_path true \<^binding>\Fun\))\ ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 111` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 112` ```abbreviation (input) swap :: \'a \ 'a \ ('a \ 'b) \ 'a \ 'b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 113` ``` where \swap a b f \ f \ transpose a b\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 114` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 115` ```lemma swap_def: ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 116` ``` \Fun.swap a b f = f (a := f b, b:= f a)\ ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 117` ``` by (simp add: fun_eq_iff) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 118` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 119` ```setup \Context.theory_map (Name_Space.map_naming (Name_Space.parent_path))\ ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 120` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 121` ```lemma swap_apply: ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 122` ``` "Fun.swap a b f a = f b" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 123` ``` "Fun.swap a b f b = f a" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 124` ``` "c \ a \ c \ b \ Fun.swap a b f c = f c" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 125` ``` by simp_all ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 126` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 127` ```lemma swap_self: "Fun.swap a a f = f" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 128` ``` by simp ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 129` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 130` ```lemma swap_commute: "Fun.swap a b f = Fun.swap b a f" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 131` ``` by (simp add: ac_simps) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 132` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 133` ```lemma swap_nilpotent: "Fun.swap a b (Fun.swap a b f) = f" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 134` ``` by (simp add: comp_assoc) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 135` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 136` ```lemma swap_comp_involutory: "Fun.swap a b \ Fun.swap a b = id" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 137` ``` by (simp add: fun_eq_iff) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 138` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 139` ```lemma swap_triple: ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 140` ``` assumes "a \ c" and "b \ c" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 141` ``` shows "Fun.swap a b (Fun.swap b c (Fun.swap a b f)) = Fun.swap a c f" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 142` ``` using assms transpose_comp_triple [of a c b] ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 143` ``` by (simp add: comp_assoc) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 144` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 145` ```lemma comp_swap: "f \ Fun.swap a b g = Fun.swap a b (f \ g)" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 146` ``` by (simp add: comp_assoc) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 147` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 148` ```lemma swap_image_eq: ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 149` ``` assumes "a \ A" "b \ A" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 150` ``` shows "Fun.swap a b f ` A = f ` A" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 151` ``` using assms by (metis image_comp transpose_image_eq) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 152` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 153` ```lemma inj_on_imp_inj_on_swap: "inj_on f A \ a \ A \ b \ A \ inj_on (Fun.swap a b f) A" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 154` ``` by (simp add: comp_inj_on) ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 155` ``` ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 156` ```lemma inj_on_swap_iff: ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 157` ``` assumes A: "a \ A" "b \ A" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 158` ``` shows "inj_on (Fun.swap a b f) A \ inj_on f A" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 159` ``` using assms by (metis inj_on_imageI inj_on_imp_inj_on_swap transpose_image_eq) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 160` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 161` ```lemma surj_imp_surj_swap: "surj f \ surj (Fun.swap a b f)" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 162` ``` by (meson comp_surj surj_transpose) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 163` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 164` ```lemma surj_swap_iff: "surj (Fun.swap a b f) \ surj f" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 165` ``` by (metis fun.set_map surj_transpose) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 166` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 167` ```lemma bij_betw_swap_iff: "x \ A \ y \ A \ bij_betw (Fun.swap x y f) A B \ bij_betw f A B" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 168` ``` by (meson bij_betw_comp_iff bij_betw_transpose_iff) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 169` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 170` ```lemma bij_swap_iff: "bij (Fun.swap a b f) \ bij f" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 171` ``` by (simp add: bij_betw_swap_iff) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 172` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 173` ```lemma swap_image: ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 174` ``` \Fun.swap i j f ` A = f ` (A - {i, j} ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 175` ``` \ (if i \ A then {j} else {}) \ (if j \ A then {i} else {}))\ ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 176` ``` by (auto simp add: Fun.swap_def) ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 177` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 178` ```lemma inv_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 179` ``` by simp ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 180` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 181` ```lemma bij_swap_comp: ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 182` ``` assumes "bij p" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 183` ``` shows "Fun.swap a b id \ p = Fun.swap (inv p a) (inv p b) p" ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 184` ``` using assms by (simp add: transpose_comp_eq) ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 185` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 186` ```lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)" ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 187` ``` by (simp add: Fun.swap_def) ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 188` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 189` ```lemma swap_unfold: ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 190` ``` \Fun.swap a b p = p \ Fun.swap a b id\ ``` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 191` ``` by simp ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 192` 73648 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 193` ```lemma swap_id_idempotent: "Fun.swap a b id \ Fun.swap a b id = id" ``` 1bd3463e30b8 more elementary swap haftmann parents: 73623 diff changeset ` 194` ``` by simp ``` 73623 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 195` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 196` ```lemma bij_swap_compose_bij: ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 197` ``` \bij (Fun.swap a b id \ p)\ if \bij p\ ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 198` ``` using that by (rule bij_comp) simp ``` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 199` 5020054b3a16 tuned theory structure haftmann parents: diff changeset ` 200` ```end ```