|
1 open Example; |
|
2 |
|
3 AddIs [widen.null]; |
|
4 |
|
5 Addsimps [inj_cnam_, inj_vnam_]; |
|
6 Addsimps [Base_not_Object,Ext_not_Object]; |
|
7 Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym]; |
|
8 |
|
9 val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"] |
|
10 "map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]); |
|
11 val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] |
|
12 "map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]); |
|
13 val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] |
|
14 "\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]); |
|
15 Delsimps[map_of_Cons]; (* sic! *) |
|
16 Addsimps[map_of_Cons1, map_of_Cons2]; |
|
17 |
|
18 val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def] |
|
19 "class tprg Object = Some (None, [], [])" |
|
20 (K [Simp_tac 1]); |
|
21 val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def, |
|
22 ExtC_def] "class tprg Base = Some (Some Object, \ |
|
23 \ [(vee, PrimT Boolean)], \ |
|
24 \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [ |
|
25 Simp_tac 1]); |
|
26 val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def, |
|
27 ExtC_def] "class tprg Ext = Some (Some Base, \ |
|
28 \ [(vee, PrimT Integer)], \ |
|
29 \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [ |
|
30 Simp_tac 1]); |
|
31 Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext]; |
|
32 |
|
33 Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R"; |
|
34 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset())); |
|
35 qed "not_Object_subcls"; |
|
36 AddSEs [not_Object_subcls]; |
|
37 |
|
38 Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object"; |
|
39 be rtrancl_induct 1; |
|
40 by Auto_tac; |
|
41 bd subcls1D 1; |
|
42 by Auto_tac; |
|
43 qed "subcls_ObjectD"; |
|
44 AddSDs[subcls_ObjectD]; |
|
45 |
|
46 Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R"; |
|
47 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset())); |
|
48 qed "not_Base_subcls_Ext"; |
|
49 AddSEs [not_Base_subcls_Ext]; |
|
50 |
|
51 Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext"; |
|
52 by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm])); |
|
53 qed "class_tprgD"; |
|
54 |
|
55 Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R"; |
|
56 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset())); |
|
57 by (ftac class_tprgD 1); |
|
58 by (auto_tac (claset() addSDs [],simpset())); |
|
59 bd rtranclD 1; |
|
60 by Auto_tac; |
|
61 qed "not_class_subcls_class"; |
|
62 AddSEs [not_class_subcls_class]; |
|
63 |
|
64 goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg"; |
|
65 by (Simp_tac 1); |
|
66 qed "unique_classes"; |
|
67 |
|
68 bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl); |
|
69 |
|
70 Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base"; |
|
71 br subcls_direct 1; |
|
72 by (Simp_tac 1); |
|
73 qed "Ext_subcls_Base"; |
|
74 Addsimps [Ext_subcls_Base]; |
|
75 |
|
76 Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base"; |
|
77 br widen.subcls 1; |
|
78 by (Simp_tac 1); |
|
79 qed "Ext_widen_Base"; |
|
80 Addsimps [Ext_widen_Base]; |
|
81 |
|
82 AddSIs ty_expr_ty_exprs_wt_stmt.intrs; |
|
83 |
|
84 |
|
85 Goal "acyclic (subcls1 tprg)"; |
|
86 br acyclicI 1; |
|
87 by Safe_tac ; |
|
88 qed "acyclic_subcls1_"; |
|
89 |
|
90 val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse); |
|
91 |
|
92 |
|
93 Addsimps[is_class_def]; |
|
94 |
|
95 val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma); |
|
96 |
|
97 Goal "fields (tprg, Object) = []"; |
|
98 by (stac fields_rec_ 1); |
|
99 by Auto_tac; |
|
100 qed "fields_Object"; |
|
101 Addsimps [fields_Object]; |
|
102 |
|
103 Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"; |
|
104 by (stac fields_rec_ 1); |
|
105 by Auto_tac; |
|
106 qed "fields_Base"; |
|
107 Addsimps [fields_Base]; |
|
108 |
|
109 Goal "fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @\ |
|
110 \ fields (tprg, Base)"; |
|
111 br trans 1; |
|
112 br fields_rec_ 1; |
|
113 by Auto_tac; |
|
114 qed "fields_Ext"; |
|
115 Addsimps [fields_Ext]; |
|
116 |
|
117 val method_rec_ = wf_subcls1_ RS method_rec_lemma; |
|
118 |
|
119 Goal "method (tprg,Object) = map_of []"; |
|
120 by (stac method_rec_ 1); |
|
121 by Auto_tac; |
|
122 qed "method_Object"; |
|
123 Addsimps [method_Object]; |
|
124 |
|
125 Goal "method (tprg, Base) = map_of \ |
|
126 \ [((foo, [Class Base]), Base, (Class Base, foo_Base))]"; |
|
127 br trans 1; |
|
128 br method_rec_ 1; |
|
129 by Auto_tac; |
|
130 qed "method_Base"; |
|
131 Addsimps [method_Base]; |
|
132 |
|
133 Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \ |
|
134 \ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"; |
|
135 br trans 1; |
|
136 br method_rec_ 1; |
|
137 by Auto_tac; |
|
138 qed "method_Ext"; |
|
139 Addsimps [method_Ext]; |
|
140 |
|
141 Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def] |
|
142 "wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"; |
|
143 by Auto_tac; |
|
144 qed "wf_foo_Base"; |
|
145 |
|
146 Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def] |
|
147 "wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"; |
|
148 by Auto_tac; |
|
149 br ty_expr_ty_exprs_wt_stmt.Cast 1; |
|
150 by (Simp_tac 2); |
|
151 br cast.subcls 2; |
|
152 by (rewtac field_def); |
|
153 by Auto_tac; |
|
154 qed "wf_foo_Ext"; |
|
155 |
|
156 Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def] |
|
157 "wf_cdecl wf_java_mdecl tprg ObjectC"; |
|
158 by (Simp_tac 1); |
|
159 qed "wf_ObjectC"; |
|
160 |
|
161 Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def] |
|
162 "wf_cdecl wf_java_mdecl tprg BaseC"; |
|
163 by (Simp_tac 1); |
|
164 by (fold_goals_tac [BaseC_def]); |
|
165 br (wf_foo_Base RS conjI) 1; |
|
166 by Auto_tac; |
|
167 qed "wf_BaseC"; |
|
168 |
|
169 Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def] |
|
170 "wf_cdecl wf_java_mdecl tprg ExtC"; |
|
171 by (Simp_tac 1); |
|
172 by (fold_goals_tac [ExtC_def]); |
|
173 br (wf_foo_Ext RS conjI) 1; |
|
174 by Auto_tac; |
|
175 bd rtranclD 1; |
|
176 by Auto_tac; |
|
177 qed "wf_ExtC"; |
|
178 |
|
179 Goalw [wf_prog_def,Let_def] |
|
180 "wf_prog wf_java_mdecl tprg"; |
|
181 by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1); |
|
182 qed "wf_tprg"; |
|
183 |
|
184 Goalw [appl_methds_def] |
|
185 "appl_methds tprg Base (foo, [NT]) = \ |
|
186 \ {((Class Base, Class Base), [Class Base])}"; |
|
187 by (Simp_tac 1); |
|
188 by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1); |
|
189 by (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def])); |
|
190 qed "appl_methds_foo_Base"; |
|
191 |
|
192 Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \ |
|
193 \ {((Class Base, Class Base), [Class Base])}"; |
|
194 by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base])); |
|
195 qed "max_spec_foo_Base"; |
|
196 |
|
197 fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm; |
|
198 Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ |
|
199 \ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>"; |
|
200 (* ?pTs' = [Class Base] *) |
|
201 by t; (* ;; *) |
|
202 by t; (* Expr *) |
|
203 by t; (* LAss *) |
|
204 by t; (* LAcc *) |
|
205 by (Simp_tac 1); |
|
206 by (Simp_tac 1); |
|
207 by t; (* NewC *) |
|
208 by (Simp_tac 1); |
|
209 by (Simp_tac 1); |
|
210 by t; (* Expr *) |
|
211 by t; (* Call *) |
|
212 by t; (* LAcc *) |
|
213 by (Simp_tac 1); |
|
214 by (Simp_tac 1); |
|
215 by t; (* Cons *) |
|
216 by t; (* Lit *) |
|
217 by (Simp_tac 1); |
|
218 by t; (* Nil *) |
|
219 by (Simp_tac 1); |
|
220 br max_spec_foo_Base 1; |
|
221 qed "wt_test"; |
|
222 |
|
223 fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm; |
|
224 |
|
225 Delsplits[split_if]; |
|
226 Addsimps[init_vars_def,c_hupd_def,cast_ok_def]; |
|
227 Goalw [test_def] |
|
228 " \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \ |
|
229 \ tprg\\<turnstile>s0 -test\\<rightarrow> ?s"; |
|
230 (* ?s = s3 *) |
|
231 by e; (* ;; *) |
|
232 by e; (* Expr *) |
|
233 by e; (* LAss *) |
|
234 by e; (* NewC *) |
|
235 by (Force_tac 1); |
|
236 by (Force_tac 1); |
|
237 by (Simp_tac 1); |
|
238 be thin_rl 1; |
|
239 by e; (* Expr *) |
|
240 by e; (* Call *) |
|
241 by e; (* LAcc *) |
|
242 by (Force_tac 1); |
|
243 by e; (* Cons *) |
|
244 by e; (* Lit *) |
|
245 by e; (* Nil *) |
|
246 by (Simp_tac 1); |
|
247 by (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1); |
|
248 by (Simp_tac 1); |
|
249 by e; (* Expr *) |
|
250 by e; (* FAss *) |
|
251 by e;(* Cast *) |
|
252 by e;(* LAcc *) |
|
253 by (Simp_tac 1); |
|
254 by (Simp_tac 1); |
|
255 by (Simp_tac 1); |
|
256 by e;(* XcptE *) |
|
257 by (Simp_tac 1); |
|
258 by (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq, |
|
259 Force_tac] 1); |
|
260 by (Simp_tac 1); |
|
261 by (Simp_tac 1); |
|
262 by e; (* XcptE *) |
|
263 qed "exec_test"; |