; $Id: Lem3.scm,v 1.2 2008/01/25 13:30:20 logik Exp $
; ***********************************************************
; ; Adapt path if necessary:
; (define path "~/minlog/examples/tait/diplomarbeit_schlenker/")

; ; Defines the function "pload" to load files 
; ; from the path defined above
; (define pload (lambda (x) (load (string-append path x))))

; ; Used Modules:
; (pload "./initiate.scm")
; (pload "./defsLamCalc.scm")
; (pload "./defsSubst.scm")
; (pload "./omega.scm")
; (pload "./defsNT.scm")
; (pload "./defsAxiomsSpecial.scm")
; (pload "./defsAxioms.scm")
; (pload "./trivial.scm")
; (pload "./auxSC.scm")
; (pload "./auxGlobal_SHORT.scm")
; (pload "./Lem2.scm")
; (pload "./auxLem3_SHORT.scm")

; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ==================
;  Section: Lemma 3
; ==================
; contains Lemma 3 of the Normalization Proof

; Lemma: "LemmaThree"
; -------------------
; Lemma 3 of the Normalization Proof
; Sketch: SCs (ss) -> SC (r[ss])

(set-goal
 (pf "all r,rhos allnc sigs,rho,ss.
      TypJ rhos r rho -> (ex as^.SCrs sigs rhos as^ ss) ->
      ex a^ SCr sigs rho a^(Sub r (Wrap 0 ss))"))

(ind)

; Case variables
(assume "k" "rhos" "sigs" "rho" "ss" "[TypJ]" "[SCs]")
(by-assume-with "[SCs]" "as^" "[SCrs Body]")
(ex-intro (pt "k thof as^"))
(use "SCrCompat2Rev" (pt "k thof rhos"))
(use "TypJVarRef")
(use "[TypJ]")
(simp "SubVar")
(use "LemmaThreeVar")
(use "[SCrs Body]")
(ng)
(use-with "[TypJ]" 'left)

(simp "<-" "SCrsLh" (pt "sigs") (pt "rhos") (pt "as^"))
(ng)
(use-with "[TypJ]" 'left)
(use "[SCrs Body]")

; Case App
(assume "r" "s" "[IHr]" "[IHs]")
(assume "rhos" "sigs" "sig" "ss" "[TypJ]" "[SCs]")
(ng #t)

(assert (pf "ex a^ SCr sigs(Typ rhos r)a^(Sub r (Wrap 0 ss))"))
(use "[IHr]" (pt "rhos"))
(ng)
(use-with "[TypJ]" 'left 'left 'left)
(use "[SCs]")
(assume "[SC 1]")
(by-assume-with "[SC 1]" "a^" "[SC 1 Body]")

(assert (pf "ex b^ SCr sigs(Typ rhos s)b^(Sub s (Wrap 0 ss))"))
(use "[IHs]" (pt "rhos"))
(ng)
(use-with "[TypJ]" 'left 'left 'right)
(use "[SCs]")
(assume "[SC 2]")
(by-assume-with "[SC 2]" "b^" "[SC 2 Body]")

(ex-intro (pt "Mod a^b^"))
(simp (pf "Equal sigs(sigs:+:(Nil type))"))
(use "SCrUnfold" (pt "Typ rhos s"))
(assert (pf "Typ rhos r=(Typ rhos s to sig)"))
(use "TypJApp")
(use "[TypJ]")
(assume "[Typ]")
(simp "<-" "[Typ]")
(use "[SC 1 Body]")
(simp "ListAppendNil")
(use "[SC 2 Body]")
(use "Eq-Symm")
(use-with "ListAppendNil" (py "type") (pt "sigs"))

; Case Abs
(assume "rho" "r" "[IHr]")
(assume "rhos" "sigs" "tau" "ss" "[TypJ]" "[SCs]")
(assert (pf "tau=(rho to Typ(rho::rhos)r)"))
(use "TypJAbsArrow")
(prop)
(assume "[tau]")
(simp "[tau]")
(use "LemmaSCFold")
(use "LemmaThreeAux1" (pt "tau")) 
(prop)
(prop)

(assume "taus" "s" "[SC]")
(use "LemmaTwo" (pt "Sub r (Wrap 0 (s::ss))"))
(use "TypJAppIntro" (pt "rho"))
(use "LemmaThreeAux1" (pt "tau"))
(prop)
(prop)
(by-assume-with "[SC]" "b^" "[SC Body]")
(use "SCrUnfoldTwo" (pt "b^"))
(prop)

(use "[IHr]" (pt "rho::rhos"))
(use "TypJAbsElim" (pt "tau"))
(prop)
(by-assume-with "[SCs]" "as^" "[SC 2 Body]")
(by-assume-with "[SC]" "b^" "[SC 3 Body]")
(ex-intro (pt "(b^ ::as^) "))

(use "SCrsDef")
(use "SCrsSTotal" (pt "sigs") (pt "rhos")
(pt "ss"))
(prop)
(prop)

(use "SCrsExtCtx")
(use "[SC 2 Body]")
(use "Ax6")
(save "LemmaThree")