Quelle  Cube.thy

(*  Title:      Cube/Cube.thy
  Author: Tobias Nipkow
*)

section ‹Barendregt's Lambda-Cube›

theory Cube
imports Pure
begin

setup Pure_Thy.old_appl_syntax_setup

named_theorems rules "Cube inference rules"

typedecl "term"
typedecl "context"
typedecl typing

axiomatization
  Abs :: "[term, term ==> term] ==> term" and
  Prod :: "[term, term ==> term] ==> term" and
  Trueprop :: "[context, typing] ==> prop" and
  MT_context :: "context" and
  Context :: "[typing, context] ==> context" and
  star :: "term"  (‹*›) and
  box :: "term"  (‹◻›) and
  app :: "[term, term] ==> term"  (infixl ‹⋅› 20) and
  Has_type :: "[term, term] ==> typing"

nonterminal context' and typing'
syntax
  "_Trueprop" :: "[context', typing'] ==> prop"  (‹(‹notation=judgment›_/ ⊨ _)›)
  "_Trueprop1" :: "typing' ==> prop"  (‹(‹notation=judgment›_)›)
  "" :: "id ==> context'"  (‹_›)
  "" :: "var ==> context'"  (‹_›)
  "_MT_context" :: "context'"  (‹›)
  "_Context" :: "[typing', context'] ==> context'"  (‹_ _›)
  "_Has_type" :: "[term, term] ==> typing'"  (‹(‹notation=‹infix Has_Type›\›_:/ _)› [0, 0] 5)
  "_Lam" :: "[idt, term, term] ==> term"  (‹(‹indent=3 notation=‹binder 🪙λ›\›\🪙λ_:_./ _)› [0, 0, 0] 10)
  "_Pi" :: "[idt, term, term] ==> term"  (‹(‹indent=3 notation=‹binder ∏›\›\∏_:_./ _)› [0, 0] 10)
  "_arrow" :: "[term, term] ==> term"  (infixr ‹→› 10)
syntax_consts
  "_Trueprop" ⇌ Trueprop and
  "_MT_context" ⇌ MT_context and
  "_Context" ⇌ Context and
  "_Has_type" ⇌ Has_type and
  "_Lam" ⇌ Abs and
  "_Pi" "_arrow" ⇌ Prod
translations
  "_Trueprop(G, t)" ⇌ "CONST Trueprop(G, t)"
  ("prop") "x:X" ⇌ ("prop") "⊨ x:X"
  "_MT_context" ⇌ "CONST MT_context"
  "_Context" ⇌ "CONST Context"
  "_Has_type" ⇌ "CONST Has_type"
  "🪙λx:A. B" ⇌ "CONST Abs(A, λx. B)"
  "∏x:A. B" ⇀ "CONST Prod(A, λx. B)"
  "A → B" ⇀ "CONST Prod(A, λ_. B)"
print_translation ‹
  [(🍋‹Prod›,
  fn _ => Syntax_Trans.dependent_tr' (🍋‹_Pi›, 🍋‹_arrow›))]
 ›

axiomatization where
  s_b: "*: ◻"  and

  strip_s: "[A:*; a:A ==> G ⊨ x:X] ==> a:A G ⊨ x:X" and
  strip_b: "[A:◻; a:A ==> G ⊨ x:X] ==> a:A G ⊨ x:X" and

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

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

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

  beta: "Abs(A, f)⋅a ≡ f(a)"

lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss

lemma imp_elim:
  assumes "f:A→B" and "a:A" and "f⋅a:B ==> PROP P"
  shows "PROP P" by (rule app assms)+

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


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)"
begin

lemmas [rules] = lam_bs pi_bs

end


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)"
begin

lemmas [rules] = lam_bb pi_bb

end


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)"
begin

lemmas [rules] = lam_sb pi_sb

end


locale LP2 = LP + L2
begin

lemmas [rules] = lam_bs pi_bs lam_sb pi_sb

end


locale Lomega2 = L2 + Lomega
begin

lemmas [rules] = lam_bs pi_bs lam_bb pi_bb

end


locale LPomega = LP + Lomega
begin

lemmas [rules] = lam_bb pi_bb lam_sb pi_sb

end


locale CC = L2 + LP + Lomega
begin

lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb

end

end