diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/Sectxt_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Sectxt_prop.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,772 @@
+theory Sectxt_prop
+imports Main Flask Flask_type Current_files_prop Current_sockets_prop Alive_prop
+begin
+
+context flask begin
+
+lemma alive_obj_has_type:
+  assumes alive: "alive s obj" and vs: "valid s"
+  shows "\<exists> t. type_of_obj s obj = Some t"
+using alive vs
+proof (induct s arbitrary:obj)
+  case Nil
+  thus ?case
+    by (simp add:init_alive_prop[THEN sym] init_obj_has_type)
+next
+  case (Cons e s)
+  hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto
+  hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" 
+    by (auto intro:vd_cons vt_grant_os vt_grant)  
+  hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. type_of_obj s obj = Some t" using Cons by auto
+  have a1': "\<And> obj. type_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1)
+  have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" by (auto intro:a1)
+  have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t"
+    by (auto intro!:a1 simp:is_file_in_current)
+  have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t" 
+    by (auto intro!:a1 simp:is_dir_in_current)
+  have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t"
+    by (auto intro!:a1 simp:is_tcp_in_current)
+  have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t"
+    by (auto intro!:a1 simp:is_udp_in_current)
+  have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t"
+    by (auto intro:a1)
+  have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" by (auto intro:a1)
+  have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" by (auto intro:a1)
+  have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" by (auto intro:a1)
+  have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>
+    \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1)
+  show ?case using a5 a2 a4 a3
+    apply (case_tac e)
+    apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
+                dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
+    done
+qed
+
+lemma alive_obj_has_user:
+  assumes alive: "alive s obj" and vs: "valid s"
+  shows "\<exists> t. user_of_obj s obj = Some t"
+using alive vs
+proof (induct s arbitrary:obj)
+  case Nil
+  thus ?case
+    by (simp add:init_alive_prop[THEN sym] init_obj_has_user)
+next
+  case (Cons e s)
+  hence a2: "alive (e # s) obj" and a3: "valid (e # s)" by auto
+  hence a4: "valid s" and a5: "os_grant s e" and a6: "grant s e" 
+    by (auto intro:vd_cons vt_grant_os vt_grant)  
+  hence a1: "\<And> obj. alive s obj \<Longrightarrow> \<exists>t. user_of_obj s obj = Some t" using Cons by auto
+  have a1': "\<And> obj. user_of_obj s obj = None \<Longrightarrow> \<not> alive s obj" by (rule_tac notI, auto dest:a1)
+  have p1: "\<And> p. p \<in> current_procs s \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" by (auto intro:a1)
+  have p2: "\<And> f. is_file s f \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t"
+    by (auto intro!:a1 simp:is_file_in_current)
+  have p3: "\<And> f. is_dir s f \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t" 
+    by (auto intro!:a1 simp:is_dir_in_current)
+  have p4: "\<And> sock. is_tcp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t"
+    by (auto intro!:a1 simp:is_tcp_in_current)
+  have p5: "\<And> sock. is_udp_sock s sock \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t"
+    by (auto intro!:a1 simp:is_udp_in_current)
+  have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t"
+    by (auto intro:a1)
+  have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" by (auto intro:a1)
+  have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" by (auto intro:a1)
+  have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" by (auto intro:a1)
+  have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>
+    \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1)
+  show ?case using a5 a2 a4 a3
+    apply (case_tac e)
+    apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
+                dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+    apply (frule_tac p = nat1 in file_fds_subset_pfds)
+    apply (rule a1, auto)
+    done
+qed
+  
+lemma alive_obj_has_type': "\<lbrakk>type_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" 
+by (rule_tac notI, auto dest:alive_obj_has_type)
+
+lemma current_proc_has_type: 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_proc p) = Some t" 
+by (auto intro:alive_obj_has_type)
+
+lemma current_proc_has_type': 
+  "\<lbrakk>type_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 
+by (rule notI, auto dest:current_proc_has_type)
+
+lemma is_file_has_type: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_file f) = Some t"
+by (auto intro:alive_obj_has_type simp:is_file_in_current)
+
+lemma is_file_has_type': "\<lbrakk>type_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"
+by (auto intro:notI dest:is_file_has_type)
+
+lemma is_dir_has_type: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_dir f) = Some t"
+by (auto intro:alive_obj_has_type simp:is_dir_in_current)
+
+lemma is_dir_has_type': "\<lbrakk>type_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
+by (auto intro:notI dest:is_dir_has_type)
+
+lemma is_tcp_has_type: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_tcp_sock sock) = Some t"
+by (auto intro:alive_obj_has_type simp:is_tcp_in_current)
+
+lemma is_tcp_has_type': "\<lbrakk>type_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"
+by (auto intro:notI dest:is_tcp_has_type)
+
+lemma is_udp_has_type: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_udp_sock sock) = Some t"
+by (auto intro:alive_obj_has_type simp:is_udp_in_current)
+
+lemma is_udp_has_type': "\<lbrakk>type_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"
+by (auto intro:notI dest:is_udp_has_type)
+
+lemma current_fd_has_type: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t"
+by (auto intro:alive_obj_has_type)
+
+lemma current_fd_has_type': "\<lbrakk>type_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"
+by (auto intro:notI dest:current_fd_has_type)
+
+lemma init_node_has_type: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" 
+by (auto intro: alive_obj_has_type)
+
+lemma init_node_has_type': "\<lbrakk>type_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 
+by (auto intro:notI dest:init_node_has_type)
+
+lemma current_shm_has_type: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" 
+by (auto intro:alive_obj_has_type)
+
+lemma current_shm_has_type': "\<lbrakk>type_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 
+by (auto intro:notI dest:current_shm_has_type)
+
+lemma current_msgq_has_type: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" 
+by (auto intro:alive_obj_has_type)
+
+lemma current_msgq_has_type': "\<lbrakk>type_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 
+by (auto intro:notI dest:current_msgq_has_type)
+
+lemma current_msg_has_type: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>
+    \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" 
+by (auto intro:alive_obj_has_type)
+
+lemma current_msg_has_type': "\<lbrakk>type_of_obj s (O_msg q m) = None; valid s\<rbrakk>
+    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 
+by (auto dest!:current_msg_has_type)
+
+lemmas current_has_type = alive_obj_has_type current_proc_has_type is_file_has_type is_dir_has_type 
+  is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type current_shm_has_type
+  current_msgq_has_type current_msg_has_type
+
+lemmas current_has_type' = alive_obj_has_type' current_proc_has_type' is_file_has_type' is_dir_has_type'
+  is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' current_shm_has_type'
+  current_msgq_has_type' current_msg_has_type' 
+
+lemma alive_obj_has_user': "\<lbrakk>user_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" 
+by (rule_tac notI, auto dest:alive_obj_has_user)
+
+lemma current_proc_has_user: 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_proc p) = Some t" 
+by (auto intro:alive_obj_has_user)
+
+lemma current_proc_has_user': 
+  "\<lbrakk>user_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 
+by (rule notI, auto dest:current_proc_has_user)
+
+lemma is_file_has_user: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_file f) = Some t"
+by (auto intro:alive_obj_has_user simp:is_file_in_current)
+
+lemma is_file_has_user': "\<lbrakk>user_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"
+by (auto intro:notI dest:is_file_has_user)
+
+lemma is_dir_has_user: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_dir f) = Some t"
+by (auto intro:alive_obj_has_user simp:is_dir_in_current)
+
+lemma is_dir_has_user': "\<lbrakk>user_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
+by (auto intro:notI dest:is_dir_has_user)
+
+lemma is_tcp_has_user: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_tcp_sock sock) = Some t"
+by (auto intro:alive_obj_has_user simp:is_tcp_in_current)
+
+lemma is_tcp_has_user': "\<lbrakk>user_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"
+by (auto intro:notI dest:is_tcp_has_user)
+
+lemma is_udp_has_user: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_udp_sock sock) = Some t"
+by (auto intro:alive_obj_has_user simp:is_udp_in_current)
+
+lemma is_udp_has_user': "\<lbrakk>user_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"
+by (auto intro:notI dest:is_udp_has_user)
+
+lemma current_fd_has_user: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t"
+by (auto intro:alive_obj_has_user)
+
+lemma current_fd_has_user': "\<lbrakk>user_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"
+by (auto intro:notI dest:current_fd_has_user)
+
+lemma init_node_has_user: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" 
+by (auto intro: alive_obj_has_user)
+
+lemma init_node_has_user': "\<lbrakk>user_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 
+by (auto intro:notI dest:init_node_has_user)
+
+lemma current_shm_has_user: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" 
+by (auto intro:alive_obj_has_user)
+
+lemma current_shm_has_user': "\<lbrakk>user_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 
+by (auto intro:notI dest:current_shm_has_user)
+
+lemma current_msgq_has_user: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" 
+by (auto intro:alive_obj_has_user)
+
+lemma current_msgq_has_user': "\<lbrakk>user_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 
+by (auto intro:notI dest:current_msgq_has_user)
+
+lemma current_msg_has_user: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>
+    \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" 
+by (auto intro:alive_obj_has_user)
+
+lemma current_msg_has_user': "\<lbrakk>user_of_obj s (O_msg q m) = None; valid s\<rbrakk>
+    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 
+by (auto dest!:current_msg_has_user)
+
+lemmas current_has_user = alive_obj_has_user current_proc_has_user is_file_has_user is_dir_has_user 
+  is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user current_shm_has_user
+  current_msgq_has_user current_msg_has_user
+
+lemmas current_has_user' = alive_obj_has_user' current_proc_has_user' is_file_has_user' is_dir_has_user'
+  is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' current_shm_has_user'
+  current_msgq_has_user' current_msg_has_user' 
+
+lemma current_proc_has_role:
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_proc s p = Some r"
+apply (induct s arbitrary:p, simp add:init_procrole_prop2)
+apply (frule vd_cons, frule vt_grant_os, frule vt_grant, case_tac a)
+apply (auto split:option.splits dest:current_has_type' simp:sectxt_of_obj_def)
+done
+
+lemma current_proc_has_role':
+  "\<lbrakk>role_of_proc s p = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s"
+by (auto dest:current_proc_has_role)
+
+lemma alive_obj_has_role:
+  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> r. role_of_obj s obj = Some r"
+by (case_tac obj, auto intro:current_proc_has_role)
+
+lemma alive_obj_has_sec:
+  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s obj = Some sec"
+apply (frule alive_obj_has_type, simp)
+apply (frule alive_obj_has_role, simp)
+apply (frule alive_obj_has_user, simp)
+apply (auto split:option.splits simp:sectxt_of_obj_def)
+done
+
+lemma alive_obj_has_sec':
+  "\<lbrakk>sectxt_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
+by (auto dest:alive_obj_has_sec)
+
+lemma alive_obj_has_sec'':
+  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s obj = Some (u,r,t)"
+by (auto dest:alive_obj_has_sec)
+
+lemma current_proc_has_sec: 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_proc p) = Some sec"
+by (rule alive_obj_has_sec, simp+) 
+
+lemma current_proc_has_sec': 
+  "\<lbrakk>sectxt_of_obj s (O_proc p) = None; valid s\<rbrakk> \<Longrightarrow> p \<notin> current_procs s" 
+by (rule notI, auto dest:current_proc_has_sec)
+
+lemma current_proc_has_sec'': 
+  "\<lbrakk>p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_proc p) = Some (u,r,t)"
+by (drule current_proc_has_sec, auto)
+
+lemma is_file_has_sec: "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_file f) = Some sec"
+by (rule alive_obj_has_sec, simp_all add:is_file_in_current)
+
+lemma is_file_has_sec': "\<lbrakk>sectxt_of_obj s (O_file f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_file s f"
+by (auto intro:notI dest:is_file_has_sec)
+
+lemma is_file_has_sec'': "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_file f) = Some (u,r,t)"
+by (drule is_file_has_sec, auto)
+
+lemma is_dir_has_sec: "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_dir f) = Some sec"
+by (rule alive_obj_has_sec, simp_all add:is_dir_in_current)
+
+lemma is_dir_has_sec': "\<lbrakk>sectxt_of_obj s (O_dir f) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
+by (auto intro:notI dest:is_dir_has_sec)
+
+lemma is_dir_has_sec'': "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_dir f) = Some (u,r,t)"
+by (drule is_dir_has_sec, auto)
+
+lemma is_tcp_has_sec: "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_tcp_sock sock) = Some sec"
+by (rule alive_obj_has_sec, simp_all add:is_tcp_in_current)
+
+lemma is_tcp_has_sec': "\<lbrakk>sectxt_of_obj s (O_tcp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_tcp_sock s sock"
+by (auto intro:notI dest:is_tcp_has_sec)
+
+lemma is_tcp_has_sec'': "\<lbrakk>is_tcp_sock s sock; valid s\<rbrakk> 
+  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_tcp_sock sock) = Some (u,r,t)"
+by (drule is_tcp_has_sec, simp_all add:is_tcp_in_current)
+
+lemma is_udp_has_sec: "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_udp_sock sock) = Some sec"
+by (rule alive_obj_has_sec, simp_all add:is_udp_in_current)
+
+lemma is_udp_has_sec': "\<lbrakk>sectxt_of_obj s (O_udp_sock sock) = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_udp_sock s sock"
+by (auto intro:notI dest:is_udp_has_sec)
+
+lemma is_udp_has_sec'': "\<lbrakk>is_udp_sock s sock; valid s\<rbrakk> 
+  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_udp_sock sock) = Some (u,r,t)"
+by (drule is_udp_has_sec, simp_all add:is_udp_in_current)
+
+lemma current_fd_has_sec: "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_fd p fd) = Some sec"
+by (rule alive_obj_has_sec, simp+)
+
+lemma current_fd_has_sec': "\<lbrakk>sectxt_of_obj s (O_fd p fd) = None; valid s\<rbrakk> \<Longrightarrow> fd \<notin> current_proc_fds s p"
+by (auto intro:notI dest:current_fd_has_sec)
+
+lemma current_fd_has_sec'': "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> 
+  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_fd p fd) = Some (u, r, t)"
+by (drule current_fd_has_sec, simp+)
+
+lemma init_node_has_sec: "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_node n) = Some sec" 
+by (rule alive_obj_has_sec, simp+)
+
+lemma init_node_has_sec': "\<lbrakk>sectxt_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes" 
+by (auto intro:notI dest:init_node_has_sec)
+
+lemma init_node_has_sec'': "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_node n) = Some (u,r,t)" 
+by (drule init_node_has_sec, simp+)
+
+lemma current_shm_has_sec: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_shm h) = Some sec" 
+by (rule alive_obj_has_sec, simp+)
+
+lemma current_shm_has_sec': "\<lbrakk>sectxt_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s" 
+by (auto intro:notI dest:current_shm_has_sec)
+
+lemma current_shm_has_sec'': "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_shm h) = Some (u,r,t)" 
+by (drule current_shm_has_sec, simp+)
+
+lemma current_msgq_has_sec: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msgq q) = Some sec" 
+by (rule alive_obj_has_sec, simp+)
+
+lemma current_msgq_has_sec': "\<lbrakk>sectxt_of_obj s (O_msgq q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s" 
+by (auto intro:notI dest:current_msgq_has_sec)
+
+lemma current_msgq_has_sec'': "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> 
+  \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msgq q) = Some (u,r,t)" 
+by (drule current_msgq_has_sec, simp+)
+
+lemma current_msg_has_sec: "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>
+    \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msg q m) = Some sec" 
+by (rule alive_obj_has_sec, simp+)
+
+lemma current_msg_has_sec': "\<lbrakk>sectxt_of_obj s (O_msg q m) = None; valid s\<rbrakk>
+    \<Longrightarrow> m \<notin> set (msgs_of_queue s q) \<or> q \<notin> current_msgqs s" 
+by (auto dest!:current_msg_has_sec)
+
+lemma current_msg_has_sec'': "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>
+    \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_msg q m) = Some (u, r, t)" 
+by (drule current_msg_has_sec, simp+)
+
+lemmas current_has_sec = alive_obj_has_sec current_proc_has_sec is_file_has_sec is_dir_has_sec 
+  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
+
+lemmas current_has_sec' = alive_obj_has_sec' current_proc_has_sec' is_file_has_sec' is_dir_has_sec'
+  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' 
+
+lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec''
+  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:
+  "valid (Execve p f fds # s) \<Longrightarrow> sectxt_of_obj (Execve p f fds # s) = 
+   (sectxt_of_obj s) (O_proc p := (
+     case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_file f)) of
+       (Some psec, Some fsec) \<Rightarrow> npctxt_execve psec fsec
+     | _ \<Rightarrow> None))"
+apply (rule ext, frule vd_cons, frule vt_grant_os, frule vt_grant,case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits 
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> sectxt_of_obj (Clone p p' fds shms # s) = (\<lambda> obj. 
+     case obj of 
+       O_proc p'' \<Rightarrow> if (p'' = p') then sectxt_of_obj s (O_proc p) 
+                     else sectxt_of_obj s obj
+     | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_fd p fd)
+                      else if (p'' = p') then None
+                      else sectxt_of_obj s obj
+     | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_tcp_sock (p, fd))
+                               else if (p'' = p') then None
+                               else sectxt_of_obj s obj
+     | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then sectxt_of_obj s (O_udp_sock (p, fd))
+                               else if (p'' = p') then None
+                               else sectxt_of_obj s obj
+     | _ \<Rightarrow> sectxt_of_obj s obj )"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_open:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow> sectxt_of_obj (Open p f flags fd opt # s) = (\<lambda> obj. 
+     case obj of
+       O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None) then 
+                      (case (parent f) of 
+                         None \<Rightarrow> None
+                       | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+                                      (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 
+                                        type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True)
+                                    | _ \<Rightarrow> None))
+                    else sectxt_of_obj s obj
+     | O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then 
+                        (case (sectxt_of_obj s (O_proc p)) of 
+                           Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                         | _ \<Rightarrow> None)
+                      else sectxt_of_obj s obj
+     | _ \<Rightarrow> sectxt_of_obj s obj)"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_mkdir:
+  "valid (Mkdir p f inum # s) \<Longrightarrow> sectxt_of_obj (Mkdir p f inum # s) = 
+     (sectxt_of_obj s) (O_dir f := 
+        (case parent f of 
+           None \<Rightarrow> None
+         | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+                         (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 
+                            type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True)
+                      | _ \<Rightarrow> None)))"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_linkhard:
+  "valid (LinkHard p f f' # s) \<Longrightarrow> sectxt_of_obj (LinkHard p f f' # s) = 
+     (sectxt_of_obj s) (O_file f' := 
+        (case parent f' of 
+           None \<Rightarrow> None
+         | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+                         (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object, 
+                            type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True)
+                      | _ \<Rightarrow> None)))"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_createmsgq:
+  "valid (CreateMsgq p q # s) \<Longrightarrow> sectxt_of_obj (CreateMsgq p q # s) = (sectxt_of_obj s) (O_msgq q := 
+     (case (sectxt_of_obj s (O_proc p)) of
+        Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+      | _ \<Rightarrow> None))"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_sendmsg:
+  "valid (SendMsg p q m # s) \<Longrightarrow> sectxt_of_obj (SendMsg p q m # s) = (sectxt_of_obj s) (O_msg q m := 
+     (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_msgq q)) of 
+        (Some psec, Some qsec) \<Rightarrow> Some (fst psec, R_object, 
+           type_transition ((snd o snd) psec) ((snd o snd) qsec) C_msg False)
+      | _ \<Rightarrow> None))"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_createshm:
+  "valid (CreateShM p h # s) \<Longrightarrow> sectxt_of_obj (CreateShM p h # s) = (sectxt_of_obj s) (O_shm h := 
+     case (sectxt_of_obj s (O_proc p)) of
+        Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+      | _ \<Rightarrow> None)"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_createsock:
+  "valid (CreateSock p af st fd inum # s) \<Longrightarrow> sectxt_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj. 
+     case obj of       
+       O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then 
+                        (case (sectxt_of_obj s (O_proc p)) of
+                           Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                         | _ \<Rightarrow> None)
+                      else sectxt_of_obj s obj
+     | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then 
+                                 (case (sectxt_of_obj s (O_proc p)) of
+                                    Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                                  | _ \<Rightarrow> None)
+                               else sectxt_of_obj s obj
+     | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then 
+                                 (case (sectxt_of_obj s (O_proc p)) of
+                                    Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                                  | _ \<Rightarrow> None)
+                               else sectxt_of_obj s obj
+     | _ \<Rightarrow> sectxt_of_obj s obj )"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_accept: 
+  "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> sectxt_of_obj (Accept p fd addr port fd' inum # s) = (\<lambda> obj. 
+     case obj of       
+       O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then 
+                        (case (sectxt_of_obj s (O_proc p)) of
+                           Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                         | _ \<Rightarrow> None)
+                      else sectxt_of_obj s obj
+     | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then 
+                                 (case (sectxt_of_obj s (O_proc p)) of
+                                    Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
+                                  | _ \<Rightarrow> None)
+                               else sectxt_of_obj s obj
+     | _ \<Rightarrow> sectxt_of_obj s obj )"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac obj)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_others :
+  "\<lbrakk>valid (e # s); 
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p f inum. e \<noteq> Mkdir p f inum;
+    \<forall> p f f'. e \<noteq> LinkHard p f f';
+    \<forall> p q. e \<noteq> CreateMsgq p q;
+    \<forall> p q m. e \<noteq> SendMsg p q m;
+    \<forall> p h. e \<noteq> CreateShM p h;
+    \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum;
+    \<forall> p fd addr port fd' inum. e \<noteq> Accept p fd addr port fd' inum
+   \<rbrakk> \<Longrightarrow> sectxt_of_obj (e # s) = sectxt_of_obj s"
+apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac e, case_tac[!] x)
+apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
+           dest!:current_has_type' current_proc_has_role' current_has_user')
+done
+
+lemma sec_kill: 
+  "valid (Kill p p' # s) \<Longrightarrow> sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_ptrace:
+  "valid (Ptrace p p' # s) \<Longrightarrow> sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_exit:
+  "valid (Exit p # s) \<Longrightarrow> sectxt_of_obj (Exit p # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_readfile:
+  "valid (ReadFile p fd # s) \<Longrightarrow> sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_writefile:
+  "valid (WriteFile p fd # s) \<Longrightarrow> sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_unlink:
+  "valid (UnLink p f # s) \<Longrightarrow> sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_Rmdir:
+  "valid (Rmdir p f # s) \<Longrightarrow> sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_truncate:
+  "valid (Truncate p f len # s) \<Longrightarrow> sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvmsg:
+  "valid (RecvMsg p q m # s) \<Longrightarrow> sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_removemsgq:
+  "valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_detach:
+  "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_bind:
+  "valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_connect:
+  "valid (Connect p fd addr # s) \<Longrightarrow> sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_listen:
+  "valid (Listen p fd # s) \<Longrightarrow> sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_sendsock:
+  "valid (SendSock p fd # s) \<Longrightarrow> sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_recvsock:
+  "valid (RecvSock p fd # s) \<Longrightarrow> sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemma sec_shutdown:
+  "valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s"
+by (auto dest!:sec_others)
+
+lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg
+  sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile
+  sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq
+  sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock
+  sec_recvsock sec_shutdown
+(* init_sectxt_prop *)
+
+(**************** get_parentfs_ctxts simpset **************)
+
+lemma parentf_is_dir_prop1: "\<lbrakk>is_dir s (x # pf); valid s\<rbrakk> \<Longrightarrow> is_dir s pf"
+apply (rule_tac f = "x # pf" in parentf_is_dir)
+by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits)
+
+lemma parentf_is_dir_prop2: "\<lbrakk>is_file s (x # pf); valid s\<rbrakk> \<Longrightarrow> is_dir s pf"
+apply (rule_tac f = "x # pf" in parentf_is_dir)
+by (auto simp:is_dir_def is_file_def current_files_def split:option.splits t_inode_tag.splits)
+
+lemma parentf_is_dir_prop3: "\<lbrakk>(x # pf) \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s pf"
+apply (rule_tac f = "x # pf" in parentf_is_dir)
+by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits)
+
+lemma get_pfs_secs_prop':
+  "\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f"
+apply (induct f)
+by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1)
+
+lemma get_pfs_secs_prop:
+  "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> asecs. get_parentfs_ctxts s f = Some asecs"
+using get_pfs_secs_prop'
+by (auto)
+
+lemma get_pfs_secs_open:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s"
+apply (frule noroot_events, frule vd_cons, frule vt_grant_os)
+apply (rule ext, induct_tac x)
+by (auto split:option.splits simp:sectxt_of_obj_simps)
+
+lemma get_pfs_secs_other:
+  "\<lbrakk>valid (e # s); \<forall> p f inum. e \<noteq> Mkdir p f inum\<rbrakk> 
+   \<Longrightarrow> get_parentfs_ctxts (e # s) = get_parentfs_ctxts s"
+apply (frule vd_cons, frule vt_grant_os, rule ext, induct_tac x)
+apply (case_tac [!] e)
+apply (auto split:option.splits if_splits simp:sectxt_of_obj_simps)
+done
+
+lemma get_pfs_secs_mkdir1:
+  assumes mkdir: "valid (Mkdir p f inum # s)" and noteq: "is_dir s f'"
+  shows "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'"
+proof-
+  from mkdir have vd: "valid s" and os: "os_grant s (Mkdir p f inum)"
+    by (frule_tac vd_cons, simp, frule_tac vt_grant_os, simp)
+  from mkdir have notroot: "f \<noteq> []" by (auto intro!:noroot_mkdir)
+  show ?thesis using noteq
+  proof (induct f')
+    case Nil
+    show ?case using notroot mkdir by (simp add:sectxt_of_obj_simps)
+  next
+    case (Cons a f')
+    hence p1: "is_dir s f'" using vd by (simp add:parentf_is_dir_prop1)
+    from Cons have p2: "is_dir s (a # f')" by simp
+    from Cons p1 have p3: "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'" by simp
+    from p2 os have p4: "a # f' \<noteq> f" by (auto simp:is_dir_in_current)
+    from p1 os have p5: "f' \<noteq> f"  by (auto simp:is_dir_in_current)
+    show ?case using mkdir vd os p4 p5  p1
+      by (auto simp:sectxt_of_obj_simps is_dir_simps p3
+              split:option.splits   dest:current_has_sec' get_pfs_secs_prop')
+  qed
+qed
+
+lemma get_pfs_secs_mkdir2:
+  "valid (Mkdir p f inum # s) \<Longrightarrow> get_parentfs_ctxts (Mkdir p f inum # s) f = (
+     case f of 
+       [] \<Rightarrow> get_parentfs_ctxts s []
+     | x#pf \<Rightarrow> (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
+                 (Some pfsecs, Some psec, Some pfsec) \<Rightarrow> Some ((fst psec, R_object, type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True) # pfsecs)
+               | _ \<Rightarrow> None))"
+apply (frule vd_cons, frule vt_grant_os)
+apply (frule noroot_events, case_tac f)
+by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop' get_pfs_secs_mkdir1
+          simp:sectxt_of_obj_simps is_dir_simps)
+
+lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2
+
+end
+
+end
\ No newline at end of file