src/ZF/Coind/Types.thy

--- a/src/ZF/Coind/Types.thy	Sat Dec 22 19:46:16 2001 +0100
+++ b/src/ZF/Coind/Types.thy	Tue Dec 25 10:02:01 2001 +0100
@@ -4,15 +4,15 @@
     Copyright   1995  University of Cambridge
 *)
 
-Types = Language +
+theory Types = Language:
 
 consts
-  Ty :: i                       (* Datatype of types *)
+  Ty :: i               (* Datatype of types *)
   TyConst :: i          (* Abstract type of type constants *)
 
 datatype
-  "Ty" = t_const ("tc \\<in> TyConst")
-       | t_fun ("t1 \\<in> Ty","t2 \\<in> Ty")
+  "Ty" = t_const ("tc \<in> TyConst")
+       | t_fun ("t1 \<in> Ty","t2 \<in> Ty")
   
 
 (* Definition of type environments and associated operators *)
@@ -22,24 +22,57 @@
 
 datatype
   "TyEnv" = te_emp
-          | te_owr ("te \\<in> TyEnv","x \\<in> ExVar","t \\<in> Ty") 
+          | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty") 
 
 consts
-  te_dom :: i => i
-  te_app :: [i,i] => i
+  te_dom :: "i => i"
+  te_app :: "[i,i] => i"
 
 
 primrec (*domain of the type environment*)
   "te_dom (te_emp) = 0"
-  "te_dom(te_owr(te,x,v)) = te_dom(te) Un {x}"
+  "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
 
 primrec (*lookup up identifiers in the type environment*)
   "te_app (te_emp,x) = 0"
   "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
 
-end
+inductive_cases te_owrE [elim!]: "te_owr(te,f,t) \<in> TyEnv"
+
+(*redundant??*)
+lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
+by simp
+
+(*redundant??*)
+lemma te_app_owr2: "x \<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)"
+by auto
+
+lemma te_app_owr [simp]:
+     "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
+by auto
+
+lemma te_appI:
+     "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty"
+apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp)
+apply (erule TyEnv.induct)
+apply auto
+done
 
 
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+end