Project

Namespaces

Public Vars

latte-integers.rec

The recursion theorems for ℤ.

int-recur

(int-recur [x T] [f-succ (==> T T)] [f-pred (==> T T)])
(q/unique (int-recur-prop x f-succ f-pred))

Axiom: The recursion principle for integers.

cf. int-recur-prop

According to [TT&FP,p. 318], this is derivable, but we introduce it as an axiom since the derivation seems rather complex.

int-recur-bijection

(int-recur-bijection [x T] [f (==> T T)] [b (fun/bijective f)])
(q/unique (int-recur-bijection-prop x f b))

Theorem: The recursion principle for integers, for bijections. This is a consequence of int-rec, cf. int-recur-bijection-prop.

int-recur-bijection-ex

(int-recur-bijection-ex [x T] [f (==> T T)] [b (fun/bijective f)])
(q/ex (int-recur-bijection-prop x f b))

Lemma:

int-recur-bijection-lemma

(int-recur-bijection-lemma [f (==> T T)] [b (fun/bijective f)] [g (==> int T)])
(<=>
 (forall
  [y int]
  (and
   (==> (positive (succ y)) (equal (g (succ y)) (f (g y))))
   (==>
    (negative (pred y))
    (equal (g (pred y)) ((fun/inverse f b) (g y))))))
 (forall [y int] (equal (g (succ y)) (f (g y)))))

Lemma:

int-recur-bijection-prop

(int-recur-bijection-prop [x T] [f (==> T T)] [b (fun/bijective f)])
(lambda
 [g (==> int T)]
 (and
  (equal (g zero) x)
  (forall [y int] (equal (g (succ y)) (f (g y))))))

Definition: Property of the recursion principle for integers, for bijections. This is a much simpler principle if the function under study is bijective on ℤ (e.g. addition).

int-recur-bijection-single

(int-recur-bijection-single [x T] [f (==> T T)] [b (fun/bijective f)])
(q/single (int-recur-bijection-prop x f b))

Lemma:

int-recur-prop

(int-recur-prop [x T] [f-succ (==> T T)] [f-pred (==> T T)])
(lambda
 [g (==> int T)]
 (and
  (equal (g zero) x)
  (forall
   [y int]
   (and
    (==> (positive (succ y)) (equal (g (succ y)) (f-succ (g y))))
    (==> (negative (pred y)) (equal (g (pred y)) (f-pred (g y))))))))

Definition: The property of the recursion principle for integers.