Theory Distinguished_Quotients

(*  Title:       Computational p-Adics: Distinguished Quotients
    Author:      Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>, 2025
    Maintainer:  Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>
*)


theory Distinguished_Quotients

imports Main

begin

section ‹Distinguished Algebraic Quotients›

text ‹
  We define quotient groups and quotient rings modulo distinguished normal subgroups and ideals,
  respectively, leading to the construction of a field as a commutative ring with 1 modulo a
  maximal ideal.
›

class distinguished_subset =
  fixes distinguished_subset :: "'a set" ("𝒩")

hide_const distinguished_subset

subsection ‹Quotient groups›

subsubsection ‹Class definitions›

text ‹Here we set up subclasses of @{class group_add} with a distinguished subgroup.›

class group_add_with_distinguished_subgroup = group_add + distinguished_subset +
  assumes distset_nonempty: "𝒩 ≠ {}"
    and   distset_diff_closed:
    "g ∈ 𝒩 ⟹ h ∈ 𝒩 ⟹ g - h ∈ 𝒩"
begin

lemma distset_zero_closed : "0 ∈ 𝒩"
proof-
  from distset_nonempty obtain g::'a where "g ∈ 𝒩" by fast
  hence "g - g ∈ 𝒩" using distset_diff_closed by fast
  thus ?thesis by simp
qed

lemma distset_uminus_closed: "a ∈ 𝒩 ⟹ -a ∈ 𝒩"
  using distset_zero_closed distset_diff_closed by force

lemma distset_add_closed:
  "a ∈ 𝒩 ⟹  b ∈ 𝒩 ⟹ a + b ∈ 𝒩"
  using distset_uminus_closed[of b] distset_diff_closed[of a "-b"] by simp

lemma distset_uminus_plus_closed:
  "a ∈ 𝒩 ⟹ b ∈ 𝒩 ⟹ -a + b ∈ 𝒩"
  using distset_uminus_closed distset_add_closed by simp

lemma distset_lcoset_closed1:
  "a ∈ 𝒩 ⟹ -a + b ∈ 𝒩 ⟹ b ∈ 𝒩"
  using add.assoc[of a "-a" b] distset_add_closed by fastforce

lemma distset_lcoset_closed2:
  "b ∈ 𝒩 ⟹ -a + b ∈ 𝒩 ⟹ a ∈ 𝒩"
proof-
  assume ab: "b ∈ 𝒩" "-a + b ∈ 𝒩"
  from ab(2) obtain z where z: "z ∈ 𝒩" "-a + b = z" by fast
  from z(2) have "a = -(z - b)" using add.assoc[of "-a" b "-b"] by simp
  with ab(1) z(1) show "a ∈ 𝒩" using distset_diff_closed by simp
qed

lemma reflp_lcosetrel: "- x + x ∈ 𝒩"
  using distset_zero_closed by simp

lemma symp_lcosetrel: "- a + b ∈ 𝒩 ⟹ - b + a ∈ 𝒩"
  using distset_uminus_closed by (fastforce simp add: minus_add)

lemma transp_lcosetrel:
  "-x + z ∈ 𝒩" if "-x + y ∈ 𝒩" and "-y + z ∈ 𝒩"
proof-
  from that obtain a a' :: 'a
    where "a ∈ 𝒩" "-x + y = a" "a' ∈ 𝒩" "-y + z = a'" by fast
  thus ?thesis using add.assoc[of a "-y" z] distset_add_closed by fastforce
qed

end (* class group_add_with_distinguished_subgroup *)

class group_add_with_distinguished_normal_subgroup = group_add_with_distinguished_subgroup +
  assumes distset_normal: "((+) g) ` 𝒩 = (λx. x + g) ` 𝒩"

class ab_group_add_with_distinguished_subgroup =
  ab_group_add + group_add_with_distinguished_subgroup
begin

subclass group_add_with_distinguished_normal_subgroup
proof (unfold_locales, rule distset_nonempty, rule distset_diff_closed)
  show "⋀g. ((+) g) ` 𝒩 = (λx. x + g) ` 𝒩" by (force simp add: add.commute)
qed

end (* class ab_group_add_with_distinguished_subgroup *)

subsubsection ‹The quotient group type›

text ‹
  Here we define a quotient type relative to the left-coset relation, and instantiate it as a
  @{class group_add}.
›

quotient_type (overloaded) 'a coset_by_dist_sbgrp =
  "'a::group_add_with_distinguished_subgroup" / "λg h :: 'a. -g + h ∈ (𝒩::'a set)"
  morphisms distinguished_quotient_coset_rep distinguished_quotient_coset
proof (rule equivpI)
  show "reflp (λg h :: 'a. -g + h ∈ 𝒩)" using reflp_lcosetrel by (fast intro: reflpI)
  show "symp (λg h :: 'a. -g + h ∈ 𝒩)" using symp_lcosetrel by (fast intro: sympI)
  show "transp (λg h :: 'a. -g + h ∈ 𝒩)" using transp_lcosetrel
    by (fast intro: transpI)
qed

lemmas distinguished_quotient_coset_rep_inverse =
        Quotient_abs_rep[OF Quotient_coset_by_dist_sbgrp]
   and coset_by_dist_sbgrp_eq_iff =
        Quotient_rel_rep[OF Quotient_coset_by_dist_sbgrp]
   and distinguished_quotient_coset_eqI =
        Quotient_rel_abs[OF Quotient_coset_by_dist_sbgrp]
   and eq_to_distinguished_quotient_cosetI =
        Quotient_rel_abs2[OF Quotient_coset_by_dist_sbgrp]

lemma coset_coset_by_dist_sbgrp_cases
  [case_names coset, cases type: coset_by_dist_sbgrp]:
  "(⋀y. z = distinguished_quotient_coset y ⟹ P) ⟹ P"
  by (induct z) auto

lemmas distinguished_quotient_coset_eq_iff = coset_by_dist_sbgrp.abs_eq_iff

lemma distinguished_quotient_coset_rep_coset_equiv:
  "- distinguished_quotient_coset_rep (distinguished_quotient_coset r) + r ∈ 𝒩"
  using Quotient_rep_abs[OF Quotient_coset_by_dist_sbgrp]
  by    (simp add: distset_zero_closed)

instantiation coset_by_dist_sbgrp ::
  (group_add_with_distinguished_normal_subgroup) group_add
begin

lift_definition zero_coset_by_dist_sbgrp :: "'a coset_by_dist_sbgrp"
  is "0::'a" .

lemmas zero_distinguished_quotient [simp] = zero_coset_by_dist_sbgrp.abs_eq[symmetric]

lemma zero_distinguished_quotient_eq_iffs:
  "(distinguished_quotient_coset x = 0) = (x ∈ 𝒩)"
  "(X = 0) = (distinguished_quotient_coset_rep X ∈ 𝒩)"
proof-
  have "distinguished_quotient_coset x = 0 ⟹ x ∈ 𝒩"
  proof transfer
    fix x::'a show "- x + 0 ∈ 𝒩 ⟹ x ∈ 𝒩"
      using distset_uminus_closed[of "-x"] by simp
  qed
  moreover have "x ∈ 𝒩 ⟹ distinguished_quotient_coset x = 0"
    by transfer (simp add: distset_uminus_closed)
  ultimately show "(distinguished_quotient_coset x = 0) = (x ∈ 𝒩)" by fast
  have "distinguished_quotient_coset_rep 0 ∈ 𝒩"
    using distinguished_quotient_coset_rep_coset_equiv[of "0::'a"] distset_uminus_closed
    by    fastforce
  moreover have "distinguished_quotient_coset_rep X ∈ 𝒩 ⟹ X = 0"
    using eq_to_distinguished_quotient_cosetI[of X 0] by (simp add: distset_uminus_closed)
  ultimately show "(X = 0) = (distinguished_quotient_coset_rep X ∈ 𝒩)" by fast
qed

lift_definition plus_coset_by_dist_sbgrp ::
  "'a coset_by_dist_sbgrp ⇒ 'a coset_by_dist_sbgrp ⇒
      'a coset_by_dist_sbgrp"
  is "λx y::'a. x + y"
proof-
  fix w x y z :: 'a assume wx: "-w+x ∈ 𝒩" and yz: "-y+z ∈ 𝒩"
  from this obtain a1 a2
    where a1: "a1 ∈ 𝒩" "-w + x = a1"
    and   a2: "a2 ∈ 𝒩" "-y + z = a2"
    by    fast
  from a1(1) obtain a3 where a3: "a3 ∈ 𝒩" "-y + a1 = a3 + -y" using distset_normal by fast
  from a1(2) a2(2) a3(2) have "-(w + y) + (x + z) = a3 + a2"
    using minus_add add.assoc[of "-y + -w" x z] add.assoc[of "-y" "-w" x] add.assoc[of a3 "-y" z]
    by    simp
  with a2(1) a3(1) show "-(w + y) + (x + z) ∈ 𝒩" using distset_add_closed by simp
qed

lemmas plus_coset_by_dist_sbgrp [simp] = plus_coset_by_dist_sbgrp.abs_eq

lift_definition uminus_coset_by_dist_sbgrp ::
  "'a coset_by_dist_sbgrp ⇒ 'a coset_by_dist_sbgrp"
  is "λx::'a. -x"
proof-
  fix x y :: 'a assume xy: "-x + y ∈ 𝒩"
  from this obtain a where a: "a ∈ 𝒩" "-x + y = a" by fast
  from a(1) obtain a' where a': "a'∈𝒩" "a + -y = -y + a'" using distset_normal by fast
  from a(2) a'(2) have "- (-x) + -y = -(- y + a') + -y"
    using add.assoc[of "-x" y "-y"] by simp
  hence "- (-x) + -y = -a'" by (simp add: minus_add)
  with a'(1) show "- (-x) + -y ∈ 𝒩" using distset_uminus_closed by simp
qed

lemmas uminus_coset_by_dist_sbgrp [simp] =
  uminus_coset_by_dist_sbgrp.abs_eq

lift_definition minus_coset_by_dist_sbgrp ::
  "'a coset_by_dist_sbgrp ⇒ 'a coset_by_dist_sbgrp ⇒
      'a coset_by_dist_sbgrp"
  is "λx y::'a. x - y"
proof-
  fix w x y z :: 'a assume wx: "-w + x ∈ 𝒩" and yz: "-y + z ∈ 𝒩"
  from this obtain a1 a2
    where a1: "a1 ∈ 𝒩" "x = w + a1"
    and   a2: "a2 ∈ 𝒩" "z = y + a2"
    by    simp
  from a1(1) obtain a3 where a3: "a3 ∈ 𝒩" "y + a1 = a3 + y" using distset_normal by auto
  from a2(1) obtain a4 where a4: "a4 ∈ 𝒩" "y + a2 = a4 + y" using distset_normal by auto
  from a3(2) a4(2) a1(2) a2(2) have "x - z = w - y + a3 + y - y - a4"
    using add.assoc[of "w - y" y a1] add.assoc[of "w - y" a3 y]
          add.assoc[of "w - y + a3" y "-y"]
    by (simp add: algebra_simps)
  hence "x - z = (w - y) + (a3 - a4)"
    using add.assoc[of "w - y + a3" y "-y"] add.assoc[of "w - y" a3 "-a4"] by simp
  hence "-(w - y) + (x - z) = a3 - a4"
    using add.assoc[of "-(w - y)" "w - y" "a3 - a4", symmetric]
          left_minus[of "w - y"]
    by    simp
  with a3(1) a4(1) show "-(w - y) + (x - z) ∈ 𝒩" using distset_diff_closed by auto
qed

lemmas minus_coset_by_dist_sbgrp [simp] = minus_coset_by_dist_sbgrp.abs_eq

instance proof
  fix x y z :: "'a coset_by_dist_sbgrp"
  show "x + y + z = x + (y + z)" by transfer (simp add: distset_zero_closed algebra_simps)
  show " 0 + x = x" by transfer (simp add: distset_zero_closed)
  show " x + 0 = x" by transfer (simp add: distset_zero_closed)
  show "-x + x = 0" by transfer (simp add: distset_zero_closed)
  show "x + - y = x - y" by transfer (simp add: distset_zero_closed algebra_simps)
qed

end (* instantiation *)

instance coset_by_dist_sbgrp ::
  (ab_group_add_with_distinguished_subgroup) ab_group_add
proof
  show "⋀x y :: 'a coset_by_dist_sbgrp. x + y = y + x"
    by transfer (simp add: distset_zero_closed)
qed auto

subsection ‹Quotient rings›

subsubsection ‹Class definitions›

text ‹Now we set up subclasses of @{class ring} with a distinguished ideal.›

class ring_with_distinguished_ideal = ring + ab_group_add_with_distinguished_subgroup +
  assumes distset_leftideal : "a ∈ 𝒩 ⟹ r * a ∈ 𝒩"
  and     distset_rightideal: "a ∈ 𝒩 ⟹ a * r ∈ 𝒩"

class ring_1_with_distinguished_ideal = ring_1 + ring_with_distinguished_ideal +
  assumes distset_no1: "1∉𝒩"
  ― ‹
    For unitary rings we do not allow the quotient to be trivial to ensure that @{term 0} and
    @{term 1} will be different.
  ›

subsubsection ‹The quotient ring type›

text ‹
  We just reuse the @{typ "'a coset_by_dist_sbgrp"} type to define a quotient ring, and
  instantiate it as a @{class ring}.
›

type_synonym 'a distinguished_quotient_ring = "'a coset_by_dist_sbgrp"
― ‹
  This is intended to be used with @{class ring_with_distinguished_ideal} or one of its subclasses.
›

instantiation coset_by_dist_sbgrp :: (ring_with_distinguished_ideal) ring
begin

lift_definition times_coset_by_dist_sbgrp ::
  "'a distinguished_quotient_ring ⇒ 'a distinguished_quotient_ring ⇒
    'a distinguished_quotient_ring"
  is "λx y::'a. x * y"
proof-
  fix w x y z :: 'a assume wx: "-w + x ∈ 𝒩" and yz: "-y + z ∈ 𝒩"
  from this obtain a1 a2
    where a1: "a1 ∈ 𝒩" "-w + x = a1"
    and   a2: "a2 ∈ 𝒩" "-y + z = a2"
    by    fast
  from a1(2) a2(2) have "-(w * y) + (x * z) = w * a2 + a1 * z"
    by (simp add: algebra_simps)
  with a1(1) a2(1) show "-(w * y) + (x * z) ∈ 𝒩"
    using distset_leftideal[of _ w] distset_rightideal[of _ z] distset_add_closed by auto
qed

lemmas times_coset_by_dist_sbgrp [simp] = times_coset_by_dist_sbgrp.abs_eq

instance proof
  fix x y z :: "'a distinguished_quotient_ring"
  show "x * y * z = x * (y * z)"      by transfer (simp add: distset_zero_closed algebra_simps)
  show "(x + y) * z = x * z + y * z"  by transfer (simp add: distset_zero_closed algebra_simps)
  show "x * (y + z) = x * y + x * z"  by transfer (simp add: distset_zero_closed algebra_simps)
qed

end (* instantiation *)

instantiation coset_by_dist_sbgrp :: (ring_1_with_distinguished_ideal) ring_1
begin

lift_definition one_coset_by_dist_sbgrp :: "'a distinguished_quotient_ring"
  is "1::'a" .

lemmas one_coset_by_dist_sbgrp [simp] = one_coset_by_dist_sbgrp.abs_eq[symmetric]

instance proof
  show "(0::'a distinguished_quotient_ring) ≠ (1::'a distinguished_quotient_ring)"
  proof transfer qed (simp add: distset_no1)
next
  fix x :: "'a distinguished_quotient_ring"
  show "1 * x = x" by transfer (simp add: distset_zero_closed algebra_simps)
  show "x * 1 = x" by transfer (simp add: distset_zero_closed algebra_simps)
qed

end (* instantiation *)

subsection ‹Quotients of commutative rings›

text ‹
  For a commutative ring, the quotient modulo a prime ideal is an integral domain, and the quotient
  modulo a maximal ideal is a field.
›

subsubsection ‹Class definitions›

class comm_ring_with_distinguished_ideal = comm_ring + ab_group_add_with_distinguished_subgroup +
  assumes distset_ideal : "a ∈ 𝒩 ⟹ r * a ∈ 𝒩"
begin

subclass ring_with_distinguished_ideal
  using distset_ideal by unfold_locales (auto simp add: mult.commute)

definition distideal_extension :: "'a ⇒ 'a set"
  where "distideal_extension a ≡ {x. ∃r z. z ∈ 𝒩 ∧ x = r * a + z}"

lemma distideal_extension: "𝒩 ⊆ distideal_extension a"
  unfolding distideal_extension_def
proof clarify
  fix x assume "x∈𝒩"
  hence "x∈𝒩 ∧ x = 0*a + x" by simp
  thus "∃r z. z ∈ 𝒩 ∧ x = r*a + z" by fast
qed

lemma distideal_extension_diff_closed:
  "r ∈ distideal_extension a ⟹ s ∈ distideal_extension a ⟹
    r - s ∈ distideal_extension a"
  unfolding distideal_extension_def
proof clarify
  fix r r' z z'
  assume "z ∈ 𝒩" "z' ∈ 𝒩"
  moreover have "r * a + z - (r' * a + z') = (r - r') * a + (z - z')"
    by (simp add: algebra_simps)
  ultimately show
    "∃r'' z''. z'' ∈ 𝒩 ∧ r * a + z - (r' * a + z') = r'' * a + z''"
    using distset_diff_closed by fast
qed

lemma distideal_extension_ideal:
  "x ∈ distideal_extension a ⟹ r * x ∈ distideal_extension a"
  unfolding distideal_extension_def
proof clarify
  fix s r z assume "z ∈ 𝒩"
  thus "∃r' z'. z' ∈ 𝒩 ∧ s * (r * a + z) = r' * a + z'"
    using distset_ideal by (fastforce simp add: algebra_simps)
qed

end (* class comm_ring_with_distinguished_ideal *)

class comm_ring_1_with_distinguished_ideal = ring_1 + comm_ring_with_distinguished_ideal +
  assumes distset_no1:
    "1∉𝒩"
  ― ‹Don't allow the quotient to be trivial.›
begin

subclass ring_1_with_distinguished_ideal using distset_no1 by unfold_locales

lemma distideal_extension_by: "a ∈ distideal_extension a"
  unfolding distideal_extension_def
proof
  have "0 ∈ 𝒩 ∧ a = 1 * a + 0" using distset_zero_closed by simp
  thus "∃r z. z ∈ 𝒩 ∧ a = r * a + z" by fastforce
qed

end (* class comm_ring_1_with_distinguished_ideal *)

class comm_ring_1_with_distinguished_pideal = comm_ring_1_with_distinguished_ideal +
  assumes distset_pideal: "r * s ∈ 𝒩 ⟹ r ∈ 𝒩 ∨ s ∈ 𝒩"

class comm_ring_1_with_distinguished_maxideal = comm_ring_1_with_distinguished_ideal +
  assumes distset_maxideal:
    "⟦
      𝒩 ⊆ I; 1∉I;
      ∀r s. r ∈ I ∧ s ∈ I ⟶ r - s ∈ I;
      ∀a r. a ∈ I ⟶ r * a ∈ I
    ⟧ ⟹ I = 𝒩"
begin

lemma distset_maxideal_vs_distideal_extension:
  "1 ∉ distideal_extension a ⟹ distideal_extension a = 𝒩"
  using distideal_extension distideal_extension_diff_closed distideal_extension_ideal
        distset_maxideal
  by    force

subclass comm_ring_1_with_distinguished_pideal
proof
  fix a b :: 'a
  assume ab: "a * b ∈ 𝒩"
  have "¬ (a ∉ 𝒩 ∧ b ∉ 𝒩)"
  proof clarify
    assume a: "a ∉ 𝒩" and b: "b ∉ 𝒩"
    define I where "I ≡ distideal_extension b"
    have "1 ∉ I"
      unfolding distideal_extension_def I_def
    proof clarify
      fix r z assume rz: "z ∈ 𝒩" "1 = r * b + z"
      from rz(2) have "a = r * (a * b) + a * z" using mult_1_right by (simp add: algebra_simps)
      moreover from ab rz(1) have "r * (a * b) ∈ 𝒩" and "a * z ∈ 𝒩"
        using distset_ideal by auto
      ultimately show False using a distset_add_closed by fastforce
    qed
    with I_def b show False
      using distset_maxideal_vs_distideal_extension distideal_extension_by by fast
  qed
  thus "a ∈ 𝒩 ∨ b ∈ 𝒩" by fast
qed

end (* class comm_ring_1_with_distinguished_maxideal *)

subsubsection ‹Instances and instantiations›

instance coset_by_dist_sbgrp :: (comm_ring_with_distinguished_ideal) comm_ring
proof
  fix x y :: "'a distinguished_quotient_ring"
  show "x * y = y * x" by transfer (simp add: distset_zero_closed algebra_simps)
qed (simp add: algebra_simps)

instance coset_by_dist_sbgrp :: (comm_ring_1_with_distinguished_ideal) comm_ring_1
 by standard (auto simp add: algebra_simps)

instance coset_by_dist_sbgrp :: (comm_ring_1_with_distinguished_pideal) idom
proof (standard, transfer)
  fix a b :: 'a show
    "-a + 0 ∉ 𝒩 ⟹ -b + 0 ∉ 𝒩 ⟹
      -(a * b) + 0 ∉ 𝒩"
    using distset_pideal distset_uminus_closed by fastforce
qed

lemma inverse_in_quotient_mod_maxideal:
  "∃y. -(y * x) + 1 ∈ 𝒩" if "x ∉ 𝒩"
  for x :: "'a::comm_ring_1_with_distinguished_maxideal"
proof-
  from that have "1 ∉ distideal_extension x ⟹ False"
    using distset_uminus_closed distset_maxideal_vs_distideal_extension distideal_extension_by
    by    auto
  from this obtain y z where yz: "z ∈ 𝒩" "1 = y * x + z"
    using distideal_extension_def by fast
  from yz(2) have "- (y * x) + 1 = z" by (simp add: algebra_simps)
  with yz(1) show "∃y. -(y * x) + 1 ∈ 𝒩" by fast
qed

instantiation coset_by_dist_sbgrp :: (comm_ring_1_with_distinguished_maxideal) field
begin

lift_definition inverse_coset_by_dist_sbgrp ::
  "'a distinguished_quotient_ring ⇒ 'a distinguished_quotient_ring"
  is "λx::'a. if x∈𝒩 then 0 else (SOME y::'a. -(y*x) + 1 ∈ 𝒩)"
proof-
  fix x x' :: 'a
  assume xx': "-x + x' ∈ 𝒩"
  define ix ix'
    where "ix  ≡ if  x ∈ 𝒩 then 0 else (SOME y::'a. -(y * x ) + 1 ∈ 𝒩)"
    and   "ix' ≡ if x' ∈ 𝒩 then 0 else (SOME y::'a. -(y * x') + 1 ∈ 𝒩)"
  show "-ix + ix' ∈ 𝒩"
  proof (cases "x∈𝒩")
    case True with xx' ix_def ix'_def show ?thesis
      using distset_lcoset_closed1[of x] distset_zero_closed by auto
  next
    case False
    with xx' have "x' ∉ 𝒩" using distset_lcoset_closed2 by fast
    with ix_def ix'_def False have "-((-ix + ix') * x) + ix' * (x + - x') ∈ 𝒩"
      using someI_ex[OF inverse_in_quotient_mod_maxideal]
            distset_uminus_plus_closed[of "-(ix * x) + 1" "-(ix' * x') + 1"]
      by    (force simp add: algebra_simps)
    moreover have "ix' * (x + -x') ∈ 𝒩"
      using distset_uminus_closed[OF xx'] distset_ideal by auto
    ultimately have "(-ix + ix') * x ∈ 𝒩" using distset_lcoset_closed2 by force
    with False show ?thesis using distset_pideal by fast
  qed
qed

lemma inverse_coset_by_dist_sbgrp_eq0 [simp]:
  "x ∈ 𝒩 ⟹ inverse (distinguished_quotient_coset x) = 0"
  by transfer (simp add: distset_zero_closed)

lemma coset_by_dist_sbgrp_inverse_rep:
  "x ∉ 𝒩 ⟹ -(y * x) + 1 ∈ 𝒩 ⟹
    inverse (distinguished_quotient_coset x) = distinguished_quotient_coset y"
proof transfer
  fix x y :: 'a
  assume xy: "x ∉ 𝒩" "-(y * x) + 1 ∈ 𝒩"
  define z :: 'a where "z ≡ (SOME y. - (y * x) + 1 ∈ 𝒩)"
  with xy have "(-z + y) * x ∈ 𝒩"
    using someI_ex[OF inverse_in_quotient_mod_maxideal]
          distset_diff_closed[of "-(z * x) + 1" "-(y * x) + 1"]
    by    (fastforce simp add: algebra_simps)
  with xy(1) show "- (if x ∈ 𝒩 then 0 else z) + y ∈ 𝒩"
    using distset_pideal by auto
qed

definition divide_coset_by_dist_sbgrp_def [simp]:
  "x div y = (x::'a distinguished_quotient_ring) * inverse y"

lemma coset_by_dist_sbgrp_divide_rep:
  "y ∉ 𝒩 ⟹ -(z * y) + 1 ∈ 𝒩 ⟹
    distinguished_quotient_coset x div distinguished_quotient_coset y
      = distinguished_quotient_coset (x * z)"
  by (simp add: coset_by_dist_sbgrp_inverse_rep)

instance proof
  show "inverse (0::'a distinguished_quotient_ring) = 0"
    by transfer (simp add: distset_zero_closed)
next
  fix x :: "'a distinguished_quotient_ring"
  show "x ≠ 0 ⟹ inverse x * x = 1"
  proof transfer
    fix a::'a
    assume "-a + 0 ∉ 𝒩"
    moreover define ia
      where "ia ≡ if a ∈ 𝒩 then 0 else (SOME b. - (b * a) + 1 ∈ 𝒩)"
    ultimately show "-(ia * a) + 1 ∈ 𝒩"
      using distset_uminus_closed someI_ex[OF inverse_in_quotient_mod_maxideal] by auto
  qed
qed (rule divide_coset_by_dist_sbgrp_def)

end (* instantiation *)


end (* theory *)