(load-file "parse.ath")

(define subset-trans "ALL s1 s2 s3 | (s1 subset s2) & (s2 subset s3) ==> s1 subset s3")
(define union-lemma "ALL s1 s2 s | (s1 subset s) & (s2 subset s) ==> (s1 union s2) subset s")
(define comp-lemma "ALL s1 s2 R | s1 subset s2 ==> s1.R subset s2.R")
(define scalar-lemma "ALL x y R | y in {x}.R <==> [x y] in R")
(define singleton-subset-lemma "ALL x S | {x} subset S <==> x in S")
(define star-pow-lemma "ALL x n R S | x in ({n}.R*).S ==> (EXISTS m k | [n m] in R^k & [m x] in S)")


(!prove subset-trans [subset-def])
(!prove union-lemma [subset-def union-def])
(!prove comp-lemma [sbdot-def subset-def])
(!prove scalar-lemma [sbdot-def singleton-def id-axiom])
(!prove singleton-subset-lemma [subset-def singleton-def id-axiom])
(!prove star-pow-lemma [sbdot-def scalar-lemma rtc-def])


(define power-sum-lemma "ALL k1 k2 x y z R | [x y] in R^k1 & [y z] in R^k2 ==> [x z] in R^k1+k2")

(define (goal k) 
   (forall ?k2 ?x ?y ?z ?R
     "[x y] in R^k & [y z] in R^k2 ==> [x z] in R^k+k2"))

;; Here's the proof of power-sum-lemma -- a simple induction on k1:

(by-induction-on ?k1 (goal ?k1)
  (zero (!prove (goal zero) [plus-def-1 pow-def-1 id-axiom]))
  ((succ k) (dlet ((ind-hyp (goal k)))
              (!prove (goal (succ k)) [plus-def-2 pow-def-2 ind-hyp id-axiom]))))

(define comp-monotonicity "ALL x y R | y in {x}.R* ==> {y}.R* subset {x}.R*")

(pick-any x y R
  (assume-let ((hyp "y in {x}.R*"))
     (dlet ((L (!prove "ALL t | t in {y}.R* ==> t in {x}.R*" 
		    [hyp power-sum-lemma rtc-def scalar-lemma])))
       (!prove "{y}.R* subset {x}.R*" [L subset-def]))))

(!claim comp-monotonicity)			           

(define rtc-zero-lemma "ALL n R | [n n] in R^0")
(define reflex-clos-lemma  "ALL n R | [n n] in R*")
(define first-power-lemma-1 "ALL x y R | [x y] in R ==> [x y] in R^1")
(define first-power-lemma "ALL x y R | [x y] in R ==> [x y] in R*")
(define subset-rtc-lemma "ALL n R | {n} subset {n}.R*")
(define zero-power-lemma "ALL S R | S.R^0 = S")
(define fun-lemma "ALL n x R | [n x] in R & is-fun(R) ==> {x} = {n}.R")

(fun-lemma BY 
  (pick-any n x R
    (assume-let ((hyp "[n x] in R & is-fun(R)"))
      (!prove-set-equality (singl x) (sbdot (singl n) R)
	 [hyp scalar-lemma is-fun-def id-axiom singleton-def]))))

(!prove rtc-zero-lemma [pow-def-1 id-axiom])
(!prove reflex-clos-lemma [pow-def-1 rtc-def id-axiom])
(!prove first-power-lemma-1 [rtc-zero-lemma id-axiom pow-def-2])
(!prove first-power-lemma [rtc-def first-power-lemma-1])
(!prove subset-rtc-lemma [reflex-clos-lemma scalar-lemma id-axiom singleton-def singleton-subset-lemma])

(zero-power-lemma BY 
   (pick-any S R
     (!prove-set-equality (sbdot S (pow R zero)) S [rtc-zero-lemma pow-def-1 scalar-lemma sbdot-def])))


(define id1 "ALL R1 R2 | inv(R1 union R2) = inv(R1) union inv(R2)")

(id1 BY
  (pick-any R1 R2
    (!prove-set-equality (inv (union R1 R2)) (union (inv R1) (inv R2)) [inv-def union-def])))

(define com-1-2-2-assoc "ALL R1 R2 R3 | (R1 . R2) . R3 = R1 . (R2 o R3)")

(com-1-2-2-assoc BY
  (pick-any R1 R2 R3
    (!prove-set-equality (sbdot (sbdot R1 R2) R3) (sbdot R1 (bbdot R2 R3)) [sbdot-def bbdot-ax])))

(define com-2-2-2-assoc "ALL R1 R2 R3 | (R1 o R2) o R3 = R1 o (R2 o R3)")

(com-2-2-2-assoc BY
  (pick-any R1 R2 R3
    (!prove-set-equality (bbdot (bbdot R1 R2) R3) (bbdot R1 (bbdot R2 R3)) [bbdot-ax])))

(define pow-comp-2-2-lemma "ALL k R | R^k+1 = R o R^k")

(pow-comp-2-2-lemma BY
  (pick-any k R
    (!prove-set-equality (pow R (succ k)) (bbdot R (pow R k)) [pow-def-2 bbdot-ax])))

(define dcom "ALL k R | R o R^k = R^k o R")

(dcom BY 
  (dlet ((goal (function (k) (forall ?R (= (bbdot ?R (pow ?R k)) (bbdot (pow ?R k) ?R))))))
    (by-induction-on ?k (goal ?k)
      (zero (pick-any R 
	      (!prove-set-equality (bbdot R (pow R zero)) (bbdot (pow R zero) R) [pow-def-1 bbdot-ax id-axiom])))
      ((succ k) (pick-any R
	          (!prove-set-equality (bbdot R (pow R (succ k))) (bbdot (pow R (succ k)) R) 
                    [pow-def-2 (goal k) pow-comp-2-2-lemma com-2-2-2-assoc]))))))

(define inv-pow-lemma "ALL k R | inv(R^k) = inv(R)^k")

(inv-pow-lemma BY
  (dlet ((goal (function (k) (forall ?R (= (inv (pow ?R k)) (pow (inv ?R) k))))))
    (by-induction-on ?k (goal ?k)
      (zero (pick-any R 
	      (!prove-set-equality (inv (pow R zero)) (pow (inv R) zero) [inv-def pow-def-1])))
      ((succ k) (pick-any R
                  (!prove-set-equality (inv (pow R (succ k))) (pow (inv R) (succ k)) 
				       [(goal k) inv-def pow-def-2 pow-comp-2-2-lemma dcom bbdot-ax]))))))

(define inv-star-lemma "ALL R | inv(R*) = inv(R)*")

(pick-any R
  (!prove-set-equality (inv (rtc R)) (rtc (inv R)) [inv-def rtc-def pow-def-1 pow-def-2 inv-pow-lemma]))


(define double-inv-lemma "ALL R | R = inv(inv(R))")

(pick-any R
  (!prove-set-equality R (inv (inv R)) [inv-def]))

(define star-com "ALL R | R o R* = R* o R")

(pick-any R
  (!prove-set-equality (bbdot R (rtc R)) (bbdot (rtc R) R) [rtc-def dcom bbdot-ax id-axiom]))