src/HOL/ex/Classpackage.thy
 author haftmann Fri Mar 17 14:20:24 2006 +0100 (2006-03-17) changeset 19281 b411f25fff25 child 19345 73439b467e75 permissions -rw-r--r--
added example for operational classes and code generator
 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 \ 'a \ 'a" (infixl "\<^loc>\" 70) ``` haftmann@19281 ` 13` ``` assumes assoc: "x \<^loc>\ y \<^loc>\ z = x \<^loc>\ (y \<^loc>\ z)" ``` haftmann@19281 ` 14` haftmann@19281 ` 15` ```instance nat :: semigroup ``` haftmann@19281 ` 16` ``` "m \ n == (m::nat) + n" ``` haftmann@19281 ` 17` ```proof ``` haftmann@19281 ` 18` ``` fix m n q :: nat ``` haftmann@19281 ` 19` ``` from semigroup_nat_def show "m \ n \ q = m \ (n \ q)" by simp ``` haftmann@19281 ` 20` ```qed ``` haftmann@19281 ` 21` haftmann@19281 ` 22` ```instance int :: semigroup ``` haftmann@19281 ` 23` ``` "k \ l == (k::int) + l" ``` haftmann@19281 ` 24` ```proof ``` haftmann@19281 ` 25` ``` fix k l j :: int ``` haftmann@19281 ` 26` ``` from semigroup_int_def show "k \ l \ j = k \ (l \ j)" by simp ``` haftmann@19281 ` 27` ```qed ``` haftmann@19281 ` 28` haftmann@19281 ` 29` ```instance (type) list :: semigroup ``` haftmann@19281 ` 30` ``` "xs \ ys == xs @ ys" ``` haftmann@19281 ` 31` ```proof ``` haftmann@19281 ` 32` ``` fix xs ys zs :: "'a list" ``` haftmann@19281 ` 33` ``` show "xs \ ys \ zs = xs \ (ys \ zs)" ``` haftmann@19281 ` 34` ``` proof - ``` haftmann@19281 ` 35` ``` from semigroup_list_def have "\xs ys::'a list. xs \ 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>\") ``` haftmann@19281 ` 42` ``` assumes neutl: "\<^loc>\ \<^loc>\ x = x" ``` haftmann@19281 ` 43` haftmann@19281 ` 44` ```instance nat :: monoidl ``` haftmann@19281 ` 45` ``` "\ == (0::nat)" ``` haftmann@19281 ` 46` ```proof ``` haftmann@19281 ` 47` ``` fix n :: nat ``` haftmann@19281 ` 48` ``` from semigroup_nat_def monoidl_nat_def show "\ \ n = n" by simp ``` haftmann@19281 ` 49` ```qed ``` haftmann@19281 ` 50` haftmann@19281 ` 51` ```instance int :: monoidl ``` haftmann@19281 ` 52` ``` "\ == (0::int)" ``` haftmann@19281 ` 53` ```proof ``` haftmann@19281 ` 54` ``` fix k :: int ``` haftmann@19281 ` 55` ``` from semigroup_int_def monoidl_int_def show "\ \ k = k" by simp ``` haftmann@19281 ` 56` ```qed ``` haftmann@19281 ` 57` haftmann@19281 ` 58` ```instance (type) list :: monoidl ``` haftmann@19281 ` 59` ``` "\ == []" ``` haftmann@19281 ` 60` ```proof ``` haftmann@19281 ` 61` ``` fix xs :: "'a list" ``` haftmann@19281 ` 62` ``` show "\ \ xs = xs" ``` haftmann@19281 ` 63` ``` proof - ``` haftmann@19281 ` 64` ``` from semigroup_list_def have "\xs ys::'a list. xs \ ys == xs @ ys". ``` haftmann@19281 ` 65` ``` moreover from monoidl_list_def have "\ == []::'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>\ \<^loc>\ = 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 \ \ = xs" ``` haftmann@19281 ` 77` ``` proof - ``` haftmann@19281 ` 78` ``` from semigroup_list_def have "\xs ys::'a list. xs \ ys == xs @ ys". ``` haftmann@19281 ` 79` ``` moreover from monoidl_list_def have "\ == []::'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>\ y = y \<^loc>\ 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 \ \ = 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 \ m = m \ 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 \ \ = 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 \ l = l \ 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. \x. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\ }" ``` haftmann@19281 ` 108` haftmann@19281 ` 109` ```lemma (in monoid) inv_obtain: ``` haftmann@19281 ` 110` ``` assumes ass: "x \ units" ``` haftmann@19281 ` 111` ``` obtains y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" ``` haftmann@19281 ` 112` ```proof - ``` haftmann@19281 ` 113` ``` from ass units_def obtain y ``` haftmann@19281 ` 114` ``` where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" 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>\ x = \<^loc>\" "x \<^loc>\ y' = \<^loc>\" ``` haftmann@19281 ` 120` ``` shows "y = y'" ``` haftmann@19281 ` 121` ```proof - ``` haftmann@19281 ` 122` ``` from eq neutr have "y = y \<^loc>\ (x \<^loc>\ y')" by simp ``` haftmann@19281 ` 123` ``` also with assoc have "... = (y \<^loc>\ x) \<^loc>\ 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>\ y = \<^loc>\" ``` haftmann@19281 ` 130` ``` and G: "x \ units" ``` haftmann@19281 ` 131` ``` shows "y \<^loc>\ x = \<^loc>\" ``` haftmann@19281 ` 132` ```proof - ``` haftmann@19281 ` 133` ``` from G inv_obtain obtain z ``` haftmann@19281 ` 134` ``` where z_choice: "z \<^loc>\ x = \<^loc>\" by blast ``` haftmann@19281 ` 135` ``` from inv neutl neutr have "x \<^loc>\ y \<^loc>\ x = x \<^loc>\ \<^loc>\" by simp ``` haftmann@19281 ` 136` ``` with assoc have "z \<^loc>\ x \<^loc>\ y \<^loc>\ x = z \<^loc>\ x \<^loc>\ \<^loc>\" 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 \ 'a \ 'a) \ 'a \ nat \ 'a \ '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 \ 'a \ 'a" ``` haftmann@19281 ` 149` ``` npow_def_prim: "npow n x = reduce (op \<^loc>\) \<^loc>\ n x" ``` haftmann@19281 ` 150` haftmann@19281 ` 151` ```abbreviation (in monoid) ``` haftmann@19281 ` 152` ``` abbrev_npow :: "'a \ nat \ 'a" (infix "\<^loc>\" 75) ``` haftmann@19281 ` 153` ``` "(x \<^loc>\ n) = npow n x" ``` haftmann@19281 ` 154` haftmann@19281 ` 155` ```lemma (in monoid) npow_def: ``` haftmann@19281 ` 156` ``` "x \<^loc>\ 0 = \<^loc>\" ``` haftmann@19281 ` 157` ``` "x \<^loc>\ Suc n = x \<^loc>\ x \<^loc>\ 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>\ \<^loc>\ n = \<^loc>\" ``` 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>\ 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@19281 ` 169` ``` case (Suc n) with prems 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 \ 'a" ("\<^loc>\
_" [81] 80) ``` haftmann@19281 ` 178` ``` assumes invl: "\<^loc>\
x \<^loc>\ x = \<^loc>\" ``` 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` ``` "\
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 "\
k \ k = \" by simp ``` haftmann@19281 ` 187` ```qed ``` haftmann@19281 ` 188` haftmann@19281 ` 189` ```lemma (in group) cancel: ``` haftmann@19281 ` 190` ``` "(x \<^loc>\ y = x \<^loc>\ z) = (y = z)" ``` haftmann@19281 ` 191` ```proof ``` haftmann@19281 ` 192` ``` fix x y z :: 'a ``` haftmann@19281 ` 193` ``` assume eq: "x \<^loc>\ y = x \<^loc>\ z" ``` haftmann@19281 ` 194` ``` hence "\<^loc>\
x \<^loc>\ (x \<^loc>\ y) = \<^loc>\
x \<^loc>\ (x \<^loc>\ z)" by simp ``` haftmann@19281 ` 195` ``` with assoc have "\<^loc>\
x \<^loc>\ x \<^loc>\ y = \<^loc>\
x \<^loc>\ x \<^loc>\ 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>\ y = x \<^loc>\ z" by simp ``` haftmann@19281 ` 201` ```qed ``` haftmann@19281 ` 202` haftmann@19281 ` 203` ```lemma (in group) neutr: ``` haftmann@19281 ` 204` ``` "x \<^loc>\ \<^loc>\ = x" ``` haftmann@19281 ` 205` ```proof - ``` haftmann@19281 ` 206` ``` from invl have "\<^loc>\
x \<^loc>\ x = \<^loc>\" by simp ``` haftmann@19281 ` 207` ``` with assoc [symmetric] neutl invl have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\) = \<^loc>\
x \<^loc>\ 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>\ \<^loc>\
x = \<^loc>\" ``` haftmann@19281 ` 213` ```proof - ``` haftmann@19281 ` 214` ``` from neutl invl have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x" by simp ``` haftmann@19281 ` 215` ``` with neutr have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 216` ``` with assoc have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\
x) = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 217` ``` with cancel show ?thesis .. ``` haftmann@19281 ` 218` ```qed ``` haftmann@19281 ` 219` haftmann@19281 ` 220` ```interpretation group < monoid ``` haftmann@19281 ` 221` ```proof ``` haftmann@19281 ` 222` ``` fix x :: "'a" ``` haftmann@19281 ` 223` ``` from neutr show "x \<^loc>\ \<^loc>\ = x" . ``` haftmann@19281 ` 224` ```qed ``` haftmann@19281 ` 225` haftmann@19281 ` 226` ```instance group < monoid ``` haftmann@19281 ` 227` ```proof ``` haftmann@19281 ` 228` ``` fix x :: "'a::group" ``` haftmann@19281 ` 229` ``` from group.mult_one.neutr [standard] show "x \ \ = x" . ``` haftmann@19281 ` 230` ```qed ``` haftmann@19281 ` 231` haftmann@19281 ` 232` ```lemma (in group) all_inv [intro]: ``` haftmann@19281 ` 233` ``` "(x::'a) \ monoid.units (op \<^loc>\) \<^loc>\" ``` haftmann@19281 ` 234` ``` unfolding units_def ``` haftmann@19281 ` 235` ```proof - ``` haftmann@19281 ` 236` ``` fix x :: "'a" ``` haftmann@19281 ` 237` ``` from invl invr have "\<^loc>\
x \<^loc>\ x = \<^loc>\" and "x \<^loc>\ \<^loc>\
x = \<^loc>\" . ``` haftmann@19281 ` 238` ``` then obtain y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" .. ``` haftmann@19281 ` 239` ``` hence "\y\'a. y \<^loc>\ x = \<^loc>\ \ x \<^loc>\ y = \<^loc>\" by blast ``` haftmann@19281 ` 240` ``` thus "x \ {y\'a. \x\'a. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" by simp ``` haftmann@19281 ` 241` ```qed ``` haftmann@19281 ` 242` haftmann@19281 ` 243` ```lemma (in group) cancer: ``` haftmann@19281 ` 244` ``` "(y \<^loc>\ x = z \<^loc>\ x) = (y = z)" ``` haftmann@19281 ` 245` ```proof ``` haftmann@19281 ` 246` ``` assume eq: "y \<^loc>\ x = z \<^loc>\ x" ``` haftmann@19281 ` 247` ``` with assoc [symmetric] have "y \<^loc>\ (x \<^loc>\ \<^loc>\
x) = z \<^loc>\ (x \<^loc>\ \<^loc>\
x)" by (simp del: invr) ``` haftmann@19281 ` 248` ``` with invr neutr show "y = z" by simp ``` haftmann@19281 ` 249` ```next ``` haftmann@19281 ` 250` ``` assume eq: "y = z" ``` haftmann@19281 ` 251` ``` thus "y \<^loc>\ x = z \<^loc>\ x" by simp ``` haftmann@19281 ` 252` ```qed ``` haftmann@19281 ` 253` haftmann@19281 ` 254` ```lemma (in group) inv_one: ``` haftmann@19281 ` 255` ``` "\<^loc>\
\<^loc>\ = \<^loc>\" ``` haftmann@19281 ` 256` ```proof - ``` haftmann@19281 ` 257` ``` from neutl have "\<^loc>\
\<^loc>\ = \<^loc>\ \<^loc>\ (\<^loc>\
\<^loc>\)" .. ``` haftmann@19281 ` 258` ``` moreover from invr have "... = \<^loc>\" by simp ``` haftmann@19281 ` 259` ``` finally show ?thesis . ``` haftmann@19281 ` 260` ```qed ``` haftmann@19281 ` 261` haftmann@19281 ` 262` ```lemma (in group) inv_inv: ``` haftmann@19281 ` 263` ``` "\<^loc>\
(\<^loc>\
x) = x" ``` haftmann@19281 ` 264` ```proof - ``` haftmann@19281 ` 265` ``` from invl invr neutr ``` haftmann@19281 ` 266` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ \<^loc>\
x \<^loc>\ x = x \<^loc>\ \<^loc>\
x \<^loc>\ x" by simp ``` haftmann@19281 ` 267` ``` with assoc [symmetric] ``` haftmann@19281 ` 268` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ (\<^loc>\
x \<^loc>\ x) = x \<^loc>\ (\<^loc>\
x \<^loc>\ x)" by simp ``` haftmann@19281 ` 269` ``` with invl neutr show ?thesis by simp ``` haftmann@19281 ` 270` ```qed ``` haftmann@19281 ` 271` haftmann@19281 ` 272` ```lemma (in group) inv_mult_group: ``` haftmann@19281 ` 273` ``` "\<^loc>\
(x \<^loc>\ y) = \<^loc>\
y \<^loc>\ \<^loc>\
x" ``` haftmann@19281 ` 274` ```proof - ``` haftmann@19281 ` 275` ``` from invl have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ (x \<^loc>\ y) = \<^loc>\" by simp ``` haftmann@19281 ` 276` ``` with assoc have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ x \<^loc>\ y = \<^loc>\" by simp ``` haftmann@19281 ` 277` ``` with neutl have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ x \<^loc>\ y \<^loc>\ \<^loc>\
y \<^loc>\ \<^loc>\
x = \<^loc>\
y \<^loc>\ \<^loc>\
x" by simp ``` haftmann@19281 ` 278` ``` with assoc have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ (x \<^loc>\ (y \<^loc>\ \<^loc>\
y) \<^loc>\ \<^loc>\
x) = \<^loc>\
y \<^loc>\ \<^loc>\
x" by simp ``` haftmann@19281 ` 279` ``` with invr neutr show ?thesis by simp ``` haftmann@19281 ` 280` ```qed ``` haftmann@19281 ` 281` haftmann@19281 ` 282` ```lemma (in group) inv_comm: ``` haftmann@19281 ` 283` ``` "x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ x" ``` haftmann@19281 ` 284` ```using invr invl by simp ``` haftmann@19281 ` 285` haftmann@19281 ` 286` ```definition (in group) ``` haftmann@19281 ` 287` ``` pow :: "int \ 'a \ 'a" ``` haftmann@19281 ` 288` ``` pow_def: "pow k x = (if k < 0 then \<^loc>\
(monoid.npow (op \<^loc>\) \<^loc>\ (nat (-k)) x) ``` haftmann@19281 ` 289` ``` else (monoid.npow (op \<^loc>\) \<^loc>\ (nat k) x))" ``` haftmann@19281 ` 290` haftmann@19281 ` 291` ```abbreviation (in group) ``` haftmann@19281 ` 292` ``` abbrev_pow :: "'a \ int \ 'a" (infix "\<^loc>\" 75) ``` haftmann@19281 ` 293` ``` "(x \<^loc>\ k) = pow k x" ``` haftmann@19281 ` 294` haftmann@19281 ` 295` ```lemma (in group) int_pow_zero: ``` haftmann@19281 ` 296` ``` "x \<^loc>\ (0::int) = \<^loc>\" ``` haftmann@19281 ` 297` ```using npow_def pow_def by simp ``` haftmann@19281 ` 298` haftmann@19281 ` 299` ```lemma (in group) int_pow_one: ``` haftmann@19281 ` 300` ``` "\<^loc>\ \<^loc>\ (k::int) = \<^loc>\" ``` haftmann@19281 ` 301` ```using pow_def nat_pow_one inv_one by simp ``` haftmann@19281 ` 302` haftmann@19281 ` 303` ```instance group_prod_def: (group, group) * :: group ``` haftmann@19281 ` 304` ``` mult_prod_def: "x \ y == let (x1, x2) = x in (let (y1, y2) = y in ``` haftmann@19281 ` 305` ``` (x1 \ y1, x2 \ y2))" ``` haftmann@19281 ` 306` ``` mult_one_def: "\ == (\, \)" ``` haftmann@19281 ` 307` ``` mult_inv_def: "\
x == let (x1, x2) = x in (\
x1, \
x2)" ``` haftmann@19281 ` 308` ```by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl) ``` haftmann@19281 ` 309` haftmann@19281 ` 310` ```instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm ``` haftmann@19281 ` 311` ```by default (simp_all add: split_paired_all group_prod_def semigroup.assoc monoidl.neutl group.invl monoid_comm.comm) ``` haftmann@19281 ` 312` haftmann@19281 ` 313` ```definition ``` haftmann@19281 ` 314` ``` "x = ((2::nat) \ \ \ 3, (2::int) \ \ \ \
3, [1::nat, 2] \ \ \ [1, 2, 3])" ``` haftmann@19281 ` 315` ``` "y = (2 :: int, \
2 :: int) \ \ \ (3, \
3)" ``` haftmann@19281 ` 316` haftmann@19281 ` 317` ```code_generate "op \" "\" "inv" ``` haftmann@19281 ` 318` ```code_generate x ``` haftmann@19281 ` 319` ```code_generate y ``` haftmann@19281 ` 320` haftmann@19281 ` 321` ```code_serialize ml (-) ``` haftmann@19281 ` 322` haftmann@19281 ` 323` ```end ```