src/HOL/ex/Classpackage.thy
 changeset 21924 fe474e69e603 parent 21911 e29bcab0c81c child 22074 de3586cb0ebd
```     1.1 --- a/src/HOL/ex/Classpackage.thy	Fri Dec 29 03:57:01 2006 +0100
1.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Dec 29 12:11:00 2006 +0100
1.3 @@ -16,14 +16,14 @@
1.4    "m \<otimes> n \<equiv> m + n"
1.5  proof
1.6    fix m n q :: nat
1.7 -  from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
1.8 +  from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
1.9  qed
1.10
1.11  instance int :: semigroup
1.12    "k \<otimes> l \<equiv> k + l"
1.13  proof
1.14    fix k l j :: int
1.15 -  from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
1.16 +  from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
1.17  qed
1.18
1.19  instance list :: (type) semigroup
1.20 @@ -32,7 +32,7 @@
1.21    fix xs ys zs :: "'a list"
1.22    show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
1.23    proof -
1.24 -    from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
1.25 +    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
1.26      thus ?thesis by simp
1.27    qed
1.28  qed
1.29 @@ -41,15 +41,15 @@
1.30    fixes one :: 'a ("\<^loc>\<one>")
1.31    assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
1.32
1.33 -instance monoidl_num_def: nat :: monoidl and int :: monoidl
1.34 +instance nat :: monoidl and int :: monoidl
1.35    "\<one> \<equiv> 0"
1.36    "\<one> \<equiv> 0"
1.37  proof
1.38    fix n :: nat
1.39 -  from monoidl_num_def show "\<one> \<otimes> n = n" by simp
1.40 +  from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
1.41  next
1.42    fix k :: int
1.43 -  from monoidl_num_def show "\<one> \<otimes> k = k" by simp
1.44 +  from mult_int_def one_int_def show "\<one> \<otimes> k = k" by simp
1.45  qed
1.46
1.47  instance list :: (type) monoidl
1.48 @@ -59,7 +59,7 @@
1.49    show "\<one> \<otimes> xs = xs"
1.50    proof -
1.51      from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
1.52 -    moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
1.53 +    moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
1.54      ultimately show ?thesis by simp
1.55    qed
1.56  qed
1.57 @@ -67,13 +67,13 @@
1.58  class monoid = monoidl +
1.59    assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
1.60
1.61 -instance monoid_list_def: list :: (type) monoid
1.62 +instance list :: (type) monoid
1.63  proof
1.64    fix xs :: "'a list"
1.65    show "xs \<otimes> \<one> = xs"
1.66    proof -
1.67      from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
1.68 -    moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
1.69 +    moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
1.70      ultimately show ?thesis by simp
1.71    qed
1.72  qed
1.73 @@ -81,19 +81,19 @@
1.74  class monoid_comm = monoid +
1.75    assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
1.76
1.77 -instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm
1.78 +instance nat :: monoid_comm and int :: monoid_comm
1.79  proof
1.80    fix n :: nat
1.81 -  from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp
1.82 +  from mult_nat_def one_nat_def show "n \<otimes> \<one> = n" by simp
1.83  next
1.84    fix n m :: nat
1.85 -  from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp
1.86 +  from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp
1.87  next
1.88    fix k :: int
1.89 -  from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp
1.90 +  from mult_int_def one_int_def show "k \<otimes> \<one> = k" by simp
1.91  next
1.92    fix k l :: int
1.93 -  from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp
1.94 +  from mult_int_def show "k \<otimes> l = l \<otimes> k" by simp
1.95  qed
1.96
1.97  context monoid
1.98 @@ -181,11 +181,11 @@
1.99
1.100  class group_comm = group + monoid_comm
1.101
1.102 -instance group_comm_int_def: int :: group_comm
1.103 +instance int :: group_comm
1.104    "\<div> k \<equiv> - (k\<Colon>int)"
1.105  proof
1.106    fix k :: int
1.107 -  from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
1.108 +  from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp
1.109  qed
1.110
1.111  lemma (in group) cancel:
1.112 @@ -296,27 +296,27 @@
1.113    "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
1.114  using pow_def nat_pow_one inv_one by simp
1.115
1.116 -instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup
1.117 +instance * :: (semigroup, semigroup) semigroup
1.118    mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
1.119                (x1 \<otimes> y1, x2 \<otimes> y2)"
1.120 -by default (simp_all add: split_paired_all semigroup_prod_def assoc)
1.121 +by default (simp_all add: split_paired_all mult_prod_def assoc)
1.122
1.123 -instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl
1.124 +instance * :: (monoidl, monoidl) monoidl
1.125    one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
1.126 -by default (simp_all add: split_paired_all monoidl_prod_def neutl)
1.127 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
1.128
1.129 -instance monoid_prod_def: * :: (monoid, monoid) monoid
1.130 -by default (simp_all add: split_paired_all monoid_prod_def neutr)
1.131 +instance * :: (monoid, monoid) monoid
1.132 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr)
1.133
1.134 -instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm
1.135 -by default (simp_all add: split_paired_all monoidl_prod_def comm)
1.136 +instance * :: (monoid_comm, monoid_comm) monoid_comm
1.137 +by default (simp_all add: split_paired_all mult_prod_def comm)
1.138
1.139 -instance group_prod_def: * :: (group, group) group
1.140 +instance * :: (group, group) group
1.141    inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
1.142 -by default (simp_all add: split_paired_all group_prod_def invl)
1.143 +by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
1.144
1.145 -instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm
1.146 -by default (simp_all add: split_paired_all group_prod_def comm)
1.147 +instance * :: (group_comm, group_comm) group_comm
1.148 +by default (simp_all add: split_paired_all mult_prod_def comm)
1.149
1.150  definition
1.151    "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
```