Theory DirectProduct_ZF

theory DirectProduct_ZF
imports func_ZF
(* 
This file is a part of IsarMathLib -
a library of formalized mathematics written for Isabelle/Isar.

Copyright (C) 2008 Seo Sanghyeon

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{DirectProduct\_ZF.thy}*}

theory DirectProduct_ZF imports func_ZF

begin

text{*This theory considers the direct product of binary operations.
Contributed by Seo Sanghyeon. *}


section{*Definition*}

text{*In group theory the notion of direct product provides a natural
way of creating a new group from two given groups.*}


text{*Given $(G,\cdot)$ and $(H,\circ)$
a new operation $(G\times H, \times )$ is defined as
$(g, h) \times (g', h') = (g \cdot g', h \circ h')$. *}


definition
"DirectProduct(P,Q,G,H) ≡
{⟨x,⟨P`⟨fst(fst(x)),fst(snd(x))⟩ , Q`⟨snd(fst(x)),snd(snd(x))⟩⟩⟩.
x ∈ (G×H)×(G×H)}"
;

text{*We define a context called @{text "direct0"} which
holds an assumption that $P, Q$ are binary operations on
$G,H$, resp. and denotes $R$ as the direct product of
$(G,P)$ and $(H,Q)$.*}


locale direct0 =
fixes P Q G H
assumes Pfun: "P : G×G->G"
assumes Qfun: "Q : H×H->H"
fixes R
defines Rdef [simp]: "R ≡ DirectProduct(P,Q,G,H)";

text{*The direct product of binary operations is a binary operation.*}

lemma (in direct0) DirectProduct_ZF_1_L1:
shows "R : (G×H)×(G×H)->G×H"
proof -
from Pfun Qfun have "∀x∈(G×H)×(G×H).
⟨P`⟨fst(fst(x)),fst(snd(x))⟩,Q`⟨snd(fst(x)),snd(snd(x))⟩⟩ ∈ G×H"

by auto;
then show ?thesis using ZF_fun_from_total DirectProduct_def
by simp;
qed;

text{*And it has the intended value.*}

lemma (in direct0) DirectProduct_ZF_1_L2:
shows "∀x∈(G×H). ∀y∈(G×H).
R`⟨x,y⟩ = ⟨P`⟨fst(x),fst(y)⟩,Q`⟨snd(x),snd(y)⟩⟩"

using DirectProduct_def DirectProduct_ZF_1_L1 ZF_fun_from_tot_val
by simp;

text{*And the value belongs to the set the operation is defined on.*}

lemma (in direct0) DirectProduct_ZF_1_L3:
shows "∀x∈(G×H). ∀y∈(G×H). R`⟨x,y⟩ ∈ G×H"
using DirectProduct_ZF_1_L1 by simp;

section{*Associative and commutative operations*}

text{*If P and Q are both associative or commutative operations,
the direct product of P and Q has the same property.*}


text{*Direct product of commutative operations is commutative.*}

lemma (in direct0) DirectProduct_ZF_2_L1:
assumes "P {is commutative on} G" and "Q {is commutative on} H"
shows "R {is commutative on} G×H"
proof -
from assms have "∀x∈(G×H). ∀y∈(G×H). R`⟨x,y⟩ = R`⟨y,x⟩"
using DirectProduct_ZF_1_L2 IsCommutative_def by simp
then show ?thesis using IsCommutative_def by simp
qed;

text{*Direct product of associative operations is associative.*}

lemma (in direct0) DirectProduct_ZF_2_L2:
assumes "P {is associative on} G" and "Q {is associative on} H"
shows "R {is associative on} G×H"
proof -
have "∀x∈G×H. ∀y∈G×H. ∀z∈G×H. R`⟨R`⟨x,y⟩,z⟩ =
⟨P`⟨P`⟨fst(x),fst(y)⟩,fst(z)⟩,Q`⟨Q`⟨snd(x),snd(y)⟩,snd(z)⟩⟩"

using DirectProduct_ZF_1_L2 DirectProduct_ZF_1_L3
by auto;
moreover have "∀x∈G×H. ∀y∈G×H. ∀z∈G×H. R`⟨x,R`⟨y,z⟩⟩ =
⟨P`⟨fst(x),P`⟨fst(y),fst(z)⟩⟩,Q`⟨snd(x),Q`⟨snd(y),snd(z)⟩⟩⟩"

using DirectProduct_ZF_1_L2 DirectProduct_ZF_1_L3 by auto;
ultimately have "∀x∈G×H. ∀y∈G×H. ∀z∈G×H. R`⟨R`⟨x,y⟩,z⟩ = R`⟨x,R`⟨y,z⟩⟩"
using assms IsAssociative_def by simp
then show ?thesis
using DirectProduct_ZF_1_L1 IsAssociative_def by simp
qed;

end