213         apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)

   213         apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)

   214         by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)

   214         by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)

   215 

   215 

   216       have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"

   216       have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"

   217         apply (clarify, case_tac a) using os fin

   217         apply (clarify, case_tac a) using os fin

   219                    split:if_splits option.splits)

   219                    split:if_splits option.splits)

   220         done

   220         done

   221       moreover 

   221       moreover 

   222       have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" 

   222       have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" 

   223         apply (clarify, case_tac a)

   223         apply (clarify, case_tac a)

   224         using vt os pin'

   224         using vt os pin'

   226         apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)

   227         apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)

   229         done

   230         done

   230       moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"

   231       moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"

   231         apply (clarify, case_tac a)    

   232         apply (clarify, case_tac a)    

   233         apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps 

   234         apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps 

   234                          is_file_def is_dir_def 

   235                          is_file_def is_dir_def 

   235                     dest:ios's_im_in_cim iof's_im_in_cim

   236                     dest:ios's_im_in_cim iof's_im_in_cim

   237         apply (drule_tac f = f' and pf = list in pin', simp, simp)

   239         apply (drule_tac f = f' and pf = list in pin', simp, simp)

   238         apply (drule_tac f = f' and pf = list2 in pin', simp, simp)

   240         apply (drule_tac f = f' and pf = list2 in pin', simp, simp)

   239         done

   241         done

   240       moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> 

   242       moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> 

   241                                parent f' = Some f \<longrightarrow> False"

   243                                parent f' = Some f \<longrightarrow> False"

   368 

   370 

   369 lemma file_of_pfd_imp_inode_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" 

   371 lemma file_of_pfd_imp_inode_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" 

   370 apply (induct \<tau>)

   372 apply (induct \<tau>)

   371 apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum)

   373 apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum)

   372 apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a)

   374 apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a)

   374            split:if_splits option.splits)

   376            split:if_splits option.splits)

   375 apply (simp add:pfdof_simp3)+

   377 apply (simp add:pfdof_simp3)+

   376 apply (simp add:proc_fd_of_file_def)+  

   378 apply (simp add:proc_fd_of_file_def)+  

   377 done

   379 done

   378 

   380 

   494 by (auto simp:current_files_def inum_of_file.simps split:option.splits)

   496 by (auto simp:current_files_def inum_of_file.simps split:option.splits)

   495 

   497 

   496 lemma current_files_linkhard: 

   498 lemma current_files_linkhard: 

   497   "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"

   499   "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"

   498 apply (frule vt_grant_os, frule vd_cons)

   500 apply (frule vt_grant_os, frule vd_cons)

   500 

   502 

   501 (*

   503 (*

   502 lemma rename_renaming_decom:

   504 lemma rename_renaming_decom:

   503   "\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f"

   505   "\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f"

   504 apply (case_tac "f\<^isub>2 \<preceq> f", simp)

   506 apply (case_tac "f\<^isub>2 \<preceq> f", simp)