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