src/HOL/Bali/TypeSafe.thy
changeset 15217 15fa818ef624
parent 15102 04b0e943fcc9
child 16417 9bc16273c2d4
equal deleted inserted replaced
15216:2fac1f11b7f6 15217:15fa818ef624
   261   wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   261   wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   262                         | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   262                         | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   263   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   263   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   264 apply (unfold init_obj_def)
   264 apply (unfold init_obj_def)
   265 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   265 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   266             simp add: obj.update_defs)
   266             )
   267 done
   267 done
   268 
   268 
   269 lemma conforms_init_class_obj: 
   269 lemma conforms_init_class_obj: 
   270  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   270  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   271   (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
   271   (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"