src/HOL/ex/Classpackage.thy
 changeset 20383 58f65fc90cf4 parent 20187 af47971ea304 child 20427 0b102b4182de
equal inserted replaced
20382:39964c8dcd54 20383:58f65fc90cf4
`   209   with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp`
`   209   with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp`
`   210   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp`
`   210   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp`
`   211   with cancel show ?thesis ..`
`   211   with cancel show ?thesis ..`
`   212 qed`
`   212 qed`
`   213 `
`   213 `
`   214 interpretation group < monoid`
`   214 instance group < monoid`
`   215 proof -`
`   215 proof -`
`   216   fix x :: "'a"`
`   216   fix x`
`   217   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .`
`   217   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .`
`   224 qed`
`   218 qed`
`   225 `
`   219 `
`   226 lemma (in group) all_inv [intro]:`
`   220 lemma (in group) all_inv [intro]:`
`   227   "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"`
`   221   "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"`
`   228   unfolding units_def`
`   222   unfolding units_def`
`   303 `
`   297 `
`   304 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm`
`   298 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm`
`   305 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)`
`   299 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)`
`   306 `
`   300 `
`   307 definition`
`   301 definition`
`   308   "x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"`
`   302   "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"`
`   309   "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"`
`   303   "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"`
`       `
`   304 `
`       `
`   305 definition`
`       `
`   306   "x1 = X (1::nat) 2 3"`
`       `
`   307   "x2 = X (1::int) 2 3"`
`       `
`   308   "y2 = Y (1::int) 2 3"`
`   310 `
`   309 `
`   311 code_generate "op \<otimes>" \<one> inv`
`   310 code_generate "op \<otimes>" \<one> inv`
`   312 code_generate (ml, haskell) x`
`   311 code_generate (ml, haskell) X Y`
`   313 code_generate (ml, haskell) y`
`   312 code_generate (ml, haskell) x1 x2 y2`
`   314 `
`   313 `
`   315 code_serialize ml (-)`
`   314 code_serialize ml (-)`
`   316 `
`   315 `
`   317 end`
`   316 end`