--- 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: