Theory DirectProduct_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.

*)

section ‹Direct product›

theory DirectProduct_ZF imports func_ZF

begin

text‹This theory considers the direct product of binary operations. 
  Contributed by Seo Sanghyeon.›

subsection‹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 ‹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

subsection‹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