theory Divisors
  imports "HOL-Number_Theory.Number_Theory" "HOL-Library.Set_Algebras"
begin

definition divisors :: "'a :: normalization_semidom \<Rightarrow> 'a set" where
  "divisors x = {y. normalize y = y \<and> y dvd x}"

lemma divisors_0_nat [simp]: "divisors (0 :: nat) = UNIV"
  by (auto simp: divisors_def)

lemma divisors_1 [simp]: "divisors 1 = {1}"
  by (auto simp: divisors_def is_unit_normalize)

lemma dvd_irreducibleD:
  assumes "irreducible x" "y dvd x"
  shows   "y dvd 1 \<or> x dvd y"
  using assms
proof -
  from assms(2) obtain z where [simp]: "x = y * z"
    by auto
  with assms(1) have "y dvd 1 \<or> z dvd 1"
    by (auto simp: irreducible_def)
  thus ?thesis
    using mult_dvd_mono[of y y z 1] by auto
qed

lemma divisors_prime:
  assumes "prime p"
  shows   "divisors p = {1, p}"
proof -
  have "x \<in> {1, p}" if "x \<in> divisors p" for x
  proof -
    from assms have "irreducible p"
      using prime_elem_imp_irreducible by blast
    moreover from that have "x dvd p"
      by (auto simp: divisors_def)
    ultimately have "is_unit x \<or> normalize x = normalize p"
      using dvd_irreducibleD[of p x] by (auto simp: associated_iff_dvd)
    with assms and that show "x \<in> {1, p}"
      by (auto simp: divisors_def is_unit_normalize)
  qed
  thus ?thesis
    using assms by (auto simp: divisors_def)
qed

lemma divisors_prime_power:
  fixes p :: "'a :: factorial_semiring"
  assumes "prime p"
  shows   "divisors (p ^ n) = (\<lambda>i. normalize (p ^ i)) ` {..n}"
proof safe
  fix x assume "x \<in> divisors (p ^ n)"
  hence [simp]: "normalize x = x" and "x dvd p ^ n"
    by (auto simp: divisors_def)
  with \<open>prime p\<close> obtain i where i: "i \<le> n" "normalize x = normalize (p ^ i)"
    using divides_primepow_weak by blast
  thus "x \<in> (\<lambda>i. normalize (p ^ i)) ` {..n}"
    by auto
qed (auto simp: divisors_def le_imp_power_dvd)

lemma normalize_in_divisors_iff: "normalize x \<in> divisors y \<longleftrightarrow> x dvd y"
  by (auto simp: divisors_def)

lemma divisors_mult_coprime:
  fixes a b :: "'a :: semiring_gcd"
  assumes "coprime a b"
  shows   "divisors (a * b) = normalize ` (divisors a * divisors b)"
proof safe
  fix x assume "x \<in> divisors a * divisors b"
  thus "normalize x \<in> divisors (a * b)"
    by (auto simp: divisors_def set_times_def intro: mult_dvd_mono)
next
  fix x assume "x \<in> divisors (a * b)"
  hence "normalize x = x" and "x dvd a * b"
    by (auto simp: divisors_def)
  then obtain x1 x2 where x12: "x = x1 * x2" "x1 dvd a" "x2 dvd b"
    using division_decomp by blast
  from x12 have "normalize x1 * normalize x2 \<in> divisors a * divisors b"
    by (auto simp: normalize_in_divisors_iff)
  moreover have "normalize (normalize x1 * normalize x2) = x"
    by (auto simp: \<open>normalize x = x\<close> simp flip: \<open>x = x1 * x2\<close>)
  ultimately show "x \<in> normalize ` (divisors a * divisors b)"
    by blast
qed

lemma normalize_mult_normalize_right_set [simp]:
  "normalize ` (A * normalize ` B) = normalize ` (A * B)"
proof (intro equalityI subsetI)
  fix z assume "z \<in> normalize ` (A * normalize ` B)"
  then obtain x y where xy: "z = normalize (x * normalize y)" "x \<in> A" "y \<in> B"
    by (auto simp: set_times_def)
  thus "z \<in> normalize ` (A * B)"
    using xy by auto
next
  fix z assume "z \<in> normalize ` (A * B)"
  then obtain x y where xy: "z = normalize (x * y)" "x \<in> A" "y \<in> B"
    by (auto simp: set_times_def)
  from xy have "z = normalize (x * normalize y)"
    by auto
  thus "z \<in> normalize ` (A * normalize ` B)"
    using xy by blast
qed

lemma normalize_mult_normalize_left_set [simp]:
  "normalize ` (normalize ` A * B) = normalize ` (A * B)"
  using normalize_mult_normalize_right_set[of B A] by (simp add: mult_ac)

lemma divisors_prod_coprime:
  fixes f :: "'a \<Rightarrow> 'b :: semiring_gcd"
  assumes "pairwise (\<lambda>x y. coprime (f x) (f y)) A"
  shows   "divisors (prod f A) = normalize ` (\<Prod>x\<in>A. divisors (f x))"
  using assms
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  have "divisors (prod f (insert x A)) = divisors (f x * prod f A)"
    using insert.hyps by simp
  also have "coprime (f x) (prod f A)"
    using insert.prems insert.hyps by (auto simp: pairwise_def intro!: prod_coprime_right)
  hence "divisors (f x * prod f A) = normalize ` (divisors (f x) * divisors (prod f A))"
    using \<open>coprime (f x) (prod f A)\<close> by (subst divisors_mult_coprime) auto
  also have "divisors (prod f A) = normalize ` (\<Prod>x\<in>A. divisors (f x))"
    using insert.prems by (subst insert.IH) (auto simp: pairwise_insert)
  finally show ?case
    using insert.hyps by simp
qed auto

lemma divisors_normalize [simp]: "divisors (normalize x) = divisors x"
  by (auto simp: divisors_def)

lemma prod_prime_factors_weak:
  assumes "x \<noteq> 0"
  shows   "normalize (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x) = normalize x"
proof -
  have "normalize x = normalize (prod_mset (prime_factorization x))"
    by (simp add: prod_mset_prime_factorization_weak assms)
  also have "prod_mset (prime_factorization x) = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
    by (subst prod_mset_multiplicity) simp_all
  also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
    by (intro prod.cong)
      (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
  finally show ?thesis ..
qed

lemma normalize_prod_normalize [simp]:
  "normalize (\<Prod>x\<in>A. normalize (f x)) = normalize (\<Prod>x\<in>A. f x)"
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  have "normalize (\<Prod>x\<in>insert x A. normalize (f x)) =
          normalize (f x * normalize (\<Prod>x\<in>A. normalize (f x)))"
    using insert.hyps by auto
  also note insert.IH
  finally show ?case
    using insert.hyps by auto
qed auto

lemma normalize_prod_normalize_set [simp]:
  "normalize ` (\<Prod>x\<in>A. normalize ` f x) = normalize ` (\<Prod>x\<in>A. f x)"
proof (induction A rule: infinite_finite_induct)
  case (insert x A)
  have "normalize ` (\<Prod>x\<in>insert x A. normalize ` (f x)) =
          normalize ` (f x * normalize ` (\<Prod>x\<in>A. normalize ` (f x)))"
    using insert.hyps by auto
  also note insert.IH
  finally show ?case
    using insert.hyps by auto
qed auto

lemma divisors_conv_prime_factorization:
  fixes x :: "'a :: factorial_semiring_gcd"
  assumes "x \<noteq> 0"
  shows   "divisors x = normalize ` (\<Prod>p\<in>prime_factors x. (\<lambda>i. p ^ i) ` {..multiplicity p x})"
proof -
  have "divisors x = divisors (normalize x)"
    by simp
  also have "normalize x = normalize ((\<Prod>p\<in>prime_factors x. p ^ multiplicity p x))"
    by (rule prod_prime_factors_weak [symmetric]) fact+
  also have "divisors \<dots> = divisors (\<Prod>p\<in>prime_factors x. p ^ multiplicity p x)"
    by simp
  also have "\<dots> = normalize ` (\<Prod>p\<in>prime_factors x. divisors (p ^ multiplicity p x))"
    by (intro divisors_prod_coprime) (auto simp: pairwise_def in_prime_factors_iff primes_coprime)
  also have "(\<Prod>p\<in>prime_factors x. divisors (p ^ multiplicity p x)) =
             (\<Prod>p\<in>prime_factors x. (\<lambda>i. normalize (p ^ i)) ` {..multiplicity p x})"
    by (intro prod.cong divisors_prime_power) auto
  also have "\<dots> = (\<Prod>p\<in>prime_factors x. normalize ` (\<lambda>i. p ^ i) ` {..multiplicity p x})"
    by (simp add: image_image)
  also have "normalize ` \<dots> = normalize ` (\<Prod>p\<in>prime_factors x. (\<lambda>i. p ^ i) ` {..multiplicity p x})"
    by simp
  finally show ?thesis .
qed

lemma divisors_conv_prime_factorization':
  fixes x :: "'a :: factorial_semiring_gcd"
  assumes "prime_factorization x = P"
  assumes "x \<noteq> 0"
  shows   "divisors x = normalize ` (\<Prod>p\<in>set_mset P. (\<lambda>i. p ^ i) ` {..count P p})"
proof -
  note [simp] = assms(1) [symmetric]
  have "(\<Prod>p\<in>set_mset P. (\<lambda>i. p ^ i) ` {..count P p}) =
        (\<Prod>p\<in>prime_factors x. (\<lambda>i. p ^ i) ` {..multiplicity p x})"
    by (intro prod.cong) (auto simp: count_prime_factorization)
  thus ?thesis using assms(2)
    by (subst divisors_conv_prime_factorization) simp_all
qed

lemma "divisors (80389990399 :: nat) =
          {1, 101, 199, 10201, 20099, 39601, 2029999, 3999701, 7880599, 403969801, 
           795940499, 80389990399}"
proof -
  have "prime (101 :: nat)" and "prime (199 :: nat)"
    by simp_all
  hence *: "prime_factorization 80389990399 = {#101, 101, 199, 199, 199::nat#}"
    by (intro prime_factorization_eqI_strong) (auto simp del: prime_nat_numeral_eq)
  show ?thesis
    by (subst divisors_conv_prime_factorization'[OF *])
       (simp_all add: set_times_image atMost_Suc insert_commute)
qed

end