92   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"

    92   "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"

    93 apply (drule has_same_inode_prop1')

    93 apply (drule has_same_inode_prop1')

    94 apply (simp add:file_of_pfd_is_file, simp+)

    94 apply (simp add:file_of_pfd_is_file, simp+)

    95 done

    95 done

    96 

    96 

    97 lemma tobj_in_init_alive:

    98 lemma tobj_in_init_alive:

    98   "tobj_in_init obj \<Longrightarrow> init_alive obj"

    99   "tobj_in_init obj \<Longrightarrow> init_alive obj"

    99 by (case_tac obj, auto)

   100 by (case_tac obj, auto)

   100 

   101 

   101 lemma tobj_in_alive:

   102 lemma tobj_in_alive:

   102   "tobj_in_init obj \<Longrightarrow> alive [] obj"

   103   "tobj_in_init obj \<Longrightarrow> alive [] obj"

   103 by (case_tac obj, auto simp:is_file_nil)

   104 by (case_tac obj, auto simp:is_file_nil)

   104 

   106 

   105 end

   107 end

   106 

   108 

   107 end

   109 end