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