doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs

+module Classes where {
+
+import Nat;
+import Integer;
+
+class Semigroup a where {
+  mult :: a -> a -> a;
+};
+
+class (Semigroup a) => Monoidl a where {
+  neutral :: a;
+};
+
+class (Monoidl a) => Group a where {
+  inverse :: a -> a;
+};
+
+inverse_int :: Integer -> Integer;
+inverse_int i = negate i;
+
+neutral_int :: Integer;
+neutral_int = 0;
+
+mult_int :: Integer -> Integer -> Integer;
+mult_int i j = i + j;
+
+instance Semigroup Integer where {
+  mult = mult_int;
+};
+
+instance Monoidl Integer where {
+  neutral = neutral_int;
+};
+
+instance Group Integer where {
+  inverse = inverse_int;
+};
+
+pow_nat :: (Monoidl a) => Nat -> a -> a;
+pow_nat (Suc n) x = mult x (pow_nat n x);
+pow_nat Zero_nat x = neutral;
+
+pow_int :: (Group a) => Integer -> a -> a;
+pow_int k x =
+  (if 0 <= k then pow_nat (nat k) x
+    else inverse (pow_nat (nat (negate k)) x));
+
+example :: Integer;
+example = pow_int 10 (-2);
+
+}