src/HOL/ex/Classpackage.thy
changeset 20427 0b102b4182de
parent 20383 58f65fc90cf4
child 20453 855f07fabd76
     1.1 --- a/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:13 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Aug 29 14:31:14 2006 +0200
     1.3 @@ -288,15 +288,27 @@
     1.4    "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
     1.5  using pow_def nat_pow_one inv_one by simp
     1.6  
     1.7 -instance group_prod_def: (group, group) * :: group
     1.8 +instance semigroup_prod_def: (semigroup, semigroup) * :: semigroup
     1.9    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
    1.10                (x1 \<otimes> y1, x2 \<otimes> y2)"
    1.11 -  mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
    1.12 -  mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.13 -by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
    1.14 +by default (simp_all add: split_paired_all semigroup_prod_def assoc)
    1.15 +
    1.16 +instance monoidl_prod_def: (monoidl, monoidl) * :: monoidl
    1.17 +  one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
    1.18 +by default (simp_all add: split_paired_all monoidl_prod_def neutl)
    1.19 +
    1.20 +instance monoid_prod_def: (monoid, monoid) * :: monoid
    1.21 +by default (simp_all add: split_paired_all monoid_prod_def neutr)
    1.22 +
    1.23 +instance monoid_comm_prod_def: (monoid_comm, monoid_comm) * :: monoid_comm
    1.24 +by default (simp_all add: split_paired_all monoidl_prod_def comm)
    1.25 +
    1.26 +instance group_prod_def: (group, group) * :: group
    1.27 +  inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.28 +by default (simp_all add: split_paired_all group_prod_def invl)
    1.29  
    1.30  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
    1.31 -by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
    1.32 +by default (simp_all add: split_paired_all group_prod_def comm)
    1.33  
    1.34  definition
    1.35    "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"