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

CONV = 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"
        symm    "M = N ==> N = 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)
end