1(* Title: ZF/Coind/Types.thy 2 Author: Jacob Frost, Cambridge University Computer Laboratory 3 Copyright 1995 University of Cambridge 4*) 5 6theory Types imports Language begin 7 8consts 9 Ty :: i (* Datatype of types *) 10 TyConst :: i (* Abstract type of type constants *) 11 12datatype 13 "Ty" = t_const ("tc \<in> TyConst") 14 | t_fun ("t1 \<in> Ty","t2 \<in> Ty") 15 16 17(* Definition of type environments and associated operators *) 18 19consts 20 TyEnv :: i 21 22datatype 23 "TyEnv" = te_emp 24 | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty") 25 26consts 27 te_dom :: "i => i" 28 te_app :: "[i,i] => i" 29 30 31primrec (*domain of the type environment*) 32 "te_dom (te_emp) = 0" 33 "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}" 34 35primrec (*lookup up identifiers in the type environment*) 36 "te_app (te_emp,x) = 0" 37 "te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))" 38 39inductive_cases te_owrE [elim!]: "te_owr(te,f,t) \<in> TyEnv" 40 41(*redundant??*) 42lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t" 43by simp 44 45(*redundant??*) 46lemma te_app_owr2: "x \<noteq> y ==> te_app(te_owr(te,x,t),y) = te_app(te,y)" 47by auto 48 49lemma te_app_owr [simp]: 50 "te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))" 51by auto 52 53lemma te_appI: 54 "[| te \<in> TyEnv; x \<in> ExVar; x \<in> te_dom(te) |] ==> te_app(te,x) \<in> Ty" 55apply (erule_tac P = "x \<in> te_dom (te) " in rev_mp) 56apply (erule TyEnv.induct, auto) 57done 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76end 77