diff -r 87fdf2de0ffa -r ac66d8ba86d9 Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Fri May 17 09:04:47 2013 +0800
+++ b/Co2sobj_prop.thy	Tue May 21 08:01:33 2013 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory Co2sobj_prop
-imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop
+imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
 begin
 (*<*)
 
@@ -371,270 +371,304 @@
            split:if_splits option.splits)                     
 done     
 
+lemma cf2sfile_other':
+  "\<lbrakk>valid (e # s); 
+    \<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'; 
+    ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"
+by (auto intro!:cf2sfile_other)
+  
 lemma cf2sfile_unlink:
   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
    \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
 apply (frule vd_cons, frule vt_grant_os)
 apply (simp add:current_files_simps split:if_splits)
 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
- split:if_splits option.splits)
-
-
-lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
-  
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-lemma cf2sfile_keep_path: "\<lbrakk>f \<preceq> f'; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"
-apply (induct f', simp add:no_junior_def)
-apply (case_tac "f = a # f'", simp add:cf2sfile.simps)
-apply (drule no_junior_noteq, simp, simp add:cf2sfile.simps)
+           split:if_splits option.splits)
 done
 
-lemma ckp'_aux: "\<not> f \<preceq> a # f' \<Longrightarrow> \<not> f \<preceq> f'"
-by (auto simp:no_junior_def)
-
-lemma cf2sfile_keep_path': "\<lbrakk>\<not> f \<preceq> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"
-apply (induct f', simp add:no_junior_def cf2sfile.simps, rule notI, drule cf2sfile_root_file, simp)
-apply (case_tac "f = a # f'", simp add:cf2sfile.simps)
-apply (rule notI)
-apply (frule ckp'_aux, simp, frule parentf_in_current', simp+)
-apply (case_tac "cf2sfile \<tau> f = cf2sfile \<tau> (a # f')", drule cf2sfile_inj, simp+)
-apply (simp add:cf2sfile.simps)
-by (drule no_junior_noteq, simp+)
-
-lemma cf2sfile_keep_path'': "\<lbrakk>cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<preceq> f'"
-using cf2sfile_keep_path'
-by (auto)
-
-lemma cf2sfile_open_some': "\<lbrakk>f \<in> current_files \<tau>; Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"
-apply (frule vt_cons')
-apply (drule vt_grant_os)
-apply (induct f)
-apply (simp add:cf2sfile.simps)+
-apply (frule parentf_in_current', simp)
-apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)
-done
-
-lemma cf2sfile_open_some: "\<lbrakk>Open p f flags fd (Some inum) # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk> 
-                           \<Longrightarrow> cf2sfile (Open p f flags fd (Some inum) # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"
-apply (case_tac f, simp)
-apply (frule vt_grant_os)
-apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_open_some')
+lemma cf2sfile_rmdir:
+  "\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>
+   \<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (simp add:current_files_simps split:if_splits)
+apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps
+           split:if_splits option.splits)
 done
 
-lemma cf2sfile_open_none: "cf2sfile (Open p f flags fd None # \<tau>) f' = cf2sfile \<tau> f'"
-apply (induct f')
-by (simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)+
+lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"
+apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")
+by (simp add:pfdof_simp2, simp)
+
+lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"
+apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")
+by (simp add:pfdof_simp2, simp)
+
+lemma cf2sfile_closefd:
+  "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>
+   \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"
+apply (frule vd_cons, frule vt_grant_os)
+apply (simp add:current_files_simps split:if_splits option.splits) 
+(* costs too much time, but solved
+
+apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 
+           split:if_splits option.splits  
+            dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file
+                 not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file
+            dest!:current_has_sec')
+done
+*)
+sorry
 
-lemma cf2sfile_open: "\<lbrakk>Open p f flags fd opt # \<tau> \<in> vt rc_cs; f' \<in> current_files (Open p f flags fd opt # \<tau>)\<rbrakk> \<Longrightarrow> 
-                       cf2sfile (Open p f flags fd opt # \<tau>) f' = (
-                         if (opt = None) then cf2sfile \<tau> f'
-                         else if (f' = f) then (case (parent f) of
-                                                  Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))
-                                                | _       \<Rightarrow> [])
-                              else cf2sfile \<tau> f'                                                          )"
-apply (frule vt_grant_os)
-by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_open_none cf2sfile_open_some cf2sfile_open_some' split:if_splits option.splits)
+lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other
+  cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd
+  
+(*********** cfd2sfd simpset *********)
+
+lemma cfd2sfd_open1:
+  "valid (Open p f flags fd opt # s)
+   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 
+     (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
+        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+      | _ \<Rightarrow> None)"
+by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)
 
-lemma cf2sfile_mkdir_some': "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"
-apply (frule vt_cons', drule vt_grant_os)
-apply (induct f, (simp add:cf2sfile.simps)+)
-apply (frule parentf_in_current', simp)
-apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)
-done
-
-lemma cf2sfile_mkdir_some: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk>
-                             \<Longrightarrow> cf2sfile (Mkdir p f inum # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"
-apply (case_tac f, simp)
-apply (frule vt_grant_os)
-apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_mkdir_some')
+lemma cfd2sfd_open_some2:
+  "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
+  \<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule file_of_proc_fd_in_curf, simp)
+apply (case_tac "f = f'", simp)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)
+apply (case_tac "p = p'", simp)
+apply (rule conjI, rule impI, simp)
+apply (drule cf2sfile_open_some1, simp)
+apply (auto split:option.splits)[1]
+apply simp
+apply (drule cf2sfile_open_some1, simp)
+apply (auto split:option.splits)[1]
 done
 
-lemma cf2sfile_mkdir: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; f' \<in> current_files (Mkdir p f inum # \<tau>)\<rbrakk> \<Longrightarrow>
-                        cf2sfile (Mkdir p f inum # \<tau>) f' = (
-                          if (f' = f) then (case (parent f) of
-                                              Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))
-                                            | _       \<Rightarrow> [])
-                          else cf2sfile \<tau> f'               ) "
-apply (frule vt_grant_os)
-by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_mkdir_some cf2sfile_mkdir_some' split:if_splits option.splits)
-
-lemma cf2sfile_linkhard_none: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"
-apply (frule vt_cons')
-apply (drule vt_grant_os)
-apply (induct f)
-apply (simp add:cf2sfile.simps)+
-apply (frule parentf_in_current', simp)
-apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)
+lemma cfd2sfd_open_none2:
+  "\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
+  \<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule file_of_proc_fd_in_curf, simp)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)
+apply (case_tac "p = p'", simp)
+apply (rule conjI, rule impI, simp)
+apply (drule cf2sfile_open_none)
+apply (auto split:option.splits)[1]
+apply simp
+apply (drule cf2sfile_open_none)
+apply (auto split:option.splits)[1]
+done
+  
+lemma cfd2sfd_open2:
+  "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>
+  \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"
+apply (case_tac opt)
+apply (simp add:cfd2sfd_open_none2)
+apply (simp add:cfd2sfd_open_some2)
 done
 
-lemma cf2sfile_linkhard_some: 
-  "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; parent f\<^isub>2 = Some pf\<^isub>2\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f\<^isub>2 = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2))"
-apply (case_tac f\<^isub>2, simp)
-apply (frule vt_grant_os)
-apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_linkhard_none)
+lemma cfd2sfd_open:
+  "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>
+   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 
+     (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
+        (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)
+      | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"
+apply (simp split:if_splits)
+apply (simp add:cfd2sfd_open1 split:option.splits)
+apply (simp add:cfd2sfd_open2)
+apply (rule impI, simp)
 done
 
-lemma cf2sfile_linkhard: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>)\<rbrakk> \<Longrightarrow>
-                           cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = (
-                             if (f = f\<^isub>2) then (case (parent f\<^isub>2) of
-                                                 Some pf\<^isub>2 \<Rightarrow> SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2)
-                                               | _        \<Rightarrow> [])
-                             else cf2sfile \<tau> f                 )"
-apply (frule vt_grant_os)
-by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_linkhard_none cf2sfile_linkhard_some split:if_splits option.splits)
+lemma cfd2sfd_closefd:
+  "\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>
+   \<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd  s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule file_of_proc_fd_in_curf, simp)
+apply (frule cf2sfile_closefd, simp)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
+apply (auto split:option.splits if_splits)
+done
 
-
-lemma no_junior_aux: "\<not> f\<^isub>2 \<preceq> a # f \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"
-by (auto simp:no_junior_def)
-
-lemma cf2sfile_rename_aux: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<noteq> f\<^isub>3 \<and> \<not> f\<^isub>3 \<preceq> f"
-apply (frule vt_grant_os, simp add:os_grant.simps, (erule exE|erule conjE)+)
-apply (rule conjI, rule notI, simp)
-apply (rule notI, drule vt_cons', simp add:ancenf_in_current)
+lemma cfd2sfd_clone:
+  "\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>
+   \<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (
+     if (p'' = p') then cfd2sfd s p fd'
+     else cfd2sfd s p'' fd')"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
+apply (frule_tac cf2sfile_other', simp+)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
+apply (case_tac "p'' = p'", simp)
+apply (auto split:option.splits if_splits)[1]
+apply (simp)
+apply (auto split:option.splits if_splits)[1]
 done
 
-lemma cf2sfile_rename'1: 
-  "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"
-apply (frule vt_cons',frule vt_grant_os,  induct f)
-apply (simp add:cf2sfile.simps)
-apply (frule parentf_in_current', simp, simp)
-apply (frule no_junior_aux, simp)
-apply (simp add:os_grant.simps, (erule exE|erule conjE)+)
-apply (drule cf2sfile_rename_aux, simp, erule conjE)
-apply (auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)
+lemma cfd2sfd_execve:
+  "\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>
+   \<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
+apply (frule_tac cf2sfile_other', simp+)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
+apply (case_tac "p' = p", simp)
+apply (auto split:option.splits if_splits)[1]
+apply (simp)
+apply (auto split:option.splits if_splits)[1]
 done
 
-lemma cf2sfile_rename'2: 
-  "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; \<not> (f\<^isub>3 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"
-apply (frule vt_cons', induct f)
-by (auto simp add:index_of_file.simps cf2sfile.simps no_junior_def split:option.splits nat.splits)
-
-lemma cf2sfile_rename1:
-  "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f\<^isub>3 = SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)"
-apply (case_tac f\<^isub>3, simp add:cf2sfile.simps)
-apply (auto dest!:cf2sfile_rename'2 simp add:no_junior_def cf2sfile.simps index_of_file.simps split:option.splits)
+lemma cfd2sfd_kill:
+  "\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>
+   \<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule proc_fd_in_procs, simp)
+apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
+apply (frule_tac cf2sfile_other', simp+)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
+apply (auto split:option.splits if_splits)
 done
 
-lemma index_of_file_rename1: "\<lbrakk>f\<^isub>2 \<preceq> f; f \<noteq> f\<^isub>2\<rbrakk> \<Longrightarrow> index_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = index_of_file \<tau> f"
-apply (clarsimp simp add:index_of_file.simps split:option.splits)
-by (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop3, simp, erule conjE, simp add:file_renaming_prop5)
-
-lemma cf2sfile_rename2: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; (file_before_rename f\<^isub>2 f\<^isub>3 f) \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"
-apply (induct f, simp add:no_junior_def)
-apply (case_tac "a # f = f\<^isub>3", simp)
-apply (drule cf2sfile_rename1, simp, simp add:file_renaming_prop0' file_renaming_prop0)
-
-apply (frule no_junior_noteq, simp, simp)
-apply (frule_tac file_renaming_prop1')
-apply (frule_tac f = f\<^isub>2 and \<tau> = \<tau> in cf2sfile_keep_path, simp add:vt_cons')
-apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop8')
-apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop6')
-apply (frule_tac f = "file_before_rename f\<^isub>2 f\<^isub>3 (a # f)" and \<tau> = \<tau> and f\<^isub>2 = f\<^isub>2 and f\<^isub>3 = f\<^isub>3 and p = p in index_of_file_rename1, simp add:file_before_rename_def)
-apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = f and a = a and f\<^isub>2 = f\<^isub>2 in file_renaming_prop9', simp)
-apply (drule parentf_in_current', simp add:vt_cons')
-apply (simp add:cf2sfile.simps)
-apply (erule file_renaming_prop6[THEN sym])
+lemma cfd2sfd_exit:
+  "\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>
+   \<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule proc_fd_in_procs, simp)
+apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)
+apply (frule_tac cf2sfile_other', simp+)
+apply (simp add:cfd2sfd_def sectxt_of_obj_simps)
+apply (auto split:option.splits if_splits)
 done
 
-lemma cf2sfile_rename2': "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"
-apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop5)
-apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1)
-apply (drule_tac f = "file_after_rename f\<^isub>2 f\<^isub>3 f" in cf2sfile_rename2, simp+)
+lemma cfd2sfd_other:
+  "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>
+   \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule proc_fd_in_fds, simp)
+apply (frule proc_fd_in_procs, simp)
+apply (frule file_of_proc_fd_in_curf, simp)
+apply (case_tac e)
+apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)
+apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)
+apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)
+done
+
+lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other
+
+(********** cpfd2sfds simpset **********)
+
+lemma current_filefd_has_flags:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"
+apply (induct s arbitrary:p)
+apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
+done
+
+lemma current_filefd_has_flags':
+  "\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+apply (case_tac "file_of_proc_fd s p fd")
+apply (simp, drule current_filefd_has_flags, simp+)
 done
 
-lemma cf2sfile_rename3: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"
-apply (case_tac "f\<^isub>2 \<preceq> f")
-apply (rule cf2sfile_rename2', simp+)
-apply (frule vt_grant_os)
-apply (frule_tac \<tau> = \<tau> in cf2sfile_keep_path', simp add:vt_cons', simp add:os_grant.simps, simp)
-apply (simp add:file_after_rename_def)
-by (rule cf2sfile_rename'1, simp+)
+lemma current_file_has_sfile':
+  "\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+by (rule notI, drule current_file_has_sfile, simp+)
 
-lemma cf2sfile_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow>
-                         cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (
-                           if (f\<^isub>3 \<preceq> f) then (case (parent f\<^isub>3) of 
-                                               Some pf\<^isub>3 \<Rightarrow> file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))
-                                             | _        \<Rightarrow> [])
-                           else cf2sfile \<tau> f               )"
-apply (frule vt_grant_os)
-apply (case_tac "f = f\<^isub>3", clarsimp simp:os_grant.simps, drule cf2sfile_rename1, simp+, simp add:file_renaming_prop0' file_renaming_prop0)
+lemma current_filefd_has_sfd:
+  "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"
+by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile' 
+         dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)
+
+lemma current_filefd_has_sfd':
+  "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"
+by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)
 
-apply (auto simp:os_grant.simps current_files_simps intro:cf2sfile_rename'2 cf2sfile_rename1 split:if_splits option.splits) 
-apply (rule cf2sfile_rename2, simp, drule rename_renaming_decom, simp+)
-apply (drule_tac f\<^isub>2 = f\<^isub>2 and f\<^isub>1 = f\<^isub>1 and f\<^isub>3 = f\<^isub>3 in file_renaming_prop5, simp+)
-done
+definition cpfd2sfds' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
+where
+  "cpfd2sfds' s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"
 
-lemma cf2sfile_other: "\<lbrakk>
-                        \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
-                        \<forall> p f im. e \<noteq> Mkdir p f im;
-                        \<forall> p f\<^isub>1 f\<^isub>2. e \<noteq> LinkHard p f\<^isub>1 f\<^isub>2;
-                        \<forall> p f\<^isub>2 f\<^isub>3. e \<noteq> Rename p f\<^isub>2 f\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (e # \<tau>) f' = cf2sfile \<tau> f'"
-apply (induct f', simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)
-apply (case_tac e, auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)
-done
+definition cph2spshs' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
+where
+  "cph2spshs' s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
 
-lemmas cf2sfile_nil = init_cf2sfile
+lemma "x \<in> cph2spshs' s p \<Longrightarrow> False"
+apply (simp add:cph2spshs'_def)
+apply (case_tac x, simp)
 
-lemma cf2sfile_nil': "f \<in> current_files [] \<Longrightarrow> cf2sfile [] f = map SInit f"
-by (simp add:cf2sfile_nil current_files_simps)
 
-lemmas cf2sfile_simps = cf2sfile_nil cf2sfile_nil' cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_rename cf2sfile_other
-
-lemmas cf2sfile_simpss = cf2sfile_nil cf2sfile_nil' cf2sfile_open_some' cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some' cf2sfile_mkdir_some
-                         cf2sfile_mkdir cf2sfile_linkhard_none cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1 cf2sfile_rename'2 cf2sfile_rename1
-                         cf2sfile_rename2 cf2sfile_rename2' cf2sfile_rename3 cf2sfile_rename cf2sfile_other
-
-lemma cf2sfile_open_some'_inum: "\<lbrakk>Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"
-by (simp add:cf2sfile_open_some' current_files_def)
+lemma cpfd2sfds_open_some1:
+  "valid (Open p f flags fd (Some inum) # s) \<Longrightarrow>
+   cpfd2sfds (Open p f flags fd (Some inum) # s) p = (
+    case (cfd2sfd (Open p f flags fd (Some inum) # s) p fd) of
+        Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}
+      | _ \<Rightarrow> cpfd2sfds s p)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (split option.splits)
+apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)
+apply (rule allI, rule impI)
+apply (rule set_eqI, rule iffI)
+unfolding cpfd2sfds_def
+thm CollectE
+apply (erule CollectE)
+apply (erule CollectE, (erule conjE|erule exE)+)
+apply (simp only:file_of_proc_fd.simps split:if_splits)
+apply (simp add:cpfd2sfds_def)
 
-lemma cf2sfile_mkdir_some'_inum: "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"
-by (simp add:cf2sfile_mkdir_some' current_files_def)
-
-lemma cf2sfile_linkhard_none_inum: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"
-by (simp add:cf2sfile_linkhard_none current_files_def)
-
-lemma cf2sfile_rename'1_inum: 
-  "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im ; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"
-by (simp add:cf2sfile_rename'1 current_files_def)
+apply (auto simp:cpfd2sfds_def split:option.splits if_splits dest:file_of_proc_fd_in_curf proc_fd_in_fds proc_fd_in_procs)
 
-lemma cf2sfile_rename2_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"
-by (simp add:cf2sfile_rename2 current_files_def)
-
-lemma cf2sfile_rename2'_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"
-by (simp add:cf2sfile_rename2' current_files_def)
+lemma cpfd2sfds_open1:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow>
+   cpfd2sfds (Open p f flags fd opt # s) p = (
+    case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+      | _ \<Rightarrow> cpfd2sfds s p)"
+apply (frule vd_cons, frule vt_grant_os)
+apply (case_tac opt)
+apply (auto simp:sectxt_of_obj_simps current_files_simps dest!:current_has_sec' current_file_has_sfile'
+  split:option.splits)
+apply (auto simp:cpfd2sfds_def split:if_splits)
+apply (auto simp:cfd2sfd_open cf2sfile_open sectxt_of_obj_simps current_files_simps split:option.splits if_splits dest!:current_has_sec' current_file_has_sfile')
+apply (frule cfd2sfd_open1)
+apply (
+apply (simp add:cpfd2sfds_def)
+apply (auto simp add:cpfd2sfds_def split:option.splits)
+apply (auto dest!:current_has_sec')
 
-lemma cf2sfile_rename3_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 
-   \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"
-by (simp add:cf2sfile_rename3 current_files_def)
+lemma cpfd2sfds_open:
+  "valid (Open p f flags fd opt # s)
+   \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (
+    case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of
+        (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}
+      | _ \<Rightarrow> cpfd2sfds s p))"
+apply (frule cfd2sfd_open1)
+apply (rule ext)
+apply (simp add:cpfd2sfds_def)
+apply (auto simp add:cpfd2sfds_def split:option.splits)
 
-lemma cf2sfile_nil'_inum: "inum_of_file [] f = Some im \<Longrightarrow> cf2sfile [] f = map SInit f"
-by (simp add:cf2sfile_nil' current_files_def)
+lemma cpfd2sfds_simps = 
 
-lemmas cf2sfile_simps_inum = cf2sfile_nil cf2sfile_nil'_inum cf2sfile_open_some'_inum cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some'_inum cf2sfile_mkdir_some
-                         cf2sfile_mkdir cf2sfile_linkhard_none_inum cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1_inum cf2sfile_rename'2 cf2sfile_rename1
-                         cf2sfile_rename2_inum cf2sfile_rename2'_inum cf2sfile_rename3_inum cf2sfile_rename cf2sfile_other
-
-(*************** cp2sproc simpset *********************)
+(******** cp2sproc simpset *********)
 
 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"
+apply (simp add:cp2sproc_def)
 by (simp add:cp2sproc_def index_of_proc.simps)
 
 lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"