src/HOL/ex/Classpackage.thy
 author wenzelm Thu Dec 07 21:44:13 2006 +0100 (2006-12-07) changeset 21707 dfc7b21d0ee9 parent 21545 54cc492d80a9 child 21911 e29bcab0c81c permissions -rw-r--r--
begin/end blocks;
tuned notation;
 haftmann@19281 ` 1` ```(* ID: \$Id\$ ``` haftmann@19281 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@19281 ` 3` ```*) ``` haftmann@19281 ` 4` wenzelm@21707 ` 5` ```header {* Test and examples for new class package *} ``` 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` wenzelm@21707 ` 99` ```context monoid ``` wenzelm@21707 ` 100` ```begin ``` wenzelm@21707 ` 101` wenzelm@21707 ` 102` ```definition ``` wenzelm@21404 ` 103` ``` units :: "'a set" where ``` wenzelm@21707 ` 104` ``` "units = {y. \x. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" ``` haftmann@19281 ` 105` wenzelm@21707 ` 106` ```lemma inv_obtain: ``` wenzelm@21707 ` 107` ``` assumes "x \ units" ``` haftmann@19281 ` 108` ``` obtains y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" ``` haftmann@19281 ` 109` ```proof - ``` wenzelm@21707 ` 110` ``` from assms units_def obtain y ``` haftmann@19281 ` 111` ``` where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" by auto ``` haftmann@19281 ` 112` ``` thus ?thesis .. ``` haftmann@19281 ` 113` ```qed ``` haftmann@19281 ` 114` wenzelm@21707 ` 115` ```lemma inv_unique: ``` wenzelm@21707 ` 116` ``` assumes "y \<^loc>\ x = \<^loc>\" "x \<^loc>\ y' = \<^loc>\" ``` haftmann@19281 ` 117` ``` shows "y = y'" ``` haftmann@19281 ` 118` ```proof - ``` wenzelm@21707 ` 119` ``` from assms neutr have "y = y \<^loc>\ (x \<^loc>\ y')" by simp ``` haftmann@19281 ` 120` ``` also with assoc have "... = (y \<^loc>\ x) \<^loc>\ y'" by simp ``` wenzelm@21707 ` 121` ``` also with assms neutl have "... = y'" by simp ``` haftmann@19281 ` 122` ``` finally show ?thesis . ``` haftmann@19281 ` 123` ```qed ``` haftmann@19281 ` 124` wenzelm@21707 ` 125` ```lemma units_inv_comm: ``` haftmann@19281 ` 126` ``` assumes inv: "x \<^loc>\ y = \<^loc>\" ``` haftmann@19281 ` 127` ``` and G: "x \ units" ``` haftmann@19281 ` 128` ``` shows "y \<^loc>\ x = \<^loc>\" ``` haftmann@19281 ` 129` ```proof - ``` haftmann@19281 ` 130` ``` from G inv_obtain obtain z ``` haftmann@19281 ` 131` ``` where z_choice: "z \<^loc>\ x = \<^loc>\" by blast ``` haftmann@19281 ` 132` ``` from inv neutl neutr have "x \<^loc>\ y \<^loc>\ x = x \<^loc>\ \<^loc>\" by simp ``` haftmann@19281 ` 133` ``` with assoc have "z \<^loc>\ x \<^loc>\ y \<^loc>\ x = z \<^loc>\ x \<^loc>\ \<^loc>\" by simp ``` haftmann@19281 ` 134` ``` with neutl z_choice show ?thesis by simp ``` haftmann@19281 ` 135` ```qed ``` haftmann@19281 ` 136` wenzelm@21707 ` 137` ```end ``` wenzelm@21707 ` 138` haftmann@19281 ` 139` ```consts ``` haftmann@19281 ` 140` ``` reduce :: "('a \ 'a \ 'a) \ 'a \ nat \ 'a \ 'a" ``` haftmann@19281 ` 141` haftmann@19281 ` 142` ```primrec ``` haftmann@19281 ` 143` ``` "reduce f g 0 x = g" ``` haftmann@19281 ` 144` ``` "reduce f g (Suc n) x = f x (reduce f g n x)" ``` haftmann@19281 ` 145` wenzelm@21707 ` 146` ```context monoid ``` wenzelm@21707 ` 147` ```begin ``` wenzelm@21707 ` 148` wenzelm@21707 ` 149` ```definition ``` wenzelm@21404 ` 150` ``` npow :: "nat \ 'a \ 'a" where ``` haftmann@19281 ` 151` ``` npow_def_prim: "npow n x = reduce (op \<^loc>\) \<^loc>\ n x" ``` haftmann@19281 ` 152` wenzelm@21707 ` 153` ```abbreviation ``` wenzelm@21707 ` 154` ``` npow_syn :: "'a \ nat \ 'a" (infix "\<^loc>\" 75) where ``` haftmann@20178 ` 155` ``` "x \<^loc>\ n \ npow n x" ``` haftmann@19281 ` 156` wenzelm@21707 ` 157` ```lemma npow_def: ``` haftmann@19281 ` 158` ``` "x \<^loc>\ 0 = \<^loc>\" ``` haftmann@19281 ` 159` ``` "x \<^loc>\ Suc n = x \<^loc>\ x \<^loc>\ n" ``` haftmann@19281 ` 160` ```using npow_def_prim by simp_all ``` haftmann@19281 ` 161` wenzelm@21707 ` 162` ```lemma nat_pow_one: ``` haftmann@19281 ` 163` ``` "\<^loc>\ \<^loc>\ n = \<^loc>\" ``` haftmann@19281 ` 164` ```using npow_def neutl by (induct n) simp_all ``` haftmann@19281 ` 165` wenzelm@21707 ` 166` ```lemma nat_pow_mult: "x \<^loc>\ n \<^loc>\ x \<^loc>\ m = x \<^loc>\ (n + m)" ``` haftmann@19281 ` 167` ```proof (induct n) ``` haftmann@19281 ` 168` ``` case 0 with neutl npow_def show ?case by simp ``` haftmann@19281 ` 169` ```next ``` haftmann@19933 ` 170` ``` case (Suc n) with Suc.hyps assoc npow_def show ?case by simp ``` haftmann@19281 ` 171` ```qed ``` haftmann@19281 ` 172` wenzelm@21707 ` 173` ```lemma nat_pow_pow: "(x \<^loc>\ m) \<^loc>\ n = x \<^loc>\ (n * m)" ``` haftmann@19281 ` 174` ```using npow_def nat_pow_mult by (induct n) simp_all ``` haftmann@19281 ` 175` wenzelm@21707 ` 176` ```end ``` wenzelm@21707 ` 177` haftmann@19281 ` 178` ```class group = monoidl + ``` haftmann@19281 ` 179` ``` fixes inv :: "'a \ 'a" ("\<^loc>\
_" [81] 80) ``` haftmann@19281 ` 180` ``` assumes invl: "\<^loc>\
x \<^loc>\ x = \<^loc>\" ``` haftmann@19281 ` 181` haftmann@19281 ` 182` ```class group_comm = group + monoid_comm ``` haftmann@19281 ` 183` haftmann@20178 ` 184` ```instance group_comm_int_def: int :: group_comm ``` haftmann@20178 ` 185` ``` "\
k \ - (k\int)" ``` haftmann@19281 ` 186` ```proof ``` haftmann@19281 ` 187` ``` fix k :: int ``` haftmann@20178 ` 188` ``` from group_comm_int_def show "\
k \ k = \" by simp ``` haftmann@19281 ` 189` ```qed ``` haftmann@19281 ` 190` haftmann@19281 ` 191` ```lemma (in group) cancel: ``` haftmann@19281 ` 192` ``` "(x \<^loc>\ y = x \<^loc>\ z) = (y = z)" ``` haftmann@19281 ` 193` ```proof ``` haftmann@19281 ` 194` ``` fix x y z :: 'a ``` haftmann@19281 ` 195` ``` assume eq: "x \<^loc>\ y = x \<^loc>\ z" ``` haftmann@19281 ` 196` ``` hence "\<^loc>\
x \<^loc>\ (x \<^loc>\ y) = \<^loc>\
x \<^loc>\ (x \<^loc>\ z)" by simp ``` haftmann@19281 ` 197` ``` with assoc have "\<^loc>\
x \<^loc>\ x \<^loc>\ y = \<^loc>\
x \<^loc>\ x \<^loc>\ z" by simp ``` haftmann@19281 ` 198` ``` with neutl invl show "y = z" by simp ``` haftmann@19281 ` 199` ```next ``` haftmann@19281 ` 200` ``` fix x y z :: 'a ``` haftmann@19281 ` 201` ``` assume eq: "y = z" ``` haftmann@19281 ` 202` ``` thus "x \<^loc>\ y = x \<^loc>\ z" by simp ``` haftmann@19281 ` 203` ```qed ``` haftmann@19281 ` 204` haftmann@19281 ` 205` ```lemma (in group) neutr: ``` haftmann@19281 ` 206` ``` "x \<^loc>\ \<^loc>\ = x" ``` haftmann@19281 ` 207` ```proof - ``` haftmann@19281 ` 208` ``` from invl have "\<^loc>\
x \<^loc>\ x = \<^loc>\" by simp ``` haftmann@19281 ` 209` ``` with assoc [symmetric] neutl invl have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\) = \<^loc>\
x \<^loc>\ x" by simp ``` haftmann@19281 ` 210` ``` with cancel show ?thesis by simp ``` haftmann@19281 ` 211` ```qed ``` haftmann@19281 ` 212` haftmann@19281 ` 213` ```lemma (in group) invr: ``` haftmann@19281 ` 214` ``` "x \<^loc>\ \<^loc>\
x = \<^loc>\" ``` haftmann@19281 ` 215` ```proof - ``` haftmann@19281 ` 216` ``` from neutl invl have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x" by simp ``` haftmann@19281 ` 217` ``` with neutr have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 218` ``` with assoc have "\<^loc>\
x \<^loc>\ (x \<^loc>\ \<^loc>\
x) = \<^loc>\
x \<^loc>\ \<^loc>\ " by simp ``` haftmann@19281 ` 219` ``` with cancel show ?thesis .. ``` haftmann@19281 ` 220` ```qed ``` haftmann@19281 ` 221` haftmann@20383 ` 222` ```instance group < monoid ``` haftmann@19928 ` 223` ```proof - ``` haftmann@20383 ` 224` ``` fix x ``` haftmann@19281 ` 225` ``` from neutr show "x \<^loc>\ \<^loc>\ = x" . ``` haftmann@19281 ` 226` ```qed ``` haftmann@19281 ` 227` haftmann@19281 ` 228` ```lemma (in group) all_inv [intro]: ``` haftmann@20178 ` 229` ``` "(x\'a) \ monoid.units (op \<^loc>\) \<^loc>\" ``` haftmann@19281 ` 230` ``` unfolding units_def ``` haftmann@19281 ` 231` ```proof - ``` haftmann@19281 ` 232` ``` fix x :: "'a" ``` haftmann@19281 ` 233` ``` from invl invr have "\<^loc>\
x \<^loc>\ x = \<^loc>\" and "x \<^loc>\ \<^loc>\
x = \<^loc>\" . ``` haftmann@19281 ` 234` ``` then obtain y where "y \<^loc>\ x = \<^loc>\" and "x \<^loc>\ y = \<^loc>\" .. ``` haftmann@19281 ` 235` ``` hence "\y\'a. y \<^loc>\ x = \<^loc>\ \ x \<^loc>\ y = \<^loc>\" by blast ``` haftmann@19281 ` 236` ``` thus "x \ {y\'a. \x\'a. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" by simp ``` haftmann@19281 ` 237` ```qed ``` haftmann@19281 ` 238` haftmann@19281 ` 239` ```lemma (in group) cancer: ``` haftmann@19281 ` 240` ``` "(y \<^loc>\ x = z \<^loc>\ x) = (y = z)" ``` haftmann@19281 ` 241` ```proof ``` haftmann@19281 ` 242` ``` assume eq: "y \<^loc>\ x = z \<^loc>\ x" ``` haftmann@19281 ` 243` ``` with assoc [symmetric] have "y \<^loc>\ (x \<^loc>\ \<^loc>\
x) = z \<^loc>\ (x \<^loc>\ \<^loc>\
x)" by (simp del: invr) ``` haftmann@19281 ` 244` ``` with invr neutr show "y = z" by simp ``` haftmann@19281 ` 245` ```next ``` haftmann@19281 ` 246` ``` assume eq: "y = z" ``` haftmann@19281 ` 247` ``` thus "y \<^loc>\ x = z \<^loc>\ x" by simp ``` haftmann@19281 ` 248` ```qed ``` haftmann@19281 ` 249` haftmann@19281 ` 250` ```lemma (in group) inv_one: ``` haftmann@19281 ` 251` ``` "\<^loc>\
\<^loc>\ = \<^loc>\" ``` haftmann@19281 ` 252` ```proof - ``` haftmann@19281 ` 253` ``` from neutl have "\<^loc>\
\<^loc>\ = \<^loc>\ \<^loc>\ (\<^loc>\
\<^loc>\)" .. ``` haftmann@19281 ` 254` ``` moreover from invr have "... = \<^loc>\" by simp ``` haftmann@19281 ` 255` ``` finally show ?thesis . ``` haftmann@19281 ` 256` ```qed ``` haftmann@19281 ` 257` haftmann@19281 ` 258` ```lemma (in group) inv_inv: ``` haftmann@19281 ` 259` ``` "\<^loc>\
(\<^loc>\
x) = x" ``` haftmann@19281 ` 260` ```proof - ``` haftmann@19281 ` 261` ``` from invl invr neutr ``` haftmann@19281 ` 262` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ \<^loc>\
x \<^loc>\ x = x \<^loc>\ \<^loc>\
x \<^loc>\ x" by simp ``` haftmann@19281 ` 263` ``` with assoc [symmetric] ``` haftmann@19281 ` 264` ``` have "\<^loc>\
(\<^loc>\
x) \<^loc>\ (\<^loc>\
x \<^loc>\ x) = x \<^loc>\ (\<^loc>\
x \<^loc>\ x)" by simp ``` haftmann@19281 ` 265` ``` with invl neutr show ?thesis by simp ``` haftmann@19281 ` 266` ```qed ``` haftmann@19281 ` 267` haftmann@19281 ` 268` ```lemma (in group) inv_mult_group: ``` haftmann@19281 ` 269` ``` "\<^loc>\
(x \<^loc>\ y) = \<^loc>\
y \<^loc>\ \<^loc>\
x" ``` haftmann@19281 ` 270` ```proof - ``` haftmann@19281 ` 271` ``` from invl have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ (x \<^loc>\ y) = \<^loc>\" by simp ``` haftmann@19281 ` 272` ``` with assoc have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ x \<^loc>\ y = \<^loc>\" by simp ``` haftmann@19281 ` 273` ``` 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 ` 274` ``` 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 ` 275` ``` with invr neutr show ?thesis by simp ``` haftmann@19281 ` 276` ```qed ``` haftmann@19281 ` 277` haftmann@19281 ` 278` ```lemma (in group) inv_comm: ``` haftmann@19281 ` 279` ``` "x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ x" ``` haftmann@19281 ` 280` ```using invr invl by simp ``` haftmann@19281 ` 281` haftmann@19281 ` 282` ```definition (in group) ``` wenzelm@21404 ` 283` ``` pow :: "int \ 'a \ 'a" where ``` wenzelm@21404 ` 284` ``` "pow k x = (if k < 0 then \<^loc>\
(monoid.npow (op \<^loc>\) \<^loc>\ (nat (-k)) x) ``` haftmann@19281 ` 285` ``` else (monoid.npow (op \<^loc>\) \<^loc>\ (nat k) x))" ``` haftmann@19281 ` 286` haftmann@19281 ` 287` ```abbreviation (in group) ``` wenzelm@21707 ` 288` ``` pow_syn :: "'a \ int \ 'a" (infix "\<^loc>\" 75) where ``` haftmann@19928 ` 289` ``` "x \<^loc>\ k \ pow k x" ``` haftmann@19281 ` 290` haftmann@19281 ` 291` ```lemma (in group) int_pow_zero: ``` haftmann@20178 ` 292` ``` "x \<^loc>\ (0\int) = \<^loc>\" ``` haftmann@19281 ` 293` ```using npow_def pow_def by simp ``` haftmann@19281 ` 294` haftmann@19281 ` 295` ```lemma (in group) int_pow_one: ``` haftmann@20178 ` 296` ``` "\<^loc>\ \<^loc>\ (k\int) = \<^loc>\" ``` haftmann@19281 ` 297` ```using pow_def nat_pow_one inv_one by simp ``` haftmann@19281 ` 298` haftmann@20597 ` 299` ```instance semigroup_prod_def: * :: (semigroup, semigroup) semigroup ``` haftmann@20178 ` 300` ``` mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in ``` haftmann@19958 ` 301` ``` (x1 \ y1, x2 \ y2)" ``` haftmann@20427 ` 302` ```by default (simp_all add: split_paired_all semigroup_prod_def assoc) ``` haftmann@20427 ` 303` haftmann@20597 ` 304` ```instance monoidl_prod_def: * :: (monoidl, monoidl) monoidl ``` haftmann@20427 ` 305` ``` one_prod_def: "\ \ (\, \)" ``` haftmann@20427 ` 306` ```by default (simp_all add: split_paired_all monoidl_prod_def neutl) ``` haftmann@20427 ` 307` haftmann@20597 ` 308` ```instance monoid_prod_def: * :: (monoid, monoid) monoid ``` haftmann@20427 ` 309` ```by default (simp_all add: split_paired_all monoid_prod_def neutr) ``` haftmann@20427 ` 310` haftmann@20597 ` 311` ```instance monoid_comm_prod_def: * :: (monoid_comm, monoid_comm) monoid_comm ``` haftmann@20427 ` 312` ```by default (simp_all add: split_paired_all monoidl_prod_def comm) ``` haftmann@20427 ` 313` haftmann@20597 ` 314` ```instance group_prod_def: * :: (group, group) group ``` haftmann@20427 ` 315` ``` inv_prod_def: "\
x \ let (x1, x2) = x in (\
x1, \
x2)" ``` haftmann@20427 ` 316` ```by default (simp_all add: split_paired_all group_prod_def invl) ``` haftmann@19281 ` 317` haftmann@20597 ` 318` ```instance group_comm_prod_def: * :: (group_comm, group_comm) group_comm ``` haftmann@20427 ` 319` ```by default (simp_all add: split_paired_all group_prod_def comm) ``` haftmann@19281 ` 320` haftmann@19281 ` 321` ```definition ``` haftmann@20383 ` 322` ``` "X a b c = (a \ \ \ b, a \ \ \ b, [a, b] \ \ \ [a, b, c])" ``` wenzelm@21404 ` 323` ```definition ``` haftmann@20383 ` 324` ``` "Y a b c = (a, \
a) \ \ \ \
(b, \
c)" ``` haftmann@20383 ` 325` wenzelm@21404 ` 326` ```definition "x1 = X (1::nat) 2 3" ``` wenzelm@21404 ` 327` ```definition "x2 = X (1::int) 2 3" ``` wenzelm@21404 ` 328` ```definition "y2 = Y (1::int) 2 3" ``` haftmann@19281 ` 329` haftmann@20453 ` 330` ```code_gen "op \" \ inv ``` haftmann@21545 ` 331` ```code_gen X Y (SML #) (Haskell -) ``` haftmann@21545 ` 332` ```code_gen x1 x2 y2 (SML #) (Haskell -) ``` haftmann@19281 ` 333` haftmann@19281 ` 334` ```end ```