# HG changeset patch
# User paulson
# Date 1052152248 -7200
# Node ID 0e0553e7d6961a52a4429808b9094be171c9450f
# Parent  c1c67582c9b523a0e85e1d6edae8c1e3b7831809
deleted obsolete group formalization

diff -r c1c67582c9b5 -r 0e0553e7d696 src/HOL/GroupTheory/Group.thy
--- a/src/HOL/GroupTheory/Group.thy	Mon May 05 18:23:40 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,369 +0,0 @@
-(*  Title:      HOL/GroupTheory/Group
-    ID:         $Id$
-    Author:     Florian Kammueller, with new proofs by L C Paulson
-*)
-
-header{*Group Theory Using Locales*}
-
-theory Group = FuncSet:
-
-subsection{*Semigroups*}
-
-record 'a semigroup =
-  carrier :: "'a set"    
-  sum :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<oplus>\<index>" 65)
-
-locale semigroup = struct S +
-  assumes sum_funcset: "sum S \<in> carrier S \<rightarrow> carrier S \<rightarrow> carrier S"
-      and sum_assoc:   
-            "[|x \<in> carrier S; y \<in> carrier S; z \<in> carrier S|] 
-             ==> (x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
-
-constdefs
-  order     :: "(('a,'b) semigroup_scheme) => nat"
-   "order(S) == card(carrier S)"
-
-
-(*Overloading is impossible because of the way record types are represented*)
-constdefs
-  subsemigroup  :: "['a set, ('a,'b) semigroup_scheme] => bool"
-   "subsemigroup H G == 
-	H <= carrier G & 
-	semigroup G &
-        semigroup (G(|carrier:=H|))"
-
-(*a characterization of subsemigroups *)
-lemma (in semigroup) subsemigroupI:
-     "[| H <= carrier S; 
-         !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |] 
-      ==> subsemigroup H S"
-apply (insert prems) 
-apply (simp add: semigroup_def subsemigroup_def, clarify) 
-apply (blast intro: funcsetI) 
-done
-
-
-subsection{*Groups*}
-
-record 'a group = "'a semigroup" +
-  gminus :: "'a \<Rightarrow> 'a"    ("(\<ominus>\<index>_)" [81] 80)
-  zero :: 'a    ("\<zero>\<index>")
-
-locale group = semigroup G +
-  assumes minus_funcset: "gminus G \<in> carrier G \<rightarrow> carrier G"
-      and zero_closed [iff]: 
-            "zero G \<in> carrier G"
-      and left_minus [simp]: 
-            "x \<in> carrier G ==> (\<ominus>x) \<oplus> x = \<zero>"
-      and left_zero [simp]:
-            "x \<in> carrier G ==> \<zero> \<oplus> x = x"
-
-
-constdefs
-  Group :: "('a,'b) group_scheme set"
-   "Group == Collect group"
-
-lemma [simp]: "(G \<in> Group) = (group G)"
-by (simp add: Group_def) 
-
-lemma "group G ==> semigroup G"
-by (simp add: group_def semigroup_def) 
-
-
-locale abelian_group = group +
-  assumes sum_commute: "[|x \<in> carrier G; y \<in> carrier G|] ==> x \<oplus> y = y \<oplus> x"
-
-lemma abelian_group_iff:
-     "abelian_group G = 
-      (group G & (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. sum G x y = sum G y x))"
-by (force simp add: abelian_group_axioms_def abelian_group_def group_def) 
-
-
-subsection{*Basic Group Theory Theorems*}
-
-lemma (in semigroup) sum_closed [simp]: 
-     "[|x \<in> carrier S; y \<in> carrier S|] ==> (x \<oplus> y) \<in> carrier S"
-apply (insert sum_funcset) 
-apply (blast dest: funcset_mem) 
-done
-
-lemma (in group) minus_closed [simp]: 
-     "x \<in> carrier G ==> (\<ominus>x) \<in> carrier G"
-apply (insert minus_funcset) 
-apply (blast dest: funcset_mem) 
-done
-
-lemma (in group) left_cancellation:
-  assumes "x \<oplus> y  =  x \<oplus> z"
-          "x \<in> carrier G" "y \<in> carrier G" "z \<in> carrier G" 
-  shows "y = z"
-proof -
-  have "((\<ominus>x) \<oplus> x) \<oplus> y = ((\<ominus>x) \<oplus> x) \<oplus> z" 
-        by (simp only: prems minus_closed sum_assoc) 
-  thus ?thesis by (simp add: prems) 
-qed
-
-lemma (in group) left_cancellation_iff [simp]:
-     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]  
-      ==> (x \<oplus> y  =  x \<oplus> z) = (y = z)"
-by (blast intro: left_cancellation)
-
-
-subsection{*The Other Directions of Basic Lemmas*}
-
-lemma (in group) right_zero [simp]: "x \<in> carrier G ==> x \<oplus> \<zero> = x"
-apply (rule left_cancellation [of "(\<ominus>x)"])
-apply (auto simp add: sum_assoc [symmetric])
-done
-
-lemma (in group) idempotent_imp_zero: "[| x \<in> carrier G; x \<oplus> x = x |] ==> x=\<zero>"
-by (rule left_cancellation [of x], auto)
-
-lemma (in group) right_minus [simp]: "x \<in> carrier G ==> x \<oplus> (\<ominus>x) = \<zero>"
-apply (rule idempotent_imp_zero)
-apply (simp_all add: sum_assoc [symmetric])
-apply (simp add: sum_assoc)
-done
-
-lemma (in group) minus_unique:
-     "[| x \<in> carrier G; y \<in> carrier G; x \<oplus> y = \<zero> |] ==> y = (\<ominus>x)"
-apply (rule left_cancellation [of x], auto)
-done
-
-lemma (in group) minus_minus [simp]:
-     "x \<in> carrier G ==> \<ominus>(\<ominus>x) = x"
-apply (rule left_cancellation [of "(\<ominus>x)"])
-apply auto
-done
-
-lemma (in group) minus_sum:
-     "[| x \<in> carrier G; y \<in> carrier G |] ==> \<ominus>(x \<oplus> y) = (\<ominus>y) \<oplus> (\<ominus>x)"
-apply (rule minus_unique [symmetric])
-apply (simp_all add: sum_assoc [symmetric])
-apply (simp add: sum_assoc) 
-done
-
-lemma (in group) right_cancellation:
-     "[| y \<oplus> x =  z \<oplus> x;   
-         x \<in> carrier G; y \<in> carrier G; z \<in> carrier G|] ==> y = z"
-apply (drule arg_cong [of concl: "%z. z \<oplus> (\<ominus>x)"])
-apply (simp add: sum_assoc)
-done
-
-lemma (in group) right_cancellation_iff [simp]:
-     "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |]  
-      ==> (y \<oplus> x =  z \<oplus> x) = (y = z)"
-by (blast intro: right_cancellation)
-
-
-subsection{*The Subgroup Relation*}
-
-constdefs  
-  subgroup  :: "['a set, ('a,'b) group_scheme] => bool"
-   "subgroup H G == 
-	H <= carrier G & 
-	group G &
-        group (G(|carrier:=H|))";
-
-
-text{*Since @{term H} is nonempty, it contains some element @{term x}.  Since
-it's closed under inverse, it contains @{text "(\<ominus>x)"}.  Since
-it's closed under sum, it contains @{text "x \<oplus> (\<ominus>x) = \<zero>"}.
-How impressive that the proof is automatic!*}
-lemma (in group) zero_in_subset:
-     "[| H <= carrier G; H \<noteq> {}; \<forall>a \<in> H. (\<ominus>a) \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<oplus> b \<in> H|]
-      ==> \<zero> \<in> H"
-by force
-
-text{*A characterization of subgroups*}
-lemma (in group) subgroupI:
-     "[| H <= carrier G;  H \<noteq> {};  
-         !!a. a \<in> H ==> (\<ominus>a) \<in> H; 
-         !!a b. [|a \<in> H; b \<in> H|] ==> a \<oplus> b \<in> H |] 
-      ==> subgroup H G"
-apply (insert prems) 
-apply (simp add: group_def subgroup_def)
-apply (simp add: semigroup_def group_axioms_def, clarify) 
-apply (simp add: funcsetI subsetD [of H "carrier G"])
-apply (blast intro: zero_in_subset)  
-done
-
-
-lemma subgroup_imp_subset: "subgroup H G  ==> H <= carrier G"
-by (simp add: subgroup_def)
-
-lemma (in group) subgroup_sum_closed:
-     "[| subgroup H G; x \<in> H; y \<in> H |] ==> x \<oplus> y \<in> H"
-by (simp add: subgroup_def group_def semigroup_def Pi_def) 
-
-lemma (in group) subgroup_minus_closed:
-     "[| subgroup H G; x \<in> H |] ==> (\<ominus>x) \<in> H"
-by (simp add: subgroup_def group_def group_axioms_def Pi_def) 
-
-lemma (in group) subgroup_zero_closed: "subgroup H G ==> \<zero> \<in> H"
-by (simp add: subgroup_def group_def group_axioms_def) 
-
-text{*Global declarations, in force outside the locale*}
-declare semigroup.sum_closed [simp]
-
-declare group.zero_closed [iff]
-    and group.minus_closed [simp]
-    and group.left_minus [simp]
-    and group.left_zero [simp]
-    and group.right_minus [simp]
-    and group.right_zero [simp]
-    and group.minus_minus [simp]
-
-
-lemma subgroup_imp_group: "subgroup H G ==> group G"
-by (simp add: subgroup_def) 
-
-lemma subgroup_nonempty: "~ subgroup {} G"
-by (blast dest: subgroup_imp_group group.subgroup_zero_closed)
-
-lemma subgroup_card_positive:
-     "[| finite(carrier G); subgroup H G |] ==> 0 < card(H)"
-apply (subgoal_tac "finite H")
- prefer 2 apply (blast intro: finite_subset dest: subgroup_imp_subset)
-apply (rule ccontr)
-apply (simp add: card_0_eq subgroup_nonempty) 
-done
-
-subsection{*Direct Product of Two Groups*}
-
-text{*We want to overload product for all algebraic structures.  But it is not
-easy.  All of them are instances of the same type, namely @{text
-carrier_field_type}, which the record declaration generates automatically.
-Overloading requires distinct types.*}
-
-constdefs 
-  ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
-  "ProdGroup G G' ==
-    (| carrier = carrier G \<times> carrier G',
-       sum = (%(x, x') (y, y'). (sum G x y, sum G' x' y')),
-       gminus = (%(x, y). (gminus G x, gminus G' y)),
-       zero = (zero G, zero G') |)"
-
-syntax (xsymbols)
-  ProdGroup :: "[('a,'c) group_scheme, ('b,'d) group_scheme] => ('a*'b) group"
-            (infixr "\<otimes>" 80)
-
-
-lemma P_carrier: "(carrier (G\<otimes>G')) = ((carrier G) \<times> (carrier G'))"
-by (simp add: ProdGroup_def)
-
-lemma P_sum: "sum (G\<otimes>G') = (%(x, x') (y, y'). (sum G x y, sum G' x' y'))"
-by (simp add: ProdGroup_def)
-
-lemma P_minus: "(gminus (G\<otimes>G')) = (%(x, y). (gminus G x, gminus G' y))"
-by (simp add: ProdGroup_def)
-
-lemma P_zero: "zero (G\<otimes>G') = (zero G, zero G')"
-by (simp add: ProdGroup_def)
-
-lemma P_sum_funcset:
-     "[|semigroup G; semigroup G'|] ==>
-      sum(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
-by (auto intro!: funcsetI 
-         simp add: semigroup.sum_closed P_sum P_carrier)
-
-lemma P_minus_funcset: 
-     "[|group G; group G'|] ==>
-      gminus(G\<otimes>G') : carrier(G\<otimes>G') \<rightarrow> carrier(G\<otimes>G')"
-by (auto intro!: funcsetI 
-         simp add: group_def group.minus_closed P_minus P_carrier)
-
-theorem ProdGroup_is_group: "[|group G; group G'|] ==> group (G\<otimes>G')"
-apply (rule group.intro)
- apply (simp add: group_def)  
- apply (rule semigroup.intro) 
-  apply (simp add: group_def P_sum_funcset)  
- apply (force simp add: ProdGroup_def semigroup.sum_assoc)
-apply (rule group_axioms.intro) 
-   apply (simp add: P_minus_funcset)  
-  apply (simp add: ProdGroup_def group.zero_closed) 
- apply (force simp add: ProdGroup_def group.left_minus) 
-apply (force simp add: ProdGroup_def group.left_zero) 
-done
-
-lemma ProdGroup_arity: "ProdGroup : Group \<rightarrow> Group \<rightarrow> Group"
-by (auto intro!: funcsetI ProdGroup_is_group)
-
-subsection{*Homomorphisms on Groups and Semigroups*}
-
-constdefs
-  hom :: "[('a,'c)semigroup_scheme, ('b,'d)semigroup_scheme] => ('a => 'b)set"
-   "hom S S' ==
-     {h. h \<in> carrier S -> carrier S' & 
-	 (\<forall>x \<in> carrier S. \<forall>y \<in> carrier S. h(sum S x y) = sum S' (h x) (h y))}"
-
-lemma hom_semigroup:
-     "semigroup S ==> semigroup (|carrier = hom S S, sum = (%h g. h o g) |)"
-apply (simp add: semigroup_def o_assoc) 
-apply (simp add: Pi_def hom_def) 
-done
-
-lemma hom_sum:
-     "[|h \<in> hom S S'; x \<in> carrier S; y \<in> carrier S|] 
-      ==> h(sum S x y) = sum S' (h x) (h y)"
-by (simp add: hom_def) 
-
-lemma hom_closed:
-     "[|h \<in> hom G G'; x \<in> carrier G|] ==> h x \<in> carrier G'"
-by (auto simp add: hom_def funcset_mem) 
-
-lemma hom_zero_closed [simp]:
-     "[|h \<in> hom G G'; group G|] ==> h (zero G) \<in> carrier G'"
-by (auto simp add: hom_closed) 
-
-text{*Or just @{text "group_hom.hom_zero [OF group_homI]"}*}
-lemma hom_zero [simp]:
-     "[|h \<in> hom G G'; group G; group G'|] ==> h (zero G) = zero G'"
-by (simp add: group.idempotent_imp_zero hom_sum [of h, symmetric]) 
-
-lemma hom_minus_closed [simp]:
-     "[|h \<in> hom G G'; x \<in> carrier G; group G|] 
-      ==> h (gminus G x) \<in> carrier G'"
-by (simp add: hom_closed) 
-
-text{*Or just @{text "group_hom.hom_minus [OF group_homI]"}*}
-lemma hom_minus [simp]:
-     "[|h \<in> hom G G'; x \<in> carrier G; group G; group G'|] 
-      ==> h (gminus G x) = gminus G' (h x)"
-by (simp add: group.minus_unique hom_closed hom_sum [of h, symmetric])
-
-
-text{*This locale uses the subscript notation mentioned by Wenzel in 
-@{text "HOL/ex/Locales.thy"}.  We fix two groups and a homomorphism between 
-them.  Then we prove theorems similar to those just above.*}
-
-locale group_homomorphism = group G + group G' +
-  fixes h
-  assumes homh: "h \<in> hom G G'"
-
-lemma (in group_homomorphism) hom_sum [simp]:
-     "[|x \<in> carrier G; y \<in> carrier G|] ==> h (x \<oplus>\<^sub>1 y) = (h x) \<oplus>\<^sub>2 (h y)"
-by (simp add: hom_sum [OF homh])
-
-lemma (in group_homomorphism) hom_zero_closed [simp]: "h \<zero>\<^sub>1 \<in> carrier G'"
-by (simp add: hom_closed [OF homh]) 
-
-lemma (in group_homomorphism) hom_zero [simp]: "h \<zero>\<^sub>1 = \<zero>\<^sub>2"
-by (simp add: idempotent_imp_zero hom_sum [symmetric]) 
-
-lemma (in group_homomorphism) hom_minus_closed [simp]:
-     "x \<in> carrier G ==> h (\<ominus>x) \<in> carrier G'"
-by (simp add: hom_closed [OF homh]) 
-
-lemma (in group_homomorphism) hom_minus [simp]:
-     "x \<in> carrier G ==> h (\<ominus>\<^sub>1 x) = \<ominus>\<^sub>2 (h x)"
-by (simp add: minus_unique hom_closed [OF homh] hom_sum [symmetric])
-
-text{*Necessary because the standard theorem
-    @{text "group_homomorphism.intro"} is unnatural.*}
-lemma group_homomorphismI:
-    "[|group G; group G'; h \<in> hom G G'|] ==> group_homomorphism G G' h"
-by (simp add: group_def group_homomorphism_def group_homomorphism_axioms_def)
-
-end
- 
diff -r c1c67582c9b5 -r 0e0553e7d696 src/HOL/GroupTheory/README.html
--- a/src/HOL/GroupTheory/README.html	Mon May 05 18:23:40 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-<!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
-
-<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
-
-<P>This directory presents proofs about group theory, by
-Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
-These theories use locales and were indeed the original motivation for
-locales.  However, this treatment of groups must still be regarded as
-experimental.  We can expect to see refinements in the future.
-
-Here is an outline of the directory's contents:
-
-<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
-semigroups, groups, homomorphisms and the subgroup relation.  It also defines
-the product of two groups.  It defines the factorization of a group and shows
-that the factorization a normal subgroup is a group.
-
-<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
-defines bijections over sets and operations on them and shows that they
-are a group.  It shows that automorphisms form a group.
-
-<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
-a few basic theorems.  Ring automorphisms are shown to form a group.
-
-<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
-contains a proof of the first Sylow theorem.
-
-<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
-abelian groups by a summation operator for finite sets (provided by
-Clemens Ballarin).
-</UL>
-
-<HR>
-<P>Last modified on $Date$
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>
diff -r c1c67582c9b5 -r 0e0553e7d696 src/HOL/GroupTheory/ROOT.ML
--- a/src/HOL/GroupTheory/ROOT.ML	Mon May 05 18:23:40 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-no_document use_thy "FuncSet";
-
-use_thy "Group";
diff -r c1c67582c9b5 -r 0e0553e7d696 src/HOL/GroupTheory/document/root.tex
--- a/src/HOL/GroupTheory/document/root.tex	Mon May 05 18:23:40 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-\documentclass[a4paper]{article}
-\usepackage{graphicx}
-\usepackage{isabelle,isabellesym,pdfsetup}
-\usepackage{amssymb,textcomp} %special symbols: old-style 0, 1, \lhd, ...
-
-\urlstyle{rm}
-\isabellestyle{tt}
-
-\begin{document}
-
-\title{Fundamentals of Group Theory and Ring Theory}
-\author{Florian Kamm{{\"u}}ller\\ Lawrence C Paulson}
-\maketitle
-
-\tableofcontents
-
-\begin{center}
-  \includegraphics[scale=0.7]{session_graph}  
-\end{center}
-
-\newpage
-
-\parindent 0pt\parskip 0.5ex
-\input{session}
-
-\end{document}