src/Cube/Cube.thy
author wenzelm
Tue Jul 31 21:19:23 2007 +0200 (2007-07-31)
changeset 24101 bdcefe679ced
parent 22809 3cf5df73d50a
child 24783 5a3e336a2e37
permissions -rw-r--r--
with_charset: setmp_noncritical;
wenzelm@22809
     1
(*  Title:      Cube/Cube.thy
wenzelm@22809
     2
    ID:         $Id$
wenzelm@22809
     3
    Author:     Tobias Nipkow
wenzelm@22809
     4
*)
wenzelm@3773
     5
wenzelm@17252
     6
header {* Barendregt's Lambda-Cube *}
wenzelm@17252
     7
wenzelm@17252
     8
theory Cube
wenzelm@17252
     9
imports Pure
wenzelm@17252
    10
begin
wenzelm@17252
    11
wenzelm@17252
    12
typedecl "term"
wenzelm@17252
    13
typedecl "context"
wenzelm@17252
    14
typedecl typing
wenzelm@17252
    15
wenzelm@17252
    16
nonterminals
wenzelm@17252
    17
  context_ typing_
wenzelm@17252
    18
wenzelm@17252
    19
consts
wenzelm@17252
    20
  Abs           :: "[term, term => term] => term"
wenzelm@17252
    21
  Prod          :: "[term, term => term] => term"
wenzelm@17252
    22
  Trueprop      :: "[context, typing] => prop"
wenzelm@17252
    23
  MT_context    :: "context"
wenzelm@17252
    24
  Context       :: "[typing, context] => context"
wenzelm@17252
    25
  star          :: "term"                               ("*")
wenzelm@17252
    26
  box           :: "term"                               ("[]")
wenzelm@17252
    27
  app           :: "[term, term] => term"               (infixl "^" 20)
wenzelm@17252
    28
  Has_type      :: "[term, term] => typing"
wenzelm@17252
    29
wenzelm@17252
    30
syntax
wenzelm@17252
    31
  Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
wenzelm@17252
    32
  Trueprop1     :: "typing_ => prop"                    ("(_)")
wenzelm@17252
    33
  ""            :: "id => context_"                     ("_")
wenzelm@17252
    34
  ""            :: "var => context_"                    ("_")
wenzelm@17252
    35
  MT_context    :: "context_"                           ("")
wenzelm@17252
    36
  Context       :: "[typing_, context_] => context_"    ("_ _")
wenzelm@17252
    37
  Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
wenzelm@17252
    38
  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
wenzelm@17252
    39
  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
wenzelm@17252
    40
  arrow         :: "[term, term] => term"               (infixr "->" 10)
wenzelm@17252
    41
wenzelm@17252
    42
translations
wenzelm@17260
    43
  ("prop") "x:X" == ("prop") "|- x:X"
wenzelm@17260
    44
  "Lam x:A. B"   == "Abs(A, %x. B)"
wenzelm@17260
    45
  "Pi x:A. B"    => "Prod(A, %x. B)"
wenzelm@17782
    46
  "A -> B"       => "Prod(A, %_. B)"
wenzelm@17252
    47
wenzelm@17252
    48
syntax (xsymbols)
wenzelm@17252
    49
  Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
wenzelm@17252
    50
  box           :: "term"                               ("\<box>")
wenzelm@17252
    51
  Lam           :: "[idt, term, term] => term"          ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
wenzelm@17252
    52
  Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
wenzelm@17252
    53
  arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
wenzelm@17252
    54
wenzelm@17252
    55
print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
wenzelm@17252
    56
wenzelm@17252
    57
axioms
wenzelm@17252
    58
  s_b:          "*: []"
wenzelm@17252
    59
wenzelm@17252
    60
  strip_s:      "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
wenzelm@17252
    61
  strip_b:      "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
wenzelm@17252
    62
wenzelm@17252
    63
  app:          "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
clasohm@0
    64
wenzelm@17252
    65
  pi_ss:        "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
wenzelm@17252
    66
wenzelm@17252
    67
  lam_ss:       "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
wenzelm@17252
    68
                   ==> Abs(A, f) : Prod(A, B)"
wenzelm@17252
    69
wenzelm@17252
    70
  beta:          "Abs(A, f)^a == f(a)"
wenzelm@17252
    71
wenzelm@17252
    72
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
wenzelm@17252
    73
lemmas rules = simple
wenzelm@17252
    74
wenzelm@17252
    75
lemma imp_elim:
wenzelm@17252
    76
  assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
wenzelm@17252
    77
  shows "PROP P" by (rule app prems)+
wenzelm@17252
    78
wenzelm@17252
    79
lemma pi_elim:
wenzelm@17252
    80
  assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
wenzelm@17252
    81
  shows "PROP P" by (rule app prems)+
wenzelm@17252
    82
wenzelm@17252
    83
wenzelm@17252
    84
locale L2 =
wenzelm@17252
    85
  assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
wenzelm@17252
    86
    and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
wenzelm@17252
    87
                   ==> Abs(A,f) : Prod(A,B)"
wenzelm@17252
    88
wenzelm@17252
    89
lemmas (in L2) rules = simple lam_bs pi_bs
wenzelm@17252
    90
wenzelm@17260
    91
wenzelm@17252
    92
locale Lomega =
wenzelm@17252
    93
  assumes
wenzelm@17252
    94
    pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
wenzelm@17252
    95
    and lam_bb: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
wenzelm@17252
    96
                   ==> Abs(A,f) : Prod(A,B)"
wenzelm@17252
    97
wenzelm@17252
    98
lemmas (in Lomega) rules = simple lam_bb pi_bb
wenzelm@17252
    99
wenzelm@17252
   100
wenzelm@17252
   101
locale LP =
wenzelm@17252
   102
  assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
wenzelm@17252
   103
    and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
wenzelm@17252
   104
                   ==> Abs(A,f) : Prod(A,B)"
wenzelm@17252
   105
wenzelm@17252
   106
lemmas (in LP) rules = simple lam_sb pi_sb
wenzelm@17252
   107
wenzelm@17260
   108
wenzelm@17252
   109
locale LP2 = LP + L2
wenzelm@17252
   110
wenzelm@17252
   111
lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb
wenzelm@17252
   112
wenzelm@17260
   113
wenzelm@17252
   114
locale Lomega2 = L2 + Lomega
wenzelm@17252
   115
wenzelm@17252
   116
lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb
wenzelm@17252
   117
wenzelm@17260
   118
wenzelm@17252
   119
locale LPomega = LP + Lomega
wenzelm@17252
   120
wenzelm@17252
   121
lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb
wenzelm@17252
   122
wenzelm@17260
   123
wenzelm@17252
   124
locale CC = L2 + LP + Lomega
wenzelm@17252
   125
wenzelm@17252
   126
lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
wenzelm@17252
   127
wenzelm@17252
   128
end