src/HOL/ex/Classpackage.thy
author haftmann
Wed Jun 28 14:36:47 2006 +0200 (2006-06-28)
changeset 19958 fc4ac94f03e0
parent 19951 d58e2c564100
child 19965 75a15223e21f
permissions -rw-r--r--
improvements in Classpackage
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@19281
     5
header {* Test and Examples for Pure/Tools/class_package.ML *}
haftmann@19281
     6
haftmann@19281
     7
theory Classpackage
haftmann@19281
     8
imports Main
haftmann@19281
     9
begin
haftmann@19281
    10
haftmann@19281
    11
class semigroup =
haftmann@19281
    12
  fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
haftmann@19281
    13
  assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
haftmann@19281
    14
haftmann@19281
    15
instance nat :: semigroup
haftmann@19958
    16
  "m \<otimes> n == m + n"
haftmann@19281
    17
proof
haftmann@19281
    18
  fix m n q :: nat 
haftmann@19281
    19
  from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
haftmann@19281
    20
qed
haftmann@19281
    21
haftmann@19281
    22
instance int :: semigroup
haftmann@19958
    23
  "k \<otimes> l == k + l"
haftmann@19281
    24
proof
haftmann@19281
    25
  fix k l j :: int
haftmann@19281
    26
  from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
haftmann@19281
    27
qed
haftmann@19281
    28
haftmann@19281
    29
instance (type) list :: semigroup
haftmann@19281
    30
  "xs \<otimes> ys == xs @ ys"
haftmann@19281
    31
proof
haftmann@19281
    32
  fix xs ys zs :: "'a list"
haftmann@19281
    33
  show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
haftmann@19281
    34
  proof -
haftmann@19281
    35
    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
haftmann@19281
    36
    thus ?thesis by simp
haftmann@19281
    37
  qed
haftmann@19281
    38
qed
haftmann@19281
    39
haftmann@19281
    40
class monoidl = semigroup +
haftmann@19281
    41
  fixes one :: 'a ("\<^loc>\<one>")
haftmann@19281
    42
  assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
haftmann@19281
    43
haftmann@19281
    44
instance nat :: monoidl
haftmann@19958
    45
  "\<one> == 0"
haftmann@19281
    46
proof
haftmann@19281
    47
  fix n :: nat
haftmann@19281
    48
  from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp
haftmann@19281
    49
qed
haftmann@19281
    50
haftmann@19281
    51
instance int :: monoidl
haftmann@19958
    52
  "\<one> == 0"
haftmann@19281
    53
proof
haftmann@19281
    54
  fix k :: int
haftmann@19281
    55
  from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp
haftmann@19281
    56
qed
haftmann@19281
    57
haftmann@19281
    58
instance (type) list :: monoidl
haftmann@19281
    59
  "\<one> == []"
haftmann@19281
    60
proof
haftmann@19281
    61
  fix xs :: "'a list"
haftmann@19281
    62
  show "\<one> \<otimes> xs = xs"
haftmann@19281
    63
  proof -
haftmann@19281
    64
    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
haftmann@19281
    65
    moreover from monoidl_list_def have "\<one> == []::'a list".
haftmann@19281
    66
    ultimately show ?thesis by simp
haftmann@19281
    67
  qed
haftmann@19281
    68
qed  
haftmann@19281
    69
haftmann@19281
    70
class monoid = monoidl +
haftmann@19281
    71
  assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
haftmann@19281
    72
haftmann@19281
    73
instance (type) list :: monoid
haftmann@19281
    74
proof
haftmann@19281
    75
  fix xs :: "'a list"
haftmann@19281
    76
  show "xs \<otimes> \<one> = xs"
haftmann@19281
    77
  proof -
haftmann@19281
    78
    from semigroup_list_def have "\<And>xs ys::'a list. xs \<otimes> ys == xs @ ys".
haftmann@19281
    79
    moreover from monoidl_list_def have "\<one> == []::'a list".
haftmann@19281
    80
    ultimately show ?thesis by simp
haftmann@19281
    81
  qed
haftmann@19281
    82
qed  
haftmann@19281
    83
haftmann@19281
    84
class monoid_comm = monoid +
haftmann@19281
    85
  assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
haftmann@19281
    86
haftmann@19281
    87
instance nat :: monoid_comm
haftmann@19281
    88
proof
haftmann@19281
    89
  fix n :: nat
haftmann@19281
    90
  from semigroup_nat_def monoidl_nat_def show "n \<otimes> \<one> = n" by simp
haftmann@19281
    91
next
haftmann@19281
    92
  fix n m :: nat
haftmann@19281
    93
  from semigroup_nat_def monoidl_nat_def show "n \<otimes> m = m \<otimes> n" by simp
haftmann@19281
    94
qed
haftmann@19281
    95
haftmann@19281
    96
instance int :: monoid_comm
haftmann@19281
    97
proof
haftmann@19281
    98
  fix k :: int
haftmann@19281
    99
  from semigroup_int_def monoidl_int_def show "k \<otimes> \<one> = k" by simp
haftmann@19281
   100
next
haftmann@19281
   101
  fix k l :: int
haftmann@19281
   102
  from semigroup_int_def monoidl_int_def show "k \<otimes> l = l \<otimes> k" by simp
haftmann@19281
   103
qed
haftmann@19281
   104
haftmann@19281
   105
definition (in monoid)
haftmann@19281
   106
  units :: "'a set"
haftmann@19281
   107
  units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
haftmann@19281
   108
haftmann@19281
   109
lemma (in monoid) inv_obtain:
haftmann@19281
   110
  assumes ass: "x \<in> units"
haftmann@19281
   111
  obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
haftmann@19281
   112
proof -
haftmann@19281
   113
  from ass units_def obtain y
haftmann@19281
   114
    where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
haftmann@19281
   115
  thus ?thesis ..
haftmann@19281
   116
qed
haftmann@19281
   117
haftmann@19281
   118
lemma (in monoid) inv_unique:
haftmann@19281
   119
  assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
haftmann@19281
   120
  shows "y = y'"
haftmann@19281
   121
proof -
haftmann@19281
   122
  from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
haftmann@19281
   123
  also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
haftmann@19281
   124
  also with eq neutl have "... = y'" by simp
haftmann@19281
   125
  finally show ?thesis .
haftmann@19281
   126
qed
haftmann@19281
   127
haftmann@19281
   128
lemma (in monoid) units_inv_comm:
haftmann@19281
   129
  assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
haftmann@19281
   130
    and G: "x \<in> units"
haftmann@19281
   131
  shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
haftmann@19281
   132
proof -
haftmann@19281
   133
  from G inv_obtain obtain z
haftmann@19281
   134
    where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
haftmann@19281
   135
  from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
haftmann@19281
   136
  with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
haftmann@19281
   137
  with neutl z_choice show ?thesis by simp
haftmann@19281
   138
qed
haftmann@19281
   139
haftmann@19281
   140
consts
haftmann@19281
   141
  reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@19281
   142
haftmann@19281
   143
primrec
haftmann@19281
   144
  "reduce f g 0 x = g"
haftmann@19281
   145
  "reduce f g (Suc n) x = f x (reduce f g n x)"
haftmann@19281
   146
haftmann@19281
   147
definition (in monoid)
haftmann@19281
   148
  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@19281
   149
  npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
haftmann@19281
   150
haftmann@19281
   151
abbreviation (in monoid)
haftmann@19281
   152
  abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
wenzelm@19363
   153
  "x \<^loc>\<up> n == npow n x"
haftmann@19281
   154
haftmann@19281
   155
lemma (in monoid) npow_def:
haftmann@19281
   156
  "x \<^loc>\<up> 0 = \<^loc>\<one>"
haftmann@19281
   157
  "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
haftmann@19281
   158
using npow_def_prim by simp_all
haftmann@19281
   159
haftmann@19281
   160
lemma (in monoid) nat_pow_one:
haftmann@19281
   161
  "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
haftmann@19281
   162
using npow_def neutl by (induct n) simp_all
haftmann@19281
   163
haftmann@19281
   164
lemma (in monoid) nat_pow_mult:
haftmann@19281
   165
  "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
haftmann@19281
   166
proof (induct n)
haftmann@19281
   167
  case 0 with neutl npow_def show ?case by simp
haftmann@19281
   168
next
haftmann@19933
   169
  case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
haftmann@19281
   170
qed
haftmann@19281
   171
haftmann@19281
   172
lemma (in monoid) nat_pow_pow:
haftmann@19281
   173
  "npow n (npow m x) = npow (n * m) x"
haftmann@19281
   174
using npow_def nat_pow_mult by (induct n) simp_all
haftmann@19281
   175
haftmann@19281
   176
class group = monoidl +
haftmann@19281
   177
  fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
haftmann@19281
   178
  assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
haftmann@19281
   179
haftmann@19281
   180
class group_comm = group + monoid_comm
haftmann@19281
   181
haftmann@19281
   182
instance int :: group_comm
haftmann@19281
   183
  "\<div> k == - (k::int)"
haftmann@19281
   184
proof
haftmann@19281
   185
  fix k :: int
haftmann@19281
   186
  from semigroup_int_def monoidl_int_def group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
haftmann@19281
   187
qed
haftmann@19281
   188
haftmann@19281
   189
lemma (in group) cancel:
haftmann@19281
   190
  "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
haftmann@19281
   191
proof
haftmann@19281
   192
  fix x y z :: 'a
haftmann@19281
   193
  assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
haftmann@19281
   194
  hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
haftmann@19281
   195
  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
haftmann@19281
   196
  with neutl invl show "y = z" by simp
haftmann@19281
   197
next
haftmann@19281
   198
  fix x y z :: 'a
haftmann@19281
   199
  assume eq: "y = z"
haftmann@19281
   200
  thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
haftmann@19281
   201
qed
haftmann@19281
   202
haftmann@19281
   203
lemma (in group) neutr:
haftmann@19281
   204
  "x \<^loc>\<otimes> \<^loc>\<one> = x"
haftmann@19281
   205
proof -
haftmann@19281
   206
  from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
haftmann@19281
   207
  with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
haftmann@19281
   208
  with cancel show ?thesis by simp
haftmann@19281
   209
qed
haftmann@19281
   210
haftmann@19281
   211
lemma (in group) invr:
haftmann@19281
   212
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
haftmann@19281
   213
proof -
haftmann@19281
   214
  from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
haftmann@19281
   215
  with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
haftmann@19281
   216
  with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
haftmann@19281
   217
  with cancel show ?thesis ..
haftmann@19281
   218
qed
haftmann@19281
   219
haftmann@19281
   220
interpretation group < monoid
haftmann@19928
   221
proof -
haftmann@19281
   222
  fix x :: "'a"
haftmann@19281
   223
  from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
haftmann@19281
   224
qed
haftmann@19281
   225
haftmann@19958
   226
print_theorems
haftmann@19958
   227
haftmann@19281
   228
instance group < monoid
haftmann@19281
   229
proof
haftmann@19281
   230
  fix x :: "'a::group"
haftmann@19928
   231
  from group.neutr show "x \<otimes> \<one> = x" .
haftmann@19281
   232
qed
haftmann@19281
   233
haftmann@19281
   234
lemma (in group) all_inv [intro]:
haftmann@19281
   235
  "(x::'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
haftmann@19281
   236
  unfolding units_def
haftmann@19281
   237
proof -
haftmann@19281
   238
  fix x :: "'a"
haftmann@19281
   239
  from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
haftmann@19281
   240
  then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
haftmann@19281
   241
  hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
haftmann@19281
   242
  thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
haftmann@19281
   243
qed
haftmann@19281
   244
haftmann@19281
   245
lemma (in group) cancer:
haftmann@19281
   246
  "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
haftmann@19281
   247
proof
haftmann@19281
   248
  assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
haftmann@19281
   249
  with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
haftmann@19281
   250
  with invr neutr show "y = z" by simp
haftmann@19281
   251
next
haftmann@19281
   252
  assume eq: "y = z"
haftmann@19281
   253
  thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
haftmann@19281
   254
qed
haftmann@19281
   255
haftmann@19281
   256
lemma (in group) inv_one:
haftmann@19281
   257
  "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
haftmann@19281
   258
proof -
haftmann@19281
   259
  from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
haftmann@19281
   260
  moreover from invr have "... = \<^loc>\<one>" by simp
haftmann@19281
   261
  finally show ?thesis .
haftmann@19281
   262
qed
haftmann@19281
   263
haftmann@19281
   264
lemma (in group) inv_inv:
haftmann@19281
   265
  "\<^loc>\<div> (\<^loc>\<div> x) = x"
haftmann@19281
   266
proof -
haftmann@19281
   267
  from invl invr neutr
haftmann@19281
   268
    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
haftmann@19281
   269
  with assoc [symmetric]
haftmann@19281
   270
    have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
haftmann@19281
   271
  with invl neutr show ?thesis by simp
haftmann@19281
   272
qed
haftmann@19281
   273
haftmann@19281
   274
lemma (in group) inv_mult_group:
haftmann@19281
   275
  "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
haftmann@19281
   276
proof -
haftmann@19281
   277
  from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
haftmann@19281
   278
  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
haftmann@19281
   279
  with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
haftmann@19281
   280
  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
haftmann@19281
   281
  with invr neutr show ?thesis by simp
haftmann@19281
   282
qed
haftmann@19281
   283
haftmann@19281
   284
lemma (in group) inv_comm:
haftmann@19281
   285
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
haftmann@19281
   286
using invr invl by simp
haftmann@19281
   287
haftmann@19281
   288
definition (in group)
haftmann@19281
   289
  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@19281
   290
  pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
haftmann@19281
   291
    else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
haftmann@19281
   292
haftmann@19281
   293
abbreviation (in group)
haftmann@19281
   294
  abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
haftmann@19928
   295
  "x \<^loc>\<up> k \<equiv> pow k x"
haftmann@19281
   296
haftmann@19281
   297
lemma (in group) int_pow_zero:
haftmann@19281
   298
  "x \<^loc>\<up> (0::int) = \<^loc>\<one>"
haftmann@19281
   299
using npow_def pow_def by simp
haftmann@19281
   300
haftmann@19281
   301
lemma (in group) int_pow_one:
haftmann@19281
   302
  "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>"
haftmann@19281
   303
using pow_def nat_pow_one inv_one by simp
haftmann@19281
   304
haftmann@19281
   305
instance group_prod_def: (group, group) * :: group
haftmann@19958
   306
  mult_prod_def: "x \<otimes> y == let (x1, x2) = x; (y1, y2) = y in
haftmann@19958
   307
              (x1 \<otimes> y1, x2 \<otimes> y2)"
haftmann@19958
   308
  mult_one_def: "\<one> == (\<one>, \<one>)"
haftmann@19958
   309
  mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)"
haftmann@19928
   310
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
haftmann@19281
   311
haftmann@19281
   312
instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
haftmann@19928
   313
by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
haftmann@19281
   314
haftmann@19281
   315
definition
haftmann@19281
   316
  "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
haftmann@19281
   317
  "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
haftmann@19281
   318
haftmann@19928
   319
code_generate "op \<otimes>" "\<one>" "inv"
haftmann@19888
   320
code_generate (ml, haskell) x
haftmann@19888
   321
code_generate (ml, haskell) y
haftmann@19281
   322
haftmann@19281
   323
code_serialize ml (-)
haftmann@19281
   324
haftmann@19281
   325
end