src/HOL/Algebra/Group.thy
changeset 35848 5443079512ea
parent 35847 19f1f7066917
child 35849 b5522b51cb1e
     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 15:57:40 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 16:51:37 2010 +0100
     1.3 @@ -24,12 +24,12 @@
     1.4  
     1.5  definition
     1.6    m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
     1.7 -  where "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
     1.8 +  where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
     1.9  
    1.10  definition
    1.11    Units :: "_ => 'a set"
    1.12    --{*The set of invertible elements*}
    1.13 -  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.14 +  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.15  
    1.16  consts
    1.17    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    1.18 @@ -479,10 +479,12 @@
    1.19  
    1.20  subsection {* Direct Products *}
    1.21  
    1.22 -definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
    1.23 -  "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
    1.24 -                mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
    1.25 -                one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
    1.26 +definition
    1.27 +  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
    1.28 +  "G \<times>\<times> H =
    1.29 +    \<lparr>carrier = carrier G \<times> carrier H,
    1.30 +     mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
    1.31 +     one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
    1.32  
    1.33  lemma DirProd_monoid:
    1.34    assumes "monoid G" and "monoid H"
    1.35 @@ -537,7 +539,7 @@
    1.36  
    1.37  definition
    1.38    hom :: "_ => _ => ('a => 'b) set" where
    1.39 -  "hom G H ==
    1.40 +  "hom G H =
    1.41      {h. h \<in> carrier G -> carrier H &
    1.42        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
    1.43  
    1.44 @@ -545,8 +547,9 @@
    1.45    "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
    1.46  by (fastsimp simp add: hom_def compose_def)
    1.47  
    1.48 -definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
    1.49 -  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    1.50 +definition
    1.51 +  iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
    1.52 +  where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
    1.53  
    1.54  lemma iso_refl: "(%x. x) \<in> G \<cong> G"
    1.55  by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)