Theory Prime_Generated

theory Prime_Generated
  imports "HOL-Computational_Algebra.Factorial_Ring"
begin

section ‹Prime-generated multiplicative sets›

text ‹
  This theory isolates the reusable combinatorial layer behind Nagata's
  factoriality theorem.  The full localization argument is developed in later
  theories; here we focus on the multiplicative sets generated by prime
  elements and on the closure lemmas that do not depend on any localization
  API.
›

definition avoids :: "'a :: comm_semiring_1 set ⇒ 'a ⇒ bool" where
  "avoids S p ⟷ (∀s∈S. ¬ p dvd s)"

definition prime_generated :: "'a :: comm_semiring_1 set ⇒ bool" where
  "prime_generated S ⟷
    (∀s∈S. ∃M. (∀q. q ∈# M ⟶ q ∈ S ∧ prime_elem q) ∧ prod_mset M = s)"

inductive_set mult_submonoid_closure :: "'a :: comm_monoid_mult set ⇒ 'a set" for A where
  one_closed: "1 ∈ mult_submonoid_closure A"
| generator: "a ∈ A ⟹ a ∈ mult_submonoid_closure A"
| mult_closed:
    "a ∈ mult_submonoid_closure A ⟹ b ∈ mult_submonoid_closure A ⟹
      a * b ∈ mult_submonoid_closure A"

definition powers_set :: "'a :: monoid_mult ⇒ 'a set" where
  "powers_set p = {x. ∃n. x = p ^ n}"

lemma prime_generatedI:
  assumes "⋀s. s ∈ S ⟹ ∃M. (∀q. q ∈# M ⟶ q ∈ S ∧ prime_elem q) ∧ prod_mset M = s"
  shows "prime_generated S"
  using assms unfolding prime_generated_def by blast

lemma prime_generatedE:
  assumes "prime_generated S" "s ∈ S"
  obtains M where "(∀q. q ∈# M ⟶ q ∈ S ∧ prime_elem q)" "prod_mset M = s"
  using assms unfolding prime_generated_def by blast

lemma prime_generated_powers_set:
  assumes "prime_elem p"
  shows "prime_generated (powers_set p)"
proof (rule prime_generatedI)
  fix s
  assume "s ∈ powers_set p"
  then obtain n where hs: "s = p ^ n"
    unfolding powers_set_def by blast
  have factors:
    "∀q. q ∈# replicate_mset n p ⟶ q ∈ powers_set p ∧ prime_elem q"
  proof
    fix q
    show "q ∈# replicate_mset n p ⟶ q ∈ powers_set p ∧ prime_elem q"
    proof (cases n)
      case 0
      then show ?thesis
        by simp
    next
      case (Suc m)
      show ?thesis
      proof
        assume "q ∈# replicate_mset n p"
        from ‹q ∈# replicate_mset n p› have "n > 0 ∧ q = p"
          by (simp only: in_replicate_mset)
        with Suc have q_eq: "q = p"
          by simp
        have q_in_powers: "q ∈ powers_set p"
          by (metis (mono_tags, lifting) mem_Collect_eq power_one_right powers_set_def q_eq)
        from q_eq assms have q_prime: "prime_elem q"
          by simp
        from q_in_powers q_prime show "q ∈ powers_set p ∧ prime_elem q"
          by blast
      qed
    qed
  qed
  show "∃M. (∀q. q ∈# M ⟶ q ∈ powers_set p ∧ prime_elem q) ∧ prod_mset M = s"
    by (rule exI[of _ "replicate_mset n p"]) (use factors hs in auto)
qed

lemma prime_generated_mult_submonoid_closure:
  assumes "⋀q. q ∈ A ⟹ prime_elem q"
  shows "prime_generated (mult_submonoid_closure A)"
proof (rule prime_generatedI)
  fix s
  assume "s ∈ mult_submonoid_closure A"
  then show
    "∃M. (∀q. q ∈# M ⟶ q ∈ mult_submonoid_closure A ∧ prime_elem q) ∧ prod_mset M = s"
  proof induction
    case one_closed
    show ?case
      by (rule exI[of _ "{#}"]) (auto intro: mult_submonoid_closure.one_closed)
  next
    case (generator a)
    show ?case
    proof (rule exI)
      from generator assms show
        "(∀q. q ∈# {#a#} ⟶ q ∈ mult_submonoid_closure A ∧ prime_elem q) ∧
          prod_mset {#a#} = a"
        by (auto intro: mult_submonoid_closure.generator)
    qed
  next
    case (mult_closed a b)
    show ?case
      by (metis mult_closed.IH Un_iff prod_mset_Un set_mset_union)
  qed
qed

lemma zero_notin_prime_generated:
  assumes "prime_generated S"
  shows "(0 :: 'a :: semidom) ∉ S"
  using assms prime_generated_def by force

end