src/HOL/ex/Classpackage.thy
 author haftmann Fri Sep 01 08:36:51 2006 +0200 (2006-09-01) changeset 20453 855f07fabd76 parent 20427 0b102b4182de child 20597 65fe827aa595 permissions -rw-r--r--
final syntax for some Isar code generator keywords
 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@19281 29 instance (type) list :: 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@19281 55 instance (type) list :: 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@20178 70 instance monoid_list_def: (type) list :: 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@20427 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@20427 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@20427 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@20427 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@20427 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@19281 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