Theory Generated_Rings

(* ************************************************************************** *)
(* Title:      Generated_Rings.thy                                            *)
(* Author:     Martin Baillon                                                 *)
(* ************************************************************************** *)

theory Generated_Rings
  imports Subrings
begin

sectionβ€ΉGenerated Ringsβ€Ί

inductive_set
  generate_ring :: "('a, 'b) ring_scheme β‡’ 'a set β‡’ 'a set"
  for R and H where
    one:   "πŸ­β‡˜R⇙ ∈ generate_ring R H"
  | incl:  "h ∈ H ⟹ h ∈ generate_ring R H"
  | a_inv: "h ∈ generate_ring R H ⟹ βŠ–β‡˜R⇙ h ∈ generate_ring R H"
  | eng_add : "⟦ h1 ∈ generate_ring R H; h2 ∈ generate_ring R H ⟧ ⟹ h1 βŠ•β‡˜R⇙ h2 ∈ generate_ring R H"
  | eng_mult: "⟦ h1 ∈ generate_ring R H; h2 ∈ generate_ring R H ⟧ ⟹ h1 βŠ—β‡˜R⇙ h2 ∈ generate_ring R H"

subsectionβ€ΉBasic Properties of Generated Rings - First Partβ€Ί

lemma (in ring) generate_ring_in_carrier:
  assumes "H βŠ† carrier R"
  shows "h ∈ generate_ring R H ⟹ h ∈ carrier R"
  apply (induction rule: generate_ring.induct) using assms 
  by blast+

lemma (in ring) generate_ring_incl:
  assumes "H βŠ† carrier R"
  shows "generate_ring R H βŠ† carrier R"
  using generate_ring_in_carrier[OF assms] by auto

lemma (in ring) zero_in_generate: "πŸ¬β‡˜R⇙ ∈ generate_ring R H"
  using one a_inv by (metis generate_ring.eng_add one_closed r_neg)

lemma (in ring) generate_ring_is_subring:
  assumes "H βŠ† carrier R"
  shows "subring (generate_ring R H) R"
  by (auto intro!: subringI[of "generate_ring R H"]
         simp add: generate_ring_in_carrier[OF assms] one a_inv eng_mult eng_add)

lemma (in ring) generate_ring_is_ring:
  assumes "H βŠ† carrier R"
  shows "ring (R ⦇ carrier := generate_ring R H ⦈)"
  using subring_iff[OF generate_ring_incl[OF assms]] generate_ring_is_subring[OF assms] by simp

lemma (in ring) generate_ring_min_subring1:
  assumes "H βŠ† carrier R" and "subring E R" "H βŠ† E"
  shows "generate_ring R H βŠ† E"
proof
  fix h assume h: "h ∈ generate_ring R H"
  show "h ∈ E"
    using h and assms(3)
      by (induct rule: generate_ring.induct)
         (auto simp add: subringE(3,5-7)[OF assms(2)])
qed

lemma (in ring) generate_ringI:
  assumes "H βŠ† carrier R"
    and "subring E R" "H βŠ† E"
    and "β‹€K. ⟦ subring K R; H βŠ† K ⟧ ⟹ E βŠ† K"
  shows "E = generate_ring R H"
proof
  show "E βŠ† generate_ring R H"
    using assms generate_ring_is_subring generate_ring.incl by (metis subset_iff)
  show "generate_ring R H βŠ† E"
    using generate_ring_min_subring1[OF assms(1-3)] by simp
qed

lemma (in ring) generate_ringE:
  assumes "H βŠ† carrier R" and "E = generate_ring R H"
  shows "subring E R" and "H βŠ† E" and "β‹€K. ⟦ subring K R; H βŠ† K ⟧ ⟹ E βŠ† K"
proof -
  show "subring E R" using assms generate_ring_is_subring by simp
  show "H βŠ† E" using assms(2) by (simp add: generate_ring.incl subsetI)
  show "β‹€K. subring K R  ⟹ H βŠ† K ⟹ E βŠ† K"
    using assms generate_ring_min_subring1 by auto
qed

lemma (in ring) generate_ring_min_subring2:
  assumes "H βŠ† carrier R"
  shows "generate_ring R H = β‹‚{K. subring K R ∧ H βŠ† K}"
proof
  have "subring (generate_ring R H) R ∧ H βŠ† generate_ring R H"
    by (simp add: assms generate_ringE(2) generate_ring_is_subring)
  thus "β‹‚{K. subring K R ∧ H βŠ† K} βŠ† generate_ring R H" by blast
next
  have "β‹€K. subring K R ∧ H βŠ† K ⟹ generate_ring R H βŠ† K"
    by (simp add: assms generate_ring_min_subring1)
  thus "generate_ring R H βŠ† β‹‚{K. subring K R ∧ H βŠ† K}" by blast
qed

lemma (in ring) mono_generate_ring:
  assumes "I βŠ† J" and "J βŠ† carrier R"
  shows "generate_ring R I βŠ† generate_ring R J"
proof-
  have "I βŠ† generate_ring R J "
    using assms generate_ringE(2) by blast
  thus "generate_ring R I βŠ† generate_ring R J"
    using generate_ring_min_subring1[of I "generate_ring R J"] assms generate_ring_is_subring[OF assms(2)]
    by blast
qed

lemma (in ring) subring_gen_incl :
  assumes "subring H R"
    and  "subring K R"
    and "I βŠ† H"
    and "I βŠ† K"
  shows "generate_ring (R⦇carrier := K⦈) I βŠ† generate_ring (R⦇carrier := H⦈) I"
proof
  have incl_HK: "generate_ring (R ⦇ carrier := J ⦈) I βŠ† J" if J_def : "subring J R" "I βŠ† J" for J
    using ring.mono_generate_ring[of "(R⦇carrier := J⦈)" I J ] subring_is_ring[OF J_def(1)]
      ring.generate_ring_in_carrier[of "R⦇carrier := J⦈"]  ring_axioms J_def(2)
    by auto

  fix x
  have "x ∈ generate_ring (R⦇carrier := K⦈) I ⟹ x ∈ generate_ring (R⦇carrier := H⦈) I" 
  proof (induction  rule : generate_ring.induct)
    case one
    have "πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™ βŠ— πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™ = πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™" by simp
    moreover have "πŸ­β‡˜R⦇carrier := Hβ¦ˆβ‡™ βŠ— πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™ = πŸ­β‡˜R⦇carrier := Kβ¦ˆβ‡™" by simp
    ultimately show ?case using assms generate_ring.one by metis
  next
    case (incl h) thus ?case using generate_ring.incl by force
  next
    case (a_inv h)
    have "a_inv (R⦇carrier := K⦈) h = a_inv R h" 
      using assms group.m_inv_consistent[of "add_monoid R" K] a_comm_group incl_HK[of K] a_inv
      unfolding subring_def comm_group_def a_inv_def by auto
    moreover have "a_inv (R⦇carrier := H⦈) h = a_inv R h"
      using assms group.m_inv_consistent[of "add_monoid R" H] a_comm_group incl_HK[of H] a_inv
      unfolding subring_def comm_group_def a_inv_def by auto
    ultimately show ?case using generate_ring.a_inv a_inv.IH by fastforce
  next
    case (eng_add h1 h2)
    thus ?case using incl_HK assms generate_ring.eng_add by force
  next
    case (eng_mult h1 h2)
    thus ?case using generate_ring.eng_mult by force
  qed
  thus "x ∈ generate_ring (R⦇carrier := K⦈) I ⟹ x ∈ generate_ring (R⦇carrier := H⦈) I"
    by auto
qed

lemma (in ring) subring_gen_equality:
  assumes "subring H R" "K βŠ† H"
  shows "generate_ring R K = generate_ring (R ⦇ carrier := H ⦈) K"
  using subring_gen_incl[OF assms(1)carrier_is_subring assms(2)] assms subringE(1)
        subring_gen_incl[OF carrier_is_subring assms(1) _ assms(2)]
  by force

end