Theory Algebraic_Integer_Divisibility

(*
  File:     Algebraic_Integer_Divisibility.thy
  Author:   Manuel Eberl, TU München
*)
section ‹Divisibility of algebraic integers›
theory Algebraic_Integer_Divisibility
  imports "Algebraic_Numbers.Algebraic_Numbers"
begin

text ‹
  In this section, we define a notion of divisibility of algebraic integers: ‹y› is divisible
  by ‹x› if ‹y / x› is an algebraic integer (or if ‹x› and ‹y› are both zero).

  Technically, the definition does not require ‹x› and ‹y› to be algebraic integers themselves,
  but we will always use it that way (in fact, in our case ‹x› will always be a rational integer).
›

definition alg_dvd :: "'a :: field ⇒ 'a ⇒ bool" (infix ‹alg'_dvd› 50) where
  "x alg_dvd y ⟷ (x = 0 ⟶ y = 0) ∧ algebraic_int (y / x)"

lemma alg_dvd_imp_algebraic_int:
  fixes x y :: "'a :: field_char_0"
  shows "x alg_dvd y ⟹ algebraic_int x ⟹ algebraic_int y"
  using algebraic_int_times[of "y / x" x] by (auto simp: alg_dvd_def)

lemma alg_dvd_0_left_iff [simp]: "0 alg_dvd x ⟷ x = 0"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_0_right [iff]: "x alg_dvd 0"
  by (auto simp: alg_dvd_def)

lemma one_alg_dvd_iff [simp]: "1 alg_dvd x ⟷ algebraic_int x"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_of_int [intro]:
  assumes "x dvd y"
  shows   "of_int x alg_dvd of_int y"
proof (cases "of_int x = (0 :: 'a)")
  case False
  from assms obtain z where z: "y = x * z"
    by (elim dvdE)
  have "algebraic_int (of_int z)"
    by auto
  also have "of_int z = of_int y / (of_int x :: 'a)"
    using False by (simp add: z field_simps)
  finally show ?thesis
    using False by (simp add: alg_dvd_def)
qed (use assms in ‹auto simp: alg_dvd_def›)

lemma alg_dvd_of_nat [intro]:
  assumes "x dvd y"
  shows   "of_nat x alg_dvd of_nat y"
  using alg_dvd_of_int[of "int x" "int y"] assms by simp

lemma alg_dvd_of_int_iff [simp]:
  "(of_int x :: 'a :: field_char_0) alg_dvd of_int y ⟷ x dvd y"
proof
  assume "(of_int x :: 'a) alg_dvd of_int y"
  hence "of_int y / (of_int x :: 'a) ∈ ℤ" and nz: "of_int x = (0::'a) ⟶ of_int y = (0::'a)"
    by (auto simp: alg_dvd_def dest!: rational_algebraic_int_is_int)
  then obtain n where "of_int y / of_int x = (of_int n :: 'a)"
    by (elim Ints_cases)
  hence "of_int y = (of_int (x * n) :: 'a)"
    unfolding of_int_mult using nz by (auto simp: field_simps)
  hence "y = x * n"
    by (subst (asm) of_int_eq_iff)
  thus "x dvd y"
    by auto
qed blast

lemma alg_dvd_of_nat_iff [simp]:
  "(of_nat x :: 'a :: field_char_0) alg_dvd of_nat y ⟷ x dvd y"
proof -
  have "(of_int (int x) :: 'a) alg_dvd of_int (int y) ⟷ x dvd y"
    by (subst alg_dvd_of_int_iff) auto
  thus ?thesis unfolding of_int_of_nat_eq .
qed

lemma alg_dvd_add [intro]:
  fixes x y z :: "'a :: field_char_0"
  shows "x alg_dvd y ⟹ x alg_dvd z ⟹ x alg_dvd (y + z)"
  unfolding alg_dvd_def by (auto simp: add_divide_distrib)

lemma alg_dvd_uminus_right [intro]: "x alg_dvd y ⟹ x alg_dvd -y"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_uminus_right_iff [simp]: "x alg_dvd -y ⟷ x alg_dvd y"
  using alg_dvd_uminus_right[of x y] alg_dvd_uminus_right[of x "-y"] by auto

lemma alg_dvd_diff [intro]:
  fixes x y z :: "'a :: field_char_0"
  shows "x alg_dvd y ⟹ x alg_dvd z ⟹ x alg_dvd (y - z)"
  unfolding alg_dvd_def by (auto simp: diff_divide_distrib)

lemma alg_dvd_triv_left [intro]: "algebraic_int y ⟹ x alg_dvd x * y"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_triv_right [intro]: "algebraic_int x ⟹ y alg_dvd x * y"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_triv_left_iff: "x alg_dvd x * y ⟷ x = 0 ∨ algebraic_int y"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_triv_right_iff: "y alg_dvd x * y ⟷ y = 0 ∨ algebraic_int x"
  by (auto simp: alg_dvd_def)

lemma alg_dvd_triv_left_iff' [simp]: "x ≠ 0 ⟹ x alg_dvd x * y ⟷ algebraic_int y"
  by (simp add: alg_dvd_triv_left_iff)

lemma alg_dvd_triv_right_iff' [simp]: "y ≠ 0 ⟹ y alg_dvd x * y ⟷ algebraic_int x"
  by (simp add: alg_dvd_triv_right_iff)

lemma alg_dvd_trans [trans]:
  fixes x y z :: "'a :: field_char_0"
  shows "x alg_dvd y ⟹ y alg_dvd z ⟹ x alg_dvd z"
  using algebraic_int_times[of "y / x" "z / y"] by (auto simp: alg_dvd_def)

lemma alg_dvd_mono [simp]: 
  fixes a b c d :: "'a :: field_char_0"
  shows "a alg_dvd c ⟹ b alg_dvd d ⟹ (a * b) alg_dvd (c * d)"
  using algebraic_int_times[of "c / a" "d / b"] by (auto simp: alg_dvd_def)

lemma alg_dvd_mult [simp]: 
  fixes a b c :: "'a :: field_char_0"
  shows "a alg_dvd c ⟹ algebraic_int b ⟹ a alg_dvd (b * c)"
  using alg_dvd_mono[of a c 1 b] by (auto simp: mult.commute)

lemma alg_dvd_mult2 [simp]:
  fixes a b c :: "'a :: field_char_0"
  shows "a alg_dvd b ⟹ algebraic_int c ⟹ a alg_dvd (b * c)"
  using alg_dvd_mult[of a b c] by (simp add: mult.commute)

text ‹
  A crucial theorem: if an integer ‹x› divides a rational number ‹y›, then ‹y› is in fact
  also an integer, and that integer is a multiple of ‹x›.
›
lemma alg_dvd_int_rat:
  fixes y :: "'a :: field_char_0"
  assumes "of_int x alg_dvd y" and "y ∈ ℚ"
  shows   "∃n. y = of_int n ∧ x dvd n"
proof (cases "x = 0")
  case False
  have "y / of_int x ∈ ℤ"
    by (intro rational_algebraic_int_is_int) (use assms in ‹auto simp: alg_dvd_def›)
  then obtain n where n: "of_int n = y / (of_int x :: 'a)"
    by (elim Ints_cases) auto
  hence "y = of_int (n * x)"
    using False by (simp add: field_simps)
  thus ?thesis by (intro exI[of _ "x * n"]) auto
qed (use assms in auto)

lemma prod_alg_dvd_prod:
  fixes f :: "'a ⇒ 'b :: field_char_0"
  assumes "⋀x. x ∈ A ⟹ f x alg_dvd g x"
  shows   "prod f A alg_dvd prod g A"
  using assms by (induction A rule: infinite_finite_induct) auto

lemma alg_dvd_sum:
  fixes f :: "'a ⇒ 'b :: field_char_0"
  assumes "⋀x. x ∈ A ⟹ y alg_dvd f x"
  shows   "y alg_dvd sum f A"
  using assms by (induction A rule: infinite_finite_induct) auto

lemma not_alg_dvd_sum:
  fixes f :: "'a ⇒ 'b :: field_char_0"
  assumes "⋀x. x ∈ A-{x'} ⟹ y alg_dvd f x"
  assumes "¬y alg_dvd f x'"
  assumes "x' ∈ A" "finite A"
  shows   "¬y alg_dvd sum f A"
proof
  assume *: "y alg_dvd sum f A"
  have "y alg_dvd sum f A - sum f (A - {x'})"
    using ‹x' ∈ A› by (intro alg_dvd_diff[OF * alg_dvd_sum] assms) auto
  also have "… = sum f (A - (A - {x'}))"
    using assms by (subst sum_diff) auto
  also have "A - (A - {x'}) = {x'}"
    using assms by auto
  finally show False using assms by simp
qed

lemma fact_dvd_pochhammer:
  assumes "m ≤ n + 1"
  shows   "fact m dvd pochhammer (int n - int m + 1) m"
proof -
  have "(real n gchoose m) * fact m = of_int (pochhammer (int n - int m + 1) m)"
    by (simp add: gbinomial_pochhammer' pochhammer_of_int [symmetric])
  also have "(real n gchoose m) * fact m = of_int (int (n choose m) * fact m)"
    by (simp add: binomial_gbinomial)
  finally have "int (n choose m) * fact m = pochhammer (int n - int m + 1) m"
    by (subst (asm) of_int_eq_iff)
  from this [symmetric] show ?thesis by simp
qed

lemma coeff_higher_pderiv:
  "coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
  by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)

lemma fact_alg_dvd_poly_higher_pderiv:
  fixes p :: "'a :: field_char_0 poly"
  assumes "⋀i. algebraic_int (poly.coeff p i)" "algebraic_int x" "m ≤ k"
  shows   "fact m alg_dvd poly ((pderiv ^^ k) p) x"
  unfolding poly_altdef
proof (intro alg_dvd_sum, goal_cases)
  case (1 i)
  have "(of_int (fact m) :: 'a) alg_dvd (of_int (fact k))"
    by (intro alg_dvd_of_int fact_dvd assms)
  also have "(of_int (fact k) :: 'a) alg_dvd of_int (pochhammer (int i + 1) k)"
    using fact_dvd_pochhammer[of k "i + k"]
    by (intro alg_dvd_of_int fact_dvd_pochhammer) (auto simp: algebra_simps)
  finally have "fact m alg_dvd (pochhammer (of_nat i + 1) k :: 'a)"
    by (simp flip: pochhammer_of_int)
  also have "… alg_dvd pochhammer (of_nat i + 1) k * poly.coeff p (i + k)"
    by (rule alg_dvd_triv_left) (rule assms)
  also have "… = poly.coeff ((pderiv ^^ k) p) i"
    unfolding coeff_higher_pderiv by (simp add: add_ac flip: pochhammer_of_int)
  also have "… alg_dvd poly.coeff ((pderiv ^^ k) p) i * x ^ i"
    by (intro alg_dvd_triv_left algebraic_int_power assms)
  finally show ?case .
qed

end