(* ungetypter Lambda-Kalkuel - Reduktion *)
(* Vigano/Leven/Friedrich/Ayari WS00/01 *)

RED = Pure +

types
        term

consts
        Abs      :: "[term => term] => term"     (binder "lam " 10)
        "^"      :: "[term, term] => term"       (infixl 20)

        K        :: "term"
        I        :: "term"
        S        :: "term"

        B        :: "term"

        YC       :: "term"
        YT       :: "term"

        Trueprop :: "[term, term] => prop"       ("(_ --> _)")

rules
        beta    "(lam x. f(x))^a --> f(a)"
        refl    "M --> M"
        trans   "[| M --> N; N --> L |] ==> M --> L"
        appr    "M --> N ==> M^Z --> N^Z"
        appl    "M --> N ==> Z^M --> Z^N"
        epsi    "[| !! x. M(x) --> N(x) |] ==> (lam x. M(x)) --> (lam x. N(x))"

        K_def   "K == lam x. (lam y. x)"
        I_def   "I == lam x. x"
        S_def   "S == lam x. (lam y. (lam z. x^z^(y^z)))"

        B_def   "B == S^(K^S)^K"

        YC_def   "YC == lam f. ((lam x. f^(x^x))^(lam x. f^(x^x)))"
        YT_def  "YT == (lam z. lam x. x^(z^z^x))^(lam z. lam x. x^(z^z^x))"

  
syntax (symbols)
  "lam "        :: "[idts, term] => term"             ("(3\\<lambda>_./ _)" [0, 10] 10)
  
syntax (xsymbols)
  "op -->"      :: "[term, term] => term"                (infixr "\\<longrightarrow>" 25)
end
  
 