src/HOL/ex/Classpackage.thy
 author haftmann Tue Sep 19 15:22:05 2006 +0200 (2006-09-19) changeset 20597 65fe827aa595 parent 20453 855f07fabd76 child 21080 7d73aa966207 permissions -rw-r--r--
 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@20178 ` 16` ``` "m \ n \ m + 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@20178 ` 23` ``` "k \ l \ k + 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@20597 ` 29` ```instance list :: (type) semigroup ``` haftmann@20178 ` 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@20178 ` 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@20178 ` 44` ```instance monoidl_num_def: nat :: monoidl and int :: monoidl ``` haftmann@20178 ` 45` ``` "\ \ 0" ``` haftmann@20178 ` 46` ``` "\ \ 0" ``` haftmann@19281 ` 47` ```proof ``` haftmann@19281 ` 48` ``` fix n :: nat ``` haftmann@20178 ` 49` ``` from monoidl_num_def show "\ \ n = n" by simp ``` haftmann@20178 ` 50` ```next ``` haftmann@19281 ` 51` ``` fix k :: int ``` haftmann@20178 ` 52` ``` from monoidl_num_def show "\ \ k = k" by simp ``` haftmann@19281 ` 53` ```qed ``` haftmann@19281 ` 54` haftmann@20597 ` 55` ```instance list :: (type) monoidl ``` haftmann@20178 ` 56` ``` "\ \ []" ``` haftmann@19281 ` 57` ```proof ``` haftmann@19281 ` 58` ``` fix xs :: "'a list" ``` haftmann@19281 ` 59` ``` show "\ \ xs = xs" ``` haftmann@19281 ` 60` ``` proof - ``` haftmann@20178 ` 61` ``` from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . ``` haftmann@20178 ` 62` ``` moreover from monoidl_list_def have "\ \ []\'a list" by simp ``` haftmann@19281 ` 63` ``` ultimately show ?thesis by simp ``` haftmann@19281 ` 64` ``` qed ``` haftmann@19281 ` 65` ```qed ``` haftmann@19281 ` 66` haftmann@19281 ` 67` ```class monoid = monoidl + ``` haftmann@19281 ` 68` ``` assumes neutr: "x \<^loc>\ \<^loc>\ = x" ``` haftmann@19281 ` 69` haftmann@20597 ` 70` ```instance monoid_list_def: list :: (type) monoid ``` haftmann@19281 ` 71` ```proof ``` haftmann@19281 ` 72` ``` fix xs :: "'a list" ``` haftmann@19281 ` 73` ``` show "xs \ \ = xs" ``` haftmann@19281 ` 74` ``` proof - ``` haftmann@20178 ` 75` ``` from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . ``` haftmann@20178 ` 76` ``` moreover from monoid_list_def have "\ \ []\'a list" by simp ``` haftmann@19281 ` 77` ``` ultimately show ?thesis by simp ``` haftmann@19281 ` 78` ``` qed ``` haftmann@19281 ` 79` ```qed ``` haftmann@19281 ` 80` haftmann@19281 ` 81` ```class monoid_comm = monoid + ``` haftmann@19281 ` 82` ``` assumes comm: "x \<^loc>\ y = y \<^loc>\ x" ``` haftmann@19281 ` 83` haftmann@20178 ` 84` ```instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm ``` haftmann@19281 ` 85` ```proof ``` haftmann@19281 ` 86` ``` fix n :: nat ``` haftmann@20178 ` 87` ``` from monoid_comm_num_def show "n \ \ = n" by simp ``` haftmann@19281 ` 88` ```next ``` haftmann@19281 ` 89` ``` fix n m :: nat ``` haftmann@20178 ` 90` ``` from monoid_comm_num_def show "n \ m = m \ n" by simp ``` haftmann@20178 ` 91` ```next ``` haftmann@19281 ` 92` ``` fix k :: int ``` haftmann@20178 ` 93` ``` from monoid_comm_num_def show "k \ \ = k" by simp ``` haftmann@19281 ` 94` ```next ``` haftmann@19281 ` 95` ``` fix k l :: int ``` haftmann@20178 ` 96` ``` from monoid_comm_num_def show "k \ l = l \ k" by simp ``` haftmann@19281 ` 97` ```qed ``` haftmann@19281 ` 98` haftmann@19281 ` 99` ```definition (in monoid) ``` haftmann@19281 ` 100` ``` units :: "'a set" ``` haftmann@19281 ` 101` ``` units_def: "units = { y. \x. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\ }" ``` haftmann@19281 ` 102` haftmann@19281 ` 103` ```lemma (in monoid) inv_obtain: ``` haftmann@19281 ` 104` ``` assumes ass: "x \ units" ``` haftmann@19281 ` 105` ``` obtains y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" ``` haftmann@19281 ` 106` ```proof - ``` haftmann@19281 ` 107` ``` from ass units_def obtain y ``` haftmann@19281 ` 108` ``` where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" by auto ``` haftmann@19281 ` 109` ``` thus ?thesis .. ``` haftmann@19281 ` 110` ```qed ``` haftmann@19281 ` 111` haftmann@19281 ` 112` ```lemma (in monoid) inv_unique: ``` haftmann@19281 ` 113` ``` assumes eq: "y \<^loc>\ x = \<^loc>\" "x \<^loc>\ y' = \<^loc>\" ``` haftmann@19281 ` 114` ``` shows "y = y'" ``` haftmann@19281 ` 115` ```proof - ``` haftmann@19281 ` 116` ``` from eq neutr have "y = y \<^loc>\ (x \<^loc>\ y')" by simp ``` haftmann@19281 ` 117` ``` also with assoc have "... = (y \<^loc>\ x) \<^loc>\ y'" by simp ``` haftmann@19281 ` 118` ``` also with eq neutl have "... = y'" by simp ``` haftmann@19281 ` 119` ``` finally show ?thesis . ``` haftmann@19281 ` 120` ```qed ``` haftmann@19281 ` 121` haftmann@19281 ` 122` ```lemma (in monoid) units_inv_comm: ``` haftmann@19281 ` 123` ``` assumes inv: "x \<^loc>\ y = \<^loc>\" ``` haftmann@19281 ` 124` ``` and G: "x \ units" ``` haftmann@19281 ` 125` ``` shows "y \<^loc>\ x = \<^loc>\" ``` haftmann@19281 ` 126` ```proof - ``` haftmann@19281 ` 127` ``` from G inv_obtain obtain z ``` haftmann@19281 ` 128` ``` where z_choice: "z \<^loc>\ x = \<^loc>\" by blast ``` haftmann@19281 ` 129` ``` from inv neutl neutr have "x \<^loc>\ y \<^loc>\ x = x \<^loc>\ \<^loc>\" by simp ``` haftmann@19281 ` 130` ``` with assoc have "z \<^loc>\ x \<^loc>\ y \<^loc>\ x = z \<^loc>\ x \<^loc>\ \<^loc>\" by simp ``` haftmann@19281 ` 131` ``` with neutl z_choice show ?thesis by simp ``` haftmann@19281 ` 132` ```qed ``` haftmann@19281 ` 133` haftmann@19281 ` 134` ```consts ``` haftmann@19281 ` 135` ``` reduce :: "('a \ 'a \ 'a) \ 'a \ nat \ 'a \ 'a" ``` haftmann@19281 ` 136` haftmann@19281 ` 137` ```primrec ``` haftmann@19281 ` 138` ``` "reduce f g 0 x = g" ``` haftmann@19281 ` 139` ``` "reduce f g (Suc n) x = f x (reduce f g n x)" ``` haftmann@19281 ` 140` haftmann@19281 ` 141` ```definition (in monoid) ``` haftmann@19281 ` 142` ``` npow :: "nat \ 'a \ 'a" ``` haftmann@19281 ` 143` ``` npow_def_prim: "npow n x = reduce (op \<^loc>\) \<^loc>\ n x" ``` haftmann@19281 ` 144` haftmann@19281 ` 145` ```abbreviation (in monoid) ``` haftmann@19281 ` 146` ``` abbrev_npow :: "'a \ nat \ 'a" (infix "\<^loc>\" 75) ``` haftmann@20178 ` 147` ``` "x \<^loc>\ n \ npow n x" ``` haftmann@19281 ` 148` haftmann@19281 ` 149` ```lemma (in monoid) npow_def: ``` haftmann@19281 ` 150` ``` "x \<^loc>\ 0 = \<^loc>\" ``` haftmann@19281 ` 151` ``` "x \<^loc>\ Suc n = x \<^loc>\ x \<^loc>\ n" ``` haftmann@19281 ` 152` ```using npow_def_prim by simp_all ``` haftmann@19281 ` 153` haftmann@19281 ` 154` ```lemma (in monoid) nat_pow_one: ``` haftmann@19281 ` 155` ``` "\<^loc>\ \<^loc>\ n = \<^loc>\" ``` haftmann@19281 ` 156` ```using npow_def neutl by (induct n) simp_all ``` haftmann@19281 ` 157` haftmann@19281 ` 158` ```lemma (in monoid) nat_pow_mult: ``` haftmann@19281 ` 159` ``` "npow n x \<^loc>\ npow m x = npow (n + m) x" ``` haftmann@19281 ` 160` ```proof (induct n) ``` haftmann@19281 ` 161` ``` case 0 with neutl npow_def show ?case by simp ``` haftmann@19281 ` 162` ```next ``` haftmann@19933 ` 163` ``` case (Suc n) with Suc.hyps assoc npow_def show ?case by simp ``` haftmann@19281 ` 164` ```qed ``` haftmann@19281 ` 165` haftmann@19281 ` 166` ```lemma (in monoid) nat_pow_pow: ``` haftmann@19281 ` 167` ``` "npow n (npow m x) = npow (n * m) x" ``` haftmann@19281 ` 168` ```using npow_def nat_pow_mult by (induct n) simp_all ``` haftmann@19281 ` 169` haftmann@19281 ` 170` ```class group = monoidl + ``` haftmann@19281 ` 171` ``` fixes inv :: "'a \ 'a" ("\<^loc>\
_" [81] 80) ``` haftmann@19281 ` 172` ``` assumes invl: "\<^loc>\
x \<^loc>\ x = \<^loc>\" ``` haftmann@19281 ` 173` haftmann@19281 ` 174` ```class group_comm = group + monoid_comm ``` haftmann@19281 ` 175` haftmann@20178 ` 176` ```instance group_comm_int_def: int :: group_comm ``` haftmann@20178 ` 177` ``` "\
k \ - (k\int)" ``` haftmann@19281 ` 178` ```proof ``` haftmann@19281 ` 179` ``` fix k :: int ``` haftmann@20178 ` 180` ``` from group_comm_int_def show "\
k \ k = \" by simp ``` haftmann@19281 ` 181` ```qed ``` haftmann@19281 ` 182` haftmann@19281 ` 183` ```lemma (in group) cancel: ``` haftmann@19281 ` 184` ``` "(x \<^loc>\ y = x \<^loc>\ z) = (y = z)" ``` haftmann@19281 ` 185` ```proof ``` haftmann@19281 ` 186` ``` fix x y z :: 'a ``` haftmann@19281 ` 187` ``` assume eq: "x \<^loc>\ y = x \<^loc>\ z" ``` haftmann@19281 ` 188` ``` hence "\<^loc>\
x \<^loc>\ (x \<^loc>\ y) = \<^loc>\
x \<^loc>\ (x \<^loc>\ z)" by simp ``` haftmann@19281 ` 189` ``` with assoc have "\<^loc>\
x \<^loc>\ x \<^loc>\ y = \<^loc>\
x \<^loc>\ x \<^loc>\ z" by simp ``` haftmann@19281 ` 190` ``` with neutl invl show "y = z" by simp ``` haftmann@19281 ` 191` ```next ``` haftmann@19281 ` 192` ``` fix x y z :: 'a ``` haftmann@19281 ` 193` ``` assume eq: "y = z" ``` haftmann@19281 ` 194` ``` thus "x \<^loc>\ y = x \<^loc>\ z" by simp ``` haftmann@19281 ` 195` ```qed ``` haftmann@19281 ` 196` haftmann@19281 ` 197` ```lemma (in group) neutr: ``` haftmann@19281 ` 198` ``` "x \<^loc>\ \<^loc>\ = x" ``` haftmann@19281 ` 199` ```proof - ``` haftmann@19281 ` 200` ``` from invl have "\<^loc>\
x \<^loc>\ x = \<^loc>\" by simp ``` haftmann@19281 ` 201` ``` with assoc [symmetric] neutl invl have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\) = \<^loc>\
x \<^loc>\ x" by simp ``` haftmann@19281 ` 202` ``` with cancel show ?thesis by simp ``` haftmann@19281 ` 203` ```qed ``` haftmann@19281 ` 204` haftmann@19281 ` 205` ```lemma (in group) invr: ``` haftmann@19281 ` 206` ``` "x \<^loc>\ \<^loc>\
x = \<^loc>\" ``` haftmann@19281 ` 207` ```proof - ``` haftmann@19281 ` 208` ``` from neutl invl have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x" by simp ``` haftmann@19281 ` 209` ``` with neutr have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 210` ``` with assoc have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\
x) = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 211` ``` with cancel show ?thesis .. ``` haftmann@19281 ` 212` ```qed ``` haftmann@19281 ` 213` haftmann@20383 ` 214` ```instance group < monoid ``` haftmann@19928 ` 215` ```proof - ``` haftmann@20383 ` 216` ``` fix x ``` haftmann@19281 ` 217` ``` from neutr show "x \<^loc>\ \<^loc>\ = x" . ``` haftmann@19281 ` 218` ```qed ``` haftmann@19281 ` 219` haftmann@19281 ` 220` ```lemma (in group) all_inv [intro]: ``` haftmann@20178 ` 221` ``` "(x\'a) \ monoid.units (op \<^loc>\) \<^loc>\" ``` haftmann@19281 ` 222` ``` unfolding units_def ``` haftmann@19281 ` 223` ```proof - ``` haftmann@19281 ` 224` ``` fix x :: "'a" ``` haftmann@19281 ` 225` ``` from invl invr have "\<^loc>\
x \<^loc>\ x = \<^loc>\" and "x \<^loc>\ \<^loc>\
x = \<^loc>\" . ``` haftmann@19281 ` 226` ``` then obtain y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" .. ``` haftmann@19281 ` 227` ``` hence "\y\'a. y \<^loc>\ x = \<^loc>\ \ x \<^loc>\ y = \<^loc>\" by blast ``` haftmann@19281 ` 228` ``` thus "x \ {y\'a. \x\'a. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" by simp ``` haftmann@19281 ` 229` ```qed ``` haftmann@19281 ` 230` haftmann@19281 ` 231` ```lemma (in group) cancer: ``` haftmann@19281 ` 232` ``` "(y \<^loc>\ x = z \<^loc>\ x) = (y = z)" ``` haftmann@19281 ` 233` ```proof ``` haftmann@19281 ` 234` ``` assume eq: "y \<^loc>\ x = z \<^loc>\ x" ``` haftmann@19281 ` 235` ``` with assoc [symmetric] have "y \<^loc>\ (x \<^loc>\ \<^loc>\
x) = z \<^loc>\ (x \<^loc>\ \<^loc>\
x)" by (simp del: invr) ``` haftmann@19281 ` 236` ``` with invr neutr show "y = z" by simp ``` haftmann@19281 ` 237` ```next ``` haftmann@19281 ` 238` ``` assume eq: "y = z" ``` haftmann@19281 ` 239` ``` thus "y \<^loc>\ x = z \<^loc>\ x" by simp ``` haftmann@19281 ` 240` ```qed ``` haftmann@19281 ` 241` haftmann@19281 ` 242` ```lemma (in group) inv_one: ``` haftmann@19281 ` 243` ``` "\<^loc>\
\<^loc>\ = \<^loc>\" ``` haftmann@19281 ` 244` ```proof - ``` haftmann@19281 ` 245` ``` from neutl have "\<^loc>\
\<^loc>\ = \<^loc>\ \<^loc>\ (\<^loc>\
\<^loc>\)" .. ``` haftmann@19281 ` 246` ``` moreover from invr have "... = \<^loc>\" by simp ``` haftmann@19281 ` 247` ``` finally show ?thesis . ``` haftmann@19281 ` 248` ```qed ``` haftmann@19281 ` 249` haftmann@19281 ` 250` ```lemma (in group) inv_inv: ``` haftmann@19281 ` 251` ``` "\<^loc>\
(\<^loc>\
x) = x" ``` haftmann@19281 ` 252` ```proof - ``` haftmann@19281 ` 253` ``` from invl invr neutr ``` haftmann@19281 ` 254` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ \<^loc>\
x \<^loc>\ x = x \<^loc>\ \<^loc>\
x \<^loc>\ x" by simp ``` haftmann@19281 ` 255` ``` with assoc [symmetric] ``` haftmann@19281 ` 256` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ (\<^loc>\
x \<^loc>\ x) = x \<^loc>\ (\<^loc>\
x \<^loc>\ x)" by simp ``` haftmann@19281 ` 257` ``` with invl neutr show ?thesis by simp ``` haftmann@19281 ` 258` ```qed ``` haftmann@19281 ` 259` haftmann@19281 ` 260` ```lemma (in group) inv_mult_group: ``` haftmann@19281 ` 261` ``` "\<^loc>\
(x \<^loc>\ y) = \<^loc>\
y \<^loc>\ \<^loc>\
x" ``` haftmann@19281 ` 262` ```proof - ``` haftmann@19281 ` 263` ``` from invl have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ (x \<^loc>\ y) = \<^loc>\" by simp ``` haftmann@19281 ` 264` ``` with assoc have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ x \<^loc>\ y = \<^loc>\" by simp ``` haftmann@19281 ` 265` ``` 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 ` 266` ``` 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 ` 267` ``` with invr neutr show ?thesis by simp ``` haftmann@19281 ` 268` ```qed ``` haftmann@19281 ` 269` haftmann@19281 ` 270` ```lemma (in group) inv_comm: ``` haftmann@19281 ` 271` ``` "x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ x" ``` haftmann@19281 ` 272` ```using invr invl by simp ``` haftmann@19281 ` 273` haftmann@19281 ` 274` ```definition (in group) ``` haftmann@19281 ` 275` ``` pow :: "int \ 'a \ 'a" ``` haftmann@19281 ` 276` ``` pow_def: "pow k x = (if k < 0 then \<^loc>\
(monoid.npow (op \<^loc>\) \<^loc>\ (nat (-k)) x) ``` haftmann@19281 ` 277` ``` else (monoid.npow (op \<^loc>\) \<^loc>\ (nat k) x))" ``` haftmann@19281 ` 278` haftmann@19281 ` 279` ```abbreviation (in group) ``` haftmann@19281 ` 280` ``` abbrev_pow :: "'a \ int \ 'a" (infix "\<^loc>\" 75) ``` haftmann@19928 ` 281` ``` "x \<^loc>\ k \ pow k x" ``` haftmann@19281 ` 282` haftmann@19281 ` 283` ```lemma (in group) int_pow_zero: ``` haftmann@20178 ` 284` ``` "x \<^loc>\ (0\int) = \<^loc>\" ``` haftmann@19281 ` 285` ```using npow_def pow_def by simp ``` haftmann@19281 ` 286` haftmann@19281 ` 287` ```lemma (in group) int_pow_one: ``` haftmann@20178 ` 288` ``` "\<^loc>\ \<^loc>\ (k\int) = \<^loc>\" ``` haftmann@19281 ` 289` ```using pow_def nat_pow_one inv_one by simp ``` haftmann@19281 ` 290` haftmann@20597 ` 291` ```instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup ``` haftmann@20178 ` 292` ``` mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in ``` haftmann@19958 ` 293` ``` (x1 \ y1, x2 \ y2)" ``` haftmann@20427 ` 294` ```by default (simp_all add: split_paired_all semigroup_prod_def assoc) ``` haftmann@20427 ` 295` haftmann@20597 ` 296` ```instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl ``` haftmann@20427 ` 297` ``` one_prod_def: "\ \ (\, \)" ``` haftmann@20427 ` 298` ```by default (simp_all add: split_paired_all monoidl_prod_def neutl) ``` haftmann@20427 ` 299` haftmann@20597 ` 300` ```instance monoid_prod_def: * :: (monoid, monoid) monoid ``` haftmann@20427 ` 301` ```by default (simp_all add: split_paired_all monoid_prod_def neutr) ``` haftmann@20427 ` 302` haftmann@20597 ` 303` ```instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm ``` haftmann@20427 ` 304` ```by default (simp_all add: split_paired_all monoidl_prod_def comm) ``` haftmann@20427 ` 305` haftmann@20597 ` 306` ```instance group_prod_def: * :: (group, group) group ``` haftmann@20427 ` 307` ``` inv_prod_def: "\
x \ let (x1, x2) = x in (\
x1, \
x2)" ``` haftmann@20427 ` 308` ```by default (simp_all add: split_paired_all group_prod_def invl) ``` haftmann@19281 ` 309` haftmann@20597 ` 310` ```instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm ``` haftmann@20427 ` 311` ```by default (simp_all add: split_paired_all group_prod_def comm) ``` haftmann@19281 ` 312` haftmann@19281 ` 313` ```definition ``` haftmann@20383 ` 314` ``` "X a b c = (a \ \ \ b, a \ \ \ b, [a, b] \ \ \ [a, b, c])" ``` haftmann@20383 ` 315` ``` "Y a b c = (a, \
a) \ \ \ \
(b, \
c)" ``` haftmann@20383 ` 316` haftmann@20383 ` 317` ```definition ``` haftmann@20383 ` 318` ``` "x1 = X (1::nat) 2 3" ``` haftmann@20383 ` 319` ``` "x2 = X (1::int) 2 3" ``` haftmann@20383 ` 320` ``` "y2 = Y (1::int) 2 3" ``` haftmann@19281 ` 321` haftmann@20453 ` 322` ```code_gen "op \" \ inv ``` haftmann@20453 ` 323` ```code_gen X Y (SML) (Haskell) ``` haftmann@20453 ` 324` ```code_gen x1 x2 y2 (SML) (Haskell) ``` haftmann@19281 ` 325` haftmann@20453 ` 326` ```code_gen (SML -) ``` haftmann@19281 ` 327` haftmann@19281 ` 328` ```end ```