src/Cube/cube.thy
author wenzelm
Tue, 06 May 1997 15:27:35 +0200
changeset 3118 24dae6222579
parent 21 b5f8677e24e7
permissions -rw-r--r--
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Cube/cube.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Barendregt's Lambda-Cube
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
Cube = Pure +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
types
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  term, context, typing 0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
arities
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  term :: logic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  Abs, Prod     :: "[term, term => term] => term"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
  Trueprop      :: "[context, typing] => prop"          ("(_/ |- _)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  Trueprop1     :: "typing => prop"                     ("(_)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  MT_context    :: "context"                            ("")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
  ""            :: "id => context"                      ("_ ")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
  ""            :: "var => context"                     ("_ ")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  Context       :: "[typing, context] => context"       ("_ _")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
  star          :: "term"                               ("*")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
  box           :: "term"                               ("[]")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
  "^"           :: "[term, term] => term"               (infixl 20)
21
b5f8677e24e7 replaced id by idt;
wenzelm
parents: 0
diff changeset
    28
  Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
b5f8677e24e7 replaced id by idt;
wenzelm
parents: 0
diff changeset
    29
  Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  "->"          :: "[term, term] => term"               (infixr 10)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  Has_type      :: "[term, term] => typing"             ("(_:/ _)" [0, 0] 5)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
translations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  (prop) "x:X"  == (prop) "|- x:X"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
  "Lam x:A. B"  == "Abs(A, %x. B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  "Pi x:A. B"   => "Prod(A, %x. B)"
21
b5f8677e24e7 replaced id by idt;
wenzelm
parents: 0
diff changeset
    37
  "A -> B"      => "Prod(A, _K(B))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  s_b           "*: []"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
  strip_s       "[| A:*;  a:A ==> G |- x:X |] ==> a:A G |- x:X"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
  strip_b       "[| A:[]; a:A ==> G |- x:X |] ==> a:A G |- x:X"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
  app           "[| F:Prod(A, B); C:A |] ==> F^C: B(C)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  pi_ss         "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  lam_ss        "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
\                   ==> Abs(A, f) : Prod(A, B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  beta          "Abs(A, f)^a == f(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
val print_translation = [("Prod", dependent_tr' ("Pi", "op ->"))];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60