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