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


; ========================================
;  Section: The Definitions for the Proof
; ========================================
; contains the specific definitions for the proof

; Subsection: Miscellaneous
; =========================

; Definition: "ABS"
; -----------------
; binds the k-th free variable with given type rho
; used as an abbreviation particularly for Ax1 and
; the definition of "Eta"

(add-program-constant "ABS" 
 (py "nat => type => term => term") 1)

(add-computation-rule (pt "ABS k rho s")
 (pt "Abs rho(Sub s (Wrap (Succ (Succ k)) 
      ((Var map(Seq 1 k)):+:(Var 0):)))"))

; Definition: "ExtCtx"
; --------------------
; "ExtCtx" stands for "Extend Context". 
; For a context "rhos" it produces as many "rho" as needed 
; for "k" to be in the context "rhos:+:(ExtCtx rhos k rho)"

(add-program-constant "ExtCtx" 
 (py "list type=>nat=>type=>list type") 1)

(add-computation-rule (pt "ExtCtx (Nil type) 0 rho")
		      (pt "rho:"))
(add-computation-rule (pt "ExtCtx (sig::rhos) 0 rho")
		      (pt "(Nil type)"))
(add-computation-rule (pt "ExtCtx (Nil type) (Succ n) rho")
		      (pt "rho::(ExtCtx (Nil type) n rho)"))
(add-computation-rule (pt "ExtCtx (sig::rhos) (Succ n) rho")
		      (pt "(ExtCtx rhos n rho)"))

(pp (nt (pt "ExtCtx (sig::sig::sig:) 4 rho")))
; rho::rho:


; Subsection: Predicates
; ======================

; Subsubsection: Declaration of the Predicates
; ::::::::::::::::::::::::::::::::::::::::::::

; Definition: "N", "A", "Head", "Fr"
; ----------------------------------

(add-predconst-name
 "N" (make-arity (py "list type") (py "type") 
                 (py "term") (py "term")))

(add-predconst-name
 "A" (make-arity (py "list type") (py "type") 
                 (py "term") (py "term")))

(add-predconst-name 
 "Head" (make-arity (py "term") (py "term")))

(add-predconst-name
 "Fr" (make-arity (py "list type") (py "type") 
                  (py "term") (py "nat")))

; Definition: "SCr"
; -----------------
(add-predconst-name
 "SCr" (make-arity (py "list type") (py "type") 
                   (py "omega") (py "term")))

; Definition: "SC"
; ----------------
(add-predconst-name
 "SC" (make-arity (py "list type") (py "type") (py "term")))


; Subsubsection: Definition of the Predicates
; :::::::::::::::::::::::::::::::::::::::::::

; Definition: "FrDef", "FrDefRev"
; -------------------------------
(add-global-assumption "FrDef"
 (pf "all rhos,rho,r,k.Fr rhos rho r k -> 
      (TypJ rhos r rho & ((k < Lh rhos) -> F))"))

(add-global-assumption "FrDefRev"
 (pf "all rhos,rho,r,k.TypJ rhos r rho -> 
      ((k < Lh rhos) -> F) -> Fr rhos rho r k "))


; Definition: "SCrIotaUnfold", "SCrIotaFold", "SCrUnfold", "SCrFold"
; ------------------------------------------------------------------
; represents the Definition of SCr
 
(add-global-assumption
 "SCrIotaUnfold"
 (pf "all rhos,a^,r.SCr rhos Iota a^ r -> 
       all k.Fr rhos Iota r k -> N rhos Iota r(ModIota a^k)"))

(add-global-assumption
 "SCrIotaFold"
 (pf "all rhos,a^,r.
       TypJ rhos r Iota -> OmegaPart a^ =Iota ->
       (all k.Fr rhos Iota r k -> N rhos Iota r(ModIota a^k)) ->
       SCr rhos Iota a^r"))

(add-global-assumption
 "SCrUnfold"
 (pf "all rhos,rho,sig,a^,r.
       SCr rhos(rho to sig)a^r ->
       all sigs,b^,s.SCr(rhos:+:sigs)rho b^s ->
                     SCr(rhos:+:sigs)sig(Mod a^b^)(r s)"))
; additionally:
(add-global-assumption
 "SCrUnfoldTwo"
 (pf "all rhos,rho,a^,r.SCr rhos rho a^r -> 
 (TypJ rhos r rho) & (OmegaPart a^ =rho)"))

(add-global-assumption
 "SCrFold"
 (pf "all rhos,rho,sig,a^,r.
       TypJ rhos r(rho to sig) -> OmegaPart a^ =(rho to sig) ->
       (all sigs,b^,s.SCr(rhos:+:sigs)rho b^s ->
                      SCr(rhos:+:sigs)sig(Mod a^b^)(r s)) ->
       SCr rhos(rho to sig)a^r"))

; Definition: "SCrs"
; ------------------
(add-ids (list (list 
 "SCrs" (make-arity (py "list type")(py "list type")
                    (py "list omega") (py "list term"))))
 '("all sigs SCrs sigs(Nil type)(Nil omega)(Nil term)" "SCrsDefNil")
 '("all sigs,rho,rhos,a^,as^,s,ss.
       STotal as^ ->
       SCr sigs rho a^s -> SCrs sigs rhos as^ss -> 
       SCrs sigs(rho::rhos)(a^ ::as^)(s::ss)" "SCrsDef"))