// Christian Semrau

Type RAT

Functions:
  mk_rat: INT x INT -/-> RAT	Konstruktor
  zaehler: RAT --> INT		Selektor
  nenner: RAT --> INT		Selektor
  is_zero: RAT --> BOOL		Praedikat
  equal: RAT x RAT --> BOOL	Praedikat
  add: RAT x RAT --> RAT
  sub: RAT x RAT --> RAT
  mult: RAT x RAT --> RAT
  div: RAT x RAT -/-> RAT
  kuerze: RAT --> RAT
// zusaetzliches Praedikat
  = : RAT x RAT --> BOOL	Praedikat (komponentenweise Uebereinstimmung)

Axioms: forall p,q,r: RAT, z,n,z2,n2: INT
  zaehler(mk_rat(z, n)) = z
  nenner(mk_rat(z, n)) = n

  is_zero(p) <-> (zaehler(p) = 0)
  equal(p, q) <-> (kuerze(p) = kuerze(q))
  (p = q) <-> (zaehler(p) = zaehler(q) AND nenner(p) = nenner(q))

  (n > 0) -> kuerze(mk_rat(z, n)) = mk_rat(z/ggt(z, n), n/ggt(z, n))
  (n < 0) ->
 kuerze(mk_rat(z, n)) = mk_rat(-z/ggt(z, n), -n/ggt(z, n))
// ich gehe davon aus, dass ggt stets eine nichtnegative zahl liefert,
// und dass ggt(0, n) = abs(n)
// kuerze() macht damit den nenner stets positiv

// die Berechnungsvorschriften:
  add (mk_rat(z, n), mk_rat(z2, n2)) = kuerze(mk_rat(z*n2 + z2*n, n*n2))
  sub (mk_rat(z, n), mk_rat(z2, n2)) = kuerze(mk_rat(z*n2 - z2*n, n*n2))
  mult(mk_rat(z, n), mk_rat(z2, n2)) = kuerze(mk_rat(z*z2, n*n2))
  div (mk_rat(z, n), mk_rat(z2, n2)) = kuerze(mk_rat(z*n2, n*z2))

Preconditions: forall z,n: INT, p,q: RAT
  pre(mk_rat(z, n)): n != 0
  pre(div(p, q)): not(is_zero(q))