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.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>"