src/HOL/ex/Classpackage.thy
changeset 20383 58f65fc90cf4
parent 20187 af47971ea304
child 20427 0b102b4182de
     1.1 --- a/src/HOL/ex/Classpackage.thy	Mon Aug 14 13:46:16 2006 +0200
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Mon Aug 14 13:46:17 2006 +0200
     1.3 @@ -211,18 +211,12 @@
     1.4    with cancel show ?thesis ..
     1.5  qed
     1.6  
     1.7 -interpretation group < monoid
     1.8 +instance group < monoid
     1.9  proof -
    1.10 -  fix x :: "'a"
    1.11 +  fix x
    1.12    from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
    1.13  qed
    1.14  
    1.15 -instance group < monoid
    1.16 -proof
    1.17 -  fix x :: "'a\<Colon>group"
    1.18 -  from group.neutr show "x \<otimes> \<one> = x" .
    1.19 -qed
    1.20 -
    1.21  lemma (in group) all_inv [intro]:
    1.22    "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
    1.23    unfolding units_def
    1.24 @@ -305,12 +299,17 @@
    1.25  by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
    1.26  
    1.27  definition
    1.28 -  "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])"
    1.29 -  "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
    1.30 +  "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
    1.31 +  "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
    1.32 +
    1.33 +definition
    1.34 +  "x1 = X (1::nat) 2 3"
    1.35 +  "x2 = X (1::int) 2 3"
    1.36 +  "y2 = Y (1::int) 2 3"
    1.37  
    1.38  code_generate "op \<otimes>" \<one> inv
    1.39 -code_generate (ml, haskell) x
    1.40 -code_generate (ml, haskell) y
    1.41 +code_generate (ml, haskell) X Y
    1.42 +code_generate (ml, haskell) x1 x2 y2
    1.43  
    1.44  code_serialize ml (-)
    1.45