--- a/Co2sobj_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Co2sobj_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -8,8 +8,6 @@
 
 (************ simpset for cf2sfile ***************)
 
-declare get_parentfs_ctxts.simps [simp del]
-
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
 by (simp add:cf2sfile_def)
@@ -71,6 +69,49 @@
 apply (auto simp:cf2sfile_def split:if_splits option.splits)
 done
 
+lemma sroot_set:
+  "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"
+apply (frule root_is_dir)
+apply (drule is_dir_has_sec, simp)
+apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 
+                 root_type_remains root_user_remains
+           dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'
+           split:option.splits)
+done
+
+lemma cf2sfile_path_file:
+  "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>
+   \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
+          (case (sectxt_of_obj s (O_file (f # pf))) of
+              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+           | None \<Rightarrow> None)
+     | _ \<Rightarrow> None)"
+apply (frule is_file_in_current, drule parentf_is_dir'', simp)
+apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
+apply (frule sroot_set)
+apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
+done
+
+lemma cf2sfile_path_dir:
+  "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>
+   \<Longrightarrow> cf2sfile s (f # pf) = (
+     case (cf2sfile s pf) of
+       Some (pfi, pfsec, psec, asecs) \<Rightarrow> 
+          (case (sectxt_of_obj s (O_dir (f # pf))) of
+              Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
+                                else Created, fsec, Some pfsec, asecs \<union> {pfsec})
+           | None \<Rightarrow> None)
+     | _ \<Rightarrow> None)"
+apply (frule is_dir_in_current, drule parentf_is_dir'', simp)
+apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)
+apply (frule_tac f = "pf" in is_dir_has_sfile, simp)
+apply (frule sroot_set)
+apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 
+done  
+
 lemma cf2sfile_path:
   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (
      case (cf2sfile s pf) of
@@ -80,16 +121,38 @@
                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
                | None \<Rightarrow> None)
          else (case (sectxt_of_obj s (O_dir (f # pf))) of
-                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)
+                 Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)
                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})
                | None \<Rightarrow> None)           )
      | None \<Rightarrow> None)"
+apply (drule is_file_or_dir, simp)
+apply (erule disjE)
+apply (frule cf2sfile_path_file, simp) defer
+apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)
+apply (auto split:option.splits)
+done
+
+
+
+apply simp
+
+thm cf2sfile_def
+apply (simp (no_asm_simp))
+apply simp
+apply (frule cf2sfile_path_file, simp)
+apply (simp add: cf2sfile_path_file)
+apply auto
+apply (simp only:cf2sfile_path_file)
+by (simp add:cf2sfile_path_file cf2sfile_path_dir)
 apply (frule parentf_is_dir'', simp)
-apply (frule parentf_in_current', simp)
 apply (frule is_file_or_dir, simp)
-apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE)
-apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop
-            simp:cf2sfile_def split:option.splits if_splits)
+apply (frule sroot_set, erule disjE)
+apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)
+apply (case_tac pf, clarsimp)
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps
+            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
+apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop 
+            simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1]
 apply (case_tac "is_file s (f # pf)")
 apply (frule is_file_has_sec, simp)
 apply (frule is_dir_has_sec, simp)

--- a/Current_files_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Current_files_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -215,25 +215,27 @@
 
       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 
+        apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_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 (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def 
+                   split:if_splits option.splits t_inode_tag.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)
+        apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp)
+        apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, 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''
+        using vt os fns'' cons
         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)
+                   split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) 
+        apply (rule_tac im = a and f = f and f' = f' in fns'', simp+)
         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
@@ -370,7 +372,7 @@
 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 
+apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def is_file_def
            split:if_splits option.splits)
 apply (simp add:pfdof_simp3)+
 apply (simp add:proc_fd_of_file_def)+  
@@ -496,7 +498,7 @@
 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)
+by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits)
 
 (*
 lemma rename_renaming_decom:

--- a/Delete_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Delete_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -25,7 +25,7 @@
 
 lemma not_deleted_init_file:
   "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"
-apply (induct s, simp add:is_init_file_prop1)
+apply (induct s, simp add:is_file_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 apply (auto simp:is_file_simps split:option.splits)
@@ -33,7 +33,7 @@
 
 lemma not_deleted_init_dir:
   "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"
-apply (induct s, simp add:is_init_dir_prop1)
+apply (induct s, simp add:is_dir_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 apply (auto simp:is_dir_simps split:option.splits)
@@ -71,7 +71,7 @@
 lemma not_deleted_init_tcp_aux:
   "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 
    \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
-apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1)
+apply (induct s arbitrary:p, simp add:is_tcp_sock_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 
@@ -90,7 +90,7 @@
 lemma not_deleted_init_udp_aux:
   "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 
    \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"
-apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1)
+apply (induct s arbitrary:p, simp add:is_udp_sock_nil)
 apply (frule vd_cons, frule vt_grant_os)
 apply (case_tac a) prefer 6 apply (case_tac option)
 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 

--- a/Flask.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Flask.thy	Wed May 15 15:42:46 2013 +0800
@@ -1017,6 +1017,23 @@
        (Some u, Some r, Some t) \<Rightarrow> Some (u, r, t)
      | _                        \<Rightarrow> None)"
 
+fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"
+where
+  "init_role_of_obj (O_proc p) = init_role_of_proc p"
+| "init_role_of_obj _          = Some R_object"
+
+definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"
+where
+  "init_sectxt_of_obj obj \<equiv>
+     (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of
+        (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t)
+      | _ \<Rightarrow> None)"
+
+definition sec_of_root :: "security_context_t"
+where
+  "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of
+     (Some u, Some t) \<Rightarrow> (u, R_object, t))"
+
 (******* flask granting ********
  * involves three kinds of rules:
  *  1. allow rule of types, allowed_rule_list_t, main

--- a/Init_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Init_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -68,19 +68,19 @@
 
 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
 
-lemma is_init_file_prop1: "is_init_file f = (f \<in> init_files \<and> is_file [] f)"
-by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"
+by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits)
 
-lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))"
-by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+lemma is_init_file_prop2: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+by (auto simp add:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
 
 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2
 
-lemma is_init_dir_prop1: "is_init_dir f = (f \<in> init_files \<and> is_dir [] f)"
+lemma is_init_dir_prop1: "is_init_dir f \<Longrightarrow> f \<in> init_files"
 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
 
-lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))"
-by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
+lemma is_init_dir_prop2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+by (auto simp add:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
 
 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2
 
@@ -94,14 +94,14 @@
   "is_udp_sock [] k = is_init_udp_sock k"
 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits)
 
-lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
+lemma is_init_udp_sock_prop1: "is_init_udp_sock s \<Longrightarrow> s \<in> init_sockets"
 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))"
-apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
-                dest:init_socket_has_inode split:option.splits)       
+lemma is_init_udp_sock_prop2: "is_init_udp_sock s \<Longrightarrow> \<not> is_init_tcp_sock s"
+apply (auto simp add:is_init_udp_sock_def is_init_tcp_sock_def  
+                dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       
 done
 
 lemma is_init_udp_sock_prop3:
@@ -121,14 +121,14 @@
   "is_tcp_sock [] k = is_init_tcp_sock k"
 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits)
 
-lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"
+lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s \<Longrightarrow> s \<in> init_sockets"
 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))"
-apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
-                dest:init_socket_has_inode split:option.splits)       
+lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s \<Longrightarrow> \<not> is_init_udp_sock s"
+apply (auto simp add:is_init_tcp_sock_def is_init_udp_sock_def  
+                dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       
 done
 
 lemma is_init_tcp_sock_prop3:
@@ -301,7 +301,8 @@
 
 lemma init_alive_prop: "init_alive obj = alive [] obj"
 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props
-         is_init_udp_sock_props init_files_props init_sockets_props)
+         is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil
+         is_tcp_sock_nil is_udp_sock_nil)
 done
 
 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp
@@ -369,7 +370,7 @@
 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3
 
 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t"
-apply (simp only: is_init_file_prop2)
+apply (drule init_alive_file)
 by (drule init_obj_has_user, auto)
 
 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None"
@@ -389,7 +390,7 @@
 lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5
 
 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t"
-apply (simp only: is_init_dir_prop2)
+apply (drule init_alive_dir)
 by (drule init_obj_has_user, auto)
 
 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None"
@@ -765,8 +766,7 @@
             dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
-apply (simp add:init_files_props)
-apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict)
+apply (drule is_init_file_prop1, simp add:init_files_props)
 done
 
 lemma s2ss_nil_prop:

--- a/Sectxt_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Sectxt_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -373,6 +373,58 @@
   is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec''
   current_msgq_has_sec'' current_msg_has_sec'' 
 
+(************ root sec remains ************)
+
+lemma root_type_remains:
+  "valid s \<Longrightarrow> type_of_obj s (O_dir []) = init_type_of_obj (O_dir [])"
+apply (induct s)
+apply (simp)
+apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 
+by (case_tac option, auto)
+
+lemma root_user_remains:
+  "valid s \<Longrightarrow> user_of_obj s (O_dir []) = init_user_of_obj (O_dir [])"
+apply (induct s)
+apply (simp)
+apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 
+by (case_tac option, auto)
+
+lemma root_has_type':
+  "\<lbrakk>type_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False"
+apply (drule alive_obj_has_type', simp)
+by (drule root_is_dir, simp)
+
+lemma root_has_user':
+  "\<lbrakk>user_of_obj s (O_dir []) = None; valid s\<rbrakk> \<Longrightarrow> False"
+apply (drule alive_obj_has_user', simp)
+by (drule root_is_dir, simp)
+
+lemma root_has_init_type':
+  "init_type_of_obj (O_dir []) = None \<Longrightarrow> False"
+using init_obj_has_type[where obj = "O_dir []"] root_is_init_dir
+by auto
+
+lemma root_has_init_user':
+  "init_user_of_obj (O_dir []) = None \<Longrightarrow> False"
+using init_obj_has_user[where obj = "O_dir []"] root_is_init_dir
+by auto
+
+lemma root_sec_remains:
+  "valid s \<Longrightarrow> sectxt_of_obj s (O_dir []) = init_sectxt_of_obj (O_dir [])"
+by (auto simp:root_user_remains root_type_remains sectxt_of_obj_def init_sectxt_of_obj_def
+        split:option.splits)
+
+lemma root_sec_set:
+  "\<exists> u t. sec_of_root = (u, R_object, t)"
+by (auto simp:sec_of_root_def split:option.splits
+        dest!: root_has_init_type' root_has_init_user')
+
+lemma sec_of_root_set:
+  "init_sectxt_of_obj (O_dir []) = Some sec_of_root"
+using root_has_init_type' root_has_init_user'
+apply (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)
+done
+
 (*************** sectxt_of_obj simpset ****************)
 
 lemma sec_execve:

--- a/Static.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Static.thy	Wed May 15 15:42:46 2013 +0800
@@ -6,18 +6,6 @@
 
 begin
 
-fun init_role_of_obj :: "t_object \<Rightarrow> role_t option"
-where
-  "init_role_of_obj (O_proc p) = init_role_of_proc p"
-| "init_role_of_obj _          = Some R_object"
-
-definition init_sectxt_of_obj :: "t_object \<Rightarrow> security_context_t option"
-where
-  "init_sectxt_of_obj obj \<equiv>
-     (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of
-        (Some u, Some r, Some t) \<Rightarrow> Some (u,r,t)
-      | _ \<Rightarrow> None)"
-
 (*
 definition init_sectxt_of_file:: "t_file \<Rightarrow> security_context_t option"
 where
@@ -27,11 +15,6 @@
      else None"
 *)
 
-definition sec_of_root :: "security_context_t"
-where
-  "sec_of_root \<equiv> (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of
-     (Some u, Some t) \<Rightarrow> (u, R_object, t))"
-
 definition sroot :: "t_sfile"
 where
   "sroot \<equiv> (Init [], sec_of_root, None, {})"