src/ZF/Coind/ECR.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 6117 f9aad8ccd590
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/Coind/ECR.thy
     2     ID:         $Id$
     3     Author:     Jacob Frost, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 *)
     6 
     7 ECR = Static + Dynamic +
     8 
     9 (* The extended correspondence relation *)
    10 
    11 consts
    12   HasTyRel :: i
    13 coinductive
    14   domains "HasTyRel" <= "Val * Ty"
    15   intrs
    16     htr_constI
    17       "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
    18     htr_closI
    19       "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; 
    20           <te,e_fn(x,e),t>:ElabRel;  
    21           ve_dom(ve) = te_dom(te);   
    22           {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  
    23       |] ==>   
    24       <v_clos(x,e,ve),t>:HasTyRel" 
    25   monos "[Pow_mono]"
    26   type_intrs "Val_ValEnv.intrs"
    27   
    28 (* Pointwise extension to environments *)
    29  
    30 consts
    31   hastyenv :: [i,i] => o
    32 defs
    33   hastyenv_def 
    34     " hastyenv(ve,te) ==                        
    35      ve_dom(ve) = te_dom(te) &          
    36      (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
    37 
    38 end