case-arith.disco

import list

f1 : N -> N
f1 (x + 1) = x
f1 0       = 0

f2 : N -> N
f2 (3 + (x + 2)) = x
f2 y             = 0

f3 : Z -> Z
f3 (3 + (x + 2)) = x
f3 y             = 0

f4 : N*Z -> N*Z + N*Z
f4 (x+1,y+2) = left (x,y)
f4 (x,  y+2) = right (x,y)

h : N -> N
h(0)    = 1
h(2k+1) = h(k)
h(2k+2) = h(k+1) + h(k)

f5 : N -> N
f5 (2x)   = x
f5 (2x-1) = x

f6 : Q -> Bool
f6 (-2/3) = True
f6 _      = False

!!! forall x:Z. Zabs(x) >= 0
Zabs : Z -> Z
Zabs (-x) = x
Zabs x    = x

type Tree = Unit + F * Tree * Tree

expandTree : N -> F -> Tree
expandTree 0 _     = left(unit)
expandTree n (a/b) = right(a/b, expandTree (n .- 1) (a/(a+b)), expandTree (n .- 1) ((a+b)/b))

cwTree : N -> Tree
cwTree n = expandTree n 1

inorder : Tree -> List(F)
inorder (left(unit))   = []
inorder (right(x,l,r)) = append(inorder(l), x :: inorder(r))

numerator : Q -> Z
numerator (p/q) = p

denominator : Q -> N
denominator (p/q) = q