Theory 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. λiI. x (f i)) (J E S) (I E S)"
proof (rule bij_betwI[where g="(λx. λiJ. 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. λiI. x (f i))  (J E S)  I E S"
    using bij_betw_apply[OF assms] by auto
  show "(λx. λiJ. x (the_inv_into I f i))  (I E S)  J E S"
    using bij_betw_apply[OF 0] by auto
  show "(λjJ. (λiI. x (f i)) (the_inv_into I f j)) = x" if "x  J E S" for x
  proof -
    have "(λiI. 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 " (λiI. (λjJ. y (the_inv_into I f j)) (f i)) = y" if "y  I E S" for y
  proof -
    have "(λjJ. 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. λiI. 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 "(λiI. 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 "(λiI. ?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 "(λiI. ?g ((λiI. f (x i)) i)) = x" if "x  (I E S)" for x
  proof -
    have "(λiI. ?g ((λiI. 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 "(λiI. f ((λiI. ?g (x i)) i)) = x" if "x  (I E T)" for x
  proof -
    have "(λiI. f ((λiI. ?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. λiI. ?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