src/Cube/Cube.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 49752 2bbb0013ff82
child 52143 36ffe23b25f8
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
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
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
     5
header {* Barendregt's Lambda-Cube *}
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
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    13
ML {*
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    14
  structure Rules = Named_Thms
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    15
  (
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    16
    val name = @{binding rules}
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    17
    val description = "Cube inference rules"
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    18
  )
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    19
*}
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    20
setup Rules.setup
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    21
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    22
typedecl "term"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    23
typedecl "context"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    24
typedecl typing
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    25
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    26
axiomatization
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    27
  Abs :: "[term, term => term] => term" and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    28
  Prod :: "[term, term => term] => term" and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    29
  Trueprop :: "[context, typing] => prop" and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    30
  MT_context :: "context" and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    31
  Context :: "[typing, context] => context" and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    32
  star :: "term"  ("*") and
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    33
  box :: "term"  ("\<box>") and
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    34
  app :: "[term, term] => term"  (infixl "^" 20) and
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    35
  Has_type :: "[term, term] => typing"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    36
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    37
nonterminal context' and typing'
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    38
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    39
syntax
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    40
  "_Trueprop" :: "[context', typing'] => prop"  ("(_/ \<turnstile> _)")
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    41
  "_Trueprop1" :: "typing' => prop"  ("(_)")
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    42
  "" :: "id => context'"  ("_")
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    43
  "" :: "var => context'"  ("_")
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    44
  "_MT_context" :: "context'"  ("")
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    45
  "_Context" :: "[typing', context'] => context'"  ("_ _")
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    46
  "_Has_type" :: "[term, term] => typing'"  ("(_:/ _)" [0, 0] 5)
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    47
  "_Lam" :: "[idt, term, term] => term"  ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    48
  "_Pi" :: "[idt, term, term] => term"  ("(3\<Pi> _:_./ _)" [0, 0] 10)
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    49
  "_arrow" :: "[term, term] => term"  (infixr "\<rightarrow>" 10)
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    50
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    51
translations
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    52
  "_Trueprop(G, t)" == "CONST Trueprop(G, t)"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    53
  ("prop") "x:X" == ("prop") "\<turnstile> x:X"
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    54
  "_MT_context" == "CONST MT_context"
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    55
  "_Context" == "CONST Context"
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    56
  "_Has_type" == "CONST Has_type"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    57
  "\<Lambda> x:A. B" == "CONST Abs(A, %x. B)"
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    58
  "\<Pi> x:A. B" => "CONST Prod(A, %x. B)"
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    59
  "A \<rightarrow> B" => "CONST Prod(A, %_. B)"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    60
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    61
syntax (xsymbols)
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    62
  "_Pi" :: "[idt, term, term] => term"    ("(3\<Pi> _:_./ _)" [0, 0] 10)
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    63
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    64
print_translation {*
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41526
diff changeset
    65
  [(@{const_syntax Prod},
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 41526
diff changeset
    66
    Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    67
*}
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    68
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    69
axiomatization where
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    70
  s_b: "*: \<box>"  and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    71
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    72
  strip_s: "[| A:*;  a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    73
  strip_b: "[| A:\<box>; a:A ==> G \<turnstile> x:X |] ==> a:A G \<turnstile> x:X" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    74
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    75
  app: "[| F:Prod(A, B); C:A |] ==> F^C: B(C)" and
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    77
  pi_ss: "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    78
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    79
  lam_ss: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    80
            ==> Abs(A, f) : Prod(A, B)" and
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    81
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
    82
  beta: "Abs(A, f)^a == f(a)"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    83
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
    84
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
    85
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    86
lemma imp_elim:
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    87
  assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 41229
diff changeset
    88
  shows "PROP P" by (rule app assms)+
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    89
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    90
lemma pi_elim:
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    91
  assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 41229
diff changeset
    92
  shows "PROP P" by (rule app assms)+
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    93
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    94
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    95
locale L2 =
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    96
  assumes pi_bs: "[| A:\<box>; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    97
    and lam_bs: "[| A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    98
                   ==> Abs(A,f) : Prod(A,B)"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
    99
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   100
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   101
lemmas [rules] = lam_bs pi_bs
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   102
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   103
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   104
17260
wenzelm
parents: 17252
diff changeset
   105
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   106
locale Lomega =
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   107
  assumes
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   108
    pi_bb: "[| A:\<box>; !!x. x:A ==> B(x):\<box> |] ==> Prod(A,B):\<box>"
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   109
    and lam_bb: "[| A:\<box>; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> |]
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   110
                   ==> Abs(A,f) : Prod(A,B)"
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   111
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   112
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   113
lemmas [rules] = lam_bb pi_bb
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   114
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   115
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   116
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   117
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   118
locale LP =
45242
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   119
  assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):\<box> |] ==> Prod(A,B):\<box>"
401f91ed8a93 discontinued redundant ASCII syntax;
wenzelm
parents: 45241
diff changeset
   120
    and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):\<box> |]
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   121
                   ==> Abs(A,f) : Prod(A,B)"
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   122
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   123
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   124
lemmas [rules] = lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   125
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   126
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   127
17260
wenzelm
parents: 17252
diff changeset
   128
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   129
locale LP2 = LP + L2
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   130
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   131
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   132
lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   133
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   134
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   135
17260
wenzelm
parents: 17252
diff changeset
   136
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   137
locale Lomega2 = L2 + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   138
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   139
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   140
lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   141
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   142
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   143
17260
wenzelm
parents: 17252
diff changeset
   144
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   145
locale LPomega = LP + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   146
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   147
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   148
lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   149
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   150
end
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   151
17260
wenzelm
parents: 17252
diff changeset
   152
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   153
locale CC = L2 + LP + Lomega
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   154
begin
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   155
49752
2bbb0013ff82 modernized dynamic "rules" -- avoid rebinding of static facts;
wenzelm
parents: 45242
diff changeset
   156
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
   157
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   158
end
45241
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   159
87950f752099 modernized specifications;
wenzelm
parents: 42284
diff changeset
   160
end