src/Cube/Cube.thy
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 39557 fe5722fce758
child 41229 d797baa3d57c
permissions -rw-r--r--
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
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
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    13
typedecl "term"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    14
typedecl "context"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    15
typedecl typing
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    16
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    17
nonterminals
24783
5a3e336a2e37 avoid internal names;
wenzelm
parents: 22809
diff changeset
    18
  context' typing'
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    19
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    20
consts
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    21
  Abs :: "[term, term => term] => term"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    22
  Prod :: "[term, term => term] => term"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    23
  Trueprop :: "[context, typing] => prop"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    24
  MT_context :: "context"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    25
  Context :: "[typing, context] => context"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    26
  star :: "term"    ("*")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    27
  box :: "term"    ("[]")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    28
  app :: "[term, term] => term"    (infixl "^" 20)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    29
  Has_type :: "[term, term] => typing"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    30
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    31
syntax
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    32
  "\<^const>Cube.Trueprop" :: "[context', typing'] => prop"    ("(_/ |- _)")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    33
  "_Trueprop1" :: "typing' => prop"    ("(_)")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    34
  "" :: "id => context'"    ("_")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    35
  "" :: "var => context'"    ("_")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    36
  "\<^const>Cube.MT_context" :: "context'"    ("")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    37
  "\<^const>Cube.Context" :: "[typing', context'] => context'"    ("_ _")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    38
  "\<^const>Cube.Has_type" :: "[term, term] => typing'"    ("(_:/ _)" [0, 0] 5)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    39
  "_Lam" :: "[idt, term, term] => term"    ("(3Lam _:_./ _)" [0, 0, 0] 10)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    40
  "_Pi" :: "[idt, term, term] => term"    ("(3Pi _:_./ _)" [0, 0] 10)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    41
  "_arrow" :: "[term, term] => term"    (infixr "->" 10)
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    42
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    43
translations
17260
wenzelm
parents: 17252
diff changeset
    44
  ("prop") "x:X" == ("prop") "|- x:X"
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    45
  "Lam x:A. B" == "CONST Abs(A, %x. B)"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    46
  "Pi x:A. B" => "CONST Prod(A, %x. B)"
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    47
  "A -> B" => "CONST Prod(A, %_. B)"
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    48
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    49
syntax (xsymbols)
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    50
  "\<^const>Cube.Trueprop" :: "[context', typing'] => prop"    ("(_/ \<turnstile> _)")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    51
  "\<^const>Cube.box" :: "term"    ("\<box>")
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    52
  "_Lam" :: "[idt, term, term] => term"    ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    53
  "_Pi" :: "[idt, term, term] => term"    ("(3\<Pi> _:_./ _)" [0, 0] 10)
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    54
  "_arrow" :: "[term, term] => term"    (infixr "\<rightarrow>" 10)
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    55
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    56
print_translation {*
35256
b73ae1a8fe7e adapted to authentic syntax;
wenzelm
parents: 35113
diff changeset
    57
  [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35054
diff changeset
    58
*}
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    59
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    60
axioms
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    61
  s_b:          "*: []"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    62
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    63
  strip_s:      "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    64
  strip_b:      "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    65
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    66
  app:          "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    68
  pi_ss:        "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    69
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    70
  lam_ss:       "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    71
                   ==> Abs(A, f) : Prod(A, B)"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    72
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    73
  beta:          "Abs(A, f)^a == f(a)"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    74
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    75
lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    76
lemmas rules = simple
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    77
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    78
lemma imp_elim:
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    79
  assumes "f:A->B" and "a:A" and "f^a:B ==> PROP P"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    80
  shows "PROP P" by (rule app prems)+
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    81
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    82
lemma pi_elim:
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    83
  assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) ==> PROP P"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    84
  shows "PROP P" by (rule app prems)+
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    85
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    86
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    87
locale L2 =
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    88
  assumes pi_bs: "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    89
    and lam_bs: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    90
                   ==> Abs(A,f) : Prod(A,B)"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    91
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    92
lemmas (in L2) rules = simple lam_bs pi_bs
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    93
17260
wenzelm
parents: 17252
diff changeset
    94
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    95
locale Lomega =
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    96
  assumes
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    97
    pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    98
    and lam_bb: "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
    99
                   ==> Abs(A,f) : Prod(A,B)"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   100
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   101
lemmas (in Lomega) rules = simple lam_bb pi_bb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   102
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   103
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   104
locale LP =
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   105
  assumes pi_sb: "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   106
    and lam_sb: "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   107
                   ==> Abs(A,f) : Prod(A,B)"
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   108
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   109
lemmas (in LP) rules = simple lam_sb pi_sb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   110
17260
wenzelm
parents: 17252
diff changeset
   111
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   112
locale LP2 = LP + L2
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   113
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   114
lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   115
17260
wenzelm
parents: 17252
diff changeset
   116
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   117
locale Lomega2 = L2 + Lomega
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   118
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   119
lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   120
17260
wenzelm
parents: 17252
diff changeset
   121
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   122
locale LPomega = LP + Lomega
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   123
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   124
lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   125
17260
wenzelm
parents: 17252
diff changeset
   126
17252
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   127
locale CC = L2 + LP + Lomega
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   128
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   129
lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   130
e352f65d5893 converted to Isar theory format;
wenzelm
parents: 11260
diff changeset
   131
end