src/HOL/Isar_examples/Group.thy
changeset 7005 cc778d613217
parent 6908 1bf0590f4790
child 7133 64c9f2364dae
equal deleted inserted replaced
7004:c799d0859638 7005:cc778d613217
   126   monoid_assoc:       "(x * y) * z = x * (y * z)"
   126   monoid_assoc:       "(x * y) * z = x * (y * z)"
   127   monoid_left_unit:   "one * x = x"
   127   monoid_left_unit:   "one * x = x"
   128   monoid_right_unit:  "x * one = x";
   128   monoid_right_unit:  "x * one = x";
   129 
   129 
   130 text {*
   130 text {*
   131  Groups are *not* yet monoids directly from the definition .  For
   131  Groups are *not* yet monoids directly from the definition.  For
   132  monoids, right_unit had to be included as an axiom, but for groups
   132  monoids, right_unit had to be included as an axiom, but for groups
   133  both right_unit and right_inverse are derivable from the other
   133  both right_unit and right_inverse are derivable from the other
   134  axioms.  With group_right_unit derived as a theorem of group theory
   134  axioms.  With group_right_unit derived as a theorem of group theory
   135  (see above), we may still instantiate group < monoid properly as
   135  (see above), we may still instantiate group < monoid properly as
   136  follows.
   136  follows.