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