; MINLOG: natnum.scm

; (load "~/minlog/init.scm")

(display"
Begin of natnum.scm

First some boolean RW-rules and THMS:

")

(set! OLD-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #f)
(exload "ordinals/boolean.scm")
(set! COMMENT-FLAG OLD-COMMENT-FLAG)




(begin


(add-alg "nat" '("ZERO" "nat") '("SUCC" "nat=>nat"))

(define (make-numeric-term n)
  (if (= n 0)
      (pt "ZERO")
      (make-term-in-app-form
       (pt "SUCC")
       (make-numeric-term (- n 1)))))

(define (is-numeric-term? term)
  (or
   (and (term-in-const-form? term)
	(string=? "ZERO" (const-to-name (term-in-const-form-to-const term))))
   (and (term-in-app-form? term)
	(let ((op (term-in-app-form-to-op term)))
	  (and (term-in-const-form? op)
	       (string=? "SUCC" (const-to-name
				 (term-in-const-form-to-const op)))
	       (is-numeric-term? (term-in-app-form-to-arg term)))))))

(define (numeric-term-to-number term)
  (if (equal? term (pt "ZERO"))
      0
      (+ 1 (numeric-term-to-number (term-in-app-form-to-arg term)))))


; natP : Predecessor  nat -> nat
(add-program-constant "natP" (mk-arrow (py "nat")(py "nat")) 1)
(acr "natP (SUCC nat)"  "nat")


; natPLUS: Addition   nat @ nat  ->  nat
(add-program-constant
 "natPLUS"
 (mk-arrow (make-alg "nat") (make-alg "nat") (make-alg "nat")) 1 'const 2)

(add-token
 "+"
 'add-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "natPLUS")) x y)))

(acr "nat1 + 0"          "nat1")
(acr "nat1 + SUCC nat2"  "SUCC (nat1+nat2)")




; natTIMES:  Multiplication   nat @ nat  ->  nat
(add-program-constant
 "natTIMES" (mk-arrow (make-alg "nat") (make-alg "nat") (make-alg "nat"))
 1 'const 2)

(add-token
 "*"
 'mul-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "natTIMES")) x y)))

(acr "nat1 * 0"          "0")
(acr "nat1 * SUCC nat2"  "(nat1 * nat2)+nat1")



; natMINUS: Substraction   nat @ nat  -> nat
(add-program-constant
 "natMINUS"
 (mk-arrow (make-alg "nat") (make-alg "nat") (make-alg "nat")) 1 'const 2)

(add-token
 "-"
 'add-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "natMINUS")) x y)))

(acr "nat1-0"            "nat1")
(acr "nat1-(SUCC nat2)"  "natP(nat1-nat2)")



; natLESS:  Smaller relation   nat @ nat  -> boole
(add-program-constant
 "natLESS" (mk-arrow (make-alg "nat") (make-alg "nat") (make-alg "boole"))
 1 'const 2)

(add-token
 "<"
 'rel-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form (pconst-name-to-pconst "natLESS")) x y)))

(add-token
 "≤"
 'rel-op
 (lambda (x y)
   (negboole
    (mk-term-in-app-form
     (make-term-in-const-form
      (pconst-name-to-pconst "natLESS")) y x))))

(acr "nat1      < 0"          "False")
(acr "0         < SUCC nat2"  "True")
(acr "SUCC nat1 < SUCC nat2"  "nat1 < nat2")



; natMAX:    nat @ nat  ->  nat
(add-program-constant
 "natMAX" (mk-arrow (make-alg "nat") (make-alg "nat") (make-alg "nat"))
 1 'const 2)

(acr "natMAX nat1 nat2" "[if (nat1<nat2) (nat2) (nat1)]")




;  DISPLAYING

(add-display
 (py "nat")
 (lambda (x)
   (if (term-in-app-form? x)
       (let* ((op (term-in-app-form-to-final-op x))
	      (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (= 2 (length args)))
	     (let ((constname (const-to-name (term-in-const-form-to-const op))))
	       (cond ((string=? "natPLUS" constname)
		      (list 'add-op "+"
			    (term-to-token-tree (car args))
			    (term-to-token-tree (cadr args))))
		     ((string=? "natTIMES" constname)
		      (list 'add-op "*"
			    (term-to-token-tree (car args))
			    (term-to-token-tree (cadr args))))
		     ((string=? "natMINUS" constname)
		      (list 'add-op "-"
			    (term-to-token-tree (car args))
			    (term-to-token-tree (cadr args))))
		     (else #f)))
	     #f))
       #f)))



(add-display
 (py "boole")
 (lambda (x)
   (if (term-in-app-form? x)
       (let* ((op (term-in-app-form-to-final-op x))
	      (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (= 2 (length args)))
	     (let ((constname (const-to-name (term-in-const-form-to-const op))))
	       (if (string=? "natLESS" constname)
		   (let* ((lhs (term-to-token-tree (car args)))
			  (rhs (term-to-token-tree (cadr args))))
		     (list 'add-op "<" lhs rhs))
		   #f))
	     #f))
       #f)))


(add-display
 (py "boole")
 (lambda (x)
   (if (neg-boole? x)
       (let* ((op (term-in-app-form-to-final-op(neg-boole-to-kernel x)))
	      (args (term-in-app-form-to-args(neg-boole-to-kernel x))))
	 (if (and (term-in-const-form? op)
		  (= 2 (length args)))
	     (let ((constname (const-to-name (term-in-const-form-to-const op))))
	       (if (string=? "natLESS" constname)
		   (let* ((lhs (term-to-token-tree (cadr args)))
			  (rhs (term-to-token-tree (car args))))
		     (list 'rel-op "≤" lhs rhs))
		   #f))
	     #f))
       #f)))





(set! OLD-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #t)

(display-constructors "nat")

(display-program-constants "natP")
(display-program-constants "natPLUS")
(display-program-constants "natTIMES")
(display-program-constants "natMINUS")
(display-program-constants "natLESS")
(display "
NOTA BENE !   nat1 ≤ nat2  :≡   ¬(nat2<nat1)
")
(display-program-constants "natMAX")
(set! COMMENT-FLAG OLD-COMMENT-FLAG)
)



(begin

(sg "(nat1=nat2)=(nat2=nat1)")
(assume "nat1" "nat2")
(cases (pt"nat1=nat2"))
(assume "1=2")
(simp "1=2")
(auto)
(assume "1≠2")
(simp(pf"nat2=nat1->F"))
(auto)
(assume "2=1")
(use "1≠2")
(simp "2=1")
(auto)
; Proof finished.
(save "natEQsym")
(display-theorems "natEQsym")
)


(display "

Some RW-rules for < and ≤

")

(begin

(sg "(0<nat)=(¬(nat=0))")
(cases)
(auto)
; Proof finished.
(arw "0<nat" "¬(nat=0)")



(display "
< is irrflexsive
≤ is reflexsive

")


(sg "nat≤nat")
(ind)
(auto)
; Proof finished.
(nrw "nat ≤ nat")


(display "
< is antisymmetric

")
(sg "¬(nat1<nat2 ∧ nat2<nat1)")

(ind)
(search)
(assume "nat1" "IH1")
(cases)
(auto)
; Proof finished.
(nrw "¬(nat1<nat2 ∧ nat2<nat1)")


(sg "nat1<nat2→(nat2<nat1)=False")
(assume "nat1" "nat2")
(cd "nat1<nat2" "1k2")
(simp(pf "False=(nat1<nat2 ∧ nat2<nat1)"))
(simp "1k2")
(use "Truth-Axiom")
(simp "BooleFalseLeft")
(auto)
; Proof finished.
(nrw "nat1<nat2→(nat2<nat1)=False")


(sg "(nat2≤nat1∧nat1≤nat2)→nat1=nat2")
(ind)
   (cases)
   (auto)
(assume "nat1" "IH1")
(cases)
  (auto)
; Proof finished.
(nrw "(nat2≤nat1∧nat1≤nat2)→nat1=nat2")
(nrw "(nat2≤nat1∧nat1≤nat2)→nat2=nat1")


(sg "(nat1≤nat2∧nat2≤nat1)→nat1=nat2")
(assume "nat2" "nat1")
(simp-with  "ANDcomm" (pt"nat1≤nat2") (pt"nat2≤nat1"))
(use "Truth-Axiom")
; Proof finished.
(nrw "(nat1≤nat2∧nat2≤nat1)→nat1=nat2")
(nrw "(nat1≤nat2∧nat2≤nat1)→nat2=nat1")



(display "
COROLLARY   < is linear:

(nat1<nat2) ∨ (nat2<nat1) ∨ (nat1=nat2)    ")
(pnt "(nat1<nat2) ∨ (nat2<nat1) ∨ (nat1=nat2)")


)





(display "

Some properties of natMAX: nat@nat -> nat

")


(begin


(sg "([if (nat1<nat2) nat2 nat1]=0)=(nat1=0 ∧ nat2=0)")
(cases)
    (cases)
    (auto)
(assume "nat1")
(cases)
    (use "Truth-Axiom")
(assume "nat2")
(ng)
(cases (pt "nat1<nat2"))
(auto)
; Proof finished.
(save "natMAX0")
(display-theorems "natMAX0")



(sg "[if (0<nat) nat 0]=nat")
(cases)
(auto)
; Proof finished.
(save "natMAX0n")
(display-theorems "natMAX0n")


(sg "natMAX nat1 nat2 = natMAX nat2 nat1")
(assume "nat1" "nat2")
(ng)
(cd "nat1<nat2" "1k2")
    (simp (pf"(nat2<nat1)=F"))
    (use "Truth-Axiom")
    (booleimp "nat1<nat2")
    (auto)
(assume "1≮2")
(cd "nat2<nat1" "2k1")
    (use "Truth-Axiom")
(assume "2≮1")
(booleimp "(nat1<nat2) ∨ (nat2<nat1) ∨ (nat1=nat2)")
(simp "1≮2")
(simp "2≮1")
(auto)
; Proof finished.
(save "natMAXcomm")
(display-theorems "natMAXcomm")
 
)




(display "

natLE_LESSorEQUAL: (nat1≤nat2)=((nat1<nat2)∨(nat1=nat2))

")

(begin
(sg "(nat1≤nat2)=((nat1<nat2)∨(nat1=nat2))")
(ind)
(cases)
(auto)
(assume "nat2" "IH2")
(cases)
(auto)
; Proof finished.
(save "natLE_LESSorEQUAL")
(display-theorems "natLE_LESSorEQUAL")

)



(display "

< is transitive:

(nat1<nat2 ∧ nat2<nat3) → nat1<nat3

")

(begin

(sg "all nat2,nat1.(nat1<nat2)→(0<nat2)")
(cases)
(auto)
; Proof finished.
(nrw"(nat1<nat2)→(1<nat2)")


(sg "all nat3,nat1,nat2.((nat1<nat2) ∧ (nat2<nat3)) → (nat1<nat3)")
(ind)
(auto)
(assume "nat3" "IH3")
(cases)
(auto)
(assume "nat1")
(cases)
(auto)
; Proof finished.
(nrw"((nat1<nat2) ∧ ((nat2<nat3)) → (nat1<nat3))")



(sg "¬(nat1≤nat2∧nat2≤nat3∧nat3<nat1)")
(assume "nat2" "nat1" "nat3")

(cases (pt "nat3<nat2"))
    (search)
(assume "3≮2")
(cd "nat3<nat1" "3<1")
(simp "natLE_LESSorEQUAL")
(ng)
(simp(pf"(nat1<nat2)=F"))
(cd "nat1=nat2" "1=2")
    (use "3≮2")
    (simp "<-" "1=2")
    (use "3<1")
(search)
(cd "nat1<nat2" "1<2")
    (use "3≮2")
    (trans "nat1")
    (simp "3<1")
    (use "1<2")
(auto)
; Proof finished
(nrw "¬(nat1≤nat2∧nat2≤nat3∧nat3<nat1)")


(set! OLD-COMMENT-FLAG COMMENT-FLAG)
(set! COMMENT-FLAG #t)

(display "
≤ is transitive:

nat1≤nat2∧nat2≤nat3 → nat1≤nat3     :  ")
(pnt "(nat1≤nat2∧nat2≤nat3) → nat1≤nat3")

(set! COMMENT-FLAG OLD-COMMENT-FLAG)



(sg "nat<SUCC nat")
(ind)
(auto)
; Proof finished.
(trw "nat<SUCC nat")


(sg "nat≤SUCC nat")
(assume "nat")
(simp "natLE_LESSorEQUAL")
(ng)
(use "Truth-Axiom")
; Proof finished.
(nrw "nat≤SUCC nat")


(sg "nat1<nat2→nat1<SUCC nat2")
(assume "nat1" "nat2")
(ass "eq")
(booleimp "nat1<nat2 ∧ nat2<SUCC nat2")
(use (pf "all nat1,nat2,nat3.nat1<nat2∧nat2<nat3→nat1<nat3"))
(auto)
; Proof finished.
(nrw "nat1<nat2→nat1<SUCC nat2")


(sg "¬(SUCC nat1≤nat2∧nat2<nat1)")
(assume "nat2" "nat1")
(simp "natLE_LESSorEQUAL")
(cd "nat2<nat1" "2<1")
(ng)
(simp "natLE_LESSorEQUAL")
(simp(pf"nat2<SUCC nat1"))
(ng)
(cd "SUCC nat1=nat2" "1+1=2")
(ng)
(simp "<-" (pf"(nat2<nat1)=F"))
(use "2<1")
(simp "<-" "1+1=2")
(auto)
(trans "nat1")
(auto)
; Proof finished.
(nrw "¬(SUCC nat1≤nat2∧nat2<nat1)")


(sg "nat1≤[if (nat1<nat2) nat2 nat1]")
(assume "nat1" "nat2")
(cases(pt "nat1<nat2"))
(ng)
(use "BooleImp")
(auto)
; Proof finished.
(nrw "nat1≤[if (nat1<nat2) nat2 nat1]")


(sg "nat2≤[if (nat1<nat2) nat2 nat1]")
(assume "nat1" "nat2")
(cases(pt"nat1<nat2"))
    (search)
(assume "1≮2")
(ng)
(simp "1≮2")
(use "Truth-Axiom")
; Proof finished.
(nrw "nat2≤[if (nat1<nat2) nat2 nat1]")



(sg "¬(nat1≤nat2∧[if (nat3<nat2) nat2 nat3]<nat1)")
(assume "nat2" "nat1" "nat3")
(cd "nat1≤nat2" "1≤2")
(ng)
(booleimp "nat1≤nat2∧nat2≤[if (nat3<nat2) nat2 nat3]")
(use (pf "all nat1,nat2,nat3.nat1≤nat2∧nat2≤nat3→nat1≤nat3"))
(auto)
; Proof finished.
(nrw "¬(nat1≤nat2∧[if (nat3<nat2) nat2 nat3]<nat1)")



(sg "all nat1.(nat1<SUCC nat2)=(nat1≤nat2)")
(ind)
    (cases)
    (auto)
(assume "nat2" "IH2")
(cases)
(auto)
; Proof finished.
(arw "nat1<SUCC nat2" "nat1≤nat2")


(sg "¬(nat1≤nat2∧[if (nat2<nat3) nat3 nat2]<nat1)")
(assume "nat2" "nat1" "nat3")
(booleimp "nat1≤nat2∧nat2≤[if (nat2<nat3) nat3 nat2]→nat1≤[if (nat2<nat3) nat3 nat2]")
(use "Truth-Axiom")
(use (pf"all nat3.nat1≤nat2∧nat2≤nat3→nat1≤nat3"))
(search)
; Proof finished.
(nrw "¬(nat1≤nat2∧[if (nat2<nat3) nat3 nat2]<nat1)")


)





(display "
natPersistency:

n≺m → [ ( ∀i≺m F^i  →  ∀i≺n F^i ) & ( ∃i≺n F^i  →  ∃i≺m F^i ) ]

")

(begin

(sg "nat1<nat2 ->
      ((all nat. nat<nat2 -> (Pvar nat)^ nat) -> (all nat. nat<nat1 -> (Pvar nat)^ nat))
    & ((ex  nat. nat<nat1 &  (Pvar nat)^ nat) -> (ex  nat. nat<nat2 &  (Pvar nat)^ nat))")

(assume "nat1" "nat2" "1<2")
(split)
    (assume "hyp" "nat" "<")
    (use "hyp")
    (trans "nat1")
    (simp "1<2")
    (use "<")
(assume "hyp")
(by-assume-with "hyp" "nat" "(*)")
(ex-intro(pt"nat"))
(split)
    (trans "nat1")
    (simp "1<2")
    (use "(*)")
(use "(*)")
; Proof finished.
(save "natPersistency")
(display-theorems "natPersistency")

)



(display "
Some RW-rules concerning natPLUS +

")

(begin

(sg "0+nat=nat")
(ind)
(auto)
; Proof finished.
(arw "0+nat" "nat")



(sg "SUCC nat1+nat2 = SUCC(nat1+nat2)")
(ind)
    (ind)
    (auto)
(assume "nat1" "IH1")
(ind)
(auto)
; Proof finished.
(arw "SUCC nat1+nat2" "SUCC(nat1+nat2)")
)





(display"

natPLUS is

commutative:  nat1 + nat2      =  nat2 + nat1

associative:  nat1+(nat2+nat3) =  nat1+nat2+nat3

")

(begin

(sg "nat1+nat2=nat2+nat1")
(ind)
(auto)
; Proof finished.
(save "natPLUScomm")
(display-theorems "natPLUScomm")


(sg "nat1+(nat2+nat3)=nat1+nat2+nat3")
(ind)
(auto)
; Proof finished.
(arw "nat1+(nat2+nat3)" "nat1+nat2+nat3")

)



(display"

End of natnum.scm

")