(* 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 @{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 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