300 "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>" |
300 "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>" |
301 using pow_def nat_pow_one inv_one by simp |
301 using pow_def nat_pow_one inv_one by simp |
302 |
302 |
303 instance group_prod_def: (group, group) * :: group |
303 instance group_prod_def: (group, group) * :: group |
304 mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in |
304 mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in |
305 (x1 \<otimes> y1, x2 \<otimes> y2))" |
305 ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))" |
306 mult_one_def: "\<one> == (\<one>, \<one>)" |
306 mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)" |
307 mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)" |
307 mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)" |
308 by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl) |
308 by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl) |
309 |
309 |
310 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm |
310 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm |
311 by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm) |
311 by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm) |