src/ZF/Coind/ECR.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Coind/ECR.thy	Mon Feb 27 18:12:21 1995 +0100
@@ -0,0 +1,38 @@
+(*  Title: 	ZF/Coind/ECR.thy
+    ID:         $Id$
+    Author: 	Jacob Frost, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+*)
+
+ECR = Static + Dynamic +
+
+(* The extended correspondence relation *)
+
+consts
+  HasTyRel :: "i"
+coinductive
+  domains "HasTyRel" <= "Val * Ty"
+  intrs
+    htr_constI
+      "[| c:Const; t:Ty; isof(c,t) |] ==> <v_const(c),t>:HasTyRel"
+    htr_closI
+      "[| x:ExVar; e:Exp; t:Ty; ve:ValEnv; te:TyEnv; \
+\	  <te,e_fn(x,e),t>:ElabRel;  \
+\	  ve_dom(ve) = te_dom(te);   \
+\	  {<ve_app(ve,y),te_app(te,y)>.y:ve_dom(ve)}:Pow(HasTyRel)  \
+\      |] ==>   \
+\      <v_clos(x,e,ve),t>:HasTyRel" 
+  monos "[Pow_mono]"
+  type_intrs "Val_ValEnv.intrs"
+  
+(* Pointwise extension to environments *)
+ 
+consts
+  hastyenv :: "[i,i] => o"
+rules
+  hastyenv_def 
+    " hastyenv(ve,te) == \
+\     ve_dom(ve) = te_dom(te) & \
+\     (ALL x:ve_dom(ve). <ve_app(ve,x),te_app(te,x)>:HasTyRel)"
+
+end