# Theory Finite_Fields.Finite_Fields_More_Bijections

```section ‹Additional results about Bijections and Digit Representations›

theory Finite_Fields_More_Bijections
imports "HOL-Library.FuncSet" Digit_Expansions.Bits_Digits
begin

lemma nth_digit_0:
assumes "x < b^k"
shows "nth_digit x k b = 0"
using assms unfolding nth_digit_def by auto

lemma nth_digit_bounded':
assumes "b > 0"
shows "nth_digit v x b < b"
using assms by (simp add: nth_digit_def)

lemma digit_gen_sum_repr':
assumes "n < b^c"
shows "n = (∑k<c. nth_digit n k b * b ^ k)"
proof -
consider (a) "b = 0" "c = 0" | (b) "b = 0" "c > 0" | (c) "b = 1" | (d) "b>1" by linarith
thus ?thesis
proof (cases)
case a thus ?thesis using assms by simp
next
case b thus ?thesis using assms by (simp add: zero_power)
next
case c thus ?thesis using assms by (simp add:nth_digit_def)
next
case d thus ?thesis by (intro digit_gen_sum_repr assms d)
qed
qed

lemma
assumes "⋀x. x ∈ A ⟹ f (g x) = x"
shows "⋀y. y ∈ g ` A ⟹ g (f y) = y"
proof -
show "g (f y) = y" if 0:"y∈ g`A" for y
proof -
obtain x where x_dom: "x ∈ A" and y_def: "y = g x"  using 0 by auto
hence "g (f y) = g (f (g x))" by simp
also have "... = g x" by (intro arg_cong[where f="g"] assms(1) x_dom)
also have "... = y" unfolding y_def by simp
finally show ?thesis by simp
qed
qed

lemma nth_digit_bij:
"bij_betw (λv. (λx∈{..<n}. nth_digit v x b)) {..<b^n} ({..<n} →⇩E {..<b})"
(is "bij_betw ?f ?A ?B")
proof -
have inj_f: "inj_on ?f ?A"
using digit_gen_sum_repr' by (intro inj_on_inverseI[where g="(λx. (∑k<n. x k * b^k))"]) auto

consider (a) "b = 0" "n= 0" | (b) "b = 0" "n>0" | (c) "b > 0" by linarith
hence "nth_digit x i b ∈ {..<b}" if "i < n" "x < b^n" for i x
proof (cases)
case a then show ?thesis using that by auto
next
case b thus ?thesis using that by (simp add:zero_power)
next
case c thus ?thesis using that by (simp add:nth_digit_def)
qed
hence "?f x ∈ ?B" if "x ∈ ?A" for x using that unfolding restrict_PiE_iff by auto
hence "?f ` ?A = ?B"
using card_image[OF inj_f] by (intro card_seteq finite_PiE image_subsetI) (auto simp:card_PiE)
thus ?thesis using inj_f unfolding bij_betw_def by auto
qed

lemma nth_digit_sum:
assumes "⋀i. i < l ⟹ f i < b"
shows "⋀k. k < l ⟹ nth_digit (∑i< l. f i * b^i) k b = f k"
and "(∑i<l. f i * b^i) < b^l"
proof -
define n where "n = (∑i< l. f i * b^i)"

have "restrict f {..<l} ∈ {..<l} →⇩E {..<b}" using assms(1) by auto
then obtain m where a:"(λx∈{..<l}. nth_digit m x b) = restrict f {..<l}" and b:"m ∈ {..<b^l}"
using bij_betw_imp_surj_on[OF nth_digit_bij[where n="l" and b="b"]]
by (metis (no_types, lifting) image_iff)

have "m = (∑i< l. nth_digit m i b * b^i)"
using b by (intro digit_gen_sum_repr') auto
also have "... = (∑i< l. f i * b^i)"
using a by (intro sum.cong arg_cong2[where f="(*)"] refl) (metis restrict_apply')
also have "... = n" unfolding n_def by simp
finally have c:"n = m"  by simp
show "(∑i<l. f i * b^i) < b^l" unfolding n_def[symmetric] c using b by auto
show "nth_digit (∑i< l. f i * b^i) k b = f k" if "k < l" for k
proof -
have "nth_digit (∑i< l. f i * b^i) k b = nth_digit m k b" unfolding n_def[symmetric] c by simp
also have "... = f k" using a that by (metis lessThan_iff restrict_apply')
finally show ?thesis by simp
qed
qed

lemma bij_betw_reindex:
assumes "bij_betw f I J"
shows "bij_betw (λx. λi∈I. x (f i)) (J →⇩E S) (I →⇩E S)"
proof (rule bij_betwI[where g="(λx. λi∈J. x (the_inv_into I f i))"])
have 0:"bij_betw (the_inv_into I f) J I"
using assms bij_betw_the_inv_into by auto

show "(λx. λi∈I. x (f i)) ∈ (J →⇩E S) → I →⇩E S"
using bij_betw_apply[OF assms] by auto
show "(λx. λi∈J. x (the_inv_into I f i)) ∈ (I →⇩E S) → J →⇩E S"
using bij_betw_apply[OF 0] by auto
show "(λj∈J. (λi∈I. x (f i)) (the_inv_into I f j)) = x" if "x ∈ J →⇩E S" for x
proof -
have "(λi∈I. x (f i)) (the_inv_into I f j) = x j" if "j ∈ J" for j
using 0 assms f_the_inv_into_f_bij_betw bij_betw_apply that by fastforce
thus ?thesis using PiE_arb[OF that] by auto
qed
show " (λi∈I. (λj∈J. y (the_inv_into I f j)) (f i)) = y" if "y ∈ I →⇩E S" for y
proof -
have "(λj∈J. y (the_inv_into I f j)) (f i) = y i" if "i ∈ I" for i
using assms 0 that the_inv_into_f_f[OF bij_betw_imp_inj_on[OF assms]] bij_betw_apply by force
thus ?thesis using PiE_arb[OF that] by auto
qed
qed

lemma lift_bij_betw:
assumes "bij_betw f S T"
shows "bij_betw (λx. λi∈I. f (x i)) (I →⇩E S) (I →⇩E T)"
proof -
let ?g = "the_inv_into S f"

have bij_g: "bij_betw ?g T S" using bij_betw_the_inv_into[OF assms] by simp
have 0:"?g(f x)=x" if "x ∈ S" for x by (intro the_inv_into_f_f that bij_betw_imp_inj_on[OF assms])
have 1:"f(?g x)=x" if "x ∈ T" for x by (intro f_the_inv_into_f_bij_betw[OF assms] that)

have "(λi∈I. f (x i)) ∈ I →⇩E T" if "x ∈ (I →⇩E S)" for x
using bij_betw_apply[OF assms] that by (auto simp: Pi_def)
moreover have "(λi∈I. ?g (x i)) ∈ I →⇩E S" if "x ∈ (I →⇩E T)" for x
using bij_betw_apply[OF bij_g] that by (auto simp: Pi_def)
moreover have "(λi∈I. ?g ((λi∈I. f (x i)) i)) = x" if "x ∈ (I →⇩E S)" for x
proof -
have "(λi∈I. ?g ((λi∈I. f (x i)) i)) i = x i" for i
using PiE_mem[OF that] using PiE_arb[OF that]  by (cases "i ∈ I")  (simp add:0)+
thus ?thesis by auto
qed
moreover have "(λi∈I. f ((λi∈I. ?g (x i)) i)) = x" if "x ∈ (I →⇩E T)" for x
proof -
have "(λi∈I. f ((λi∈I. ?g (x i)) i)) i = x i" for i
using PiE_mem[OF that] using PiE_arb[OF that]  by (cases "i ∈ I")  (simp add:1)+
thus ?thesis by auto
qed
ultimately show ?thesis
by (intro bij_betwI[where g="(λx. λi∈I. ?g (x i))"]) simp_all
qed

lemma lists_bij:
"bij_betw (λx. map x [ 0..<d] ) ({..<d} →⇩E S) {x. set x ⊆ S ∧ length x = d}"
proof (intro bij_betwI[where g="(λx. λi∈{..<d}. x ! i)"] funcsetI CollectI, goal_cases)
case (1 x)
hence " x ` {0..<d} ⊆ S" by (intro image_subsetI) auto
thus ?case by simp
next
case (2 x) thus ?case by auto
next
case (3 x)
have "restrict ((!) (map x [ 0..<d] )) {..<d} j = x j" for j
using PiE_arb[OF 3] by (cases "j ∈ {..<d}") auto
thus ?case by auto
next
case (4 y)
have "map (restrict ((!) y) {..<d}) [ 0..<d ] = map (((!) y)) [ 0..<d]" by (intro map_cong) auto
also have "... = y" using 4 map_nth by blast
finally show ?case by auto
qed

lemma bij_betw_prod: "bij_betw (λx. (x mod s, x div s)) {..<s * t} ({..<(s::nat)} × {..<t})"
proof -
have bij_betw_aux: "x + s * y < s * t" if "x < s" "y < t" for x y :: nat
proof -
have "x + s * y < s + s * y" using that by simp
also have "... = s * (y+1)" by simp
also have "... ≤ s * t" using that by (intro mult_left_mono) auto
finally show ?thesis by simp
qed

show ?thesis
proof (cases "s > 0 ∧ t > 0")
case True
then show ?thesis using less_mult_imp_div_less bij_betw_aux
by (intro bij_betwI[where g="(λx. fst x + s * snd x)"]) (auto simp:mult.commute)
next
case False then show ?thesis by (auto simp:bij_betw_def)
qed
qed

end```