src/HOL/ex/Classpackage.thy
changeset 20383 58f65fc90cf4
parent 20187 af47971ea304
child 20427 0b102b4182de
equal deleted 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" .
   218 qed
       
   219 
       
   220 instance group < monoid
       
   221 proof
       
   222   fix x :: "'a\<Colon>group"
       
   223   from group.neutr show "x \<otimes> \<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