231 |
231 |
232 |
232 |
233 (** hconf **) |
233 (** hconf **) |
234 |
234 |
235 |
235 |
236 Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>"; |
236 Goal "hp x = None \\<longrightarrow> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G\\<turnstile>h hp(newref hp\\<mapsto>obj)\\<surd>"; |
237 by (asm_full_simp_tac (simpset() addsplits [split_split] |
237 by (asm_full_simp_tac (simpset() addsplits [split_split] |
238 addsimps [hconf_def]) 1); |
238 addsimps [hconf_def]) 1); |
239 by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1); |
239 by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1); |
240 qed_spec_mp "hconf_imp_hconf_newref"; |
240 qed_spec_mp "hconf_imp_hconf_newref"; |
241 |
241 |
242 |
242 |
243 Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \ |
243 Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \ |
244 \ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>"; |
244 \ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G\\<turnstile>h hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<surd>"; |
245 by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1); |
245 by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1); |
246 by (fast_tac (claset() addIs |
246 by (fast_tac (claset() addIs |
247 [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update] |
247 [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update] |
248 addss (simpset() addsimps [obj_ty_def])) 1); |
248 addss (simpset() addsimps [obj_ty_def])) 1); |
249 qed_spec_mp "hconf_imp_hconf_field_update"; |
249 qed_spec_mp "hconf_imp_hconf_field_update"; |