src/Cube/Cube.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58617 4f169d2cf6f3
child 61387 f068e84cb9f3
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      Cube/Cube.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 section \<open>Barendregt's Lambda-Cube\<close>
     6 
     7 theory Cube
     8 imports Pure
     9 begin
    10 
    11 setup Pure_Thy.old_appl_syntax_setup
    12 
    13 named_theorems rules "Cube inference rules"
    14 
    15 typedecl "term"
    16 typedecl "context"
    17 typedecl typing
    18 
    19 axiomatization
    20   Abs :: "[term, term => term] => term" and
    21   Prod :: "[term, term => term] => term" and
    22   Trueprop :: "[context, typing] => prop" and
    23   MT_context :: "context" and
    24   Context :: "[typing, context] => context" and
    25   star :: "term"  ("*") and
    26   box :: "term"  ("\<box>") and
    27   app :: "[term, term] => term"  (infixl "^" 20) and
    28   Has_type :: "[term, term] => typing"
    29 
    30 nonterminal context' and typing'
    31 
    32 syntax
    33   "_Trueprop" :: "[context', typing'] => prop"  ("(_/ \<turnstile> _)")
    34   "_Trueprop1" :: "typing' => prop"  ("(_)")
    35   "" :: "id => context'"  ("_")
    36   "" :: "var => context'"  ("_")
    37   "_MT_context" :: "context'"  ("")
    38   "_Context" :: "[typing', context'] => context'"  ("_ _")
    39   "_Has_type" :: "[term, term] => typing'"  ("(_:/ _)" [0, 0] 5)
    40   "_Lam" :: "[idt, term, term] => term"  ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
    41   "_Pi" :: "[idt, term, term] => term"  ("(3\<Pi> _:_./ _)" [0, 0] 10)
    42   "_arrow" :: "[term, term] => term"  (infixr "\<rightarrow>" 10)
    43 
    44 translations
    45   "_Trueprop(G, t)" == "CONST Trueprop(G, t)"
    46   ("prop") "x:X" == ("prop") "\<turnstile> x:X"
    47   "_MT_context" == "CONST MT_context"
    48   "_Context" == "CONST Context"
    49   "_Has_type" == "CONST Has_type"
    50   "\<Lambda> x:A. B" == "CONST Abs(A, %x. B)"
    51   "\<Pi> x:A. B" => "CONST Prod(A, %x. B)"
    52   "A \<rightarrow> B" => "CONST Prod(A, %_. B)"
    53 
    54 syntax (xsymbols)
    55   "_Pi" :: "[idt, term, term] => term"    ("(3\<Pi> _:_./ _)" [0, 0] 10)
    56 
    57 print_translation \<open>
    58   [(@{const_syntax Prod},
    59     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
    60 \<close>
    61 
    62 axiomatization where
    63   s_b: "*: \<box>"  and
    64 
    65   strip_s: "[| A:*;  a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and
    66   strip_b: "[| A:\<box>; a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and
    67 
    68   app: "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" and
    69 
    70   pi_ss: "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" and
    71 
    72   lam_ss: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
    73             ==> Abs(A, f) : Prod(A, B)" and
    74 
    75   beta: "Abs(A, f)^a == f(a)"
    76 
    77 lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
    78 
    79 lemma imp_elim:
    80   assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
    81   shows "PROP P" by (rule app assms)+
    82 
    83 lemma pi_elim:
    84   assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
    85   shows "PROP P" by (rule app assms)+
    86 
    87 
    88 locale L2 =
    89   assumes pi_bs: "[| A:\<box>; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
    90     and lam_bs: "[| A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
    91                    ==> Abs(A,f) : Prod(A,B)"
    92 begin
    93 
    94 lemmas [rules] = lam_bs pi_bs
    95 
    96 end
    97 
    98 
    99 locale Lomega =
   100   assumes
   101     pi_bb: "[| A:\<box>; !!x. x:A ==> B(x):\<box> |] ==> Prod(A,B):\<box>"
   102     and lam_bb: "[| A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> |]
   103                    ==> Abs(A,f) : Prod(A,B)"
   104 begin
   105 
   106 lemmas [rules] = lam_bb pi_bb
   107 
   108 end
   109 
   110 
   111 locale LP =
   112   assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):\<box> |] ==> Prod(A,B):\<box>"
   113     and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> |]
   114                    ==> Abs(A,f) : Prod(A,B)"
   115 begin
   116 
   117 lemmas [rules] = lam_sb pi_sb
   118 
   119 end
   120 
   121 
   122 locale LP2 = LP + L2
   123 begin
   124 
   125 lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
   126 
   127 end
   128 
   129 
   130 locale Lomega2 = L2 + Lomega
   131 begin
   132 
   133 lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
   134 
   135 end
   136 
   137 
   138 locale LPomega = LP + Lomega
   139 begin
   140 
   141 lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
   142 
   143 end
   144 
   145 
   146 locale CC = L2 + LP + Lomega
   147 begin
   148 
   149 lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
   150 
   151 end
   152 
   153 end