# Theory Cube

Up to index of Isabelle/Cube

theory Cube
imports Pure
begin

    header {* Barendregt's Lambda-Cube *}

    theory Cube
    imports Pure
    begin

    typedecl "term"
    typedecl "context"
    typedecl typing

    nonterminals
      context_ typing_

    consts
      Abs           :: "[term, term => term] => term"
      Prod          :: "[term, term => term] => term"
      Trueprop      :: "[context, typing] => prop"
      MT_context    :: "context"
      Context       :: "[typing, context] => context"
      star          :: "term"                               ("*")
      box           :: "term"                               ("[]")
      app           :: "[term, term] => term"               (infixl "^" 20)
      Has_type      :: "[term, term] => typing"

    syntax
      Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
      Trueprop1     :: "typing_ => prop"                    ("(_)")
      ""            :: "id => context_"                     ("_")
      ""            :: "var => context_"                    ("_")
      MT_context    :: "context_"                           ("")
      Context       :: "[typing_, context_] => context_"    ("_ _")
      Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
      Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
      Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
      arrow         :: "[term, term] => term"               (infixr "->" 10)

    translations
      ("prop") "x:X" == ("prop") "|- x:X"
      "Lam x:A. B"   == "Abs(A, %x. B)"
      "Pi x:A. B"    => "Prod(A, %x. B)"
      "A -> B"       => "Prod(A, _K(B))"

    syntax (xsymbols)
      Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
      box           :: "term"                               ("\<box>")
      Lam           :: "[idt, term, term] => term"          ("(3Λ _:_./ _)" [0, 0, 0] 10)
      Pi            :: "[idt, term, term] => term"          ("(3Π _:_./ _)" [0, 0] 10)
      arrow         :: "[term, term] => term"               (infixr "->" 10)

    print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}

    axioms
      s_b:          "*: []"

      strip_s:      "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
      strip_b:      "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"

      app:          "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"

      pi_ss:        "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"

      lam_ss:       "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
                       ==> Abs(A, f) : Prod(A, B)"

      beta:          "Abs(A, f)^a == f(a)"

    lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
    lemmas rules = simple

    lemma imp_elim:
      assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
      shows "PROP P" by (rule app prems)+

    lemma pi_elim:
      assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
      shows "PROP P" by (rule app prems)+

    locale L2 =
      assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
        and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
                       ==> Abs(A,f) : Prod(A,B)"

    lemmas (in L2) rules = simple lam_bs pi_bs

    locale Lomega =
      assumes
        pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
        and lam_bb: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
                       ==> Abs(A,f) : Prod(A,B)"

    lemmas (in Lomega) rules = simple lam_bb pi_bb

    locale LP =
      assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
        and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
                       ==> Abs(A,f) : Prod(A,B)"

    lemmas (in LP) rules = simple lam_sb pi_sb

    locale LP2 = LP + L2

    lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb

    locale Lomega2 = L2 + Lomega

    lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb

    locale LPomega = LP + Lomega

    lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb

    locale CC = L2 + LP + Lomega

    lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb

    end

lemmas simple:

      *: []

      [| A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

lemmas simple:

      *: []

      [| A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

lemmas rules:

      *: []

      [| A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

lemmas rules:

      *: []

      [| A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

lemma imp_elim:

      [| f: A -> B; a: A; f ^ a: B ==> PROP P |] ==> PROP P

lemma pi_elim:

      [| F: Prod(A, B); a: A; F ^ a: B(a) ==> PROP P |] ==> PROP P

lemmas rules:

      PROP L2 ==> *: []

      [| PROP L2; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP L2; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP L2; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP L2; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP L2; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP L2; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP L2; A: []; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

lemmas rules:

      PROP Lomega ==> *: []

      [| PROP Lomega; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP Lomega; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP Lomega; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP Lomega; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP Lomega; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP Lomega; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP Lomega; A: []; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

lemmas rules:

      PROP LP ==> *: []

      [| PROP LP; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LP; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LP; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP LP; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LP; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP LP; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LP; A: *; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

lemmas rules:

      PROP LP2 ==> *: []

      [| PROP LP2; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LP2; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LP2; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP LP2; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LP2; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP LP2; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LP2; A: []; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP LP2; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LP2; A: *; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

lemmas rules:

      PROP Lomega2 ==> *: []

      [| PROP Lomega2; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP Lomega2; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP Lomega2; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP Lomega2; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP Lomega2; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP Lomega2; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP Lomega2; A: []; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP Lomega2; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP Lomega2; A: []; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

lemmas rules:

      PROP LPomega ==> *: []

      [| PROP LPomega; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LPomega; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP LPomega; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP LPomega; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LPomega; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP LPomega; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LPomega; A: []; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

      [| PROP LPomega; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP LPomega; A: *; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

lemmas rules:

      PROP CC ==> *: []

      [| PROP CC; A: *; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP CC; A: []; a: A ==> G |- x: X |] ==> a: A G |- x: X

      [| PROP CC; F: Prod(A, B); C: A |] ==> F ^ C: B(C)

      [| PROP CC; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP CC; A: *; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP CC; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): * |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP CC; A: []; !!x. x: A ==> B(x): * |] ==> Prod(A, B): *

      [| PROP CC; A: []; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP CC; A: []; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []

      [| PROP CC; A: *; !!x. x: A ==> f(x): B(x); !!x. x: A ==> B(x): [] |]
      ==> Abs(A, f): Prod(A, B)

      [| PROP CC; A: *; !!x. x: A ==> B(x): [] |] ==> Prod(A, B): []