; $Id: ring.scm,v 1.4 2008/01/25 13:30:14 logik Exp $

; MINLOG: ring.scm

; ring.scm
; General introduction of rings
; for use in reflection_ring.scm

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

(add-alg "ring" 
         '("a" "ring")
         '("C" "ring=>ring"))

(add-program-constant "Rnull" (py "ring") 1)
(add-program-constant "Runum" (py "ring") 1)
(add-program-constant "RingAdd"  (py "ring=>ring=>ring") 1)
(add-program-constant "RingTimes" (py "ring=>ring=>ring") 1)

(let ((termcreator
       (lambda (string)
         (lambda (x y)
           (mk-term-in-app-form
            (make-term-in-const-form (pconst-name-to-pconst string))
            x y)))))
  (add-token "+"   'add-op (termcreator "RingAdd"))
  (add-token "*"   'mul-op (termcreator "RingTimes")))

(let ((disp-term
       (lambda (const-name symbol token-type)
         (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)
                          (string=? const-name
                                    (const-to-name
                                     (term-in-const-form-to-const op)))
                          (= 2 (length args)))
                     (list token-type symbol
                           (term-to-token-tree (car args))
                           (term-to-token-tree (cadr args)))
                     #f))
               #f)))))
  (add-display (py "ring") (disp-term "RingAdd"  "+"   'add-op))
  (add-display (py "ring") (disp-term "RingTimes" "*"   'mul-op)))


(av "ri" (py "ring"))

(aga "RingAddAssoc"    (pf "all ri1,ri2,ri3.ri1+(ri2+ri3) = (ri1+ri2)+ri3"))
(aga "RingAddNeutral"  (pf "all ri.Rnull+ri = ri"))
(aga "RingAddInverse"  (pf "all ri1.ex ri2.ri2+ri1 = Rnull"))
(aga "RingAddComm"     (pf "all ri1,ri2.ri1+ri2 = ri2+ri1"))

(aga "RingTimesAssoc"   (pf "all ri1,ri2,ri3.ri1*(ri2*ri3) = (ri1*ri2)*ri3"))
(aga "RingTimesNeutral" (pf "all ri. Runum*ri = ri"))
(aga "RingTimesComm"    (pf "all ri1,ri2.ri1*ri2 = ri2*ri1"))

(aga "Distr1"      (pf "all ri1,ri2,ri3.ri1*(ri2+ri3) = (ri1*ri2)+(ri1*ri3)"))
(aga "Distr2"      (pf "all ri1,ri2,ri3.(ri1+ri2)*ri3 = (ri1*ri3)+(ri2*ri3)"))


(display-global-assumptions)




; there exist a unique neutral element

(define (neutral-element var)
 (string-append "(all ri0.ri0+" var " = ri0)"))

(sg (neutral-element "ri") " ->  ri=Rnull")
(assume "ri" "§")
(simp-with "<-" "RingAddNeutral" (pt"ri"))
(simp-with "§" (pt"Rnull"))
(use "Truth-Axiom")
; Proof finished
(save "ringUniqueNull")
(display-theorems "ringUniqueNull")




; there exist a unique 1

(sg "all ri. all ri1 ri1*ri = ri1 -> ri=Runum")
(assume "ri" "*")
(simp-with "<-" "RingTimesNeutral" (pt "ri"))
(simp-with "*" (pt "Runum"))
(use "Truth-Axiom")
; Proof finished.

(sg "all ri. all ri1 ri*ri1 = ri1 -> ri=Runum")
(assume "ri" "*")
(simp-with "<-" "RingTimesNeutral" (pt "ri"))
(simp-with "RingTimesComm" (pt "Runum") (pt "ri"))
(use-with "*" (pt "Runum"))
; Proof finished.


; ; RingAddNeutral from left
; (sg "all r.r+null=r")
; (strip)
; (simp "RingAddComm")
; (simp "RingAddNeutral")
; (use "Truth-Axiom")
; ; Proof finished.
; (save "RingAddNeutralLeft")

; ; RingTimesNeutral from left
; (sg "all r.r*unum=r")
; (strip)
; (simp "RingTimesComm")
; (simp "RingTimesNeutral")
; (use "Truth-Axiom")
; ; Proof finished.
; (save "RingTimesNeutralLeft")