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