Theory Algebraic_Numbers.Min_Int_Poly

(*
  File:     Min_Int_Poly.thy
  Author:   Manuel Eberl, TU München
*)
section ‹The minimal polynomial of an algebraic number›
theory Min_Int_Poly
imports
  Algebraic_Numbers_Prelim
begin

text ‹
  Given an algebraic number ‹x› in a field, the minimal polynomial is the unique irreducible
  integer polynomial with positive leading coefficient that has ‹x› as a root.

  Note that we assume characteristic 0 since the material upon which all of this builds also
  assumes it.
›

definition min_int_poly :: "'a :: field_char_0 ⇒ int poly" where
  "min_int_poly x =
     (if algebraic x then THE p. p represents x ∧ irreducible p ∧ lead_coeff p > 0
      else [:0, 1:])"

lemma
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows min_int_poly_represents [intro]: "algebraic x ⟹ min_int_poly x represents x"
  and   min_int_poly_irreducible [intro]: "irreducible (min_int_poly x)"
  and   lead_coeff_min_int_poly_pos: "lead_coeff (min_int_poly x) > 0"
proof -
  note * = theI'[OF algebraic_imp_represents_unique, of x]
  show "min_int_poly x represents x" if "algebraic x"
    using *[OF that] by (simp add: that min_int_poly_def)
  have "irreducible [:0, 1::int:]"
    by (rule irreducible_linear_poly) auto
  thus "irreducible (min_int_poly x)"
    using * by (auto simp: min_int_poly_def)
  show "lead_coeff (min_int_poly x) > 0"
    using * by (auto simp: min_int_poly_def)
qed

lemma 
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows degree_min_int_poly_pos [intro]: "degree (min_int_poly x) > 0"
    and degree_min_int_poly_nonzero [simp]: "degree (min_int_poly x) ≠ 0"
proof -
  show "degree (min_int_poly x) > 0"
  proof (cases "algebraic x")
    case True
    hence "min_int_poly x represents x"
      by auto
    thus ?thesis by blast
  qed (auto simp: min_int_poly_def)
  thus "degree (min_int_poly x) ≠ 0"
    by blast
qed

lemma min_int_poly_primitive [intro]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "primitive (min_int_poly x)"
  by (rule irreducible_imp_primitive) auto

lemma min_int_poly_content [simp]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "content (min_int_poly x) = 1"
  using min_int_poly_primitive[of x] by (simp add: primitive_def)

lemma ipoly_min_int_poly [simp]: 
  "algebraic x ⟹ ipoly (min_int_poly x) (x :: 'a :: {field_gcd, field_char_0}) = 0"
  using min_int_poly_represents[of x] by (auto simp: represents_def)

lemma min_int_poly_nonzero [simp]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "min_int_poly x ≠ 0"
  using lead_coeff_min_int_poly_pos[of x] by auto

lemma min_int_poly_normalize [simp]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "normalize (min_int_poly x) = min_int_poly x"
  unfolding normalize_poly_def using lead_coeff_min_int_poly_pos[of x] by simp

lemma min_int_poly_prime_elem [intro]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "prime_elem (min_int_poly x)"
  using min_int_poly_irreducible[of x] by blast

lemma min_int_poly_prime [intro]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  shows "prime (min_int_poly x)"
  using min_int_poly_prime_elem[of x]
  by (simp only: prime_normalize_iff [symmetric] min_int_poly_normalize)

lemma min_int_poly_unique:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  assumes "p represents x" "irreducible p" "lead_coeff p > 0"
  shows "min_int_poly x = p"
proof -
  from assms(1) have x: "algebraic x"
    using algebraic_iff_represents by blast
  thus ?thesis
    using the1_equality[OF algebraic_imp_represents_unique[OF x], of p] assms
    unfolding min_int_poly_def by auto
qed

lemma min_int_poly_of_int [simp]:
  "min_int_poly (of_int n :: 'a :: {field_char_0, field_gcd}) = [:-of_int n, 1:]"
  by (intro min_int_poly_unique irreducible_linear_poly) auto

lemma min_int_poly_of_nat [simp]:
  "min_int_poly (of_nat n :: 'a :: {field_char_0, field_gcd}) = [:-of_nat n, 1:]"
  using min_int_poly_of_int[of "int n"] by (simp del: min_int_poly_of_int)

lemma min_int_poly_0 [simp]: "min_int_poly (0 :: 'a :: {field_char_0, field_gcd}) = [:0, 1:]"
  using min_int_poly_of_int[of 0] unfolding of_int_0 by simp

lemma min_int_poly_1 [simp]: "min_int_poly (1 :: 'a :: {field_char_0, field_gcd}) = [:-1, 1:]"
  using min_int_poly_of_int[of 1] unfolding of_int_1 by simp

lemma poly_min_int_poly_0_eq_0_iff [simp]:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  assumes "algebraic x"
  shows "poly (min_int_poly x) 0 = 0 ⟷ x = 0"
proof
  assume *: "poly (min_int_poly x) 0 = 0"
  show "x = 0"
  proof (rule ccontr)
    assume "x ≠ 0"
    hence "poly (min_int_poly x) 0 ≠ 0"
      using assms by (intro represents_irr_non_0) auto
    with * show False by contradiction
  qed
qed auto

lemma min_int_poly_eqI:
  fixes x :: "'a :: {field_char_0, field_gcd}"
  assumes "p represents x" "irreducible p" "lead_coeff p ≥ 0"
  shows   "min_int_poly x = p"
proof -
  from assms have [simp]: "p ≠ 0"
    by auto
  have "lead_coeff p ≠ 0"
    by auto
  with assms(3) have "lead_coeff p > 0"
    by linarith
  moreover have "algebraic x"
    using ‹p represents x› by (meson algebraic_iff_represents)
  ultimately show ?thesis
    unfolding min_int_poly_def
    using the1_equality[OF algebraic_imp_represents_unique[OF ‹algebraic x›], of p] assms by auto
qed

text ‹Implementation for real and rational numbers›

lemma min_int_poly_of_rat: "min_int_poly (of_rat r :: 'a :: {field_char_0, field_gcd}) = poly_rat r"
  by (intro min_int_poly_unique, auto)

definition min_int_poly_real :: "real ⇒ int poly" where
  [simp]: "min_int_poly_real = min_int_poly"

lemma min_int_poly_real_code_unfold [code_unfold]: "min_int_poly = min_int_poly_real"
  by simp

lemma min_int_poly_real_basic_impl[code]: "min_int_poly_real (real_of_rat x) = poly_rat x" 
  unfolding min_int_poly_real_def by (rule min_int_poly_of_rat)

lemma min_int_poly_rat_code_unfold [code_unfold]: "min_int_poly = poly_rat"
  by (intro ext, insert min_int_poly_of_rat[where ?'a = rat], auto)
 
end