src/HOL/ex/Classpackage.thy
author haftmann
Fri Aug 24 14:14:20 2007 +0200 (2007-08-24)
changeset 24423 ae9cd0e92423
parent 24348 c708ea5b109a
child 24657 185502d54c3d
permissions -rw-r--r--
overloaded definitions accompanied by explicit constants
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@22424
     5
header {* Test and examples for Isar class package *}
haftmann@19281
     6
haftmann@19281
     7
theory Classpackage
haftmann@19281
     8
imports Main
haftmann@19281
     9
begin
haftmann@19281
    10
haftmann@22473
    11
class semigroup = type +
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@20178
    16
  "m \<otimes> n \<equiv> m + n"
haftmann@19281
    17
proof
haftmann@19281
    18
  fix m n q :: nat 
haftmann@21924
    19
  from mult_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@20178
    23
  "k \<otimes> l \<equiv> k + l"
haftmann@19281
    24
proof
haftmann@19281
    25
  fix k l j :: int
haftmann@21924
    26
  from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
haftmann@19281
    27
qed
haftmann@19281
    28
haftmann@23952
    29
instance * :: (semigroup, semigroup) semigroup
haftmann@23952
    30
  mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
haftmann@23952
    31
              (x1 \<otimes> y1, x2 \<otimes> y2)"
haftmann@23952
    32
by default (simp_all add: split_paired_all mult_prod_def assoc)
haftmann@23952
    33
haftmann@20597
    34
instance list :: (type) semigroup
haftmann@20178
    35
  "xs \<otimes> ys \<equiv> xs @ ys"
haftmann@19281
    36
proof
haftmann@19281
    37
  fix xs ys zs :: "'a list"
haftmann@19281
    38
  show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
haftmann@19281
    39
  proof -
haftmann@21924
    40
    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
haftmann@19281
    41
    thus ?thesis by simp
haftmann@19281
    42
  qed
haftmann@19281
    43
qed
haftmann@19281
    44
haftmann@19281
    45
class monoidl = semigroup +
haftmann@19281
    46
  fixes one :: 'a ("\<^loc>\<one>")
haftmann@19281
    47
  assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
haftmann@19281
    48
haftmann@21924
    49
instance nat :: monoidl and int :: monoidl
haftmann@20178
    50
  "\<one> \<equiv> 0"
haftmann@20178
    51
  "\<one> \<equiv> 0"
haftmann@19281
    52
proof
haftmann@19281
    53
  fix n :: nat
haftmann@21924
    54
  from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp
haftmann@20178
    55
next
haftmann@19281
    56
  fix k :: int
haftmann@21924
    57
  from mult_int_def one_int_def show "\<one> \<otimes> k = k" by simp
haftmann@19281
    58
qed
haftmann@19281
    59
haftmann@23952
    60
instance * :: (monoidl, monoidl) monoidl
haftmann@23952
    61
  one_prod_def: "\<one> \<equiv> (\<one>, \<one>)"
haftmann@23952
    62
by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl)
haftmann@23952
    63
haftmann@20597
    64
instance list :: (type) monoidl
haftmann@20178
    65
  "\<one> \<equiv> []"
haftmann@19281
    66
proof
haftmann@19281
    67
  fix xs :: "'a list"
haftmann@19281
    68
  show "\<one> \<otimes> xs = xs"
haftmann@19281
    69
  proof -
haftmann@20178
    70
    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
haftmann@21924
    71
    moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
haftmann@19281
    72
    ultimately show ?thesis by simp
haftmann@19281
    73
  qed
haftmann@19281
    74
qed  
haftmann@19281
    75
haftmann@19281
    76
class monoid = monoidl +
haftmann@19281
    77
  assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
wenzelm@21707
    78
begin
wenzelm@21707
    79
wenzelm@21707
    80
definition
wenzelm@21404
    81
  units :: "'a set" where
wenzelm@21707
    82
  "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
haftmann@19281
    83
haftmann@23952
    84
end context monoid begin
haftmann@22384
    85
wenzelm@21707
    86
lemma inv_obtain:
wenzelm@21707
    87
  assumes "x \<in> units"
haftmann@19281
    88
  obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
haftmann@19281
    89
proof -
wenzelm@21707
    90
  from assms units_def obtain y
haftmann@19281
    91
    where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
haftmann@19281
    92
  thus ?thesis ..
haftmann@19281
    93
qed
haftmann@19281
    94
wenzelm@21707
    95
lemma inv_unique:
wenzelm@21707
    96
  assumes "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
haftmann@19281
    97
  shows "y = y'"
haftmann@19281
    98
proof -
wenzelm@21707
    99
  from assms neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
haftmann@19281
   100
  also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
wenzelm@21707
   101
  also with assms neutl have "... = y'" by simp
haftmann@19281
   102
  finally show ?thesis .
haftmann@19281
   103
qed
haftmann@19281
   104
wenzelm@21707
   105
lemma units_inv_comm:
haftmann@19281
   106
  assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
haftmann@19281
   107
    and G: "x \<in> units"
haftmann@19281
   108
  shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
haftmann@19281
   109
proof -
haftmann@19281
   110
  from G inv_obtain obtain z
haftmann@19281
   111
    where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
haftmann@19281
   112
  from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
haftmann@19281
   113
  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
   114
  with neutl z_choice show ?thesis by simp
haftmann@19281
   115
qed
haftmann@19281
   116
haftmann@23952
   117
fun
haftmann@23952
   118
  npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@23952
   119
where
haftmann@23952
   120
  "npow 0 x = \<^loc>\<one>"
haftmann@23952
   121
  | "npow (Suc n) x = x \<^loc>\<otimes> npow n x"
haftmann@19281
   122
haftmann@23952
   123
end context monoid begin
haftmann@22384
   124
wenzelm@21707
   125
abbreviation
wenzelm@21707
   126
  npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
haftmann@20178
   127
  "x \<^loc>\<up> n \<equiv> npow n x"
haftmann@19281
   128
wenzelm@21707
   129
lemma nat_pow_one:
haftmann@19281
   130
  "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
haftmann@23952
   131
using neutl by (induct n) simp_all
haftmann@19281
   132
wenzelm@21707
   133
lemma nat_pow_mult: "x \<^loc>\<up> n \<^loc>\<otimes> x \<^loc>\<up> m = x \<^loc>\<up> (n + m)"
haftmann@19281
   134
proof (induct n)
haftmann@23952
   135
  case 0 with neutl show ?case by simp
haftmann@19281
   136
next
haftmann@23952
   137
  case (Suc n) with Suc.hyps assoc show ?case by simp
haftmann@19281
   138
qed
haftmann@19281
   139
wenzelm@21707
   140
lemma nat_pow_pow: "(x \<^loc>\<up> m) \<^loc>\<up> n = x \<^loc>\<up> (n * m)"
haftmann@23952
   141
using nat_pow_mult by (induct n) simp_all
haftmann@19281
   142
wenzelm@21707
   143
end
wenzelm@21707
   144
haftmann@23952
   145
instance * :: (monoid, monoid) monoid
haftmann@24282
   146
by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr)
haftmann@23952
   147
haftmann@23952
   148
instance list :: (type) monoid
haftmann@23952
   149
proof
haftmann@23952
   150
  fix xs :: "'a list"
haftmann@23952
   151
  show "xs \<otimes> \<one> = xs"
haftmann@23952
   152
  proof -
haftmann@23952
   153
    from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
haftmann@23952
   154
    moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
haftmann@23952
   155
    ultimately show ?thesis by simp
haftmann@23952
   156
  qed
haftmann@23952
   157
qed  
haftmann@23952
   158
haftmann@23952
   159
class monoid_comm = monoid +
haftmann@23952
   160
  assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
haftmann@23952
   161
haftmann@23952
   162
instance nat :: monoid_comm and int :: monoid_comm
haftmann@23952
   163
proof
haftmann@23952
   164
  fix n :: nat
haftmann@23952
   165
  from mult_nat_def one_nat_def show "n \<otimes> \<one> = n" by simp
haftmann@23952
   166
next
haftmann@23952
   167
  fix n m :: nat
haftmann@23952
   168
  from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp
haftmann@23952
   169
next
haftmann@23952
   170
  fix k :: int
haftmann@23952
   171
  from mult_int_def one_int_def show "k \<otimes> \<one> = k" by simp
haftmann@23952
   172
next
haftmann@23952
   173
  fix k l :: int
haftmann@23952
   174
  from mult_int_def show "k \<otimes> l = l \<otimes> k" by simp
haftmann@23952
   175
qed
haftmann@23952
   176
haftmann@23952
   177
instance * :: (monoid_comm, monoid_comm) monoid_comm
haftmann@23952
   178
by default (simp_all add: split_paired_all mult_prod_def comm)
haftmann@23952
   179
haftmann@19281
   180
class group = monoidl +
haftmann@19281
   181
  fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
haftmann@19281
   182
  assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
haftmann@23952
   183
begin
haftmann@19281
   184
haftmann@23952
   185
lemma cancel:
haftmann@19281
   186
  "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
haftmann@19281
   187
proof
haftmann@19281
   188
  fix x y z :: 'a
haftmann@19281
   189
  assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
haftmann@19281
   190
  hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
haftmann@19281
   191
  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
   192
  with neutl invl show "y = z" by simp
haftmann@19281
   193
next
haftmann@19281
   194
  fix x y z :: 'a
haftmann@19281
   195
  assume eq: "y = z"
haftmann@19281
   196
  thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
haftmann@19281
   197
qed
haftmann@19281
   198
haftmann@23952
   199
lemma neutr:
haftmann@19281
   200
  "x \<^loc>\<otimes> \<^loc>\<one> = x"
haftmann@19281
   201
proof -
haftmann@19281
   202
  from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
haftmann@19281
   203
  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
   204
  with cancel show ?thesis by simp
haftmann@19281
   205
qed
haftmann@19281
   206
haftmann@23952
   207
lemma invr:
haftmann@19281
   208
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
haftmann@19281
   209
proof -
haftmann@19281
   210
  from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
haftmann@19281
   211
  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
   212
  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
   213
  with cancel show ?thesis ..
haftmann@19281
   214
qed
haftmann@19281
   215
haftmann@23952
   216
end
haftmann@23952
   217
haftmann@22321
   218
instance advanced group < monoid
haftmann@22179
   219
proof unfold_locales
haftmann@20383
   220
  fix x
haftmann@19281
   221
  from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
haftmann@19281
   222
qed
haftmann@24282
   223
haftmann@24282
   224
hide const npow (*FIXME*)
haftmann@24282
   225
lemmas neutr = monoid_class.mult_one.neutr
haftmann@24282
   226
lemmas inv_obtain = monoid_class.inv_obtain
haftmann@24282
   227
lemmas inv_unique = monoid_class.inv_unique
haftmann@24282
   228
lemmas nat_pow_mult = monoid_class.nat_pow_mult
haftmann@24282
   229
lemmas nat_pow_one = monoid_class.nat_pow_one
haftmann@24282
   230
lemmas nat_pow_pow = monoid_class.nat_pow_pow
haftmann@24282
   231
lemmas units_def = monoid_class.units_def
haftmann@24282
   232
lemmas mult_one_def = monoid_class.units_inv_comm
haftmann@19281
   233
haftmann@23952
   234
context group
haftmann@23952
   235
begin
haftmann@23952
   236
haftmann@23952
   237
lemma all_inv [intro]:
haftmann@23952
   238
  "(x\<Colon>'a) \<in> units"
haftmann@19281
   239
  unfolding units_def
haftmann@19281
   240
proof -
haftmann@19281
   241
  fix x :: "'a"
haftmann@19281
   242
  from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" . 
haftmann@19281
   243
  then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
haftmann@19281
   244
  hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
haftmann@19281
   245
  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
   246
qed
haftmann@19281
   247
haftmann@23952
   248
lemma cancer:
haftmann@19281
   249
  "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
haftmann@19281
   250
proof
haftmann@19281
   251
  assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
haftmann@19281
   252
  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
   253
  with invr neutr show "y = z" by simp
haftmann@19281
   254
next
haftmann@19281
   255
  assume eq: "y = z"
haftmann@19281
   256
  thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
haftmann@19281
   257
qed
haftmann@19281
   258
haftmann@23952
   259
lemma inv_one:
haftmann@19281
   260
  "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
haftmann@19281
   261
proof -
haftmann@19281
   262
  from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
haftmann@19281
   263
  moreover from invr have "... = \<^loc>\<one>" by simp
haftmann@19281
   264
  finally show ?thesis .
haftmann@19281
   265
qed
haftmann@19281
   266
haftmann@23952
   267
lemma inv_inv:
haftmann@19281
   268
  "\<^loc>\<div> (\<^loc>\<div> x) = x"
haftmann@19281
   269
proof -
haftmann@19281
   270
  from invl invr neutr
haftmann@19281
   271
    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
   272
  with assoc [symmetric]
haftmann@19281
   273
    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
   274
  with invl neutr show ?thesis by simp
haftmann@19281
   275
qed
haftmann@19281
   276
haftmann@23952
   277
lemma inv_mult_group:
haftmann@19281
   278
  "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
haftmann@19281
   279
proof -
haftmann@19281
   280
  from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
haftmann@19281
   281
  with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
haftmann@19281
   282
  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
   283
  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
   284
  with invr neutr show ?thesis by simp
haftmann@19281
   285
qed
haftmann@19281
   286
haftmann@23952
   287
lemma inv_comm:
haftmann@19281
   288
  "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
haftmann@19281
   289
using invr invl by simp
haftmann@19281
   290
haftmann@23952
   291
definition
haftmann@23952
   292
  pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@23952
   293
where
haftmann@23952
   294
  "pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x)
haftmann@23952
   295
    else (npow (nat k) x))"
haftmann@23952
   296
haftmann@24282
   297
end
haftmann@24282
   298
haftmann@24282
   299
(*FIXME*)
haftmann@24282
   300
lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
haftmann@24282
   301
haftmann@24282
   302
context group begin
haftmann@19281
   303
haftmann@23952
   304
abbreviation
haftmann@23952
   305
  pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75)
haftmann@23952
   306
where
haftmann@23952
   307
  "x \<^loc>\<up>\<up> k \<equiv> pow k x"
haftmann@19281
   308
haftmann@23952
   309
lemma int_pow_zero:
haftmann@23952
   310
  "x \<^loc>\<up>\<up> (0\<Colon>int) = \<^loc>\<one>"
haftmann@23952
   311
using pow_def by simp
haftmann@19281
   312
haftmann@23952
   313
lemma int_pow_one:
haftmann@23952
   314
  "\<^loc>\<one> \<^loc>\<up>\<up> (k\<Colon>int) = \<^loc>\<one>"
haftmann@19281
   315
using pow_def nat_pow_one inv_one by simp
haftmann@19281
   316
haftmann@23952
   317
end
haftmann@20427
   318
haftmann@21924
   319
instance * :: (group, group) group
haftmann@20427
   320
  inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
haftmann@22384
   321
by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl)
haftmann@19281
   322
haftmann@23952
   323
class group_comm = group + monoid_comm
haftmann@23952
   324
haftmann@23952
   325
instance int :: group_comm
haftmann@23952
   326
  "\<div> k \<equiv> - (k\<Colon>int)"
haftmann@23952
   327
proof
haftmann@23952
   328
  fix k :: int
haftmann@23952
   329
  from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp
haftmann@23952
   330
qed
haftmann@23952
   331
haftmann@21924
   332
instance * :: (group_comm, group_comm) group_comm
haftmann@22384
   333
by default (simp_all add: split_paired_all mult_prod_def comm)
haftmann@19281
   334
haftmann@19281
   335
definition
haftmann@23952
   336
  "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, npow 3 [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
haftmann@23952
   337
wenzelm@21404
   338
definition
haftmann@24282
   339
  "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> pow (-3) c)"
haftmann@20383
   340
wenzelm@21404
   341
definition "x1 = X (1::nat) 2 3"
wenzelm@21404
   342
definition "x2 = X (1::int) 2 3"
wenzelm@21404
   343
definition "y2 = Y (1::int) 2 3"
haftmann@19281
   344
haftmann@24423
   345
export_code mult x1 x2 y2 in SML module_name Classpackage
haftmann@23810
   346
  in OCaml file -
haftmann@23810
   347
  in Haskell file -
haftmann@19281
   348
haftmann@19281
   349
end