135 lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t\<noteq>a" |
135 lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t\<noteq>a" |
136 apply (unfold conf_def) |
136 apply (unfold conf_def) |
137 apply auto |
137 apply auto |
138 done |
138 done |
139 |
139 |
140 lemma conf_RefTD [rule_format (no_asm)]: |
140 lemma conf_RefTD [rule_format]: |
141 "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null | |
141 "G,h\<turnstile>a'::\<preceq>RefT T \<Longrightarrow> a' = Null \<or> |
142 (\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)" |
142 (\<exists>a obj T'. a' = Addr a \<and> h a = Some obj \<and> obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)" |
143 apply (unfold conf_def) |
143 unfolding conf_def by (induct a') auto |
144 apply(induct_tac "a'") |
|
145 apply(auto) |
|
146 done |
|
147 |
144 |
148 lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null" |
145 lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null" |
149 apply (drule conf_RefTD) |
146 apply (drule conf_RefTD) |
150 apply auto |
147 apply auto |
151 done |
148 done |
316 lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo" |
313 lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo" |
317 by (simp add: xconf_def preallocated_def hext_def) |
314 by (simp add: xconf_def preallocated_def hext_def) |
318 |
315 |
319 lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] |
316 lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] |
320 ==> (x,(h',l))::\<preceq>(G,lT)" |
317 ==> (x,(h',l))::\<preceq>(G,lT)" |
321 by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) |
318 by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext) |
322 |
319 |
323 |
320 |
324 lemma conforms_upd_obj: |
321 lemma conforms_upd_obj: |
325 "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] |
322 "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] |
326 ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |
323 ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)" |