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