Theory Ring_ZF_1

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES 
OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

section ‹More on rings›

theory Ring_ZF_1 imports Ring_ZF Group_ZF_3

begin

text‹This theory is devoted to the part of ring theory specific the 
  construction of real numbers in the ‹Real_ZF_x› series of theories. 
  The goal is to 
  show that classes of almost homomorphisms form a ring.›

subsection‹The ring of classes of almost homomorphisms›

text‹Almost homomorphisms do not form a ring as the regular homomorphisms 
  do because the lifted group operation is not distributive with respect to 
  composition -- we have $s\circ (r\cdot q) \neq s\circ r\cdot s\circ q$ in 
  general. However, we do have 
  $s\circ (r\cdot q) \approx s\circ r\cdot s\circ q$ in the sense of the 
  equivalence relation defined by the group of finite range
  functions (that is a normal subgroup of almost homomorphisms, 
  if the group is abelian). This allows to define a natural ring structure 
  on the classes of almost homomorphisms.›

text‹The next lemma provides a formula useful for proving that two sides 
  of the distributive law equation for almost homomorphisms are almost 
  equal.›

lemma (in group1) Ring_ZF_1_1_L1: 
  assumes A1: "s∈AH" "r∈AH" "q∈AH" and A2: "n∈G"
  shows 
  "((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
  "((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
proof -
  from groupAssum isAbelian A1 have T1:
    "r∙q ∈ AH" "s∘r ∈ AH"  "s∘q ∈ AH" "(s∘r)∙(s∘q) ∈ AH"
    "r∘s ∈ AH" "q∘s ∈ AH"  "(r∘s)∙(q∘s) ∈ AH"
    using Group_ZF_3_2_L15 Group_ZF_3_4_T1 by auto
  from A1 A2 have T2: "r`(n) ∈ G" "q`(n) ∈ G" "s`(n) ∈ G"
    "s`(r`(n)) ∈ G" "s`(q`(n)) ∈ G" "δ(s,⟨ r`(n),q`(n)⟩) ∈ G"
    "s`(r`(n))⋅s`(q`(n)) ∈ G" "r`(s`(n)) ∈ G" "q`(s`(n)) ∈ G"
    "r`(s`(n))⋅q`(s`(n)) ∈ G"
    using AlmostHoms_def apply_funtype Group_ZF_3_2_L4B 
    group0_2_L1 monoid0.group0_1_L1 by auto
  with T1 A1 A2 isAbelian show  
    "((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
    "((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
    using Group_ZF_3_2_L12 Group_ZF_3_4_L2 Group_ZF_3_4_L1 group0_4_L6A
    by auto  
qed

text‹The sides of the distributive law equations for almost homomorphisms 
  are almost equal.›

lemma (in group1) Ring_ZF_1_1_L2:
  assumes A1: "s∈AH" "r∈AH" "q∈AH"
  shows 
  "s∘(r∙q) ≅ (s∘r)∙(s∘q)" 
  "(r∙q)∘s = (r∘s)∙(q∘s)"
proof -
  from A1 have "∀n∈G. ⟨ r`(n),q`(n)⟩ ∈ G×G"
    using AlmostHoms_def apply_funtype by auto
  moreover from A1 have "{δ(s,x). x ∈ G×G} ∈ Fin(G)"
    using AlmostHoms_def by simp
  ultimately have "{δ(s,⟨ r`(n),q`(n)⟩). n∈G} ∈ Fin(G)"
    by (rule Finite1_L6B)
  with A1 have 
    "{((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯. n ∈ G} ∈ Fin(G)"
    using Ring_ZF_1_1_L1 by simp
  moreover from groupAssum isAbelian A1 A1 have 
    "s∘(r∙q) ∈ AH" "(s∘r)∙(s∘q) ∈ AH"
    using Group_ZF_3_2_L15 Group_ZF_3_4_T1 by auto
  ultimately show "s∘(r∙q) ≅ (s∘r)∙(s∘q)"
    using Group_ZF_3_4_L12 by simp
  from groupAssum isAbelian A1 have 
    "(r∙q)∘s : G→G" "(r∘s)∙(q∘s) : G→G"
    using Group_ZF_3_2_L15 Group_ZF_3_4_T1 AlmostHoms_def
    by auto
  moreover from A1 have
    "∀n∈G. ((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
    using Ring_ZF_1_1_L1 by simp
  ultimately show "(r∙q)∘s = (r∘s)∙(q∘s)"
    using fun_extension_iff by simp
qed
    
text‹The essential condition to show the distributivity for the 
  operations defined on classes of almost homomorphisms.›

lemma (in group1) Ring_ZF_1_1_L3: 
  assumes A1: "R = QuotientGroupRel(AH,Op1,FR)"
  and A2: "a ∈ AH//R" "b ∈ AH//R" "c ∈ AH//R"
  and A3: "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
  shows "M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩ ∧ 
  M`⟨A`⟨ b,c⟩,a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
proof
  from A2 obtain s q r where D1: "s∈AH" "r∈AH" "q∈AH"
    "a = R``{s}" "b = R``{q}" "c = R``{r}"
    using quotient_def by auto
  from A1 have T1:"equiv(AH,R)"
      using Group_ZF_3_3_L3 by simp
  with A1 A3 D1 groupAssum isAbelian have 
    "M`⟨  a,A`⟨ b,c⟩ ⟩ = R``{s∘(q∙r)}"
    using Group_ZF_3_3_L4 EquivClass_1_L10
    Group_ZF_3_2_L15 Group_ZF_3_4_L13A by simp
  also have "R``{s∘(q∙r)} = R``{(s∘q)∙(s∘r)}"
  proof -
    from T1 D1 have "equiv(AH,R)" "s∘(q∙r) ≅ (s∘q)∙(s∘r)"
      using Ring_ZF_1_1_L2 by auto
    with A1 show ?thesis using equiv_class_eq by simp
  qed
  also from A1 T1 D1 A3 have 
    "R``{(s∘q)∙(s∘r)} = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩"
    using Group_ZF_3_3_L4 Group_ZF_3_4_T1 EquivClass_1_L10
    Group_ZF_3_3_L3 Group_ZF_3_4_L13A EquivClass_1_L10 Group_ZF_3_4_T1
    by simp
  finally show "M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩" by simp 
  from A1 A3 T1 D1 groupAssum isAbelian show 
    "M`⟨A`⟨ b,c⟩,a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
    using Group_ZF_3_3_L4 EquivClass_1_L10 Group_ZF_3_4_L13A 
      Group_ZF_3_2_L15 Ring_ZF_1_1_L2 Group_ZF_3_4_T1 by simp
qed

text‹The projection of the first group operation on almost homomorphisms
  is distributive with respect to the second group operation.›

lemma (in group1) Ring_ZF_1_1_L4: 
  assumes A1: "R = QuotientGroupRel(AH,Op1,FR)"
  and A2: "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
  shows "IsDistributive(AH//R,A,M)"
proof -
  from A1 A2 have "∀a∈(AH//R).∀b∈(AH//R).∀c∈(AH//R).
  M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩, M`⟨ a,c⟩⟩ ∧ 
  M`⟨A`⟨ b,c⟩, a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
    using Ring_ZF_1_1_L3 by simp
  then show ?thesis using IsDistributive_def by simp
qed

text‹The classes of almost homomorphisms form a ring.›

theorem (in group1) Ring_ZF_1_1_T1: 
  assumes "R = QuotientGroupRel(AH,Op1,FR)"
  and "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
  shows "IsAring(AH//R,A,M)"
  using assms QuotientGroupOp_def Group_ZF_3_3_T1 Group_ZF_3_4_T2 
    Ring_ZF_1_1_L4 IsAring_def by simp
  
end