src/ZF/Coind/Static.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6141 a6922171b396
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      ZF/Coind/Static.thy
lcp@916
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Jacob Frost, Cambridge University Computer Laboratory
lcp@916
     4
    Copyright   1995  University of Cambridge
lcp@916
     5
*)
lcp@916
     6
lcp@916
     7
Static = BCR +
lcp@916
     8
lcp@916
     9
consts
clasohm@1401
    10
  ElabRel :: i
lcp@916
    11
inductive
lcp@916
    12
  domains "ElabRel" <= "TyEnv * Exp * Ty"
lcp@916
    13
  intrs
lcp@916
    14
    elab_constI
clasohm@1155
    15
      " [| te:TyEnv; c:Const; t:Ty; isof(c,t) |] ==>   
clasohm@1155
    16
       <te,e_const(c),t>:ElabRel "
lcp@916
    17
    elab_varI
clasohm@1155
    18
      " [| te:TyEnv; x:ExVar; x:te_dom(te) |] ==>   
clasohm@1155
    19
       <te,e_var(x),te_app(te,x)>:ElabRel "
lcp@916
    20
    elab_fnI
clasohm@1155
    21
      " [| te:TyEnv; x:ExVar; e:Exp; t1:Ty; t2:Ty;   
clasohm@1155
    22
          <te_owr(te,x,t1),e,t2>:ElabRel |] ==>   
clasohm@1155
    23
       <te,e_fn(x,e),t_fun(t1,t2)>:ElabRel "
lcp@916
    24
    elab_fixI
clasohm@1155
    25
      " [| te:TyEnv; f:ExVar; x:ExVar; t1:Ty; t2:Ty;   
clasohm@1155
    26
          <te_owr(te_owr(te,f,t_fun(t1,t2)),x,t1),e,t2>:ElabRel |] ==>   
clasohm@1155
    27
       <te,e_fix(f,x,e),t_fun(t1,t2)>:ElabRel "
lcp@916
    28
    elab_appI
clasohm@1155
    29
      " [| te:TyEnv; e1:Exp; e2:Exp; t1:Ty; t2:Ty;   
clasohm@1155
    30
          <te,e1,t_fun(t1,t2)>:ElabRel;   
clasohm@1155
    31
          <te,e2,t1>:ElabRel |] ==>   
clasohm@1155
    32
       <te,e_app(e1,e2),t2>:ElabRel "
lcp@916
    33
  type_intrs "te_appI::Exp.intrs@Ty.intrs"
lcp@916
    34
lcp@916
    35
end
lcp@916
    36
  
lcp@916
    37
lcp@916
    38
lcp@916
    39
lcp@916
    40
lcp@916
    41
lcp@916
    42
lcp@916
    43
lcp@916
    44
lcp@916
    45
lcp@916
    46
lcp@916
    47
lcp@916
    48
lcp@916
    49
lcp@916
    50
lcp@916
    51
lcp@916
    52
lcp@916
    53
lcp@916
    54
lcp@916
    55
lcp@916
    56
lcp@916
    57