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

updated

module Classes where {


data Nat = Suc Classes.Nat | Zero_nat;

data Bit = B1 | B0;

nat_aux :: Integer -> Classes.Nat -> Classes.Nat;
nat_aux i n =
  (if i <= 0 then n else Classes.nat_aux (i - 1) (Classes.Suc n));

nat :: Integer -> Classes.Nat;
nat i = Classes.nat_aux i Classes.Zero_nat;

class Semigroup a where {
  mult :: a -> a -> a;
};

class (Classes.Semigroup a) => Monoidl a where {
  neutral :: a;
};

class (Classes.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 Classes.Semigroup Integer where {
  mult = Classes.mult_int;
};

instance Classes.Monoidl Integer where {
  neutral = Classes.neutral_int;
};

instance Classes.Group Integer where {
  inverse = Classes.inverse_int;
};

pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b;
pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x);
pow_nat Classes.Zero_nat x = Classes.neutral;

pow_int :: (Classes.Group a) => Integer -> a -> a;
pow_int k x =
  (if 0 <= k then Classes.pow_nat (Classes.nat k) x
    else Classes.inverse (Classes.pow_nat (Classes.nat (negate k)) x));

example :: Integer;
example = Classes.pow_int 10 (-2);

}