diff -r 34d01e9a772e -r 7d9c0ed02b56 Current_files_prop.thy
--- /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