; $Id: auxLem3.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 "./auxGlobal_SHORT.scm")
;
; NOTICE: Uncomment modules only when file is run on its own
; ***********************************************************


; ==================================
;  Section: Auxiliaries for Lemma 3
; ==================================
; contains all auxiliaries for Lemma 3

; Lemma: "FrExtCtxRev"
; --------------------
(set-goal
   (pf "all rhos, sigs, rho, r, k. 
        TypJ rhos r rho -> 
        Fr(rhos:+:sigs) rho r k -> Fr rhos rho r k"))

(assume "rhos" "sigs" "rho" "r" "k" 1 2)
(use "FrDefRev")
(use 1)
(assert (pf "k<Lh (rhos:+:sigs) -> F"))
(use "FrDef" (pt "rho") (pt "r"))
(use 2)
(assert (pf "Lh (rhos :+: sigs) = Lh rhos + Lh sigs"))
(use "LhRhosSigs")
(assume 1)
(simp-with 3)
(use "Trivial7")
(save "FrExtCtxRev")

; Lemma: "SCrExtCtx"
; ------------------
(set-goal
 (pf "all rho,rhos,sigs,a^,s.
      SCr rhos rho a^ s -> SCr (rhos:+:sigs) rho a^ s"))

(ind)

;Case: Iota
(assume "rhos" "sigs" "a^" "s" 1)
(use "SCrIotaFold")
(assert (pf "TypJ rhos s Iota"))
(use "SCrUnfoldTwo" (pt "a^"))
(use 1)
(assume 2)
(use "TypJExtCtx")
(use 2)

(use "SCrUnfoldTwo" (pt "rhos") (pt "s"))
(use 1)

(assert (pf "all k.Fr rhos Iota s k 
             -> N rhos Iota s (ModIota a^ k)"))
(use "SCrIotaUnfold")
(use 1)

(assume "[neu]")
(assume "k" 2)

(use "Ax9")
(use "SCrIotaUnfold")
(use 1)

(use "FrExtCtxRev" (pt "sigs"))
(use "SCrUnfoldTwo" (pt "a^"))
(use 1)
(use 3)

; Case (rho to sig)
(assume "rho" "sig" "[IH rho]" "[IH sig]")

; Case: sigs = (Nil type)
(assume "rhos" "sigs" "a^" "s" 1)

(assert (pf "all sigs,b^,r.SCr (rhos:+:sigs) rho b^ r ->
             SCr(rhos:+:sigs) sig (Mod a^ b^) (s r)"))

(use "SCrUnfold")
(use 3)

(assume "[SCr]")

(use "SCrFold")
(assert (pf "TypJ rhos s (rho to sig)"))
(use "SCrUnfoldTwo" (pt "a^"))
(use 3)
(assume 2)
(use "TypJExtCtx")
(use 5)

(use "SCrUnfoldTwo" (pt "rhos") (pt "s"))
(use 3)

(assume "taus" "b^" "r" 1)

(assert (pf "(rhos:+:sigs:+:taus) =
             (rhos:+:(sigs:+:taus))"))
(use "ListAssoc")
(assume 1) 
(simp-with 6)

(use "[SCr]")
(simp-with "<-" 6)
(use 5)
(save "SCrExtCtx")

; Lemma: "SCrsExtCtxSTotal"
; -------------------------
(set-goal
 (pf "all sigs,taus,rhos,as^.STotal as^ -> all ss.
      SCrs sigs rhos as^ss -> SCrs(sigs:+:taus)rhos as^ss"))


(assume "sigs" "taus")
(ind)

(cases)
(cases)
(assume 1)
(use "SCrsDefNil")

(assume "r" "rs" 1)
; contradiction:
(assert (pf " Lh (Nil type) = Lh (r::rs)"))
(use "SCrsLh" (pt "sigs") (pt "(Nil omega)"))

(use 1)
(assume 2)
(ng)
(prop)

(assume "a^" "as^" "[STotal]" "ss" 1)
; contradiction:
(assert (pf " Lh (a^ ::as^) = Lh (Nil type)"))
(use "SCrsLh" (pt "sigs") (pt "ss"))

(prop)
(assume 1)
(prop)

(assume "rho" "rhos" "[IH]")
(cases)
(assume "ss" 1)
; contradiction:
(assert (pf " Lh (Nil omega) = Lh (rho::rhos)"))
(use "SCrsLh" (pt "sigs") (pt "ss"))
(use 2)
(assume 3)
(ng)
(prop)

(assume "a^" "as^")
(assume "[STotal]")
(cases)
(assume 1)
; contradiction:
(assert (pf " Lh (rho::rhos) = Lh (Nil term)"))
(use "SCrsLh" (pt "sigs") (pt "(a^ ::as^)"))

(use 3)
(assume 4)
(ng)
(prop)

(assume "r" "rs" "[SCrs]")
(use "SCrsDef")
(use "[STotal]")

(assert (pf "SCr sigs  rho a^ r"))
(use "SCrsDefRev" (pt "rhos") (pt "as^") (pt "rs"))
(use "[SCrs]")
(assume "[SCr]")
(use "SCrExtCtx")
(use "[SCr]")

(use "[IH]")
(use "[STotal]")

(use "SCrsDefRev" (pt "rho") (pt "a^") (pt "r"))
(use "[SCrs]")
(save "SCrsExtCtxSTotal")

; Lemma: "SCrsExtCtx"
; -------------------
(set-goal
 (pf "all sigs,taus,rhos,as^,ss.
      SCrs sigs rhos as^ss -> SCrs(sigs:+:taus)rhos as^ss"))

(strip)
(use "SCrsExtCtxSTotal")
(use "SCrsSTotal" (pt "sigs") (pt "rhos")
(pt "ss"))
(prop)
(prop)
(save "SCrsExtCtx")

; Lemma: "TypJAbsElim"
; --------------------
(set-goal (pf "all rhos,rho,tau,r.
 TypJ rhos(Abs rho r)tau -> TypJ(rho::rhos)r(Typ(rho::rhos)r)"))

(assume "rhos" "rho" "tau" "r" 1)
(ng)
(use-with 1 'left)
(save "TypJAbsElim")

; Lemma: "TypJVarRef"
; -------------------
(set-goal
 (pf "all k,rhos,rho.
      TypJ rhos(Var k)rho -> rho=(k thof rhos)"))

(ind)
(ind)
(assume "rho" 1)
(ng)
(prop)

(assume "rho" "rhos" "IH")
(assume "sig" 2)
(ng)
(simp-with "<-" 2)
(prop)

(assume "n" "IH")
(ind)
(assume "rho" 2)
(ng)
(prop)

(assume "rho" "rhos" "IH 2")
(assume "sig" 1)
(ng)
(inst-with "IH" (pt "rhos") (pt "sig") 3)
(prop)
(save "TypJVarRef")

; Lemma: "TypJAbsArrow"
; ---------------------
(set-goal
  (pf "all rhos,rho,tau,r.
       TypJ rhos(Abs rho r)tau ->
       tau=(rho to Typ(rho::rhos)r)"))

(assume "rhos" "rho" "tau" "r" 1)
(assert (pf "tau= Typ rhos (Abs rho r)"))
(use "TypJTyp")
(use 1)
(assume 2)
(simp-with 2)
(prop)
(save "TypJAbsArrow")

; Lemma: "LemmaThreeVarSTotal"
; ----------------------------
(set-goal
 (pf "all sigs,rhos,k,as^.STotal as^ -> all ss.
      SCrs sigs rhos as^ ss -> k<Lh rhos -> 
      SCr sigs(k thof rhos)(k thof as^)(k thof ss)"))

(assume "sigs")
(ind)
(assume "k" "as^" 1 "ss" 2 3)
(ng)
(prop)

(assume "rho" "rhos" "IH" "k")

(cases)
(cases)

(assume 1 2)
; contradiction:
(assert (pf "Lh (rho::rhos) = Lh (Nil term)"))
(use "SCrsLh" (pt "sigs") (pt "(Nil omega)"))
(use 2)
(assume 4)
(ng)
(prop)

(assume "r" "rs" "IH 2" 3)
; contradiction:
(assert (pf "Lh (Nil omega) = Lh (rho::rhos)"))
(use "SCrsLh" (pt "sigs") (pt "(r::rs)"))
(use 2)
(assume 4)
(ng)
(prop)

(assume "a^" "as^" "[STotal]")
(cases)
(assume 3 4)
; contradiction:
(assert (pf "Lh (rho::rhos) = Lh (Nil term)"))
(use "SCrsLh" (pt "sigs") (pt "a^ ::as^"))
(use 3)
(assume 5)
(ng)
(prop)

(assume "r" "rs" 1 2)
(inst-with "SCrsDefRev" (pt "sigs")
 (pt "rho") (pt "rhos") (pt "a^") (pt "as^")
 (pt  "r") (pt "rs") 3)
(cases (pt "k"))
(assume 6)
(ng)
(use-with 5 'left)

(assume "n" 6)
(ng)
(use "IH")
(use "[STotal]")
(use-with 5 'right)
(assert (pf "Succ n < Succ Lh rhos"))
(simp-with "<-" 6)
(use 4)
(ng)
(prop)
(save "LemmaThreeVarSTotal")

; Lemma: "LemmaThreeVar"
; ----------------------
(set-goal
 (pf "all sigs,rhos,k,as^,ss.
      SCrs sigs rhos as^ ss -> k<Lh rhos -> 
      SCr sigs(k thof rhos)(k thof as^)(k thof ss)"))

(strip)
(use "LemmaThreeVarSTotal")
(use "SCrsSTotal" (pt "sigs") (pt "rhos")
(pt "ss"))
(prop)
(prop)
(prop)
(save "LemmaThreeVar")

; Lemma: "TypJApp"
; ----------------
; auxiliary for LemmaThree

(set-goal
  (pf "all sig,rhos,r,s.
        TypJ rhos(r s)sig -> 
        Typ rhos r = (Typ rhos s to sig)"))

(ng)
(assume "sig" "rhos" "r" "s" "[Ass1]")
(simp "<-" (pf "Valtyp(Typ rhos r)=sig"))
(use-with "[Ass1]" 'left 'right)
(use-with "[Ass1]" 'right)
(save "TypJApp")


; Subsection: LemmaThreeAux1
; ==========================
; makes particularly use of "TypJSub" from the global auxiliaries

; Lemma: "SCrsTypJsAllSTotal"
; ---------------------------
(set-goal
 (pf "all sigs,rhos,ss,as^.STotal as^ ->
      SCrs sigs rhos as^ ss -> 
      TypJs sigs ss rhos"))

(assume "sigs")
(ind)
(ind)
(assume "as^" "[STotal]" "[SCrs]")
(ng)
(prop)

(assume "r" "rs" "[IH rhos]")
(assume  "as^" "[STotal]" "[SCrs]")
;contradiction
(assert (pf " Lh (Nil type) = Lh (r::rs)"))
(use "SCrsLh" (pt "sigs") (pt "as^"))
(use "[SCrs]")
(assume 2)
(ng)
(prop)

(assume "rho" "rhos" "[IH rhos]")
(ind)
(assume "as^" "[STotal]" "[SCrs]")
;contradiction
(assert (pf " Lh (rho::rhos) = Lh (Nil term)"))
(use "SCrsLh" (pt "sigs") (pt "as^"))
(use "[SCrs]")
(assume 2)
(ng)
(prop)

(assume "r" "rs" "[IH ss]")
(cases)
(assume "[SCrs]")
;contradiction
(assert (pf " Lh (Nil omega) = Lh (rho::rhos)"))
(use "SCrsLh" (pt "sigs") (pt "(r::rs)"))
(use "[SCrs]")
(assume 2)
(ng)
(prop)

(assume "a^" "as^" "[STotal]" "[SCrs]") 
(assert (pf "TypJ sigs r rho"))
(use "SCrUnfoldTwo" (pt "a^"))
(use "SCrsDefRev" (pt "rhos") (pt "as^") (pt "rs"))
(use "[SCrs]")

(assume "[TypJ]")
(ng)
(split)
(use "[TypJ]")

(use "[IH rhos]" (pt "as^"))
(use "[STotal]")
(use "SCrsDefRev" (pt "rho") (pt "a^") (pt "r"))
(use "[SCrs]")
(save "SCrsTypJsAllSTotal")

; Lemma: "SCrsTypJsAll"
; ---------------------
(set-goal
 (pf "all sigs,rhos,ss,as^.
      SCrs sigs rhos as^ ss -> 
      TypJs sigs ss rhos"))

(strip)
(use "SCrsTypJsAllSTotal" (pt "as^"))
(use "SCrsSTotal" (pt "sigs") (pt "rhos")
(pt "ss"))
(prop)
(prop)
(save "SCrsTypJsAll")

; Lemma: "SCrsTypJs"
; -------------------
(set-goal
 (pf "all sigs,rhos,ss.
      (ex as^.SCrs sigs rhos as^ ss) -> 
      TypJs sigs ss rhos"))

(assume "sigs" "rhos" "ss" 1)
(by-assume-with 1 "as^" 2)
(use "SCrsTypJsAll" (pt "as^"))
(prop)
(save "SCrsTypJs")

; Lemma: "TypJSubSCrs"
; --------------------
(set-goal
 (pf "all rhos,sigs,rho,r,ss.TypJ rhos r rho ->
      (ex as^.SCrs sigs rhos as^ ss) -> 
      TypJ sigs (Sub r (Wrap 0 ss)) rho"))

(assume "rhos" "sigs" "rho" "r" "ss" 1 2)
(use "TypJSub" (pt "rhos"))
(use 1)

(use "SCrsTypJs")
(use 2)
(save "TypJSubSCrs")

; Lemma:  "LemmaThreeAux1"
; ------------------------
(set-goal
  (pf "all rhos,sigs,rho,tau,r,ss.TypJ rhos(Abs rho r)tau ->
       (ex as^.SCrs sigs rhos as^ ss) -> 
       TypJ sigs(Sub(Abs rho r) 
        (Wrap 0 ss))(rho to Typ(rho::rhos)r)"))

(assume "rhos" "sigs" "rho" "tau" "r" "ss" 1 2)
(assert (pf "tau=(rho to Typ(rho::rhos)r)"))
(use "TypJAbsArrow")
(prop)
(assume "[tau]")
(simp "<-" "[tau]")
(use "TypJSubSCrs" (pt "rhos"))
(use 1)
(use 2)
(save "LemmaThreeAux1")