src/Cube/Cube.thy
author wenzelm
Wed, 10 Feb 2016 14:14:43 +0100
changeset 62278 c04e97be39d3
parent 61389 509d7ee638f8
child 69593 3dda49e08b9d
permissions -rw-r--r--
misc tuning and updates;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
22809
3cf5df73d50a added header;
wenzelm
parents: 17782
diff changeset
     1
(*  Title:      Cube/Cube.thy
3cf5df73d50a added header;
wenzelm
parents: 17782
diff changeset
     2
    Author:     Tobias Nipkow
3cf5df73d50a added header;
wenzelm
parents: 17782
diff changeset
     3
*)
3773
989ef5e9d543 syntactic constants;
wenzelm
parents: 1149
diff changeset
     4
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 58617
diff changeset
     5
section \<open>Barendregt's Lambda-Cube\<close>
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
     6
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
     7
theory Cube
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
     8
imports Pure
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
     9
begin
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    10
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 35256
diff changeset
    11
setup Pure_Thy.old_appl_syntax_setup
26956
1309a6a0a29f setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
wenzelm
parents: 24783
diff changeset
    12
57945
cacb00a569e0 prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents: 52143
diff changeset
    13
named_theorems rules "Cube inference rules"
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    14
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    15
typedecl "term"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    16
typedecl "context"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    17
typedecl typing
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    18
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    19
axiomatization
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    20
  Abs :: "[term, term \<Rightarrow> term] \<Rightarrow> term" and
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    21
  Prod :: "[term, term \<Rightarrow> term] \<Rightarrow> term" and
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    22
  Trueprop :: "[context, typing] \<Rightarrow> prop" and
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    23
  MT_context :: "context" and
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    24
  Context :: "[typing, context] \<Rightarrow> context" and
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    25
  star :: "term"  ("*") and
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    26
  box :: "term"  ("\<box>") and
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    27
  app :: "[term, term] \<Rightarrow> term"  (infixl "\<cdot>" 20) and
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    28
  Has_type :: "[term, term] \<Rightarrow> typing"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    29
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    30
nonterminal context' and typing'
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    31
syntax
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    32
  "_Trueprop" :: "[context', typing'] \<Rightarrow> prop"  ("(_/ \<turnstile> _)")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    33
  "_Trueprop1" :: "typing' \<Rightarrow> prop"  ("(_)")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    34
  "" :: "id \<Rightarrow> context'"  ("_")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    35
  "" :: "var \<Rightarrow> context'"  ("_")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    36
  "_MT_context" :: "context'"  ("")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    37
  "_Context" :: "[typing', context'] \<Rightarrow> context'"  ("_ _")
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    38
  "_Has_type" :: "[term, term] \<Rightarrow> typing'"  ("(_:/ _)" [0, 0] 5)
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    39
  "_Lam" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10)
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    40
  "_Pi" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Prod>_:_./ _)" [0, 0] 10)
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    41
  "_arrow" :: "[term, term] \<Rightarrow> term"  (infixr "\<rightarrow>" 10)
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    42
translations
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    43
  "_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    44
  ("prop") "x:X" \<rightleftharpoons> ("prop") "\<turnstile> x:X"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    45
  "_MT_context" \<rightleftharpoons> "CONST MT_context"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    46
  "_Context" \<rightleftharpoons> "CONST Context"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    47
  "_Has_type" \<rightleftharpoons> "CONST Has_type"
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    48
  "\<^bold>\<lambda>x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)"
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    49
  "\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    50
  "A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)"
58617
4f169d2cf6f3 more cartouches;
wenzelm
parents: 57945
diff changeset
    51
print_translation \<open>
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41526
diff changeset
    52
  [(@{const_syntax Prod},
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 49752
diff changeset
    53
    fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
58617
4f169d2cf6f3 more cartouches;
wenzelm
parents: 57945
diff changeset
    54
\<close>
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    55
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    56
axiomatization where
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    57
  s_b: "*: \<box>"  and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    58
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    59
  strip_s: "\<lbrakk>A:*; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    60
  strip_b: "\<lbrakk>A:\<box>; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    61
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    62
  app: "\<lbrakk>F:Prod(A, B); C:A\<rbrakk> \<Longrightarrow> F\<cdot>C: B(C)" and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    64
  pi_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A, B):*" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    65
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    66
  lam_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):* \<rbrakk>
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    67
            \<Longrightarrow> Abs(A, f) : Prod(A, B)" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    68
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    69
  beta: "Abs(A, f)\<cdot>a \<equiv> f(a)"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    70
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    71
lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    72
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    73
lemma imp_elim:
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    74
  assumes "f:A\<rightarrow>B" and "a:A" and "f\<cdot>a:B \<Longrightarrow> PROP P"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 41229
diff changeset
    75
  shows "PROP P" by (rule app assms)+
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    76
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    77
lemma pi_elim:
61388
92e97b800d1e tuned syntax -- more symbols;
wenzelm
parents: 61387
diff changeset
    78
  assumes "F:Prod(A,B)" and "a:A" and "F\<cdot>a:B(a) \<Longrightarrow> PROP P"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 41229
diff changeset
    79
  shows "PROP P" by (rule app assms)+
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    80
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    81
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    82
locale L2 =
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    83
  assumes pi_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A,B):*"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    84
    and lam_bs: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk>
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    85
                   \<Longrightarrow> Abs(A,f) : Prod(A,B)"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    86
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    87
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    88
lemmas [rules] = lam_bs pi_bs
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    89
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    90
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    91
17260
wenzelm
parents: 17252
diff changeset
    92
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    93
locale Lomega =
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    94
  assumes
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    95
    pi_bb: "\<lbrakk>A:\<box>; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    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>
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
    97
                   \<Longrightarrow> Abs(A,f) : Prod(A,B)"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    98
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    99
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   100
lemmas [rules] = lam_bb pi_bb
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   101
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   102
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   103
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   104
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   105
locale LP =
61387
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
   106
  assumes pi_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk> \<Longrightarrow> Prod(A,B):\<box>"
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
   107
    and lam_sb: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):\<box>\<rbrakk>
f068e84cb9f3 more symbols;
wenzelm
parents: 58889
diff changeset
   108
                   \<Longrightarrow> Abs(A,f) : Prod(A,B)"
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   109
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   110
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   111
lemmas [rules] = lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   112
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   113
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   114
17260
wenzelm
parents: 17252
diff changeset
   115
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   116
locale LP2 = LP + L2
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   117
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   118
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   119
lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   120
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   121
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   122
17260
wenzelm
parents: 17252
diff changeset
   123
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   124
locale Lomega2 = L2 + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   125
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   126
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   127
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   128
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   129
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   130
17260
wenzelm
parents: 17252
diff changeset
   131
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   132
locale LPomega = LP + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   133
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   134
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   135
lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   136
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   137
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   138
17260
wenzelm
parents: 17252
diff changeset
   139
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   140
locale CC = L2 + LP + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   141
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   142
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   143
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   144
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   145
end
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   146
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   147
end