;; natplus.scm einladen (Pfad falls nötig anpassen)
(set! COMMENT-FLAG #f)
(load "./natplus.scm")
(set! COMMENT-FLAG #t)
; In natplus.scm wird der einfache Typ Nat definiert, welcher den natürlichen Zahlen entspricht und durch die Kunstruktoren
;   0    : ℕ
;   Succ : ℕ → ℕ
; aufgebaut wird. Succ 0 stellt also bspw. die Eins und Succ (Succ 0) die 2 dar.
(pp (pt "Succ 0"))
(pp (pt "Succ (Succ 0)"))
(pp (pt "2")) ; Wir können Succ (Succ 0) direkt als 2 notieren
; Weiter werden zahlreiche Operationen auf Nat definiert. Uns interessieren hier nur NatPlus und =.
; NatPlus wird durch + notiert und entspricht natürlich der Addition. NatPlus hat die Rechenregeln
;   alln n + 0 eqd n                   : NatPlus0CompRule
;   alln,m n + Succ m eqd Succ (n + m) : NatPlus1CompRule
; Hier bedeuted eqd, dass die linke Seite per Definition der rechten Seite entspricht. NatPlus (also +) ist so definiert, sodass für alle n, die Aussage n+0 zu n reduziert.
(pp "NatPlus0CompRule") ; Ihr könnte die ^ zunächst ignorieren
(pp "NatPlus1CompRule")
(pp (pt "2+1"))
(pp (pt "NatPlus 2 1")) ; Wir können auch NatPlus schreiben
; Zuletzt haben wir noch =. = ist die entscheidbare Gleichheit auf den natürlichen Zahlen ℕ. Gegeben zwei Zahlen berechnet = also ob die Zahlen äquivalent sind und gibt den entsprechenden Wahrheitswert zurück. Es gilt also das 2=1 gleich F (Falsch) und 1=1 gleich T (Wahr) ist.

;; Für die Aufgaben nötige Befehle
;; (assume …)
; Siehe vorherige Aufgaben
;; (use …)
; Siehe vorherige Aufgaben
;; (ind)
; Wenn das Ziel die Form ∀ₙA(n) hat, dann beginnt (ind) einen Induktionsbeweis über n an. D.h. (ind) erstellt zwei neue Ziele, den Induktionsanfang A(0) und den Induktionsschritt ∀ₙ(A(n) → A(n+1)).
;; (simp …)
; Simp akzeptiert den Namen eines Theorems oder einer Variable, welche eine Gleichheit (D.h. die entsprechende Formel sollte von der Form "… eqd …" oder " … = …" sein) ausdrückt und wendet diese Gleichheit auf das Ziel an.

;; Als einfaches Beispiel für simp und die Verwendung von NatPlus0CompRule zeigen wir:
(set-goal "1+2=3")
(simp "NatPlus1CompRule")
; Wir können die Regel auch rückwärts anwenden:
(simp "<-" "NatPlus1CompRule")
; Zurück zum Beweis:
(simp "NatPlus1CompRule")
(simp "NatPlus1CompRule")
(simp "NatPlus0CompRule")
; Da der Term berechenbar wahr ist, können wir folgendes verwenden:
(use "Truth")

; Wie auch in ueb00.scm erwähnt, können wir Theoreme speichern und später mit simp oder use verwenden.
(save "OnePlusTwoEqualsThree")

; Da "1+2=3" berechenbar wahr ist, können wir auch direkt (use "Truth") verwenden:
(set-goal "1+2=3")
(use "Truth")

;; Zuletzt ist noch der Befehl (pp) zu empfehlen. Mit diesem können insbesondere die Aussagen von Theoremen bestimmt werden:
(pp "OnePlusTwoEqualsThree")

(set-goal "all n 0+n=n")
(ind)
; In dieser Aufgabe sind nur die folgenden Befehle nötig:
; (assume …)
; (simp …)
; (use "Truth")
;; IA
; …
;; IS
; …
(save "NatZeroPlus")

(set-goal "all n,m Succ m+n=Succ(m+n)")
; …
(save "NatSuccPlus")

(set-goal "all n,m,l n+(m+l)=n+m+l")
; …
(save "NatPlusAssoc")

(set-goal "all n,m n+m=m+n")
; …
(save "NatPlusComm")