src/Cube/Cube.thy
author wenzelm
Sat Nov 04 19:17:19 2017 +0100 (21 months ago)
changeset 67006 b1278ed3cd46
parent 61389 509d7ee638f8
child 69593 3dda49e08b9d
permissions -rw-r--r--
prefer main entry points of HOL;
     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 \<Rightarrow> term] \<Rightarrow> term" and
    21   Prod :: "[term, term \<Rightarrow> term] \<Rightarrow> term" and
    22   Trueprop :: "[context, typing] \<Rightarrow> prop" and
    23   MT_context :: "context" and
    24   Context :: "[typing, context] \<Rightarrow> context" and
    25   star :: "term"  ("*") and
    26   box :: "term"  ("\<box>") and
    27   app :: "[term, term] \<Rightarrow> term"  (infixl "\<cdot>" 20) and
    28   Has_type :: "[term, term] \<Rightarrow> typing"
    29 
    30 nonterminal context' and typing'
    31 syntax
    32   "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  ("(_/ \<turnstile> _)")
    33   "_Trueprop1" :: "typing' \<Rightarrow> prop"  ("(_)")
    34   "" :: "id \<Rightarrow> context'"  ("_")
    35   "" :: "var \<Rightarrow> context'"  ("_")
    36   "_MT_context" :: "context'"  ("")
    37   "_Context" :: "[typing', context'] \<Rightarrow> context'"  ("_ _")
    38   "_Has_type" :: "[term, term] \<Rightarrow> typing'"  ("(_:/ _)" [0, 0] 5)
    39   "_Lam" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10)
    40   "_Pi" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Prod>_:_./ _)" [0, 0] 10)
    41   "_arrow" :: "[term, term] \<Rightarrow> term"  (infixr "\<rightarrow>" 10)
    42 translations
    43   "_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
    44   ("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X"
    45   "_MT_context" \<rightleftharpoons> "CONST MT_context"
    46   "_Context" \<rightleftharpoons> "CONST Context"
    47   "_Has_type" \<rightleftharpoons> "CONST Has_type"
    48   "\<^bold>\<lambda>x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)"
    49   "\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
    50   "A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)"
    51 print_translation \<open>
    52   [(@{const_syntax Prod},
    53     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
    54 \<close>
    55 
    56 axiomatization where
    57   s_b: "*: \<box>"  and
    58 
    59   strip_s: "\<lbrakk>A:*; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
    60   strip_b: "\<lbrakk>A:\<box>; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
    61 
    62   app: "\<lbrakk>F:Prod(A, B); C:A\<rbrakk> \<Longrightarrow> F\<cdot>C: B(C)" and
    63 
    64   pi_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A, B):*" and
    65 
    66   lam_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):* \<rbrakk>
    67             \<Longrightarrow> Abs(A, f) : Prod(A, B)" and
    68 
    69   beta: "Abs(A, f)\<cdot>a \<equiv> f(a)"
    70 
    71 lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
    72 
    73 lemma imp_elim:
    74   assumes "f:A\<rightarrow>B" and "a:A" and "f\<cdot>a:B \<Longrightarrow> PROP P"
    75   shows "PROP P" by (rule app assms)+
    76 
    77 lemma pi_elim:
    78   assumes "F:Prod(A,B)" and "a:A" and "F\<cdot>a:B(a) \<Longrightarrow> PROP P"
    79   shows "PROP P" by (rule app assms)+
    80 
    81 
    82 locale L2 =
    83   assumes pi_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A,B):*"
    84     and lam_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk>
    85                    \<Longrightarrow> Abs(A,f) : Prod(A,B)"
    86 begin
    87 
    88 lemmas [rules] = lam_bs pi_bs
    89 
    90 end
    91 
    92 
    93 locale Lomega =
    94   assumes
    95     pi_bb: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>"
    96     and lam_bb: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk>
    97                    \<Longrightarrow> Abs(A,f) : Prod(A,B)"
    98 begin
    99 
   100 lemmas [rules] = lam_bb pi_bb
   101 
   102 end
   103 
   104 
   105 locale LP =
   106   assumes pi_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>"
   107     and lam_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk>
   108                    \<Longrightarrow> Abs(A,f) : Prod(A,B)"
   109 begin
   110 
   111 lemmas [rules] = lam_sb pi_sb
   112 
   113 end
   114 
   115 
   116 locale LP2 = LP + L2
   117 begin
   118 
   119 lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
   120 
   121 end
   122 
   123 
   124 locale Lomega2 = L2 + Lomega
   125 begin
   126 
   127 lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
   128 
   129 end
   130 
   131 
   132 locale LPomega = LP + Lomega
   133 begin
   134 
   135 lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
   136 
   137 end
   138 
   139 
   140 locale CC = L2 + LP + Lomega
   141 begin
   142 
   143 lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
   144 
   145 end
   146 
   147 end