Theory Localization_Ring.Localization

theory Localization
  imports Main "HOL-Algebra.Group" "HOL-Algebra.Ring" "HOL-Algebra.AbelCoset"
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents: 
 We define the localization of a commutative ring R with respect to a multiplicative subset, 
i.e. with respect to a submonoid of R (seen as a multiplicative monoid), cf. [rec_rng_of_frac›]. 
 We prove that this localization is a commutative ring (cf. [crng_rng_of_frac›]) equipped with a 
homomorphism of rings from R (cf. [rng_to_rng_of_frac_is_ring_hom›]).
›

section ‹The Localization of a Commutative Ring›

subsection ‹Localization›

locale submonoid = monoid M for M (structure) +
  fixes S
  assumes subset : "S  carrier M"
    and m_closed [intro, simp] : "x  S; y  S  x  y  S"
    and one_closed [simp] : "𝟭  S"

lemma (in submonoid) is_submonoid: "submonoid M S"
  by (rule submonoid_axioms)

locale mult_submonoid_of_rng = ring R + submonoid R S for R and S

locale mult_submonoid_of_crng = cring R + mult_submonoid_of_rng R S for R and S

locale eq_obj_rng_of_frac = cring R + mult_submonoid_of_crng R S for R (structure) and S +
  fixes rel
  defines "rel  carrier = carrier R × S, eq = λ(r,s) (r',s'). tS. t  ((s' r)  (s  r')) = 𝟬"

lemma (in abelian_group) minus_to_eq :
  assumes "abelian_group G" and "x  carrier G" and "y  carrier G" and "x  y = 𝟬"
  shows "x = y"
  by (metis add.inv_solve_right assms(2) assms(3) assms(4) l_zero minus_eq zero_closed)

lemma (in eq_obj_rng_of_frac) equiv_obj_rng_of_frac:
  shows "equivalence rel"
proof
  show "x. x  carrier rel  x .=relx"
  proof-
    fix x
    assume "x  carrier rel"
    then have f1:"𝟭  ((snd x  fst x)  (snd x  fst x)) = 𝟬"
      using rel_def subset l_one minus_eq add.r_inv rev_subsetD 
      by auto
    moreover have "x = (fst x, snd x)"
      by simp
    thus "x .=relx" 
      using rel_def one_closed f1 
      by auto
  qed
  show "x y. x .=rely  x  carrier rel  y  carrier rel  y .=relx"
  proof-
    fix x y
    assume a1:"x .=rely" and a2:"x  carrier rel" and a3:"y  carrier rel"
    then obtain t where f1:"t  S" and f2:"t  ((snd y  fst x)  (snd x  fst y)) = 𝟬"
      using rel_def 
      by fastforce
    then have "(snd x  fst y)  (snd y  fst x) =  ((snd y  fst x)  (snd x  fst y))"
      using abelian_group.minus_add abelian_group.minus_minus
      by (smt a2 a3 a_minus_def abelian_group.a_inv_closed add.inv_mult_group is_abelian_group 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse 
          rel_def rev_subsetD subset)
    then have "t  ((snd x  fst y)  (snd y  fst x)) = 𝟬"
      using minus_zero r_minus f2
      by (smt a2 a3 f1 mem_Sigma_iff minus_closed partial_object.select_convs(1) prod.collapse 
          rel_def semiring_simprules(3) rev_subsetD subset)
    thus "y .=relx"
      using f1 rel_def 
      by auto
  qed
  show "x y z. 
    x .=rely  y .=relz  x  carrier rel  y  carrier rel  z  carrier rel  x .=relz"
  proof-
    fix x y z
    assume a1:"x .=rely" and a2:"y .=relz" and a3:"x  carrier rel" and a4:"y  carrier rel" 
      and a5:"z  carrier rel"
    then obtain t where f1:"t  S" and f2:"t  ((snd y  fst x)  (snd x  fst y)) = 𝟬"
      using rel_def 
      by fastforce
    then obtain t' where f3:"t'  S" and f4:"t'  ((snd z  fst y)  (snd y  fst z)) = 𝟬"
      using rel_def a2 
      by fastforce
    then have "t  (snd y  fst x)  t  (snd x  fst y) = 𝟬"
      using f1 subset r_distr f2
      by (smt a3 a4 a_minus_def abelian_group.a_inv_closed is_abelian_group mem_Sigma_iff 
          monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse r_minus rel_def 
          subset_iff)
    then have "t'  (t  (snd y  fst x))  t'  (t  (snd x  fst y)) = 𝟬"
      using f3 subset r_distr
      by (smt a3 a4 a_minus_def f1 is_abelian_group mem_Sigma_iff minus_to_eq 
          partial_object.select_convs(1) prod.collapse r_neg rel_def semiring_simprules(3) subset_iff)
    then have f5:"snd z  (t'  (t  (snd y  fst x)))  snd z  (t'  (t  (snd x  fst y))) = 𝟬"
      using a5 rel_def r_distr
      by (smt a3 a4 a_minus_def f1 f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg subset subset_iff)
    have "t'  (snd z  fst y)  t'  (snd y  fst z) = 𝟬"
      using f3 f4 subset r_distr
      by (smt a4 a5 a_minus_def abelian_group.a_inv_closed is_abelian_group mem_Sigma_iff 
          monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse r_minus rel_def 
          rev_subsetD)
    then have "t  (t'  (snd z  fst y))  t  (t'  (snd y  fst z)) = 𝟬"
      using f1 subset r_distr
      by (smt a4 a5 a_minus_def f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg rel_def subset_iff)
    then have f6:"snd x  (t  (t'  (snd z  fst y)))  snd x  (t  (t'  (snd y  fst z))) = 𝟬"
      using a3 rel_def r_distr
      by (smt a4 a5 a_minus_def f1 f3 is_abelian_group mem_Sigma_iff minus_to_eq monoid.m_closed 
          monoid_axioms partial_object.select_convs(1) prod.collapse r_neg subset subset_iff)
    have "snd z  (t'  (t  (snd x  fst y))) = snd x  (t  (t'  (snd z  fst y)))"
      using comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 m_assoc
      by (smt m_lcomm mem_Sigma_iff partial_object.select_convs(1) partial_object_ext_def rel_def 
          semiring_simprules(3) rev_subsetD surjective_pairing)
    then have "snd z  (t'  (t  (snd y  fst x)))  snd z  (t'  (t  (snd x  fst y)))  
      snd x  (t  (t'  (snd z  fst y)))  snd x  (t  (t'  (snd y  fst z))) = 
      snd z  (t'  (t  (snd y  fst x)))  snd x  (t  (t'  (snd y  fst z)))"
        using add.l_inv
        by (smt a3 a4 a5 f1 f3 f5 is_abelian_group local.semiring_axioms mem_Sigma_iff minus_to_eq 
            monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.collapse rel_def 
            semiring.semiring_simprules(6) subset subset_iff)
    then have f7:"snd z  (t'  (t  (snd y  fst x)))  snd x  (t  (t'  (snd y  fst z))) = 𝟬"
      using f5 f6
      by (smt snd z  (t'  (t  (snd x  fst y))) = snd x  (t  (t'  (snd z  fst y))) 
          t'  (snd z  fst y)  t'  (snd y  fst z) = 𝟬 a4 a5 f3 is_abelian_group mem_Sigma_iff 
          minus_to_eq partial_object.select_convs(1) prod.collapse rel_def semiring_simprules(3) 
          subset subset_iff)
    moreover have "(t  t'  snd y)  ((snd z  fst x)  (snd x  fst z)) = ((t  t'  snd y)  (snd z  fst x))  ((t  t'  snd y)  (snd x  fst z))"
      using r_distr f1 f3 subset a3 a4 a5 rel_def a_minus_def r_minus
      by (smt SigmaE abelian_group.a_inv_closed is_abelian_group monoid.m_closed monoid_axioms 
          partial_object.select_convs(1) prod.sel(1) prod.sel(2) subset_iff)
    moreover have f8:"(t  t'  snd y)  (snd z  fst x) = snd z  (t'  (t  (snd y  fst x)))"
      using m_assoc comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 rel_def rev_subsetD
      by (smt SigmaE local.semiring_axioms m_lcomm partial_object.select_convs(1) prod.sel(1) 
          prod.sel(2) semiring.semiring_simprules(3))
    moreover have f9:"(t  t'  snd y)  (snd x  fst z) = snd x  (t  (t'  (snd y  fst z)))"
      using m_assoc comm_monoid_axioms_def[of R] f1 f3 subset a3 a4 a5 rel_def rev_subsetD
      by (smt SigmaE m_comm monoid.m_closed monoid_axioms partial_object.select_convs(1) prod.sel(1) 
          prod.sel(2))
    then have f10:"(t  t'  snd y)  (snd z  fst x)  (t  t'  snd y)  (snd x  fst z) = 𝟬"
      using f7 f8 f9 
      by simp
    moreover have "t  t'  snd y  S"
      using f1 f3 a4 rel_def m_closed
      by (simp add: mem_Times_iff)
    then have "(t  t'  snd y)  (snd z  fst x  snd x  fst z) = 𝟬"
      using r_distr subset rev_subsetD f10 calculation(2) 
      by auto
    thus " x .=relz"
      using rel_def t  t'  snd y  S 
      by auto
  qed
qed

definition  eq_class_of_rng_of_frac:: "_  'a  'b  _set" (infix "|ı" 10)
  where "r |rels  {(r', s')  carrier rel. (r, s) .=rel(r', s')}"

lemma class_of_to_rel:
  shows "class_ofrel(r, s) = (r |rels)"
  using eq_class_of_def[of rel] eq_class_of_rng_of_frac_def[of rel] 
  by auto

lemma (in eq_obj_rng_of_frac) zero_in_mult_submonoid:
  assumes "𝟬  S" and "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) = (r' |rels')"
proof
  show "(r |rels)  (r' |rels')"
  proof
    fix x
    assume a1:"x  (r |rels)"
    have " 𝟬  (s'  fst x  snd x  r') = 𝟬"
      using l_zero subset rel_def a1 eq_class_of_rng_of_frac_def
      by (smt abelian_group.minus_closed assms(3) is_abelian_group l_null mem_Collect_eq mem_Sigma_iff 
          monoid.m_closed monoid_axioms old.prod.case partial_object.select_convs(1) subset_iff surjective_pairing)
    thus "x  (r' |rels')"
      using assms(1) assms(3) rel_def eq_class_of_rng_of_frac_def
      by (smt SigmaE a1 eq_object.select_convs(1) l_null mem_Collect_eq minus_closed old.prod.case 
          partial_object.select_convs(1) prod.collapse semiring_simprules(3) subset subset_iff)
  qed
  show "(r' |rels')  (r |rels)"
  proof
    fix x
    assume a1:"x  (r' |rels')"
    have " 𝟬  (s  fst x  snd x  r) = 𝟬"
      using l_zero subset rel_def a1 eq_class_of_rng_of_frac_def
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms(2) l_null mem_Sigma_iff 
          minus_closed partial_object.select_convs(1) semiring_simprules(3) rev_subsetD)
    thus "x  (r |rels)"
      using assms(1) assms(2) rel_def eq_class_of_rng_of_frac_def
      by (smt SigmaE a1 eq_object.select_convs(1) l_null mem_Collect_eq minus_closed old.prod.case 
          partial_object.select_convs(1) prod.collapse semiring_simprules(3) subset subset_iff)
  qed
qed

definition set_eq_class_of_rng_of_frac:: "_  _set" ("set'_class'_ofı")
  where "set_class_ofrel {(r |rels)| r s. (r, s)  carrier rel}"

(* The lemma below should be moved to theory Congruence in HOL-Algebra *)
lemma elem_eq_class:
  assumes "equivalence S" and "x  carrier S" and "y  carrier S" and "x .=Sy"
  shows "class_ofSx = class_ofSy"
proof
  show "class_ofSx  class_ofSy"
  proof
    fix z
    assume "z  class_ofSx"
    then have "y .=Sz"
      using assms eq_class_of_def[of S x] equivalence.sym[of S x y] equivalence.trans
      by (metis (mono_tags, lifting) mem_Collect_eq)
    thus "z  class_ofSy"
      using z  class_ofSx
      by (simp add: eq_class_of_def)
  qed
  show "class_ofSy  class_ofSx"
  proof
    fix z
    assume "z  class_ofSy"
    then have "x .=Sz"
      using assms eq_class_of_def equivalence.trans
      by (metis (mono_tags, lifting) mem_Collect_eq)
    thus "z  class_ofSx"
      using z  class_ofSy
      by (simp add: eq_class_of_def)
  qed
qed

lemma (in abelian_group) four_elem_comm:
  assumes "a  carrier G" and "b  carrier G" and "c  carrier G" and "d  carrier G"
  shows "a  c  b  d = a  b  c  d"
  using assms a_assoc a_comm
  by (simp add: a_minus_def)

lemma (in abelian_monoid) right_add_eq:
  assumes "a = b"
  shows "c  a = c  b"
  using assms 
  by simp

lemma (in abelian_monoid) right_minus_eq:
  assumes "a = b"
  shows "c  a = c  b"
  by (simp add: assms)

lemma (in abelian_group) inv_add:
  assumes "a  carrier G" and "b  carrier G"
  shows " (a  b) =  a  b"
  using assms minus_add
  by (simp add: a_minus_def)

lemma (in abelian_group) right_inv_add:
  assumes "a  carrier G" and "b  carrier G" and "c  carrier G"
  shows "c  a  b = c  (a  b)" 
  using assms
  by (simp add: a_minus_def add.m_assoc local.minus_add)

context eq_obj_rng_of_frac 
begin

definition carrier_rng_of_frac:: "_ partial_object"
  where "carrier_rng_of_frac  carrier = set_class_ofrel"

definition mult_rng_of_frac:: "[_set, _set]  _set"
  where "mult_rng_of_frac X Y  
let x' = (SOME x. x  X) in 
let y' = (SOME y. y  Y) in 
(fst x'  fst y')|rel(snd x'  snd y')"

definition rec_monoid_rng_of_frac:: "_ monoid"
  where "rec_monoid_rng_of_frac   carrier = set_class_ofrel, mult = mult_rng_of_frac, one = (𝟭|rel𝟭)"

lemma member_class_to_carrier:
  assumes "x  (r |rels)" and "y  (r' |rels')"
  shows "(fst x  fst y, snd x  snd y)  carrier rel"
  using assms rel_def eq_class_of_rng_of_frac_def
  by (metis (no_types, lifting) Product_Type.Collect_case_prodD m_closed mem_Sigma_iff 
      partial_object.select_convs(1) semiring_simprules(3))

lemma member_class_to_member_class:
  assumes "x  (r |rels)" and "y  (r' |rels')"
  shows "(fst x  fst y |relsnd x  snd y)  set_class_ofrel⇙"
  using assms member_class_to_carrier[of x r s y r' s'] set_eq_class_of_rng_of_frac_def[of rel] 
    eq_class_of_rng_of_frac_def 
  by auto

lemma closed_mult_rng_of_frac :
  assumes "(r, s)  carrier rel" and "(t, u)  carrier rel"
  shows "(r |rels) rec_monoid_rng_of_frac(t |relu)  set_class_ofrel⇙"
proof-
  have "(r, s) .=rel(r, s)"
    using assms(1) equiv_obj_rng_of_frac equivalence_def[of "rel"] 
    by blast
  then have "(r, s)  (r |rels)"
    using assms(1)
    by (simp add: eq_class_of_rng_of_frac_def)
  then have f1:"x. x  (r |rels)"
    by auto
  have f2:"y. y (t |relu)"
    using assms(2) equiv_obj_rng_of_frac equivalence.refl eq_class_of_rng_of_frac_def 
    by fastforce
  show "(r |rels) rec_monoid_rng_of_frac(t |relu)  set_class_ofrel⇙"
    using f1 f2 rec_monoid_rng_of_frac_def mult_rng_of_frac_def[of "(r |rels)" "(t |relu)"] 
      set_eq_class_of_rng_of_frac_def[of "rel"] member_class_to_member_class[of x' r s y' t u]
    by (metis (mono_tags, lifting) mem_Collect_eq member_class_to_carrier monoid.select_convs(1) 
        someI_ex)
qed

lemma non_empty_class:
  assumes "(r, s)  carrier rel"
  shows "(r |rels)  {}"
  using assms eq_class_of_rng_of_frac_def equiv_obj_rng_of_frac equivalence.refl 
  by fastforce

lemma mult_rng_of_frac_fundamental_lemma:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) rec_monoid_rng_of_frac(r' |rels') = (r  r' |rels  s')"
proof-
  have f1:"(r |rels)  {}"
    using assms(1) non_empty_class 
    by auto
  have "(r' |rels')  {}"
    using assms(2) non_empty_class 
    by auto
  then have "x  (r |rels). x'  (r' |rels'). (r |rels) rec_monoid_rng_of_frac(r' |rels') =
    (fst x  fst x' |relsnd x  snd x')"
      using f1 rec_monoid_rng_of_frac_def
      by (metis monoid.select_convs(1) mult_rng_of_frac_def some_in_eq)
  then obtain x and x' where f2:"x  (r |rels)" and f3:"x'  (r' |rels')" 
    and "(r |rels) rec_monoid_rng_of_frac(r' |rels') = (fst x  fst x' |relsnd x  snd x')"
    by blast
  then have "(r, s) .=rel(fst x, snd x)"
    using rel_def
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def)
  then obtain t where f4:"t  S" and f5:"t  ((snd x  r)  (s  fst x)) = 𝟬"
    using rel_def 
    by auto
  have "(r', s') .=rel(fst x', snd x')"
    using rel_def f3
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def)
  then obtain t' where f6:"t'  S" and f7:"t'  (snd x'  r'  s'  fst x') = 𝟬"
    using rel_def 
    by auto
  have f8:"t  carrier R"
    using f4 subset rev_subsetD 
    by auto
  have f9:"snd x  r  carrier R" 
    using subset rev_subsetD f2 assms(1)
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3))
  have f10:" (s  fst x)  carrier R"
    using assms(1) subset rev_subsetD f2
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD abelian_group.a_inv_closed 
        eq_class_of_rng_of_frac_def is_abelian_group mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rel_def)
  then have "t  (snd x  r)  t  (s  fst x) = 𝟬"
    using f8 f9 f10 f5 r_distr[of "snd x  r" " (s  fst x)" t] a_minus_def r_minus[of t "s  fst x"]
    by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f2 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f11:"t  (snd x  r) = t  (s  fst x)"
    by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f2 f8 is_abelian_group 
        mem_Sigma_iff minus_to_eq monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have f12:"t'  carrier R"
    using f6 subset rev_subsetD 
    by auto
  have f13:"snd x'  r'  carrier R"
    using assms(2) f3 subset rev_subsetD
    by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
        mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
  have f14:" (s'  fst x')  carrier R"
    using assms(2) f3 subset rev_subsetD
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD abelian_group.a_inv_closed 
        eq_class_of_rng_of_frac_def is_abelian_group mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rel_def)
  then have "t'  (snd x'  r')  t'  (s'  fst x') = 𝟬"
    using f12 f13 f14 f7 r_distr[of "snd x'  r'" " (s'  fst x')" t'] a_minus_def 
      r_minus[of t' "s'  fst x'"]
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f3 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f15:"t'  (snd x'  r') = t'  (s'  fst x')"
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f3 f12 is_abelian_group 
        mem_Sigma_iff minus_to_eq monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have "t'  t  S"
    using f4 f6 m_closed 
    by auto
  then have f16:"t'  t  carrier R"
    using subset rev_subsetD 
    by auto
  have f17:"(snd x  snd x')  (r  r')  carrier R"
    using assms f2 f3
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  have f18:"(s  s')  (fst x  fst x')  carrier R"
    using assms f2 f3
    by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  then have f19:"(t'  t)  ((snd x  snd x')  (r  r')  (s  s')  (fst x  fst x')) = 
    ((t'  t)  (snd x  snd x'))  (r  r')  (t'  t)  ((s  s')  (fst x  fst x'))"
      using f16 f17 f18 r_distr m_assoc r_minus a_minus_def
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f14 f2 f3 
          m_comm mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def 
          subset subset_iff)
  then have f20:"(t'  t)  (snd x  snd x')  (r  r') = (t'  t)  (snd x  r  snd x'  r')"
    using m_assoc m_comm f16 assms rel_def f2 f3
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
        partial_object.select_convs(1) semiring_simprules(3) subset subset_iff)
  then have "((t'  t)  (snd x  snd x'))  (r  r') = t'  ((t  snd x  r)  snd x'  r')"
    using m_assoc assms f2 f3 rel_def f8 f12
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff monoid.m_closed 
        monoid_axioms partial_object.select_convs(1) subset subset_iff)
  then have f21:"((t'  t)  (snd x  snd x'))  (r  r') = t'  (t  s  fst x)  snd x'  r'"
    using f11 m_assoc
    by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f12 f2 f3 f8 
        mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
  moreover have "(t'  t)  ((s  s')  (fst x  fst x')) = (t'  s'  fst x')  t  s  fst x"
    using assms f2 f3 f8 f12 m_assoc m_comm rel_def
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff monoid.m_closed 
        monoid_axioms partial_object.select_convs(1) subset subset_iff)
  then have "(t'  t)  ((s  s')  (fst x  fst x')) = (t'  snd x'  r')  t  s  fst x"
    using f15 m_assoc
    by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f12 f3 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def subset subset_iff)
  then have f22:"(t'  t)  ((s  s')  (fst x  fst x')) = t'  ((t  snd x  r)  snd x'  r')"
    using m_assoc m_comm assms
    by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f12 f2 f21 f3 f8 mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
  then have f23:"(t'  t)  ((snd x  snd x')  (r  r')  (s  s')  (fst x  fst x')) = 𝟬"
    using f19 f21 f22
    by (metis t'  t  (snd x  snd x')  (r  r') = t'  (t  snd x  r  snd x'  r') 
        a_minus_def f16 f18 r_neg semiring_simprules(3))
  have f24:"(r  r', s  s')  carrier rel"
    using assms rel_def 
    by auto
  have f25: "(fst x  fst x', snd x  snd x')  carrier rel"
    using f2 f3 member_class_to_carrier 
    by auto
  then have "(r  r', s  s') .=rel(fst x  fst x', snd x  snd x')"
    using f23 f24 rel_def t'  t  S 
    by auto
  then have "class_ofrel(r  r', s  s') = class_ofrel(fst x  fst x', snd x  snd x')"
    using f24 f25 equiv_obj_rng_of_frac elem_eq_class[of rel "(r  r', s  s')" "(fst x  fst x', snd x  snd x')"] 
      eq_class_of_rng_of_frac_def 
    by auto
  then have "(r  r' |rels  s') = (fst x  fst x' |relsnd x  snd x')"
    using class_of_to_rel[of rel] 
    by auto
  thus ?thesis
    using (r |rels) rec_monoid_rng_of_frac(r' |rels') = (fst x  fst x' |relsnd x  snd x') 
      trans sym 
    by auto
qed

lemma member_class_to_assoc:
  assumes "x  (r |rels)" and "y  (t |relu)" and "z  (v |relw)"
  shows "((fst x  fst y)  fst z |rel(snd x  snd y)  snd z) = (fst x  (fst y  fst z) |relsnd x  (snd y  snd z))"
  using assms m_assoc subset rel_def rev_subsetD
  by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff partial_object.select_convs(1))

lemma assoc_mult_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(t, u)  carrier rel" and "(v, w)  carrier rel"
  shows "((r |rels) rec_monoid_rng_of_frac(t |relu)) rec_monoid_rng_of_frac(v |relw) =
         (r |rels) rec_monoid_rng_of_frac((t |relu) rec_monoid_rng_of_frac(v |relw))"
proof-
  have "((r  t)  v, (s  u)  w) = (r  (t  v), s  (u  w))"
    using assms m_assoc
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1) rel_def rev_subsetD subset)
  then have f1:"((r  t)  v |rel(s  u)  w) = (r  (t  v) |rels  (u  w))"
    by simp
  have f2:"((r |rels) rec_monoid_rng_of_frac(t |relu)) rec_monoid_rng_of_frac(v |relw) =
    ((r  t)  v |rel(s  u)  w)"
    using assms mult_rng_of_frac_fundamental_lemma rel_def 
    by auto
  have f3:"(r |rels) rec_monoid_rng_of_frac((t |relu) rec_monoid_rng_of_frac(v |relw)) =
    (r  (t  v) |rels  (u  w))"
    using assms mult_rng_of_frac_fundamental_lemma rel_def 
    by auto
  thus ?thesis
    using f1 f2 f3 
    by simp
qed

lemma left_unit_mult_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "𝟭rec_monoid_rng_of_fracrec_monoid_rng_of_frac(r |rels) = (r |rels)"
  using assms subset rev_subsetD rec_monoid_rng_of_frac_def mult_rng_of_frac_fundamental_lemma[of 𝟭 𝟭 r s] 
    l_one[of r] l_one[of s] rel_def 
  by auto

lemma right_unit_mult_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "(r |rels) rec_monoid_rng_of_frac𝟭rec_monoid_rng_of_frac= (r |rels)"
  using assms subset rev_subsetD rec_monoid_rng_of_frac_def mult_rng_of_frac_fundamental_lemma[of r s 𝟭 𝟭]
    r_one[of r] r_one[of s] rel_def 
  by auto

lemma monoid_rng_of_frac:
  shows "monoid (rec_monoid_rng_of_frac)"
proof
  show "x y. x  carrier rec_monoid_rng_of_frac 
           y  carrier rec_monoid_rng_of_frac  x rec_monoid_rng_of_fracy  carrier rec_monoid_rng_of_frac"
    using rec_monoid_rng_of_frac_def closed_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  show "x y z. x  carrier rec_monoid_rng_of_frac 
             y  carrier rec_monoid_rng_of_frac 
             z  carrier rec_monoid_rng_of_frac 
             x rec_monoid_rng_of_fracy rec_monoid_rng_of_fracz =
             x rec_monoid_rng_of_frac(y rec_monoid_rng_of_fracz)"
    using assoc_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "𝟭rec_monoid_rng_of_frac carrier rec_monoid_rng_of_frac"
    using rec_monoid_rng_of_frac_def rel_def set_eq_class_of_rng_of_frac_def 
    by fastforce
  show "x. x  carrier rec_monoid_rng_of_frac  𝟭rec_monoid_rng_of_fracrec_monoid_rng_of_fracx = x"
    using left_unit_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "x. x  carrier rec_monoid_rng_of_frac  x rec_monoid_rng_of_frac𝟭rec_monoid_rng_of_frac= x"
    using right_unit_mult_rng_of_frac
    by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
qed

lemma comm_mult_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) rec_monoid_rng_of_frac(r' |rels') = (r' |rels') rec_monoid_rng_of_frac(r |rels)"
proof-
  have f1:"(r |rels) rec_monoid_rng_of_frac(r' |rels') = (r  r' |rels  s')"
    using assms mult_rng_of_frac_fundamental_lemma 
    by simp
  have f2:"(r' |rels') rec_monoid_rng_of_frac(r |rels) = (r'  r |rels'  s)"
    using assms mult_rng_of_frac_fundamental_lemma 
    by simp
  have f3:"r  r' = r'  r"
    using assms rel_def m_comm 
    by simp
  have f4:"s  s' = s'  s"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  thus ?thesis
    using f1 f2 f3 f4 
    by simp
qed

lemma comm_monoid_rng_of_frac:
  shows "comm_monoid (rec_monoid_rng_of_frac)"
  using comm_monoid_def Group.comm_monoid_axioms_def monoid_rng_of_frac comm_mult_rng_of_frac
  by (smt mem_Collect_eq partial_object.select_convs(1) rec_monoid_rng_of_frac_def set_eq_class_of_rng_of_frac_def)

definition add_rng_of_frac:: "[_set, _set]  _set"
  where "add_rng_of_frac X Y  
let x' = (SOME x. x  X) in 
let y' = (SOME y. y  Y) in 
(snd y'  fst x'  snd x'  fst y') |rel(snd x'  snd y')"

definition rec_rng_of_frac:: "_ ring"
  where "rec_rng_of_frac  
carrier = set_class_ofrel, mult = mult_rng_of_frac, one = (𝟭|rel𝟭), zero = (𝟬 |rel𝟭), add = add_rng_of_frac "

lemma add_rng_of_frac_fundamental_lemma:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
proof-
  have "x'  (r |rels). y'  (r' |rels'). (r |rels) rec_rng_of_frac(r' |rels') = 
    (snd y'  fst x'  snd x'  fst y' |relsnd x'  snd y')"
    using assms rec_rng_of_frac_def add_rng_of_frac_def[of "(r |rels)" "(r' |rels')"]
    by (metis non_empty_class ring_record_simps(12) some_in_eq)
  then obtain x' and y' where f1:"x'  (r |rels)" and f2:"y'  (r' |rels')" and 
    f3:"(r |rels) rec_rng_of_frac(r' |rels') = (snd y'  fst x'  snd x'  fst y' |relsnd x'  snd y')"
    by auto
  then have "(r, s) .=relx'"
    using f1 rel_def eq_class_of_rng_of_frac_def[of rel r s]
    by auto
  then obtain t where f4:"t  S" and f5:"t  (snd x'  r  s  fst x') = 𝟬"
    using rel_def 
    by auto
  have "(r', s') .=rely'"
    using f2 rel_def eq_class_of_rng_of_frac_def[of rel r' s']
    by auto
  then obtain t' where f6:"t'  S" and f7:"t'  (snd y'  r'  s'  fst y') = 𝟬"
    using rel_def 
    by auto
  then have f8:"t  t'  S"
    using m_closed f4 f6
    by simp
  then have "(s'  r  s  r', s  s') .=rel(snd y'  fst x'  snd x'  fst y', snd x'  snd y')"
  proof-
    have f9:"t'  s'  snd y'  carrier R"
      using f6 assms(2) f2 subset rev_subsetD eq_class_of_rng_of_frac_def rel_def 
      by fastforce
    have f10:"snd x'  r  carrier R"
      using assms(1) f1 rel_def subset rev_subsetD
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
    have f11:"s  fst x'  carrier R"
      using assms(1) subset rev_subsetD f1 rel_def
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3)) 
    have "t  (snd x'  r  s  fst x') = t  (snd x'  r)  t  (s  fst x')"
      using f9 f10 f11 f4 subset rev_subsetD r_distr[of "snd x'  r" "s  fst x'" t] a_minus_def 
        r_minus[of t "s  fst x'"]
      by (smt add.inv_closed monoid.m_closed monoid_axioms r_distr)
    then have f12:"(t'  s'  snd y')  (t  (snd x'  r  s  fst x')) =
      t'  s'  snd y'  t  (snd x'  r)  (t'  s'  snd y'  t  (s  fst x'))"
      using f9 r_distr[of _ _ "t'  s'  snd y'"] rel_def r_minus a_minus_def
      by (smt abelian_group.minus_to_eq f10 f11 f4 f5 is_abelian_group m_assoc monoid.m_closed 
          monoid_axioms r_neg r_null subset subset_iff)
    have f13:"(snd x'  snd y')  (s'  r)  carrier R"
      using assms f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    have f14:"(s  s')  (snd y'  fst x')  carrier R"
      using assms f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    then have "(t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')) =
      (t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))"
      using f13 f14 f8 subset rev_subsetD r_distr rel_def r_minus a_minus_def
      by (smt add.inv_closed semiring_simprules(3))
    have f15:"s  s'  carrier R"
      using assms rel_def subset rev_subsetD 
      by auto
    have f16:"snd y'  fst x'  carrier R"
      using f1 f2 rel_def subset rev_subsetD[of _ S] monoid.m_closed[of R "snd y'" "fst x'"]
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff monoid_axioms partial_object.select_convs(1))
    have f17:"t  carrier R"
      using f4 subset rev_subsetD 
      by auto
    have f18:"t'  carrier R"
      using f6 subset rev_subsetD 
      by auto
    have f19:"s  carrier R"
      using assms(1) rel_def subset 
      by auto
    have f20:"s'  carrier R"
      using assms(2) rel_def subset 
      by auto
    have f21:"snd y'  carrier R"
      using f2 rel_def subset rev_subsetD
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1))
    have f22:"fst x'  carrier R"
      using f1 rel_def
      by (metis (no_types, lifting) Product_Type.Collect_case_prodD eq_class_of_rng_of_frac_def mem_Sigma_iff 
          partial_object.select_convs(1))
    then have f23:"(t  t')  ((s  s')  (snd y'  fst x')) = t'  s'  snd y'  t  (s  fst x')"
      using f17 f18 f19 f20 f21 m_assoc m_comm 
      by (smt BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f1 f4 f6 mem_Sigma_iff 
          partial_object.select_convs(1) rel_def semiring_simprules(3) subset_iff) 
    have f24:"(t  t')  ((snd x'  snd y')  (s'  r)) = t'  s'  snd y'  t  (snd x'  r)"
      using f17 f18 f20 f21 m_assoc m_comm
      by (smt BNF_Def.Collect_case_prodD assms(1) eq_class_of_rng_of_frac_def f1 f2 f4 f6 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff) 
    then have "(t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))=
      (t'  s'  snd y'  t  (snd x'  r))  (t'  s'  snd y'  t  (s  fst x'))"
      using f23 f24 
      by simp
    then have f25:"(t'  s'  snd y')  (t  (snd x'  r  s  fst x')) = 
      (t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))"
      using f12 
      by simp
    have f26:"(t  t')  ((snd x'  snd y')  (s  r'))  (t  t')  ((s  s')  (snd x'  fst y')) =
      t  s  snd x'  t'  (snd y'  r')  (t  s  snd x'  t'  (s'  fst y'))"
      by (smt BNF_Def.Collect_case_prodD assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 f19 f2 
          m_assoc m_comm mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def subset subset_iff)
    have f27:"snd y'  r'  carrier R"
      using assms(2) f21 rel_def 
      by auto
    have f28:"s'  fst y'  carrier R"
      using f20 assms(2)
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f2 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def)
    then have "t'  (snd y'  r'  s'  fst y') = t'  (snd y'  r')  t'  (s'  fst y')"
      using f18 f27 f28 r_minus[of t' "s'  fst y'"]
      by (simp add: a_minus_def r_distr)
    then have f29:"(t  s  snd x')  (t'  (snd y'  r'  s'  fst y')) = 
      (t  s  snd x')  (t'  (snd y'  r')  t'  (s'  fst y'))"
      by simp
    have "t  s  snd x'  carrier R"
      using f17 f19 f1 subset assms(1) eq_class_of_rng_of_frac_def f4 rel_def 
      by fastforce
    then have f30:"(t  s  snd x')  (t'  (snd y'  r'  s'  fst y')) = 
      (t  t')  ((snd x'  snd y')  (s  r'))  (t  t')  ((s  s')  (snd x'  fst y'))"
      using f26 f29 r_distr
      by (smt t'  (snd y'  r'  s'  fst y') = t'  (snd y'  r')  t'  (s'  fst y') 
          a_minus_def abelian_group.minus_to_eq f18 f27 f28 f7 is_abelian_group m_assoc monoid.m_closed 
          monoid_axioms r_neg semiring_simprules(15))
    then have f31:"((t'  s'  snd y')  (t  (snd x'  r  s  fst x')))  ((t  s  snd x')  (t'  (snd y'  r'  s'  fst y')))
      = ((t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x')))  
      ((t  t')  ((snd x'  snd y')  (s  r'))  (t  t')  ((s  s')  (snd x'  fst y')))"
      using f25 f30 
      by simp
    have f32:"(t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))
      = (t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))"
      using f17 f18 r_distr
      by (simp add: t  t'  (snd x'  snd y'  (s'  r)  s  s'  (snd y'  fst x')) = t  t'  (snd x'  snd y'  (s'  r))  t  t'  (s  s'  (snd y'  fst x')))
    have f33:"(t  t')  ((snd x'  snd y')  (s  r'))  (t  t')  ((s  s')  (snd x'  fst y')) =
      (t  t')  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y'))"
      using r_distr[of _ _ "t  t'"] f17 f18 a_minus_def r_minus
      by (smt BNF_Def.Collect_case_prodD abelian_group.a_inv_closed assms(1) assms(2) 
          eq_class_of_rng_of_frac_def f1 f2 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    have f34:"(snd x'  snd y')  (s'  r  s  r') = (snd x'  snd y')  (s'  r)  (snd x'  snd y')  (s  r')"
      using r_distr
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def 
          f1 f2 mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) rel_def 
          subset subset_iff)
    then have "(t  t')  ((snd x'  snd y')  (s'  r  s  r')) = 
      (t  t')  (snd x'  snd y')  (s'  r)  (t  t')  (snd x'  snd y')  (s  r')"
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 
          f2 m_assoc mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) 
          r_distr rel_def subset subset_iff)
    have f35:"(s  s')  (snd y'  fst x'  snd x'  fst y') = (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      using r_distr f19 f20
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def f1 f2 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    then have f36:"(t  t')  (s  s')  (snd y'  fst x'  snd x'  fst y') = 
      (t  t')  (s  s')  (snd y'  fst x')  (t  t')  (s  s')  (snd x'  fst y')"
      by (smt BNF_Def.Collect_case_prodD assms(1) assms(2) eq_class_of_rng_of_frac_def f1 f17 f18 f2 
          mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) r_distr rel_def 
          subset subset_iff)
    have f37:"(t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))  carrier R"
      by (simp add: f13 f14 f17 f18)
    have f38:"(t  t')  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y'))  carrier R"
      using t  s  snd x'  carrier R f30 f33 f7 zero_closed 
      by auto
    have f39:"(t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))  carrier R"
      by (simp add: f32 f37)
    have "snd x'  snd y'  carrier R"
      using f1 f2 subset rev_subsetD
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD eq_class_of_rng_of_frac_def 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3))
    have "(t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')) 
      (t  t')  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')) =
      (t  t')  ((snd x'  snd y')  (s'  r))  (t  t')  ((s  s')  (snd y'  fst x'))  
      (t  t')  ((snd x'  snd y')  (s  r'))  (t  t')  ((s  s')  (snd x'  fst y'))"
      using f32 f33 snd x'  snd y'  carrier R t  s  snd x'  carrier R assms(2) f17 f18 f19 
        f25 f30 f5 f7 f9 l_zero r_null rel_def zero_closed 
      apply clarsimp
      using l_zero semiring_simprules(3) by presburger
    then have f40:"((t'  s'  snd y')  (t  (snd x'  r  s  fst x')))  
      ((t  s  snd x')  (t'  (snd y'  r'  s'  fst y'))) = 
      ((t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')))  
      ((t  t')  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')))"
      using f31
      by (simp add: f32 f33)
    have f41:"(snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')  carrier R"
      by (simp add: f13 f14)
    have f42:"(snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')  carrier R"
      by (smt BNF_Def.Collect_case_prodD abelian_group.minus_closed assms(1) assms(2) 
          eq_class_of_rng_of_frac_def f1 f2 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) 
          rel_def semiring_simprules(3) subset subset_iff)
    then have "(t'  s'  snd y')  (t  (snd x'  r  s  fst x'))  
      (t  s  snd x')  (t'  (snd y'  r'  s'  fst y')) = 
      (t  t')  (((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')))"
      using r_distr[of "(snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')" "(snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')" "t  t'"]
      f17 f18  f40 f41 f42 
      by simp
    have "(snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')  (snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y') =
      (snd x'  snd y')  (s'  r)  (snd x'  snd y')  (s  r')  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      using four_elem_comm[of "(snd x'  snd y')  (s'  r)" "(snd x'  snd y')  (s  r')" "(s  s')  (snd y'  fst x')" "(s  s')  (snd x'  fst y')"]
      by (smt BNF_Def.Collect_case_prodD assms eq_class_of_rng_of_frac_def f1 f2 
          mem_Sigma_iff partial_object.select_convs(1) rel_def semiring_simprules(3) subset subset_iff)
    then have "(snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')  (snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y') =
      ((snd x'  snd y')  (s'  r)  (snd x'  snd y')  (s  r'))  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      by blast
    then have f43:"(snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')  (snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y') =
      (snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      using f34 
      by simp
    have "(snd x'  snd y')  (s  r')  carrier R"
      using snd x'  snd y'  carrier R assms(2) f19 rel_def 
      by auto
    have "(s  s')  (snd x'  fst y')  carrier R"
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms 
          eq_class_of_rng_of_frac_def f1 f2 mem_Sigma_iff partial_object.select_convs(1) rel_def 
          semiring_simprules(3) subset subset_iff)
    then have f43bis:"((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')) =
      (snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      using a_assoc a_minus_def f41 f43
      by (smt snd x'  snd y'  (s  r')  carrier R add.l_inv_ex add.m_closed minus_equality)
    have f44:"s  s'  (snd y'  fst x')  carrier R"
      by (simp add: f14)
    have f45:"s  s'  (snd x'  fst y')  carrier R"
      by (metis (no_types, lifting) BNF_Def.Collect_case_prodD assms 
          eq_class_of_rng_of_frac_def f1 f2 mem_Sigma_iff partial_object.select_convs(1) rel_def 
          semiring_simprules(3) subset subset_iff)
    then have " ((s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')) =
       ((s  s')  (snd y'  fst x'))  ((s  s')  (snd x'  fst y'))"
      using f44 f45 inv_add  
      by auto
    then have " ((s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')) =
       (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y')"
      using l_minus[of "s  s'"]
      by (simp add: a_minus_def f15 f16 f45)
    then have "(snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y') =
      (snd x'  snd y')  (s'  r  s  r')  ((s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y'))"
      using right_inv_add snd x'  snd y'  carrier R assms(2) f13 f19 f34 f44 f45 rel_def 
      by auto
    then have "(snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x')  (s  s')  (snd x'  fst y') =
      (snd x'  snd y')  (s'  r  s  r')  ((s  s')  (snd y'  fst x'  snd x'  fst y'))"
      using r_distr
      by (simp add: f35)
    then have "((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')) 
      = (snd x'  snd y')  (s'  r  s  r')  ((s  s')  (snd y'  fst x'  snd x'  fst y'))"
      using f43bis 
      by simp
    then have "(t  t')  (((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x'))  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')))
      = (t  t')  ((snd x'  snd y')  (s'  r  s  r')  ((s  s')  (snd y'  fst x'  snd x'  fst y')))"
      by simp
    then have "(t  t')  ((snd x'  snd y')  (s'  r)  (s  s')  (snd y'  fst x')) 
      (t  t')  ((snd x'  snd y')  (s  r')  (s  s')  (snd x'  fst y')) =
      (t  t')  ((snd x'  snd y')  (s'  r  s  r')  ((s  s')  (snd y'  fst x'  snd x'  fst y')))"
      using r_distr[of _ _ "t  t'"] f17 f18 t'  s'  snd y'  (t  (snd x'  r  s  fst x'))  t  s  snd x'  (t'  (snd y'  r'  s'  fst y')) = t  t'  (snd x'  snd y'  (s'  r)  s  s'  (snd y'  fst x')  (snd x'  snd y'  (s  r')  s  s'  (snd x'  fst y'))) f40 
      by auto
    then have "(t'  s'  snd y')  (t  (snd x'  r  s  fst x'))  
      (t  s  snd x')  (t'  (snd y'  r'  s'  fst y')) = 
      (t  t')  ((snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x'  snd x'  fst y'))"
      using f40 
      by simp
    then have "(t  t')  ((snd x'  snd y')  (s'  r  s  r')  (s  s')  (snd y'  fst x'  snd x'  fst y')) = 𝟬"
      using f5 f7
      by (simp add: t  s  snd x'  carrier R f9)
    thus ?thesis
      using rel_def f8 
      by auto
  qed
  then have "(s'  r  s  r' |rels  s') = (snd y'  fst x'  snd x'  fst y' |relsnd x'  snd y')"
  proof-
    have "(s'  r  s  r', s  s')  carrier rel"
      using assms rel_def submonoid.m_closed
      by (smt add.m_closed m_closed mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1) 
          rev_subsetD subset)
    have "(snd y'  fst x'  snd x'  fst y', snd x'  snd y')  carrier rel"
      using rel_def f1 f2 subset submonoid.m_closed eq_class_of_rng_of_frac_def
      by (smt Product_Type.Collect_case_prodD add.m_closed mem_Sigma_iff member_class_to_carrier 
          partial_object.select_convs(1) semiring_simprules(3) rev_subsetD)
    thus ?thesis
      using elem_eq_class[of rel] equiv_obj_rng_of_frac
      by (metis (s'  r  s  r', s  s') .=rel(snd y'  fst x'  snd x'  fst y', snd x'  snd y') 
          (s'  r  s  r', s  s')  carrier rel class_of_to_rel)
  qed
  thus ?thesis
    using f3 
    by simp
qed

lemma closed_add_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) rec_rng_of_frac(r' |rels')  set_class_ofrel⇙"
proof-
  have f1:"(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  have f2:"s'  r  s  r'  carrier R"
    using assms rel_def
    by (metis (no_types, lifting) add.m_closed mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rev_subsetD subset)
  have f3:"s  s'  S"
    using assms rel_def submonoid.m_closed 
    by simp
  from f2 and f3 have "(s'  r  s  r', s  s')  carrier rel"
    by (simp add: rel_def)
  thus ?thesis
    using set_eq_class_of_rng_of_frac_def f1 
    by auto
qed

lemma closed_rel_add:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(s'  r  s  r', s  s')  carrier rel"
proof-
  have "s  s'  S"
    using assms rel_def submonoid.m_closed 
    by simp
  have "s'  r  s  r'  carrier R"
    using assms rel_def
    by (metis (no_types, lifting) add.m_closed mem_Sigma_iff monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) rev_subsetD subset)
  thus ?thesis
    using rel_def
    by (simp add: s  s'  S)
qed

lemma assoc_add_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel" and "(r'', s'')  carrier rel"
  shows "(r |rels) rec_rng_of_frac(r' |rels') rec_rng_of_frac(r''|rels'') =
  (r |rels) rec_rng_of_frac((r' |rels') rec_rng_of_frac(r'' |rels''))"
proof-
  have "(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"(r |rels) rec_rng_of_frac(r' |rels') rec_rng_of_frac(r''|rels'') =
    (s''  (s'  r  s  r')  (s  s')  r'' |rel(s  s')  s'')"
    using assms add_rng_of_frac_fundamental_lemma closed_rel_add 
    by simp
  have "(r' |rels') rec_rng_of_frac(r'' |rels'') = (s''  r'  s'  r'' |rels'  s'')"
    using assms(2) assms(3) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f2:"(r |rels) rec_rng_of_frac((r' |rels') rec_rng_of_frac(r'' |rels'')) =
    ((s'  s'')  r  s  (s''  r'  s'  r'') |rels  (s'  s''))"
    using assms add_rng_of_frac_fundamental_lemma closed_rel_add 
    by simp
  have f3:"(s  s')  s'' = s  (s'  s'')"
    using m_assoc subset assms rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1) rev_subsetD)
  have "s''  (s'  r  s  r')  (s  s')  r'' = (s'  s'')  r  s  (s''  r'  s'  r'')"
    by (smt a_assoc assms m_comm mem_Sigma_iff monoid.m_assoc monoid.m_closed monoid_axioms 
        partial_object.select_convs(1) r_distr rel_def subset subset_iff)
  thus ?thesis
    using f1 f2 f3 
    by simp
qed

lemma add_rng_of_frac_zero:
  shows "(𝟬 |rel𝟭)  set_class_ofrel⇙"
  by (metis (no_types, lifting) closed_mult_rng_of_frac mem_Sigma_iff monoid.simps(2) one_closed 
      partial_object.select_convs(1) rec_monoid_rng_of_frac_def rel_def right_unit_mult_rng_of_frac semiring_simprules(4) zero_closed)

lemma l_unit_add_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "𝟬rec_rng_of_fracrec_rng_of_frac(r |rels) = (r |rels)"
proof-
  have "(𝟬 |rel𝟭) rec_rng_of_frac(r |rels) = (s  𝟬  𝟭  r |rel𝟭  s)"
    using assms add_rng_of_frac_fundamental_lemma
    by (simp add: rel_def)
  then have "(𝟬 |rel𝟭) rec_rng_of_frac(r |rels) = (r |rels)"
    using assms rel_def subset 
    by auto
  thus ?thesis
    using rec_rng_of_frac_def 
    by simp
qed

lemma r_unit_add_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "(r |rels) rec_rng_of_frac𝟬rec_rng_of_frac= (r |rels)"
proof-
  have "(r |rels) rec_rng_of_frac(𝟬 |rel𝟭) = (𝟭  r  s  𝟬 |rels  𝟭)"
    using assms add_rng_of_frac_fundamental_lemma
    by (simp add: rel_def)
  then have "(r |rels) rec_rng_of_frac(𝟬 |rel𝟭) = (r |rels)"
    using assms rel_def subset 
    by auto
  thus ?thesis
    using rec_rng_of_frac_def 
    by simp
qed

lemma comm_add_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel"
  shows "(r |rels) rec_rng_of_frac(r' |rels') = (r' |rels') rec_rng_of_frac(r |rels)"
proof-
  have f1:"(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
 have f2:"(r' |rels') rec_rng_of_frac(r |rels) = (s  r'  s'  r |rels'  s)"
   using assms add_rng_of_frac_fundamental_lemma 
   by simp
  thus ?thesis
    using f1 f2
    by (metis (no_types, lifting) add.m_comm assms(1) assms(2) m_comm mem_Sigma_iff 
        partial_object.select_convs(1) rel_def semiring_simprules(3) rev_subsetD subset)
qed

lemma class_of_zero_rng_of_frac:
  assumes "s  S"
  shows "(𝟬 |rels) = 𝟬rec_rng_of_frac⇙"
proof-
  have f1:"(𝟬, s)  carrier rel"
    using assms rel_def 
    by simp
  have "𝟭  (𝟭  𝟬  s  𝟬) = 𝟬"
    using assms local.ring_axioms rev_subsetD ring.ring_simprules(14) subset 
    by fastforce
  then have "(𝟬, s) .=rel(𝟬, 𝟭)"
    using rel_def submonoid.one_closed 
    by auto
  thus ?thesis
    using elem_eq_class equiv_obj_rng_of_frac f1 rec_rng_of_frac_def
    by (metis (no_types, lifting) class_of_to_rel mem_Sigma_iff one_closed partial_object.select_convs(1) 
        rel_def ring_record_simps(11))
qed

lemma r_inv_add_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "(r |rels) rec_rng_of_frac( r |rels) = 𝟬rec_rng_of_frac⇙"
proof-
  have "( r, s)  carrier rel"
    using assms rel_def 
    by simp
  then have "(r |rels) rec_rng_of_frac( r |rels) = (s  r  s   r |rels  s)"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  then have "(r |rels) rec_rng_of_frac( r |rels) = (𝟬 |rels  s)"
    using r_minus[of s r] assms rel_def subset rev_subsetD r_neg 
    by auto
  thus ?thesis
    using class_of_zero_rng_of_frac assms rel_def submonoid.m_closed 
    by simp
qed

lemma l_inv_add_rng_of_frac:
  assumes "(r, s)  carrier rel"
  shows "( r |rels) rec_rng_of_frac(r |rels) = 𝟬rec_rng_of_frac⇙"
proof-
  have "( r, s)  carrier rel"
    using assms rel_def 
    by simp
  then have "( r |rels) rec_rng_of_frac(r |rels) = (s   r  s  r |rels  s)"
    using assms add_rng_of_frac_fundamental_lemma 
    by simp
  then have "( r |rels) rec_rng_of_frac(r |rels) = (𝟬 |rels  s)"
    using r_minus[of s r] assms rel_def subset rev_subsetD l_neg 
    by auto
  thus ?thesis
    using class_of_zero_rng_of_frac assms rel_def submonoid.m_closed 
    by simp
qed

lemma abelian_group_rng_of_frac:
  shows "abelian_group (rec_rng_of_frac)"
proof
  show "x y. x  carrier (add_monoid rec_rng_of_frac);
            y  carrier (add_monoid rec_rng_of_frac)
            x add_monoid rec_rng_of_fracy
                carrier (add_monoid rec_rng_of_frac)"
    using closed_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "x y z.
       x  carrier (add_monoid rec_rng_of_frac);
        y  carrier (add_monoid rec_rng_of_frac);
        z  carrier (add_monoid rec_rng_of_frac)
        x add_monoid rec_rng_of_fracy add_monoid rec_rng_of_fracz =
           x add_monoid rec_rng_of_frac(y add_monoid rec_rng_of_fracz)"
    using assoc_add_rng_of_frac
    by (smt mem_Collect_eq monoid.simps(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "𝟭add_monoid rec_rng_of_frac carrier (add_monoid rec_rng_of_frac)"
    using add_rng_of_frac_zero by (simp add: rec_rng_of_frac_def)
  show "x. x  carrier (add_monoid rec_rng_of_frac) 
         𝟭add_monoid rec_rng_of_fracadd_monoid rec_rng_of_fracx = x"
    using l_unit_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) 
        rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "x. x  carrier (add_monoid rec_rng_of_frac) 
         x add_monoid rec_rng_of_frac𝟭add_monoid rec_rng_of_frac= x"
    using r_unit_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) monoid.select_convs(2) partial_object.select_convs(1) 
        rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def)
  show "x y. x  carrier (add_monoid rec_rng_of_frac); y  carrier (add_monoid rec_rng_of_frac)
            x add_monoid rec_rng_of_fracy = y add_monoid rec_rng_of_fracx"
    using comm_add_rng_of_frac
    by (smt mem_Collect_eq monoid.select_convs(1) partial_object.select_convs(1) rec_rng_of_frac_def 
        set_eq_class_of_rng_of_frac_def)
  show "carrier (add_monoid rec_rng_of_frac)  Units (add_monoid rec_rng_of_frac)"
  proof
    show "x  Units (add_monoid rec_rng_of_frac)" if "x  carrier (add_monoid rec_rng_of_frac)" for x
    proof-
      have "x  set_class_ofrel⇙"
        using that rec_rng_of_frac_def by simp
      then obtain r and s where f1:"(r, s)  carrier rel" and f2:"x = (r |rels)"
        using set_eq_class_of_rng_of_frac_def
        by (smt mem_Collect_eq)
      then have f3:"(r |rels) rec_rng_of_frac( r |rels) = 𝟬rec_rng_of_frac⇙"
        using f1 r_inv_add_rng_of_frac[of r s] 
        by simp
      have f4:"( r |rels) rec_rng_of_frac(r |rels) = 𝟬rec_rng_of_frac⇙"
        using f1 l_inv_add_rng_of_frac[of r s] 
        by simp
      then have "y  set_class_ofrel. y rec_rng_of_fracx = 𝟬rec_rng_of_frac x rec_rng_of_fracy = 𝟬rec_rng_of_frac⇙"
        using f2 f3 f4
        by (metis (no_types, lifting) abelian_group.a_inv_closed class_of_zero_rng_of_frac 
            closed_add_rng_of_frac f1 is_abelian_group mem_Sigma_iff partial_object.select_convs(1) 
            rel_def r_unit_add_rng_of_frac zero_closed) 
      thus "x  Units (add_monoid rec_rng_of_frac)"
        using rec_rng_of_frac_def that by (simp add: Units_def)
    qed
  qed
qed

lemma r_distr_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel" and "(r'', s'')  carrier rel"
  shows "((r |rels) rec_rng_of_frac(r' |rels')) rec_rng_of_frac(r'' |rels'') = 
    (r |rels) rec_rng_of_frac(r'' |rels'') rec_rng_of_frac(r' |rels') rec_rng_of_frac(r'' |rels'')"
proof-
  have "(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"((r |rels) rec_rng_of_frac(r' |rels')) rec_rng_of_frac(r'' |rels'') =
    ((s'  r  s  r')  r'' |rel(s  s')  s'')"
    using assms mult_rng_of_frac_fundamental_lemma
    by (simp add: closed_rel_add rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f2:"(r |rels) rec_rng_of_frac(r'' |rels'') = (r  r'' |rels  s'')"
    using assms(1) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f3:"(r' |rels') rec_rng_of_frac(r'' |rels'') = (r'  r'' |rels'  s'')"
    using assms(2) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f4:"(r  r'', s  s'')  carrier rel"
    using rel_def assms(1) assms(3) submonoid.m_closed 
    by simp
  have f5:"(r'  r'', s'  s'')  carrier rel"
    using rel_def assms(2) assms(3) submonoid.m_closed 
    by simp
  from f2 and f3 have f6:"(r |rels) rec_rng_of_frac(r'' |rels'') rec_rng_of_frac(r' |rels') rec_rng_of_frac(r'' |rels'')
    = ((s'  s'')  (r  r'')  (s  s'')  (r'  r'') |rel(s  s'')  (s'  s''))"
    using assms f4 f5 submonoid.m_closed add_rng_of_frac_fundamental_lemma 
    by simp
  have "(s  s''  (s'  s''))  ((s'  r  s  r')  r'') = (s  s''  (s'  s''))  (s'  r   r''  s  r'  r'')"
    using assms rel_def subset rev_subsetD l_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have f7:"(s  s''  (s'  s''))  ((s'  r  s  r')  r'') = 
    (s  s''  (s'  s''))  (s'  r   r'')  (s  s''  (s'  s''))  (s  r'  r'')"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  have f8:"(s  s'  s'')  (s'  s''  (r  r'')  s  s''  (r'  r'')) = 
    (s  s'  s'')  (s'  s''  (r  r''))  (s  s'  s'')  (s  s''  (r'  r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s  s''  (s'  s'')) = (s  (s''  s')  s'')"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f9:"(s  s''  (s'  s'')) = (s  s'  (s''  s''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f10:"(s  s''  (s'  s''))  (s'  r   r'') = (s  s'  s'')  (s'  s''  (r  r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc m_comm
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s  s''  (r'  r'')) = (s''  s  (r'  r''))"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s  s''  (s'  s''))  (s  r'  r'') = (s  s'  s'')  (s  s''  (r'  r''))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc f9
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have "((s  s''  (s'  s''))  ((s'  r  s  r')  r'') = (s  s'  s'')  (s'  s''  (r  r'')  s  s''  (r'  r'')))"
    using  f7 f8 f10 
    by presburger
  then have "((s  s''  (s'  s''))  ((s'  r  s  r')  r'')  (s  s'  s'')  (s'  s''  (r  r'')  s  s''  (r'  r''))) = 𝟬"
    by (smt a_minus_def assms(1) assms(2) assms(3) closed_rel_add mem_Sigma_iff 
        partial_object.select_convs(1) r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have f11:"𝟭  (((s  s''  (s'  s''))  ((s'  r  s  r')  r'')  (s  s'  s'')  (s'  s''  (r  r'')  s  s''  (r'  r'')))) = 𝟬"
    by simp
  have f12:"((s'  r  s  r')  r'', s  s'  s'')  carrier rel"
    using assms closed_rel_add rel_def 
    by auto
  have f13:"(s'  s''  (r  r'')  s  s''  (r'  r''), s  s''  (s'  s''))  carrier rel"
    by (simp add: closed_rel_add f4 f5)
  have "𝟭  S"
    using submonoid.one_closed 
    by simp
  then have "((s'  r  s  r')  r'', s  s'  s'') .=rel(s'  s''  (r  r'')  s  s''  (r'  r''), s  s''  (s'  s''))"
    using rel_def f11 f13 f12 
    by auto
  then have "((s'  r  s  r')  r''|rels  s'  s'') = (s'  s''  (r  r'')  s  s''  (r'  r'') |rels  s''  (s'  s''))"
    using elem_eq_class
    by (metis class_of_to_rel equiv_obj_rng_of_frac f12 f13)
  thus ?thesis
    using f1 f6 
    by simp
qed

lemma l_distr_rng_of_frac:
  assumes "(r, s)  carrier rel" and "(r', s')  carrier rel" and "(r'', s'')  carrier rel"
  shows "(r'' |rels'') rec_rng_of_frac((r |rels) rec_rng_of_frac(r' |rels')) = 
    (r'' |rels'') rec_rng_of_frac(r |rels) rec_rng_of_frac(r'' |rels'') rec_rng_of_frac(r' |rels')"
proof-
  have "(r |rels) rec_rng_of_frac(r' |rels') = (s'  r  s  r' |rels  s')"
    using assms(1) assms(2) add_rng_of_frac_fundamental_lemma 
    by simp
  then have f1:"(r'' |rels'') rec_rng_of_frac((r |rels) rec_rng_of_frac(r' |rels')) =
    (r''  (s'  r  s  r') |rels''  (s  s'))"
    using assms mult_rng_of_frac_fundamental_lemma
    by (simp add: closed_rel_add rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f2:"(r'' |rels'') rec_rng_of_frac(r |rels) = (r''  r |rels''  s)"
    using assms(1) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f3:"(r'' |rels'') rec_rng_of_frac(r' |rels') = (r''  r' |rels''  s')"
    using assms(2) assms(3) mult_rng_of_frac_fundamental_lemma
    by (simp add: rec_monoid_rng_of_frac_def rec_rng_of_frac_def)
  have f4:"(r''  r, s''  s)  carrier rel"
    using rel_def assms(1) assms(3) submonoid.m_closed 
    by simp
  have f5:"(r''  r', s''  s')  carrier rel"
    using rel_def assms(2) assms(3) submonoid.m_closed 
    by simp
  from f2 and f3 have f6:"(r'' |rels'') rec_rng_of_frac(r |rels) rec_rng_of_frac(r'' |rels'') rec_rng_of_frac(r' |rels')
    = ((s''  s')  (r''  r)  (s''  s)  (r''  r') |rel(s''  s)  (s''  s'))"
    using assms f4 f5 submonoid.m_closed add_rng_of_frac_fundamental_lemma 
    by simp
  have "(s''  s  (s''  s'))  (r''  (s'  r  s  r')) = (s''  s  (s''  s'))  (r''  (s'  r)  r''  (s  r'))"
    using assms rel_def subset rev_subsetD r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have f7:"(s''  s  (s''  s'))  (r''  (s'  r  s  r')) = 
    (s''  s  (s''  s'))  (r''  (s'  r))  (s''  s  (s''  s'))  (r''  (s  r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  have f8:"(s''  s  s')  (s''  s'  (r''  r)  s''  s  (r''  r')) = 
    (s''  s  s')  (s''  s'  (r''  r))  (s''  s  s')  (s''  s  (r''  r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed r_distr
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s''  s  (s''  s')) = (s''  (s  s'')  s')"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f9:"(s''  s  (s''  s')) = (s''  s''  (s  s'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  then have f10:"(s''  s  (s''  s'))  (r''  s'  r) = (s''  s  s')  (s''  s'  (r''  r))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_assoc m_comm
    by (smt mem_Sigma_iff partial_object.select_convs(1) semiring_simprules(3))
  have "(s''  s  (r''  r')) = (s  s''  (r''  r'))"
    using assms rel_def subset rev_subsetD m_comm
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s''  s  (s''  s'))  (r''  s  r') = (s''  s  s')  (s''  s  (r''  r'))"
    using assms rel_def subset rev_subsetD submonoid.m_closed m_comm m_assoc f9
    by (smt mem_Sigma_iff monoid.m_closed monoid_axioms partial_object.select_convs(1))
  then have "((s''  s  (s''  s'))  (r''  (s'  r  s  r')) = (s''  (s  s'))  (s''  s'  (r''  r)  s''  s  (r''  r')))"
    using  f7 f8 f10
    by (smt assms(1) assms(2) assms(3) m_assoc mem_Sigma_iff partial_object.select_convs(1) rel_def 
        rev_subsetD subset)
  then have "((s''  s  (s''  s'))  (r''  (s'  r  s  r'))  (s''  (s  s'))  (s''  s'  (r''  r)  s''  s  (r''  r'))) = 𝟬"
    by (smt a_minus_def assms(1) assms(2) assms(3) closed_rel_add mem_Sigma_iff partial_object.select_convs(1) 
        r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have f11:"𝟭  (((s''  s  (s''  s'))  (r''  (s'  r  s  r'))  (s''  (s  s'))  (s''  s'  (r''  r)  s''  s  (r''  r')))) = 𝟬"
    by simp
  have f12:"(r''  (s'  r  s  r'), s''  (s  s'))  carrier rel"
    using assms closed_rel_add rel_def 
    by auto
  have f13:"(s''  s'  (r''  r)  s''  s  (r''  r'), s''  s  (s''  s'))  carrier rel"
    by (simp add: closed_rel_add f4 f5)
  have "𝟭  S"
    using submonoid.one_closed 
    by simp
  then have "(r''  (s'  r  s  r'), s''  (s  s')) .=rel(s''  s'  (r''  r)  s''  s  (r''  r'), s''  s  (s''  s'))"
    using rel_def f11 f13 f12 
    by auto
  then have "(r''  (s'  r  s  r') |rels''  (s  s')) = (s''  s'  (r''  r)  s''  s  (r''  r') |rels''  s  (s''  s'))"
    using elem_eq_class
    by (metis class_of_to_rel equiv_obj_rng_of_frac f12 f13)
  thus ?thesis
    using f1 f6 
    by simp
qed

lemma rng_rng_of_frac:
  shows "ring (rec_rng_of_frac)"
proof-
  have f1:"x y z. x  carrier rec_rng_of_frac  y  carrier rec_rng_of_frac  z  carrier rec_rng_of_frac 
     (x rec_rng_of_fracy) rec_rng_of_fracz = x rec_rng_of_fracz rec_rng_of_fracy rec_rng_of_fracz"
    using r_distr_rng_of_frac rec_rng_of_frac_def
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  have f2:"x y z. x  carrier rec_rng_of_frac  y  carrier rec_rng_of_frac  z  carrier rec_rng_of_frac 
     z rec_rng_of_frac(x rec_rng_of_fracy) = z rec_rng_of_fracx rec_rng_of_fracz rec_rng_of_fracy"
    using l_distr_rng_of_frac rec_rng_of_frac_def
    by (smt mem_Collect_eq partial_object.select_convs(1) set_eq_class_of_rng_of_frac_def)
  then have "ring_axioms (rec_rng_of_frac)"
    using ring_axioms_def f1 f2 
    by auto
  thus ?thesis  
    using ring_def[of rec_rng_of_frac] abelian_group_rng_of_frac monoid_rng_of_frac rec_rng_of_frac_def 
      abelian_group_axioms_def rec_monoid_rng_of_frac_def eq_class_of_rng_of_frac_def
    by (simp add: Group.monoid_def)
qed

lemma crng_rng_of_frac:
  shows "cring (rec_rng_of_frac)"
  using cring_def[of rec_rng_of_frac] rng_rng_of_frac comm_monoid_rng_of_frac rec_rng_of_frac_def 
    rec_monoid_rng_of_frac_def eq_class_of_rng_of_frac_def
  by (metis (no_types, lifting) comm_monoid.m_comm monoid.monoid_comm_monoidI monoid.select_convs(1) 
      partial_object.select_convs(1) ring.is_monoid)

lemma simp_in_frac:
  assumes "(r, s)  carrier rel" and "s'  S"
  shows "(r |rels) = (s'  r |rels'  s)"
proof-
  have f1:"(s'  r, s'  s)  carrier rel"
    using assms rel_def submonoid.m_closed subset rev_subsetD 
    by auto
  have "(s'  s)  r  s  (s'  r) = (s'  s)  r  (s  s')  r"
    using assms subset rev_subsetD m_assoc[of s s' r] rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s'  s)  r  s  (s'  r) = (s'  s)  r  (s'  s)  r"
    using m_comm[of s s'] assms subset rev_subsetD rel_def
    by (metis (no_types, lifting) mem_Sigma_iff partial_object.select_convs(1))
  then have "(s'  s)  r  s  (s'  r) = 𝟬"
    by (metis (no_types, lifting) a_minus_def assms mem_Sigma_iff partial_object.select_convs(1) 
        r_neg rel_def semiring_simprules(3) rev_subsetD subset)
  then have "𝟭  ((s'  s)  r  s  (s'  r)) = 𝟬"
    by simp
  then have "(r, s) .=rel(s'  r, s'  s)"
    using assms(1) f1 rel_def one_closed 
    by auto
  thus ?thesis
    using elem_eq_class
    by (metis assms(1) class_of_to_rel equiv_obj_rng_of_frac f1)
qed

subsection ‹The Natural Homomorphism from a Ring to Its Localization›

definition rng_to_rng_of_frac :: "'a  ('a × 'a) set" where
"rng_to_rng_of_frac r  (r |rel𝟭)"

lemma rng_to_rng_of_frac_is_ring_hom :
  shows "rng_to_rng_of_frac  ring_hom R rec_rng_of_frac"
proof-
  have f1:"rng_to_rng_of_frac  carrier R  carrier rec_rng_of_frac"
    using rng_to_rng_of_frac_def rec_rng_of_frac_def set_eq_class_of_rng_of_frac_def rel_def 
    by fastforce
  have f2:"x y. x  carrier R  y  carrier R 
     rng_to_rng_of_frac (x Ry) = rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y"
  proof(rule allI, rule allI, rule impI)
    fix x y
    assume "x  carrier R  y  carrier R"
    have f1:"rng_to_rng_of_frac (x Ry) = (x  y |rel𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    have "rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y = (x |rel𝟭) rec_rng_of_frac(y |rel𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    then have "rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y = (x  y |rel𝟭)"
      using mult_rng_of_frac_fundamental_lemma
      by (simp add: x  carrier R  y  carrier R rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def)
    thus "rng_to_rng_of_frac (x Ry) = rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y"
      using f1 
      by auto
  qed
  have f3:"x y. x  carrier R  y  carrier R
     rng_to_rng_of_frac (x Ry) = rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y"
  proof(rule allI, rule allI, rule impI)
    fix x y
    assume a:"x  carrier R  y  carrier R"
    have f1:"rng_to_rng_of_frac (x Ry) = (x  y |rel𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    have "rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y = (x |rel𝟭) rec_rng_of_frac(y |rel𝟭)"
      using rng_to_rng_of_frac_def 
      by simp
    then have "rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y = (𝟭  x  𝟭  y |rel𝟭  𝟭)"
      using mult_rng_of_frac_fundamental_lemma a 
        eq_obj_rng_of_frac.add_rng_of_frac_fundamental_lemma eq_obj_rng_of_frac.rng_to_rng_of_frac_def 
        eq_obj_rng_of_frac_axioms f1 
      by fastforce
    then have "rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y = (x  y |rel𝟭)"
      using l_one a 
      by simp     
    thus "rng_to_rng_of_frac (x Ry) = rng_to_rng_of_frac x rec_rng_of_fracrng_to_rng_of_frac y"
      using f1 
      by auto
  qed
  have "rng_to_rng_of_frac 𝟭 = (𝟭 |rel𝟭)"
    using rng_to_rng_of_frac_def 
    by simp
  then have f4:"rng_to_rng_of_frac 𝟭R= 𝟭rec_rng_of_frac⇙"
    using rec_rng_of_frac_def 
    by simp
  thus ?thesis
    using ring_hom_def[of R rec_rng_of_frac] f1 f2 f3 f4 
    by simp
qed

lemma Im_rng_to_rng_of_frac_unit:
  assumes "x  rng_to_rng_of_frac ` S"
  shows "x  Units rec_rng_of_frac"
proof-
  obtain s where a1:"s  S" and a2:"x = (s |rel𝟭)"
    using assms rng_to_rng_of_frac_def rel_def
    by auto
  then have "(s |rel𝟭) rec_rng_of_frac(𝟭 |rels) = (s  𝟭 |rels  𝟭)"
    using mult_rng_of_frac_fundamental_lemma rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def subset 
    by auto
  then have f1:"(s |rel𝟭) rec_rng_of_frac(𝟭 |rels) = (𝟭 |rel𝟭)"
    using simp_in_frac a1 rel_def 
    by auto
  have "(𝟭 |rels) rec_rng_of_frac(s |rel𝟭) = (s  𝟭 |rels  𝟭)"
    using mult_rng_of_frac_fundamental_lemma rec_monoid_rng_of_frac_def rec_rng_of_frac_def rel_def 
      subset a1 
    by auto
  then have f2:"(𝟭 |rels) rec_rng_of_frac(s |rel𝟭) = (𝟭 |rel𝟭)"
    using simp_in_frac  a1 rel_def
    by auto
  then have f3:"ycarrier rec_rng_of_frac. y rec_rng_of_fracx = 𝟭rec_rng_of_frac 
    x rec_rng_of_fracy = 𝟭rec_rng_of_frac⇙"
    using rec_rng_of_frac_def f1 f2 a2 rel_def a1
    by (metis (no_types, lifting) class_of_zero_rng_of_frac closed_add_rng_of_frac l_unit_add_rng_of_frac 
        mem_Sigma_iff monoid.select_convs(2) partial_object.select_convs(1) semiring_simprules(4) zero_closed)
  have "x  carrier rec_rng_of_frac"
    using a2 a1 subset rev_subsetD rec_rng_of_frac_def
    by (metis (no_types, opaque_lifting) ring_hom_closed rng_to_rng_of_frac_def rng_to_rng_of_frac_is_ring_hom)
  thus ?thesis
    using Units_def[of rec_rng_of_frac] f3 
    by auto
qed

lemma eq_class_to_rel:
  assumes "(r, s)  carrier R × S" and "(r', s')  carrier R × S" and "(r |rels) = (r' |rels')"
  shows "(r, s) .=rel(r', s')"
proof-
  have "(r, s)  (r |rels)"
    using assms(1) equiv_obj_rng_of_frac equivalence_def
    by (metis (no_types, lifting) CollectI case_prodI eq_class_of_rng_of_frac_def 
        partial_object.select_convs(1) rel_def)
  then have "(r, s)  (r' |rels')"
    using assms(3) 
    by simp
  then have "(r', s') .=rel(r, s)"
    by (simp add: eq_class_of_rng_of_frac_def)
  thus ?thesis
    using equiv_obj_rng_of_frac equivalence_def
    by (metis (no_types, lifting) assms(1) assms(2) partial_object.select_convs(1) rel_def)
qed

lemma rng_to_rng_of_frac_without_zero_div_is_inj:
  assumes "𝟬  S" and "a  carrier R.b  carrier R. a  b = 𝟬  a = 𝟬  b = 𝟬"
  shows "a_kernel R rec_rng_of_frac rng_to_rng_of_frac = {𝟬}"
proof-
  have "{r carrier R. rng_to_rng_of_frac r = 𝟬rec_rng_of_frac}  {𝟬}"
  proof(rule subsetI)
    fix x
    assume a1:"x  {r  carrier R. rng_to_rng_of_frac r = 𝟬rec_rng_of_frac}"
    then have "(x, 𝟭) .=rel(𝟬, 𝟭)"
      using rng_to_rng_of_frac_def rec_rng_of_frac_def eq_class_to_rel 
      by simp
    then obtain t where f1:"t  S" and f2:"t  (𝟭  x  𝟭  𝟬) = 𝟬"
      using rel_def 
      by auto
    have f3:"x carrier R"
      using a1 
      by simp
    then have f4:"t  x = 𝟬"
      using l_one r_zero f2 
      by (simp add: a_minus_def)
    have "t  𝟬"
      using f1 assms(1) 
      by auto
    then have "x = 𝟬"
      using assms(2) f1 f3 f4 subset rev_subsetD 
      by auto
    thus "x  {𝟬}"
      by simp
  qed
  have "{𝟬}  {r carrier R. rng_to_rng_of_frac r = 𝟬rec_rng_of_frac}"
    using subsetI rng_to_rng_of_frac_def rec_rng_of_frac_def 
    by simp
  then have "{r carrier R. rng_to_rng_of_frac r = 𝟬rec_rng_of_frac} = {𝟬}"
    using {r carrier R. rng_to_rng_of_frac r = 𝟬rec_rng_of_frac}  {𝟬} 
    by auto
  thus ?thesis
    by (simp add: a_kernel_def kernel_def)
qed

end


end