1(*  Title:      ZF/Coind/Values.thy
2    Author:     Jacob Frost, Cambridge University Computer Laboratory
3    Copyright   1995  University of Cambridge
4*)
5
6theory Values imports Language Map begin
7
8(* Values, values environments and associated operators *)
9
10consts
11  Val  :: i
12  ValEnv  :: i
13  Val_ValEnv  :: i
14
15codatatype
16    "Val" = v_const ("c \<in> Const")
17          | v_clos ("x \<in> ExVar","e \<in> Exp","ve \<in> ValEnv")
18  and
19    "ValEnv" = ve_mk ("m \<in> PMap(ExVar,Val)")
20  monos       PMap_mono
21  type_intros  A_into_univ mapQU
22
23consts
24  ve_owr :: "[i,i,i] => i"
25  ve_dom :: "i=>i"
26  ve_app :: "[i,i] => i"
27
28
29primrec "ve_owr(ve_mk(m), x, v) = ve_mk(map_owr(m,x,v))"
30
31primrec "ve_dom(ve_mk(m)) = domain(m)"
32
33primrec "ve_app(ve_mk(m), a) = map_app(m,a)"
34
35definition
36  ve_emp :: i  where
37   "ve_emp == ve_mk(map_emp)"
38
39
40(* Elimination rules *)
41
42lemma ValEnvE:
43  "[| ve \<in> ValEnv; !!m.[| ve=ve_mk(m); m \<in> PMap(ExVar,Val) |] ==> Q |] ==> Q"
44apply (unfold Part_def Val_def ValEnv_def, clarify) 
45apply (erule Val_ValEnv.cases) 
46apply (auto simp add: Val_def Part_def Val_ValEnv.con_defs)
47done
48
49lemma ValE:
50  "[| v \<in> Val;  
51      !!c. [| v = v_const(c); c \<in> Const |] ==> Q; 
52      !!e ve x.  
53        [| v = v_clos(x,e,ve); x \<in> ExVar; e \<in> Exp; ve \<in> ValEnv |] ==> Q  
54   |] ==>  
55   Q"
56apply (unfold Part_def Val_def ValEnv_def, clarify) 
57apply (erule Val_ValEnv.cases) 
58apply (auto simp add: ValEnv_def Part_def Val_ValEnv.con_defs)
59done
60
61(* Nonempty sets *)
62
63lemma v_closNE [simp]: "v_clos(x,e,ve) \<noteq> 0"
64by (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs, blast)
65
66declare v_closNE [THEN notE, elim!]
67
68
69lemma v_constNE [simp]: "c \<in> Const ==> v_const(c) \<noteq> 0"
70apply (unfold QPair_def QInl_def QInr_def Val_ValEnv.con_defs)
71apply (drule constNEE, auto)
72done
73
74
75(* Proving that the empty set is not a value *)
76
77lemma ValNEE: "v \<in> Val ==> v \<noteq> 0"
78by (erule ValE, auto)
79
80(* Equalities for value environments *)
81
82lemma ve_dom_owr [simp]:
83     "[| ve \<in> ValEnv; v \<noteq>0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) \<union> {x}"
84apply (erule ValEnvE)
85apply (auto simp add: map_domain_owr)
86done
87
88lemma ve_app_owr [simp]:
89     "ve \<in> ValEnv  
90      ==> ve_app(ve_owr(ve,y,v),x) = (if x=y then v else ve_app(ve,x))"
91by (erule ValEnvE, simp add: map_app_owr)
92
93(* Introduction rules for operators on value environments *)
94
95lemma ve_appI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> ve_app(ve,x):Val"
96by (erule ValEnvE, simp add: pmap_appI) 
97
98lemma ve_domI: "[| ve \<in> ValEnv; x \<in> ve_dom(ve) |] ==> x \<in> ExVar"
99apply (erule ValEnvE, simp) 
100apply (blast dest: pmap_domainD)
101done
102
103lemma ve_empI: "ve_emp \<in> ValEnv"
104apply (unfold ve_emp_def)
105apply (rule Val_ValEnv.intros)
106apply (rule pmap_empI)
107done
108
109lemma ve_owrI:
110     "[|ve \<in> ValEnv; x \<in> ExVar; v \<in> Val |] ==> ve_owr(ve,x,v):ValEnv"
111apply (erule ValEnvE, simp)
112apply (blast intro: pmap_owrI Val_ValEnv.intros)
113done
114
115end
116