Theory Ring_ZF_1

theory Ring_ZF_1
imports Ring_ZF Group_ZF_3
(* 
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.
*)


header{*\isaheader{Ring\_ZF\_1.thy}*}

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 @{text "Real_ZF_x"} series of theories.
The goal is to
show that classes of almost homomorphisms form a ring.*}


section{*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
"((so(r•q))`(n))·(((sor)•(soq))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
"((r•q)os)`(n) = ((ros)•(qos))`(n)"
proof -;
from groupAssum isAbelian A1 have T1:
"r•q ∈ AH" "sor ∈ AH" "soq ∈ AH" "(sor)•(soq) ∈ AH"
"ros ∈ AH" "qos ∈ AH" "(ros)•(qos) ∈ 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
"((so(r•q))`(n))·(((sor)•(soq))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
"((r•q)os)`(n) = ((ros)•(qos))`(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
"so(r•q) ≈ (sor)•(soq)"
"(r•q)os = (ros)•(qos)"
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
"{((so(r•q))`(n))·(((sor)•(soq))`(n))¯. n ∈ G} ∈ Fin(G)"
using Ring_ZF_1_1_L1 by simp;
moreover from groupAssum isAbelian A1 A1 have
"so(r•q) ∈ AH" "(sor)•(soq) ∈ AH"
using Group_ZF_3_2_L15 Group_ZF_3_4_T1 by auto;
ultimately show "so(r•q) ≈ (sor)•(soq)"
using Group_ZF_3_4_L12 by simp;
from groupAssum isAbelian A1 have
"(r•q)os : G->G" "(ros)•(qos) : 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)os)`(n) = ((ros)•(qos))`(n)"
using Ring_ZF_1_1_L1 by simp;
ultimately show "(r•q)os = (ros)•(qos)"
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``{so(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``{so(q•r)} = R``{(soq)•(sor)}"
proof -
from T1 D1 have "equiv(AH,R)" "so(q•r)≈(soq)•(sor)"
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``{(soq)•(sor)} = 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