src/HOL/ex/Classpackage.thy
changeset 19958 fc4ac94f03e0
parent 19951 d58e2c564100
child 19965 75a15223e21f
     1.1 --- a/src/HOL/ex/Classpackage.thy	Wed Jun 28 14:36:09 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Wed Jun 28 14:36:47 2006 +0200
     1.3 @@ -13,14 +13,14 @@
     1.4    assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
     1.5  
     1.6  instance nat :: semigroup
     1.7 -  "m \<otimes> n == (m::nat) + n"
     1.8 +  "m \<otimes> n == m + n"
     1.9  proof
    1.10    fix m n q :: nat 
    1.11    from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
    1.12  qed
    1.13  
    1.14  instance int :: semigroup
    1.15 -  "k \<otimes> l == (k::int) + l"
    1.16 +  "k \<otimes> l == k + l"
    1.17  proof
    1.18    fix k l j :: int
    1.19    from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
    1.20 @@ -42,14 +42,14 @@
    1.21    assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
    1.22  
    1.23  instance nat :: monoidl
    1.24 -  "\<one> == (0::nat)"
    1.25 +  "\<one> == 0"
    1.26  proof
    1.27    fix n :: nat
    1.28    from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp
    1.29  qed
    1.30  
    1.31  instance int :: monoidl
    1.32 -  "\<one> == (0::int)"
    1.33 +  "\<one> == 0"
    1.34  proof
    1.35    fix k :: int
    1.36    from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp
    1.37 @@ -223,6 +223,8 @@
    1.38    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
    1.39  qed
    1.40  
    1.41 +print_theorems
    1.42 +
    1.43  instance group < monoid
    1.44  proof
    1.45    fix x :: "'a::group"
    1.46 @@ -301,10 +303,10 @@
    1.47  using pow_def nat_pow_one inv_one by simp
    1.48  
    1.49  instance group_prod_def: (group, group) * :: group
    1.50 -  mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in
    1.51 -              ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))"
    1.52 -  mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)"
    1.53 -  mult_inv_def: "\<div> x == let (x1::'a::group, x2::'b::group) = x in (\<div> x1, \<div> x2)"
    1.54 +  mult_prod_def: "x \<otimes> y == let (x1, x2) = x; (y1, y2) = y in
    1.55 +              (x1 \<otimes> y1, x2 \<otimes> y2)"
    1.56 +  mult_one_def: "\<one> == (\<one>, \<one>)"
    1.57 +  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
    1.58  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
    1.59  
    1.60  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm