|
1 (* Title: ZF/Coind/Values.ML |
|
2 ID: $Id$ |
|
3 Author: Jacob Frost, Cambridge University Computer Laboratory |
|
4 Copyright 1995 University of Cambridge |
|
5 *) |
|
6 |
|
7 open Values; |
|
8 |
|
9 (* Elimination rules *) |
|
10 |
|
11 val prems = goalw Values.thy (Part_def::(tl (tl Val_ValEnv.defs))) |
|
12 "[| ve:ValEnv; !!m.[| ve=ve_mk(m); m:PMap(ExVar,Val) |] ==> Q |] ==> Q"; |
|
13 by (cut_facts_tac prems 1); |
|
14 by (etac CollectE 1); |
|
15 by (etac exE 1); |
|
16 by (etac Val_ValEnv.elim 1); |
|
17 by (eresolve_tac prems 3); |
|
18 by (rewrite_tac Val_ValEnv.con_defs); |
|
19 by (ALLGOALS (fast_tac qsum_cs)); |
|
20 qed "ValEnvE"; |
|
21 |
|
22 val prems = goalw Values.thy (Part_def::[hd (tl Val_ValEnv.defs)]) |
|
23 "[| v:Val; \ |
|
24 \ !!c. [| v = v_const(c); c:Const |] ==> Q;\ |
|
25 \ !!e ve x. \ |
|
26 \ [| v = v_clos(x,e,ve); x:ExVar; e:Exp; ve:ValEnv |] ==> Q \ |
|
27 \ |] ==> \ |
|
28 \ Q"; |
|
29 by (cut_facts_tac prems 1); |
|
30 by (etac CollectE 1); |
|
31 by (etac exE 1); |
|
32 by (etac Val_ValEnv.elim 1); |
|
33 by (eresolve_tac prems 1); |
|
34 by (assume_tac 1); |
|
35 by (eresolve_tac prems 1); |
|
36 by (assume_tac 1); |
|
37 by (assume_tac 1); |
|
38 by (assume_tac 1); |
|
39 by (rewrite_tac Val_ValEnv.con_defs); |
|
40 by (fast_tac qsum_cs 1); |
|
41 qed "ValE"; |
|
42 |
|
43 (* Nonempty sets *) |
|
44 |
|
45 val prems = goal Values.thy "A ~= 0 ==> EX a.a:A"; |
|
46 by (cut_facts_tac prems 1); |
|
47 by (rtac (foundation RS disjE) 1); |
|
48 by (fast_tac ZF_cs 1); |
|
49 by (fast_tac ZF_cs 1); |
|
50 qed "set_notemptyE"; |
|
51 |
|
52 goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs) |
|
53 "v_clos(x,e,ve) ~= 0"; |
|
54 by (rtac not_emptyI 1); |
|
55 by (rtac UnI2 1); |
|
56 by (rtac SigmaI 1); |
|
57 by (rtac singletonI 1); |
|
58 by (rtac UnI1 1); |
|
59 by (fast_tac ZF_cs 1); |
|
60 qed "v_closNE"; |
|
61 |
|
62 goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs) |
|
63 "!!c.c:Const ==> v_const(c) ~= 0"; |
|
64 by (dtac constNEE 1); |
|
65 by (etac not_emptyE 1); |
|
66 by (rtac not_emptyI 1); |
|
67 by (rtac UnI2 1); |
|
68 by (rtac SigmaI 1); |
|
69 by (rtac singletonI 1); |
|
70 by (rtac UnI2 1); |
|
71 by (rtac SigmaI 1); |
|
72 by (rtac singletonI 1); |
|
73 by (assume_tac 1); |
|
74 qed "v_constNE"; |
|
75 |
|
76 (* Proving that the empty set is not a value *) |
|
77 |
|
78 goal Values.thy "!!v.v:Val ==> v ~= 0"; |
|
79 by (etac ValE 1); |
|
80 by (ALLGOALS hyp_subst_tac); |
|
81 by (etac v_constNE 1); |
|
82 by (rtac v_closNE 1); |
|
83 qed "ValNEE"; |
|
84 |
|
85 (* Equalities for value environments *) |
|
86 |
|
87 val prems = goalw Values.thy [ve_dom_def,ve_owr_def] |
|
88 "[| ve:ValEnv; v ~=0 |] ==> ve_dom(ve_owr(ve,x,v)) = ve_dom(ve) Un {x}"; |
|
89 by (cut_facts_tac prems 1); |
|
90 by (etac ValEnvE 1); |
|
91 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
92 by (rtac (map_domain_owr RS ssubst) 1); |
|
93 by (assume_tac 1); |
|
94 by (rtac Un_commute 1); |
|
95 qed "ve_dom_owr"; |
|
96 |
|
97 goalw Values.thy [ve_app_def,ve_owr_def] |
|
98 "!!ve. ve:ValEnv ==> ve_app(ve_owr(ve,x,v),x) = v"; |
|
99 by (etac ValEnvE 1); |
|
100 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
101 by (rtac map_app_owr1 1); |
|
102 qed "ve_app_owr1"; |
|
103 |
|
104 goalw Values.thy [ve_app_def,ve_owr_def] |
|
105 "!!ve.ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)"; |
|
106 by (etac ValEnvE 1); |
|
107 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
108 by (rtac map_app_owr2 1); |
|
109 by (fast_tac ZF_cs 1); |
|
110 qed "ve_app_owr2"; |
|
111 |
|
112 (* Introduction rules for operators on value environments *) |
|
113 |
|
114 goalw Values.thy [ve_app_def,ve_owr_def,ve_dom_def] |
|
115 "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> ve_app(ve,x):Val"; |
|
116 by (etac ValEnvE 1); |
|
117 by (hyp_subst_tac 1); |
|
118 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
119 by (rtac pmap_appI 1); |
|
120 by (assume_tac 1); |
|
121 by (assume_tac 1); |
|
122 qed "ve_appI"; |
|
123 |
|
124 goalw Values.thy [ve_dom_def] |
|
125 "!!ve.[| ve:ValEnv; x:ve_dom(ve) |] ==> x:ExVar"; |
|
126 by (etac ValEnvE 1); |
|
127 by (hyp_subst_tac 1); |
|
128 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
129 by (rtac pmap_domainD 1); |
|
130 by (assume_tac 1); |
|
131 by (assume_tac 1); |
|
132 qed "ve_domI"; |
|
133 |
|
134 goalw Values.thy [ve_emp_def] "ve_emp:ValEnv"; |
|
135 by (rtac Val_ValEnv.ve_mk_I 1); |
|
136 by (rtac pmap_empI 1); |
|
137 qed "ve_empI"; |
|
138 |
|
139 goalw Values.thy [ve_owr_def] |
|
140 "!!ve.[|ve:ValEnv; x:ExVar; v:Val |] ==> ve_owr(ve,x,v):ValEnv"; |
|
141 by (etac ValEnvE 1); |
|
142 by (hyp_subst_tac 1); |
|
143 by (asm_full_simp_tac (ZF_ss addsimps Val_ValEnv.case_eqns) 1); |
|
144 by (rtac Val_ValEnv.ve_mk_I 1); |
|
145 by (etac pmap_owrI 1); |
|
146 by (assume_tac 1); |
|
147 by (assume_tac 1); |
|
148 qed "ve_owrI"; |
|
149 |
|
150 |
|
151 |