src/HOL/ex/Classpackage.thy
changeset 20178 e56fa3c8b1f1
parent 20106 a3d4b4eb35b9
child 20187 af47971ea304
     1.1 --- a/src/HOL/ex/Classpackage.thy	Fri Jul 21 14:47:22 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Jul 21 14:47:44 2006 +0200
     1.3 @@ -13,26 +13,26 @@
     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 + n"
     1.8 +  "m \<otimes> n \<equiv> 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 + l"
    1.16 +  "k \<otimes> l \<equiv> 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  qed
    1.21  
    1.22  instance (type) list :: semigroup
    1.23 -  "xs \<otimes> ys == xs @ ys"
    1.24 +  "xs \<otimes> ys \<equiv> xs @ ys"
    1.25  proof
    1.26    fix xs ys zs :: "'a list"
    1.27    show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
    1.28    proof -
    1.29 -    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
    1.30 +    from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
    1.31      thus ?thesis by simp
    1.32    qed
    1.33  qed
    1.34 @@ -41,28 +41,25 @@
    1.35    fixes one :: 'a ("\<^loc>\<one>")
    1.36    assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
    1.37  
    1.38 -instance nat :: monoidl
    1.39 -  "\<one> == 0"
    1.40 +instance monoidl_num_def: nat :: monoidl and int :: monoidl
    1.41 +  "\<one> \<equiv> 0"
    1.42 +  "\<one> \<equiv> 0"
    1.43  proof
    1.44    fix n :: nat
    1.45 -  from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp
    1.46 -qed
    1.47 -
    1.48 -instance int :: monoidl
    1.49 -  "\<one> == 0"
    1.50 -proof
    1.51 +  from monoidl_num_def show "\<one> \<otimes> n = n" by simp
    1.52 +next
    1.53    fix k :: int
    1.54 -  from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp
    1.55 +  from monoidl_num_def show "\<one> \<otimes> k = k" by simp
    1.56  qed
    1.57  
    1.58  instance (type) list :: monoidl
    1.59 -  "\<one> == []"
    1.60 +  "\<one> \<equiv> []"
    1.61  proof
    1.62    fix xs :: "'a list"
    1.63    show "\<one> \<otimes> xs = xs"
    1.64    proof -
    1.65 -    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys" .
    1.66 -    moreover from monoidl_list_def have "\<one> == []::'a list" by simp
    1.67 +    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
    1.68 +    moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
    1.69      ultimately show ?thesis by simp
    1.70    qed
    1.71  qed  
    1.72 @@ -70,13 +67,13 @@
    1.73  class monoid = monoidl +
    1.74    assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
    1.75  
    1.76 -instance (type) list :: monoid
    1.77 +instance monoid_list_def: (type) list :: monoid
    1.78  proof
    1.79    fix xs :: "'a list"
    1.80    show "xs \<otimes> \<one> = xs"
    1.81    proof -
    1.82 -    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys" .
    1.83 -    moreover from monoidl_list_def have "\<one> == []::'a list" by simp
    1.84 +    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
    1.85 +    moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
    1.86      ultimately show ?thesis by simp
    1.87    qed
    1.88  qed  
    1.89 @@ -84,22 +81,19 @@
    1.90  class monoid_comm = monoid +
    1.91    assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
    1.92  
    1.93 -instance nat :: monoid_comm
    1.94 +instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm
    1.95  proof
    1.96    fix n :: nat
    1.97 -  from semigroup_nat_def monoidl_nat_def show "n \<otimes> \<one> = n" by simp
    1.98 +  from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp
    1.99  next
   1.100    fix n m :: nat
   1.101 -  from semigroup_nat_def monoidl_nat_def show "n \<otimes> m = m \<otimes> n" by simp
   1.102 -qed
   1.103 -
   1.104 -instance int :: monoid_comm
   1.105 -proof
   1.106 +  from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp
   1.107 +next
   1.108    fix k :: int
   1.109 -  from semigroup_int_def monoidl_int_def show "k \<otimes> \<one> = k" by simp
   1.110 +  from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp
   1.111  next
   1.112    fix k l :: int
   1.113 -  from semigroup_int_def monoidl_int_def show "k \<otimes> l = l \<otimes> k" by simp
   1.114 +  from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp
   1.115  qed
   1.116  
   1.117  definition (in monoid)
   1.118 @@ -150,7 +144,7 @@
   1.119  
   1.120  abbreviation (in monoid)
   1.121    abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
   1.122 -  "x \<^loc>\<up> n == npow n x"
   1.123 +  "x \<^loc>\<up> n \<equiv> npow n x"
   1.124  
   1.125  lemma (in monoid) npow_def:
   1.126    "x \<^loc>\<up> 0 = \<^loc>\<one>"
   1.127 @@ -179,11 +173,11 @@
   1.128  
   1.129  class group_comm = group + monoid_comm
   1.130  
   1.131 -instance int :: group_comm
   1.132 -  "\<div> k == - (k::int)"
   1.133 +instance group_comm_int_def: int :: group_comm
   1.134 +  "\<div> k \<equiv> - (k\<Colon>int)"
   1.135  proof
   1.136    fix k :: int
   1.137 -  from semigroup_int_def monoidl_int_def group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
   1.138 +  from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
   1.139  qed
   1.140  
   1.141  lemma (in group) cancel:
   1.142 @@ -225,12 +219,12 @@
   1.143  
   1.144  instance group < monoid
   1.145  proof
   1.146 -  fix x :: "'a::group"
   1.147 +  fix x :: "'a\<Colon>group"
   1.148    from group.neutr show "x \<otimes> \<one> = x" .
   1.149  qed
   1.150  
   1.151  lemma (in group) all_inv [intro]:
   1.152 -  "(x::'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
   1.153 +  "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
   1.154    unfolding units_def
   1.155  proof -
   1.156    fix x :: "'a"
   1.157 @@ -293,31 +287,32 @@
   1.158    "x \<^loc>\<up> k \<equiv> pow k x"
   1.159  
   1.160  lemma (in group) int_pow_zero:
   1.161 -  "x \<^loc>\<up> (0::int) = \<^loc>\<one>"
   1.162 +  "x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>"
   1.163  using npow_def pow_def by simp
   1.164  
   1.165  lemma (in group) int_pow_one:
   1.166 -  "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>"
   1.167 +  "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
   1.168  using pow_def nat_pow_one inv_one by simp
   1.169  
   1.170  instance group_prod_def: (group, group) * :: group
   1.171 -  mult_prod_def: "x \<otimes> y == let (x1, x2) = x; (y1, y2) = y in
   1.172 +  mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
   1.173                (x1 \<otimes> y1, x2 \<otimes> y2)"
   1.174 -  mult_one_def: "\<one> == (\<one>, \<one>)"
   1.175 -  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
   1.176 +  mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
   1.177 +  mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
   1.178  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
   1.179  
   1.180  instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
   1.181  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
   1.182  
   1.183  definition
   1.184 -  "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
   1.185 -  "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
   1.186 +  "x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
   1.187 +  "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
   1.188  
   1.189 -code_generate "op \<otimes>" "\<one>" "inv"
   1.190 +code_generate "op \<otimes>" \<one> inv
   1.191  code_generate (ml, haskell) x
   1.192  code_generate (ml, haskell) y
   1.193  
   1.194 +code_serialize ml (_)
   1.195  code_serialize ml (-)
   1.196  
   1.197  end