CommRing.thy

theory CommRing
imports Main
begin

no_notation plus (infixl "+" 65)
no_notation minus (infixl "-" 65)
no_notation times (infixl "*" 70)
no_notation zero_class.zero ("0")
no_notation one_class.one ("1")

locale Monoid =
  fixes carrier and mult (infixl "⋆" 70) and one ("1")
  assumes mult_closed [intro, simp]: "⟦ x ∈ carrier; y ∈ carrier ⟧ ⟹ x ⋆ y ∈ carrier"
  and     one_closed [intro, simp]: "1 ∈ carrier"
  assumes assoc: "⟦ x ∈ carrier; y ∈ carrier; z ∈ carrier ⟧ ⟹ (x ⋆ y) ⋆ z = x ⋆ (y ⋆ z)"
  and     one_r [simp]: "x ∈ carrier ⟹ x ⋆ 1 = x"
  and     one_l [simp]: "x ∈ carrier ⟹ 1 ⋆ x = x"

locale closed =
  fixes carrier and mult (infixl "⋆" 70) and one ("1") and inv
  assumes mult_closed [intro]: "⟦ x ∈ carrier; y ∈ carrier ⟧ ⟹ x ⋆ y ∈ carrier"
  and     one_closed [intro]: "1 ∈ carrier"
  and     inv_closed [intro]: "x ∈ carrier ⟹ inv x ∈ carrier"

locale Group = closed +
  assumes assoc: "⟦ x ∈ carrier; y ∈ carrier; z ∈ carrier ⟧ ⟹ (x ⋆ y) ⋆ z = x ⋆ (y ⋆ z)"
  and     one_r [simp]: "x ∈ carrier ⟹ x ⋆ 1 = x"
  and     one_l [simp]: "x ∈ carrier ⟹ 1 ⋆ x = x"
  and     inv_r [simp]: "x ∈ carrier ⟹ x ⋆ inv x = 1"
  and     inv_l [simp]: "x ∈ carrier ⟹ inv x ⋆ x = 1"

locale AbelianGroup = Group +
  assumes mult_comm: "⟦ x ∈ carrier; y ∈ carrier ⟧ ⟹ x ⋆ y = y ⋆ x"

context Group begin
  definition subgroup where
    "subgroup H ≡ H ⊆ carrier ∧ closed H (op ⋆) 1 inv"

  lemma inv_inv_id [simp]:
    shows "x ∈ carrier ⟹ inv (inv x) = x"
  proof-
    fix x
    assume x_in: "x ∈ carrier"
    hence inv_x_in: "inv x ∈ carrier" by auto
    hence inv_inv_x_in: "inv (inv x) ∈ carrier" by auto
  
    have "inv (inv x) = 1 ⋆ inv (inv x)" using inv_inv_x_in by auto
    also have "… = x ⋆ inv x ⋆ inv (inv x)" using x_in by simp
    also have "… = x ⋆ (inv x ⋆ inv (inv x))" using x_in inv_x_in inv_inv_x_in by (rule_tac assoc)
    also have "… = x" using x_in and inv_x_in by simp
    finally
      show "inv (inv x) = x" by simp
  qed

  lemma inv_uniqueness [simp]:
    shows "⟦ x ∈ carrier; y ∈ carrier ⟧ ⟹ x ⋆ y = 1 ⟹ y = inv x"
  proof-
    assume x_in: "x ∈ carrier" and y_in: "y ∈ carrier"
    hence invx_in: "inv x ∈ carrier" by auto
    assume "x ⋆ y = 1"

    have "y = (inv x ⋆ x) ⋆ y" using x_in and y_in by auto
    also have "… = inv x ⋆ (x ⋆ y)" using x_in and y_in and invx_in by (rule_tac assoc)
    also have "… = inv x ⋆ 1" using `x ⋆ y = 1` by simp
    also have "… = inv x" using invx_in by (rule_tac one_r)
    finally
      show "y = inv x" by auto
  qed

  lemma one_uniqueness [simp]:
    assumes "x ∈ carrier"
    shows "x ⋆ x = x ⟹ x = 1"
  proof-
    assume "x ⋆ x = x"
    have "x = (inv x ⋆ x) ⋆ x" using assms by auto
    also have "… = inv x ⋆ (x ⋆ x)" using assms and inv_closed by (rule_tac assoc)
    also have "… = inv x ⋆ x" using assms and `x ⋆ x = x` by auto
    also have "… = 1" using assms by auto
    finally show "x = 1" by simp
  qed
end

context AbelianGroup begin
  definition abelian_subgroup where
    "abelian_subgroup H ≡ H ⊆ carrier ∧ closed H (op ⋆) 1 inv"
end

locale SubGroup =
  fixes H
  fixes carrier and mult and one and inv
  assumes group [intro]: "Group carrier mult one inv"
  and     subset [simp]: "H ⊆ carrier"
  and     closed [intro]: "closed H mult one inv"

locale AbelianSubGroup =
  fixes H
  fixes carrier and mult and one and inv
  assumes abelian_group [intro]: "AbelianGroup carrier mult one inv"
  and     subset [simp]: "H ⊆ carrier"
  and     closed [intro]: "closed H mult one inv"

lemma (in Group) group_subgroup:
  shows "SubGroup carrier carrier mult one inv"
proof
  show "carrier ⊆ carrier" by auto
qed

lemma (in Group) trivial_group:
  shows "Group {1} (op ⋆) 1 inv"
unfolding Group_def
proof auto
  show "closed {1} (op ⋆) 1 inv"
    unfolding closed_def
  proof auto
    show "1 ⋆ 1 = 1" using one_closed by auto
    have "inv 1 = inv 1 ⋆ 1" using one_closed and inv_closed by simp
    also have "… = 1" using one_closed and inv_closed by (rule_tac inv_l)
    finally show "inv 1 = 1" by simp
  qed
  show "Group_axioms {1} op ⋆ 1 inv"
    unfolding Group_axioms_def
    by (auto simp add: one_closed)
qed

locale Ring =
  fixes carrier
  fixes add (infixl "+" 65) and zero ("0") and negative
  fixes mult (infixl "*" 70) and one ("1")
  assumes add_abelian [intro]: "AbelianGroup carrier add zero negative"
  and     mult_monoid [intro]: "Monoid carrier mult one"
  and     distributive_r [simp]: "⟦ x ∈ carrier; y ∈ carrier; z ∈ carrier ⟧ ⟹ x * (y + z) = (x * y) + (x * z)"
  and     distributive_l [simp]: "⟦ x ∈ carrier; y ∈ carrier; z ∈ carrier ⟧ ⟹ (y + z) * x = (y * x) + (z * x)"
  and     mult_comm [simp]: "⟦ x ∈ carrier; y ∈ carrier ⟧ ⟹ x * y = y * x"

context Ring
begin
lemma add_abelian_group [simp]: "Group carrier add zero negative"
  using add_abelian unfolding AbelianGroup_def by auto
lemma add_abelian_closed [simp]: "closed carrier add zero negative" 
  using add_abelian unfolding AbelianGroup_def Group_def by auto

lemma zero_l:
  assumes "x ∈ carrier"
  shows "0 * x = 0"
proof-
  have "0 ∈ carrier" using add_abelian_closed unfolding closed_def by auto
  then have "0 + 0 = 0" using add_abelian_group unfolding Group_def Group_axioms_def by auto
  have "0 * x ∈ carrier" using mult_monoid and `0 ∈ carrier` and `x ∈ carrier`
    by (rule_tac Monoid.mult_closed)

  have "0 * x + 0 * x = (0 + 0) * x"
    using assms and add_abelian unfolding AbelianGroup_def Group_def closed_def by auto
  also have "… = 0 * x"
    using add_abelian and `0 + 0 = 0` unfolding AbelianGroup_def Group_def by auto
  finally have "0 * x + 0 * x = 0 * x" by simp
  thus "0 * x = 0" using `0 * x ∈ carrier` and add_abelian_group
    by (rule_tac Group.one_uniqueness)
qed

lemma zero_r:
  assumes "x ∈ carrier"
  shows "x * 0 = 0"
proof-
  have "0 ∈ carrier" using add_abelian_closed unfolding closed_def by auto
  then have "0 + 0 = 0" using add_abelian_group unfolding Group_def Group_axioms_def by auto
  have "x * 0 ∈ carrier" using mult_monoid and `0 ∈ carrier` and `x ∈ carrier`
    by (rule_tac Monoid.mult_closed)

  have "x * 0 + x * 0 = x * (0 + 0)"
    using assms and add_abelian unfolding AbelianGroup_def Group_def closed_def by auto
  also have "… = x * 0"
    using add_abelian and `0 + 0 = 0` unfolding AbelianGroup_def Group_def by auto
  finally have "x * 0 + x * 0 = x * 0" by simp
  thus "x * 0 = 0" using `x * 0 ∈ carrier` and add_abelian_group
    by (rule_tac Group.one_uniqueness)
qed

definition minus (infixl "-" 65) where
  "minus x y ≡ x + (negative y)"

lemma negative_closed [simp]:
  shows "x ∈ carrier ⟹ negative x ∈ carrier"
proof-
  assume "x ∈ carrier" with add_abelian
  show "negative x ∈ carrier"
    using add_abelian_closed
    by (rule_tac closed.inv_closed)
qed

lemma negative_minus [simp]:
  shows "x ∈ carrier ⟹ negative x = 0 - x"
unfolding minus_def
proof-
  assume "x ∈ carrier"
  from this show "negative x = 0 + negative x"
    using add_abelian_group and negative_closed
    unfolding Group_def Group_axioms_def
    by auto
qed

lemma mult_negative [simp]:
  shows "⟦ x ∈ carrier; z ∈ carrier ⟧ ⟹ x * (negative z) = negative (x * z)"
proof-
  assume x_in: "x ∈ carrier" and z_in: "z ∈ carrier"
  from x_in z_in have xz_in: "x * z ∈ carrier" using mult_monoid unfolding Monoid_def by simp
  from z_in have nz_in: "negative z ∈ carrier" by (rule_tac negative_closed)
  from x_in and nz_in have xnz_in: "x * negative z ∈ carrier"
    using mult_monoid by (rule_tac Monoid.mult_closed)
  from x_in z_in have nxz_in: "negative (x * z) ∈ carrier"
    proof (rule_tac negative_closed)
      from x_in z_in show "x * z ∈ carrier" using mult_monoid by (rule_tac Monoid.mult_closed)
    qed

  have "x * z + x * (negative z) = x * (z + negative z)"
    using x_in z_in nz_in by (rule_tac distributive_r [symmetric])
  also have "… = x * 0"
    using z_in nz_in add_abelian unfolding AbelianGroup_def Group_def Group_axioms_def by auto
  also have "… = 0"
    using x_in by (rule_tac zero_r)
  finally
    have "(x * z) + x * (negative z) = 0" by simp
  thus "x * (negative z) = negative (x * z)"
    using add_abelian_group and xz_in and nxz_in and xnz_in
    by (rule_tac Group.inv_uniqueness)
qed

end

locale Ideal =
  fixes I
  fixes carrier and add (infixl "+" 65) and zero ("0") and negative
  fixes mult (infixl "*" 70) and one ("1")
  assumes ring: "Ring carrier add zero negative mult one"
  and     subgroup: "AbelianSubGroup I carrier add zero negative"
  and     mult_closed: "⟦ x ∈ I; a ∈ carrier ⟧ ⟹ a * x ∈ I"

definition (in Ring) GenIdeal where
  "GenIdeal a = {a * x| x. x ∈ carrier}"

lemma (in Ring) genideal_ideal:
  assumes "a ∈ carrier"
  shows "Ideal (GenIdeal a) carrier add 0 negative mult 1"
unfolding Ideal_def Ring_def GenIdeal_def AbelianSubGroup_def
proof auto
  fix xa
  assume "xa ∈ carrier"
  from `a ∈ carrier` and `xa ∈ carrier` and mult_monoid show "a * xa ∈ carrier"
    by (rule_tac Monoid.mult_closed)
next
  show "closed {a * x |x. x ∈ carrier} add 0 negative"
  unfolding closed_def
  proof auto
    fix xa xb
    assume xa_in: "xa ∈ carrier" and xb_in: "xb ∈ carrier"
    with `a ∈ carrier` have 1: "a * xa + a * xb = a * (xa + xb)" by auto
    from xa_in and xb_in and add_abelian have 2: "(xa + xb) ∈ carrier"
      unfolding AbelianGroup_def and Group_def and closed_def
      by auto
    from 1 and 2 have "a * xa + a * xb = a * (xa + xb)" and "(xa + xb) ∈ carrier" by auto
    thus "∃x. a * xa + a * xb = a * x ∧ x ∈ carrier" by auto
  next
    have "0 ∈ carrier" using add_abelian
      unfolding AbelianGroup_def and Group_def and closed_def
      by auto
    moreover have "0 = a * 0" using `a ∈ carrier`
      by (rule_tac zero_r [symmetric])
    ultimately
      show "∃x. 0 = a * x ∧ x ∈ carrier" by auto
  next
    fix xa assume "xa ∈ carrier"
    have "negative (a * xa) = a * (negative xa)"
      using `a ∈ carrier` and `xa ∈ carrier`
      by (rule_tac mult_negative [symmetric])
    moreover have "negative xa ∈ carrier"
      using add_abelian_closed and `xa ∈ carrier`
      by (rule_tac negative_closed)
    ultimately
      show "∃x. negative (a * xa) = a * x ∧ x ∈ carrier" by auto
  qed
next
  fix xa aa
  assume xa_in: "xa ∈ carrier" and aa_in: "aa ∈ carrier"
  have "aa * (a * xa) = aa * a * xa"
    using mult_monoid using xa_in aa_in and `a ∈ carrier` by (rule_tac Monoid.assoc [symmetric])
  also have "… = a * aa * xa" using aa_in and `a ∈ carrier` and xa_in by auto
  also have "… = a * (aa * xa)"
    using mult_monoid using xa_in aa_in and `a ∈ carrier` by (rule_tac Monoid.assoc)
  finally have "aa * (a * xa) = a * (aa * xa)" by simp
  moreover have "aa * xa ∈ carrier" using mult_monoid and xa_in aa_in by (rule_tac Monoid.mult_closed)
  ultimately
    show "∃x. aa * (a * xa) = a * x ∧ x ∈ carrier" by auto
qed

definition (in Ring) Unit where
  "Unit = {x | x. x ∈ carrier & (∃ y ∈ carrier. x * y = 1)}"

lemma (in Ring) one_in_ideal:
  assumes idealI: "Ideal I carrier add 0 negative mult 1" and "1 ∈ I"
  shows "I = carrier"
proof auto
  fix x
  assume "x ∈ I"
  with this and idealI show "x ∈ carrier"
    unfolding Ideal_def and AbelianSubGroup_def
    by auto
next
  fix x
  assume "x ∈ carrier"
  with this and `1 ∈ I` and idealI
  have "x * 1 ∈ I" unfolding Ideal_def by auto
  show "x ∈ I"
  proof-
    from `x ∈ carrier`
    have "x = x * 1" using mult_monoid unfolding Monoid_def by auto
    with `x * 1 ∈ I` show "x ∈ I" by auto
  qed
qed

lemma (in Ring) unit_iff:
  assumes "a ∈ carrier"
  shows "a ∈ Unit ⟷ carrier = GenIdeal a"
proof
  assume "a ∈ Unit"
  then obtain b where "b ∈ carrier" and "a * b = 1"
    unfolding Unit_def by auto
  then have "a * b ∈ GenIdeal a"
    unfolding GenIdeal_def
    by auto
  with `b ∈ carrier` and `a * b = 1` have "1 ∈ GenIdeal a"
    by auto
  from this and `a ∈ carrier`
  have "GenIdeal a = carrier"
    by (auto simp add: genideal_ideal one_in_ideal)
  thus "carrier = GenIdeal a" by auto
next
  assume 1: "carrier = GenIdeal a"
  have "1 ∈ carrier" using mult_monoid by (rule_tac Monoid.one_closed)
  then have "1 ∈ GenIdeal a" using 1 by simp
  then have "∃b. b ∈ carrier & a * b = 1" unfolding GenIdeal_def by auto
  then show "a ∈ Unit" unfolding Unit_def using `a ∈ carrier` by auto
qed

definition (in Ring) Ideals where
  "Ideals = {I | I. Ideal I carrier op + 0 negative op * 1}"

locale Domain = Ring +
  assumes zero_divisor [simp]: "⟦ a ∈ carrier; b ∈ carrier; a * b = 0 ⟧ ⟹ a = 0 ∨ b = 0"

locale Field = Domain +
  assumes all_unit [intro]: "⟦ a ∈ carrier; a ≠ 0 ⟧ ⟹ a ∈ Unit"

(*
lemma (in Field) field_ideal:
  assumes "Ideal I carrier op + 0 negative op * 1"
  shows "Ideals = {{0}, carrier}" (is "_ = ?P")
proof
  show "Ideals ⊆ {{0}, carrier}"
  proof
    fix x assume "x ∈ Ideals"
    then have idealx: "Ideal x carrier op + 0 negative op * 1"
      unfolding Ideals_def by auto
    show "x ∈ {{0}, carrier}"
    proof (cases "x = {0}")
      case True
        have "{0} ∈ ?P" by simp
        thus "x ∈ ?P" using `x = {0}` by simp
      case False
        show "(x ≠ {0}) ⟹ x ∈ ?P" oops
*)

locale maximalIdeal = Ideal +
  assumes maximal [intro]: "Ideal J carrier op + 0 negative op * 1 ⟹ J ⊆ I"