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])"