src/HOL/Algebra/Group.thy
changeset 35847 19f1f7066917
parent 35416 d8d7d1b785af
child 35848 5443079512ea
     1.1 --- a/src/HOL/Algebra/Group.thy	Sun Mar 21 06:59:23 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 15:57:40 2010 +0100
     1.3 @@ -22,13 +22,14 @@
     1.4    mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
     1.5    one     :: 'a ("\<one>\<index>")
     1.6  
     1.7 -constdefs (structure G)
     1.8 +definition
     1.9    m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
    1.10 -  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    1.11 +  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.12  
    1.13 +definition
    1.14    Units :: "_ => 'a set"
    1.15    --{*The set of invertible elements*}
    1.16 -  "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    1.17 +  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.18  
    1.19  consts
    1.20    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
    1.21 @@ -534,8 +535,8 @@
    1.22  
    1.23  subsection {* Homomorphisms and Isomorphisms *}
    1.24  
    1.25 -constdefs (structure G and H)
    1.26 -  hom :: "_ => _ => ('a => 'b) set"
    1.27 +definition
    1.28 +  hom :: "_ => _ => ('a => 'b) set" where
    1.29    "hom G H ==
    1.30      {h. h \<in> carrier G -> carrier H &
    1.31        (\<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)}"