--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Current_files_prop.thy Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,736 @@
+(*<*)
+theory Current_files_prop
+imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop
+begin
+(*<*)
+
+context init begin
+
+lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None"
+by (simp add:current_files_def)
+
+(************** file_of_proc_fd vs proc_fd_of_file *****************)
+lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f"
+by (simp add:proc_fd_of_file_def)
+
+lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
+by (simp add:proc_fd_of_file_def)
+
+lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')"
+by (simp add:proc_fd_of_file_def, auto)
+
+lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd"
+by (drule pfdof_simp3, auto)
+
+end
+
+context flask begin
+
+(***************** inode number lemmas *************************)
+
+lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+by (auto simp add:current_inode_nums_def current_file_inums_def)
+
+lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def)
+
+lemma fim_noninter_sim_aux[rule_format]:
+ "\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps)
+apply (drule init_inum_sock_file_noninter, simp, simp)
+apply ((rule allI|rule impI|erule conjE)+)
+apply (frule vd_cons, frule vt_grant_os, simp, case_tac a)
+apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits
+ dest:ios's_im_in_cim iof's_im_in_cim)
+done
+
+lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (auto intro:fim_noninter_sim_aux)
+
+lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (auto intro:fim_noninter_sim_aux)
+
+lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}"
+by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format])
+
+(******************* file inum has inode tag ************************)
+
+lemma finum_has_itag_aux[rule_format]:
+ "\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
+apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def
+ dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits)
+done
+
+lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
+by (auto dest:conjI[THEN finum_has_itag_aux])
+
+(*********************** file inum is file itag *************************)
+
+lemma finum_has_ftag_aux[rule_format]:
+ "\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
+apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps
+ split:if_splits option.splits t_socket_type.splits
+ dest:ios's_im_in_cim iof's_im_in_cim)
+done
+
+lemma finum_has_ftag:
+ "\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"
+by (auto intro:finum_has_ftag_aux)
+
+lemma finum_has_ftag':
+ "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR"
+apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+)
+apply (case_tac tag, auto)
+done
+
+(******************* sock inum has inode tag ************************)
+
+lemma sinum_has_itag_aux[rule_format]:
+ "\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
+apply (drule init_inumos_prop4, clarsimp)
+apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
+ dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
+ split:option.splits if_splits t_socket_type.splits)
+done
+
+lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
+by (auto dest:conjI[THEN sinum_has_itag_aux])
+
+(********************** socket inum is socket itag **********************)
+
+lemma sinum_has_stag_aux[rule_format]:
+ "\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
+apply (drule init_inumos_prop4, clarsimp)
+apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
+ dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
+ split:option.splits if_splits t_socket_type.splits)
+done
+
+lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag"
+by (auto dest:conjI[THEN sinum_has_stag_aux])
+
+lemma sinum_has_stag':
+ "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk>
+ \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK"
+apply (frule sinum_has_itag, simp, erule exE)
+apply (drule sinum_has_stag, simp+, case_tac tag, simp+)
+done
+
+(************************************ 4 in 1 *************************************)
+
+lemma file_leveling: "valid \<tau> \<longrightarrow> (
+ (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
+ (\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
+ (\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
+ (\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )"
+proof (induct \<tau>)
+ case Nil
+ show ?case
+ apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits)
+ apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum)
+ apply (rule init_parent_file_has_inum, simp+)
+ apply (rule init_file_has_no_son', simp+)
+ apply (rule init_file_hung_has_no_son, simp+)
+ done
+next
+ case (Cons a \<tau>)
+ assume pre: "valid \<tau> \<longrightarrow>
+ (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
+ (\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
+ (\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
+ (\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
+ show ?case
+ proof
+ assume cons:"valid (a # \<tau>)"
+ show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and>
+ (\<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) \<and>
+ (\<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) \<and>
+ (\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
+ proof-
+ have vt: "valid \<tau>" using cons by (auto dest:vd_cons)
+ have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os)
+ have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto
+ have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None"
+ using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False"
+ using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False"
+ using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ proof
+ fix f'
+ show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ proof (induct f')
+ case Nil show ?case by (auto simp: no_junior_def)
+ next
+ case (Cons a f')
+ assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ proof clarify
+ fix f im
+ assume h1: "f \<preceq> a # f'"
+ and h2: "inum_of_file \<tau> (a # f') = Some im"
+ show "\<exists>y. inum_of_file \<tau> f = Some y"
+ proof-
+ have h3: "\<exists> y. inum_of_file \<tau> f' = Some y"
+ proof-
+ have "parent (a # f') = Some f'" by simp
+ hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast
+ with h1 show ?thesis by simp
+ qed
+ from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
+ moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
+ moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h3 by simp
+ moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp
+ ultimately show ?thesis by auto
+ qed
+ qed
+ qed
+ qed
+
+ have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto
+ have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
+ using pin by auto
+ have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto
+ have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False"
+ by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def)
+ have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto
+ have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto
+ have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False"
+ apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)
+ by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)
+
+ have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"
+ apply (clarify, case_tac a) using os fin
+ apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def
+ split:if_splits option.splits)
+ done
+ moreover
+ 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"
+ apply (clarify, case_tac a)
+ using vt os pin'
+ apply (auto simp:os_grant.simps current_files_def inum_of_file.simps split:if_splits option.splits)
+ apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)
+ apply (drule_tac f = list and f' = f in fns', simp, simp, simp)
+ apply (drule_tac f = list and f' = f in dns', simp, simp, simp)
+ done
+ 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"
+ apply (clarify, case_tac a)
+ using vt os fns''
+ apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps
+ is_file_def is_dir_def
+ dest:ios's_im_in_cim iof's_im_in_cim
+ split:if_splits option.splits t_inode_tag.splits t_socket_type.splits)
+ apply (drule_tac f = f' and pf = list in pin', simp, simp)
+ apply (drule_tac f = f' and pf = list2 in pin', simp, simp)
+ done
+ moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and>
+ parent f' = Some f \<longrightarrow> False"
+ apply (clarify, case_tac a)
+ using vt os hns'
+ apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps
+ split:if_splits option.splits t_sock_addr.splits)
+ apply (drule fns', simp+)
+ done
+ ultimately show ?thesis by blast
+ qed
+ qed
+qed
+
+(**************** hung file in current ***********************)
+
+lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+by (drule file_leveling[rule_format], blast)
+
+lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
+by (auto dest:hung_file_has_inum)
+
+lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (clarsimp simp add:current_files_def hung_file_has_inum')
+
+lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None"
+by (drule file_leveling[rule_format], blast)
+
+lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
+by (auto dest:parentf_has_inum)
+
+lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
+by (clarsimp simp add:current_files_def parentf_has_inum')
+
+lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
+apply (subgoal_tac "parent (a # pf) = Some pf")
+by (erule parentf_in_current, simp+)
+
+lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+proof (induct f')
+ case Nil show ?case by (auto simp: no_junior_def)
+next
+ case (Cons a f')
+ assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ proof clarify
+ fix f im
+ assume h1: "f \<preceq> a # f'"
+ and h2: "inum_of_file \<tau> (a # f') = Some im"
+ and h3: "valid \<tau>"
+ show "\<exists>y. inum_of_file \<tau> f = Some y"
+ proof-
+ have h4: "\<exists> y. inum_of_file \<tau> f' = Some y"
+ proof-
+ have "parent (a # f') = Some f'" by simp
+ hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast
+ with h1 show ?thesis by simp
+ qed
+ from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
+ moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
+ moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp
+ moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp
+ ultimately show ?thesis by auto
+ qed
+ qed
+qed
+
+lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+by (rule ancenf_has_inum_aux[rule_format], auto)
+
+lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'"
+by (auto dest:ancenf_has_inum)
+
+lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum')
+
+lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule file_leveling[rule_format], blast)
+
+lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (simp add:current_files_def, erule exE, auto intro:file_has_no_son)
+
+lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
+by (drule file_leveling[rule_format], blast)
+
+lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
+by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son)
+
+lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False"
+proof (induct f')
+ case Nil
+ show ?case
+ by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits)
+next
+ case (Cons a pf)
+ assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False"
+ show ?case
+ proof clarify
+ fix f
+ assume h1: "f \<in> files_hung_by_del \<tau>"
+ and h2: "valid \<tau>"
+ and h3: "a # pf \<in> current_files \<tau>"
+ and h4: "f \<preceq> a # pf"
+ and h5: "f \<noteq> a # pf"
+ have h6: "parent (a # pf) = Some pf" by simp
+ with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
+ from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
+ show False
+ proof (cases "f = pf")
+ case True with h6 h2 h3 h1
+ show False by (auto intro!:hung_file_no_son')
+ next
+ case False with pre h1 h2 h7 h8
+ show False by blast
+ qed
+ qed
+qed
+
+lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False"
+by (rule hung_file_no_des_aux[rule_format], blast)
+
+lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f"
+apply (frule hung_file_has_inum', simp, erule exE)
+apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits)
+by (simp add: noJ_Anc, auto dest:hung_file_no_des)
+
+
+
+(************** file_of_proc_fd in current ********************)
+
+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"
+apply (induct \<tau>)
+apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum)
+apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def
+ split:if_splits option.splits)
+apply (simp add:pfdof_simp3)+
+apply (simp add:proc_fd_of_file_def)+
+done
+
+lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+by (rule file_of_pfd_imp_inode_aux[rule_format], blast)
+
+lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
+by (auto dest!:file_of_pfd_imp_inode')
+
+lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def)
+
+
+(*************** file_of_proc_fd is file *********************)
+
+lemma file_of_pfd_is_file_tag:
+ "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE"
+apply (induct \<tau> arbitrary:p, simp)
+apply (drule init_filefd_prop5, simp add:is_init_file_def split:option.splits t_inode_tag.splits)
+apply (frule vd_cons, frule vt_grant_os, simp, case_tac a)
+by (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits
+ dest:file_of_pfd_imp_inode' iof's_im_in_cim
+ simp:is_file_def is_dir_def dir_is_empty_def current_files_def)
+
+lemma file_of_pfd_is_file:
+ "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"
+apply (frule file_of_pfd_imp_inode, simp, erule exE)
+apply (drule file_of_pfd_is_file_tag, simp+)
+by (simp add:is_file_def)
+
+lemma file_of_pfd_is_file':
+ "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
+
+(************** parent file / ancestral file is dir *******************)
+
+lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
+apply (induct \<tau>)
+apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir')
+apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps
+ current_files_def is_dir_def is_file_def
+ dest: ios's_im_in_cim iof's_im_in_cim
+ split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits)
+apply (drule parentf_has_inum', simp, simp, simp)+
+done
+
+lemma parentf_has_dirtag:
+ "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk>
+ \<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
+by (auto intro:parentf_is_dir_aux[rule_format])
+
+lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits)
+by (auto dest:parentf_has_dirtag)
+
+lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+by (clarsimp simp:current_files_def parentf_is_dir')
+
+lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
+proof (induct f')
+ case Nil show ?case
+ by (auto simp:current_files_def no_junior_def)
+next
+ case (Cons a pf)
+ assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
+ show ?case
+ proof clarify
+ fix f
+ assume h1: "f \<preceq> a # pf"
+ and h2: "f \<noteq> a # pf"
+ and h3: "a # pf \<in> current_files \<tau>"
+ and h4: "valid \<tau>"
+ have h5: "parent (a # pf) = Some pf" by simp
+ with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
+ from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
+ show "is_dir \<tau> f"
+ proof (cases "f = pf")
+ case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto)
+ next
+ case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast
+ qed
+ qed
+qed
+
+lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f"
+by (auto intro:ancenf_is_dir_aux[rule_format])
+
+(************* rebuild current_files simpset ***********************)
+
+lemma current_files_nil: "current_files [] = init_files"
+apply (simp add:current_files_def inum_of_file.simps)
+by (auto dest:inof_has_file_tag init_file_has_inum)
+
+lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)"
+by (auto simp add:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>"
+by (simp add:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = (
+ case (file_of_proc_fd \<tau> p fd) of
+ Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>))
+ then current_files \<tau> - {f}
+ else current_files \<tau>)
+ | _ \<Rightarrow> current_files \<tau> )"
+by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)"
+by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then current_files \<tau> - {f} else current_files \<tau>)"
+by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)"
+by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+
+lemma current_files_linkhard:
+ "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>)"
+apply (frule vt_grant_os, frule vd_cons)
+by (auto simp:current_files_def inum_of_file.simps os_grant.simps split:option.splits)
+
+(*
+lemma rename_renaming_decom:
+ "\<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"
+apply (case_tac "f\<^isub>2 \<preceq> f", simp)
+apply (simp add:file_after_rename_def split:if_splits)
+by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current)
+
+lemma rename_renaming_decom':
+ "\<lbrakk>\<not> 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> \<not> f\<^isub>2 \<preceq> f"
+by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+)
+
+lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}"
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits)
+apply (rule_tac x = x in exI, simp add:file_after_rename_def)
+apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5')
+apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp)
+apply (rule_tac x = x in exI, simp add:file_after_rename_def)
+apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp)
+apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp)
+apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5)
+apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
+apply (simp add:file_after_rename_def)
+apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
+apply (simp add:file_after_rename_def)
+done
+*)
+
+lemma current_files_other:
+ "\<lbrakk>\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p f. e \<noteq> UnLink p f;
+ \<forall> p f. e \<noteq> Rmdir p f;
+ \<forall> p f i. e \<noteq> Mkdir p f i;
+ \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>"
+by (case_tac e, auto simp:current_files_def inum_of_file.simps)
+
+lemmas current_files_simps = current_files_nil current_files_open current_files_open'
+ current_files_closefd current_files_unlink current_files_rmdir
+ current_files_mkdir current_files_linkhard current_files_other
+
+
+(******************** is_file simpset *********************)
+
+lemma is_file_nil: "is_file [] = is_init_file"
+by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
+
+lemma is_file_open:
+ "valid (Open p f flags fd opt # s) \<Longrightarrow>
+ is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))"
+apply (frule vd_cons, drule vt_grant_os, rule ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim
+ split:if_splits option.splits t_inode_tag.splits
+ simp:is_file_def current_files_def)
+done
+
+lemma is_file_closefd:
+ "valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = (
+ case (file_of_proc_fd s p fd) of
+ Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
+ then (is_file s) (f := False)
+ else is_file s)
+ | _ \<Rightarrow> is_file s )"
+apply (frule vd_cons, drule vt_grant_os, rule ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim
+ split:if_splits option.splits t_inode_tag.splits
+ simp:is_file_def)
+done
+
+lemma is_file_unlink:
+ "valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = (
+ if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)"
+apply (frule vd_cons, drule vt_grant_os, rule ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim
+ split:if_splits option.splits t_inode_tag.splits
+ simp:is_file_def)
+done
+
+lemma is_file_linkhard:
+ "valid (LinkHard p f f' # s) \<Longrightarrow> is_file (LinkHard p f f' # s) = (is_file s) (f' := True)"
+apply (frule vd_cons, drule vt_grant_os, rule ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim
+ split:if_splits option.splits t_inode_tag.splits
+ simp:is_file_def)
+done
+
+lemma is_file_other:
+ "\<lbrakk>valid (e # \<tau>);
+ \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p f. e \<noteq> UnLink p f;
+ \<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> is_file (e # \<tau>) = is_file \<tau>"
+apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
+apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
+done
+
+lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False"
+by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
+
+lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f"
+by (rule notI, erule file_dir_conflict, simp)
+
+lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f"
+by (rule notI, erule file_dir_conflict, simp)
+
+lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other
+
+(********* is_dir simpset **********)
+
+lemma is_dir_nil: "is_dir [] = is_init_dir"
+by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
+
+lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)"
+apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
+done
+
+lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)"
+apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
+apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
+apply (drule pfdof_simp2)
+apply (drule file_of_pfd_is_file, simp)
+apply (simp add:is_file_def split:t_inode_tag.splits option.splits)
+done
+
+lemma is_dir_other:
+ "\<lbrakk>valid (e # s);
+ \<forall> p f. e \<noteq> Rmdir p f;
+ \<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s"
+apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
+apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
+apply (drule file_of_pfd_is_file, simp)
+apply (simp add:is_file_def split:t_inode_tag.splits option.splits)
+done
+
+lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other
+
+(*********** no root dir involved ***********)
+
+lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []"
+apply (induct s, simp add:is_dir_nil root_is_init_dir)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto simp:is_dir_simps)
+done
+
+lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False"
+apply (drule root_is_dir)
+apply (erule file_dir_conflict, simp)
+done
+
+lemma noroot_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_execve':
+ "valid (Execve p [] fds # s) \<Longrightarrow> False"
+by (drule noroot_execve, simp)
+
+lemma noroot_open:
+ "valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits)
+
+lemma noroot_open':
+ "valid (Open p [] flags fd opt # s) \<Longrightarrow> False"
+by (drule noroot_open, simp)
+
+lemma noroot_filefd':
+ "\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s arbitrary:p, simp)
+apply (drule init_filefd_prop5, erule root_is_init_dir')
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest!:root_is_dir')
+done
+
+lemma noroot_filefd:
+ "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []"
+by (rule notI, simp, erule noroot_filefd', simp)
+
+lemma noroot_unlink:
+ "valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_unlink':
+ "valid (UnLink p [] # s) \<Longrightarrow> False"
+by (drule noroot_unlink, simp)
+
+lemma noroot_rmdir:
+ "valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_rmdir':
+ "valid (Rmdir p [] # s) \<Longrightarrow> False"
+by (drule noroot_rmdir, simp)
+
+lemma noroot_mkdir:
+ "valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_mkdir':
+ "valid (Mkdir p [] inum # s) \<Longrightarrow> False"
+by (drule noroot_mkdir, simp)
+
+lemma noroot_linkhard:
+ "valid (LinkHard p f f' # s) \<Longrightarrow> f \<noteq> [] \<and> f' \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_linkhard':
+ "valid (LinkHard p [] f # s) \<Longrightarrow> False"
+by (drule noroot_linkhard, simp)
+
+lemma noroot_linkhard'':
+ "valid (LinkHard p f [] # s) \<Longrightarrow> False"
+by (drule noroot_linkhard, simp)
+
+lemma noroot_truncate:
+ "valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []"
+by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+
+lemma noroot_truncate':
+ "valid (Truncate p [] len # s) \<Longrightarrow> False"
+by (drule noroot_truncate, simp)
+
+lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir
+ noroot_mkdir noroot_linkhard noroot_truncate
+
+lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir'
+ noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate'
+
+end
+
+end
\ No newline at end of file