src/HOL/Algebra/Group.thy
changeset 61382 efac889fccbc
parent 61169 4de9ff3ea29a
child 61384 9f5145281888
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:21:34 2015 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 16:26:23 2015 +0200
     1.3 @@ -8,13 +8,13 @@
     1.4  imports Lattice "~~/src/HOL/Library/FuncSet"
     1.5  begin
     1.6  
     1.7 -section {* Monoids and Groups *}
     1.8 +section \<open>Monoids and Groups\<close>
     1.9  
    1.10 -subsection {* Definitions *}
    1.11 +subsection \<open>Definitions\<close>
    1.12  
    1.13 -text {*
    1.14 +text \<open>
    1.15    Definitions follow @{cite "Jacobson:1985"}.
    1.16 -*}
    1.17 +\<close>
    1.18  
    1.19  record 'a monoid =  "'a partial_object" +
    1.20    mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
    1.21 @@ -26,7 +26,7 @@
    1.22  
    1.23  definition
    1.24    Units :: "_ => 'a set"
    1.25 -  --{*The set of invertible elements*}
    1.26 +  --\<open>The set of invertible elements\<close>
    1.27    where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
    1.28  
    1.29  consts
    1.30 @@ -187,7 +187,7 @@
    1.31    with G show ?thesis by (simp del: r_one add: m_assoc Units_closed)
    1.32  qed
    1.33  
    1.34 -text {* Power *}
    1.35 +text \<open>Power\<close>
    1.36  
    1.37  lemma (in monoid) nat_pow_closed [intro, simp]:
    1.38    "x \<in> carrier G ==> x (^) (n::nat) \<in> carrier G"
    1.39 @@ -218,11 +218,11 @@
    1.40  (* Jacobson defines the order of a monoid here. *)
    1.41  
    1.42  
    1.43 -subsection {* Groups *}
    1.44 +subsection \<open>Groups\<close>
    1.45  
    1.46 -text {*
    1.47 +text \<open>
    1.48    A group is a monoid all of whose elements are invertible.
    1.49 -*}
    1.50 +\<close>
    1.51  
    1.52  locale group = monoid +
    1.53    assumes Units: "carrier G <= Units G"
    1.54 @@ -321,7 +321,7 @@
    1.55    using Units_l_inv by simp
    1.56  
    1.57  
    1.58 -subsection {* Cancellation Laws and Basic Properties *}
    1.59 +subsection \<open>Cancellation Laws and Basic Properties\<close>
    1.60  
    1.61  lemma (in group) l_cancel [simp]:
    1.62    "[| x \<in> carrier G; y \<in> carrier G; z \<in> carrier G |] ==>
    1.63 @@ -397,7 +397,7 @@
    1.64    "\<lbrakk> a \<in> carrier G; b \<in> carrier G; c \<in> carrier G \<rbrakk> \<Longrightarrow> a = b \<otimes> inv c \<longleftrightarrow> b = a \<otimes> c"
    1.65    by (metis inv_equality l_inv_ex l_one m_assoc r_inv)
    1.66  
    1.67 -text {* Power *}
    1.68 +text \<open>Power\<close>
    1.69  
    1.70  lemma (in group) int_pow_def2:
    1.71    "a (^) (z::int) = (if z < 0 then inv (a (^) (nat (-z))) else a (^) (nat z))"
    1.72 @@ -435,7 +435,7 @@
    1.73  qed
    1.74  
    1.75   
    1.76 -subsection {* Subgroups *}
    1.77 +subsection \<open>Subgroups\<close>
    1.78  
    1.79  locale subgroup =
    1.80    fixes H and G (structure)
    1.81 @@ -469,18 +469,18 @@
    1.82      done
    1.83  qed
    1.84  
    1.85 -text {*
    1.86 +text \<open>
    1.87    Since @{term H} is nonempty, it contains some element @{term x}.  Since
    1.88    it is closed under inverse, it contains @{text "inv x"}.  Since
    1.89    it is closed under product, it contains @{text "x \<otimes> inv x = \<one>"}.
    1.90 -*}
    1.91 +\<close>
    1.92  
    1.93  lemma (in group) one_in_subset:
    1.94    "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
    1.95     ==> \<one> \<in> H"
    1.96  by force
    1.97  
    1.98 -text {* A characterization of subgroups: closed, non-empty subset. *}
    1.99 +text \<open>A characterization of subgroups: closed, non-empty subset.\<close>
   1.100  
   1.101  lemma (in group) subgroupI:
   1.102    assumes subset: "H \<subseteq> carrier G" and non_empty: "H \<noteq> {}"
   1.103 @@ -513,7 +513,7 @@
   1.104  *)
   1.105  
   1.106  
   1.107 -subsection {* Direct Products *}
   1.108 +subsection \<open>Direct Products\<close>
   1.109  
   1.110  definition
   1.111    DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
   1.112 @@ -533,7 +533,7 @@
   1.113  qed
   1.114  
   1.115  
   1.116 -text{*Does not use the previous result because it's easier just to use auto.*}
   1.117 +text\<open>Does not use the previous result because it's easier just to use auto.\<close>
   1.118  lemma DirProd_group:
   1.119    assumes "group G" and "group H"
   1.120    shows "group (G \<times>\<times> H)"
   1.121 @@ -571,7 +571,7 @@
   1.122  qed
   1.123  
   1.124  
   1.125 -subsection {* Homomorphisms and Isomorphisms *}
   1.126 +subsection \<open>Homomorphisms and Isomorphisms\<close>
   1.127  
   1.128  definition
   1.129    hom :: "_ => _ => ('a => 'b) set" where
   1.130 @@ -611,8 +611,8 @@
   1.131  by (auto simp add: iso_def hom_def inj_on_def bij_betw_def)
   1.132  
   1.133  
   1.134 -text{*Basis for homomorphism proofs: we assume two groups @{term G} and
   1.135 -  @{term H}, with a homomorphism @{term h} between them*}
   1.136 +text\<open>Basis for homomorphism proofs: we assume two groups @{term G} and
   1.137 +  @{term H}, with a homomorphism @{term h} between them\<close>
   1.138  locale group_hom = G: group G + H: group H for G (structure) and H (structure) +
   1.139    fixes h
   1.140    assumes homh: "h \<in> hom G H"
   1.141 @@ -665,13 +665,13 @@
   1.142    unfolding hom_def by (simp add: int_pow_mult)
   1.143  
   1.144  
   1.145 -subsection {* Commutative Structures *}
   1.146 +subsection \<open>Commutative Structures\<close>
   1.147  
   1.148 -text {*
   1.149 +text \<open>
   1.150    Naming convention: multiplicative structures that are commutative
   1.151    are called \emph{commutative}, additive structures are called
   1.152    \emph{Abelian}.
   1.153 -*}
   1.154 +\<close>
   1.155  
   1.156  locale comm_monoid = monoid +
   1.157    assumes m_comm: "\<lbrakk>x \<in> carrier G; y \<in> carrier G\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x"
   1.158 @@ -753,9 +753,9 @@
   1.159    by (simp add: m_ac inv_mult_group)
   1.160  
   1.161  
   1.162 -subsection {* The Lattice of Subgroups of a Group *}
   1.163 +subsection \<open>The Lattice of Subgroups of a Group\<close>
   1.164  
   1.165 -text_raw {* \label{sec:subgroup-lattice} *}
   1.166 +text_raw \<open>\label{sec:subgroup-lattice}\<close>
   1.167  
   1.168  theorem (in group) subgroups_partial_order:
   1.169    "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"