diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/Init_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Init_prop.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,758 @@
+(*<*)
+theory Init_prop
+imports Main OS_type_def Flask Flask_type Static_type Static
+begin
+(*>*)
+
+context init begin
+
+lemma init_files_prop1: "init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files"
+by (simp add:inof_has_file_tag)
+
+lemma init_files_prop2: "finite init_files" 
+by (simp add:init_finite_sets)
+
+lemma init_files_prop3: "f \<in> init_files \<Longrightarrow> init_inum_of_file f \<noteq> None"
+by (auto dest:init_file_has_inum)
+
+lemma init_files_prop4: "(f \<in> init_files) = (f \<in> current_files [])"
+apply (simp add:current_files_def, rule iffI)
+using init_files_prop1 init_files_prop3 by auto
+
+lemmas init_files_props = init_file_has_inum init_files_prop1 init_files_prop2 init_files_prop3 init_files_prop4
+
+lemma init_inumof_prop1: "init_inum_of_file f = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag"
+by (auto dest:inof_has_file_tag)
+
+lemma init_inumof_prop2:  "init_inum_of_file f = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"
+by (auto dest:inof_has_file_tag)
+
+lemma init_inumof_prop3: "\<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some tag\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"
+by (auto dest:inof_has_file_tag)
+
+lemmas init_inum_of_file_props = init_files_prop1 init_inumof_prop1 init_inumof_prop2 init_inumof_prop3
+
+lemma init_inumos_prop1: "init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets"
+by (auto dest:inos_has_sock_tag)
+
+lemma init_inumos_prop2: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im = Some Tag_TCP_SOCK \<or> init_itag_of_inum im = Some Tag_UDP_SOCK"
+apply (auto dest!:inos_has_sock_tag) 
+apply (case_tac tag, simp+)
+done
+
+lemma init_inumos_prop3: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"
+by (auto dest:inos_has_sock_tag)
+
+lemma init_inumos_prop4: "init_inum_of_socket s = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag"
+by (auto dest!:inos_has_sock_tag) 
+
+lemmas init_inum_of_socket_props = init_inumos_prop1 init_inumos_prop2 init_inumos_prop3 init_inumos_prop4
+
+lemma init_sockets_prop1: "(p, fd) \<in> init_sockets \<Longrightarrow> p \<in> init_procs"
+by (auto dest: init_socket_has_inode)
+
+lemma init_sockets_prop2: "(p, fd) \<in> init_sockets \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto dest:init_socket_has_inode)
+
+lemma init_sockets_prop3: "s \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket s = Some im"
+by (case_tac s, auto dest:init_socket_has_inode)
+
+lemma init_sockets_prop4: "s \<in> init_sockets \<Longrightarrow> init_inum_of_socket s \<noteq> None"
+by (simp add:init_sockets_prop3)
+
+lemma init_sockets_prop5: "s \<in> init_sockets = (s \<in> current_sockets [])"
+apply (simp add:current_sockets_def, rule iffI)
+using init_sockets_prop4 inos_has_sock_tag apply auto
+apply (case_tac s, auto)
+done
+
+lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest: init_socket_has_inode)
+
+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 \<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 \<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 \<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 \<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
+
+lemma is_file_nil: "is_file [] = is_init_file"
+by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)
+
+lemma is_dir_nil: "is_dir [] = is_init_dir"
+by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)
+
+lemma is_udp_sock_nil:
+  "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 \<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 \<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:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+lemma is_init_udp_sock_prop4:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+lemma is_init_udp_sock_prop5:
+  "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6)
+
+lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3
+  is_init_udp_sock_prop4 is_init_udp_sock_prop5
+
+lemma is_tcp_sock_nil:
+  "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 \<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 \<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:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"
+by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+lemma is_init_tcp_sock_prop4:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits
+         dest:init_socket_has_inode inos_has_sock_tag)
+
+lemma is_init_tcp_sock_prop5:
+  "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"
+by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6)
+
+lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3
+  is_init_tcp_sock_prop4 is_init_tcp_sock_prop5
+
+lemma init_parent_file_prop1: 
+  "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"
+apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3)
+apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+)
+by (simp add:is_init_dir_def)
+
+lemma init_parent_file_prop1': 
+  "a # f \<in> init_files \<Longrightarrow> is_init_dir f"
+by (rule_tac pf = f in init_parent_file_prop1, auto)
+
+lemma init_parent_file_prop2:
+  "\<lbrakk>parent f = Some pf; is_init_file f\<rbrakk> \<Longrightarrow> is_init_dir pf"
+by (rule init_parent_file_prop1, simp, simp add: is_init_file_props)
+
+lemma init_parent_file_prop2':
+  "is_init_file (f#pf) \<Longrightarrow> is_init_dir pf"
+apply (rule init_parent_file_prop2)
+by auto
+
+lemma init_parent_file_prop3:
+  "\<lbrakk>parent f = Some pf; is_init_dir f\<rbrakk> \<Longrightarrow> is_init_dir pf"
+by (rule init_parent_file_prop1, simp, simp add: is_init_dir_props)
+
+lemma init_parent_file_prop3':
+  "is_init_dir (f#pf) \<Longrightarrow> is_init_dir pf"
+apply (rule init_parent_file_prop3)
+by auto
+
+lemma parent_file_in_init': "a # f \<in> init_files \<Longrightarrow> f \<in> init_files"
+by (subgoal_tac "parent (a # f) = Some f", drule parent_file_in_init, auto)
+
+lemmas init_parent_file_props = parent_file_in_init init_parent_file_prop1 parent_file_in_init' init_parent_file_prop1' init_parent_file_prop2 init_parent_file_prop2' init_parent_file_prop3 init_parent_file_prop3'
+
+lemma root_in_filesystem:  "[] \<in> init_files" 
+using init_files_prop1 root_is_dir by auto
+
+lemma root_is_init_dir: "is_init_dir []"
+using root_is_dir
+by (auto simp add:is_init_dir_def split:option.splits)
+
+lemma root_is_init_dir': "is_init_file [] \<Longrightarrow> False"
+using root_is_dir
+by (auto simp:is_init_file_def split:option.splits)
+
+
+lemma init_files_hung_prop1: "f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files"
+by (auto dest:init_files_hung_valid)
+
+lemma init_files_hung_prop2: "f \<in> init_files_hung_by_del \<Longrightarrow> \<exists> p fd. init_file_of_proc_fd p fd = Some f"
+by (auto dest:init_files_hung_valid)
+
+lemmas init_files_hung_by_del_props = init_files_hung_prop1 init_files_hung_prop2 init_files_hung_valid'
+
+
+lemma init_fds_of_proc_prop1: "fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs"
+by (auto dest!:init_procfds_valid)
+
+lemma init_fds_of_proc_prop2: "fd \<in> init_fds_of_proc p \<Longrightarrow> (\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets"
+by (auto dest:init_procfds_valid)
+
+lemmas init_fds_of_proc_props = init_fds_of_proc_prop1 init_fds_of_proc_prop2
+
+lemma init_filefd_prop1: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> f \<in> init_files"
+by (auto dest!:init_filefd_valid intro:init_files_prop1)
+
+lemma init_filefd_prop2: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> p \<in> init_procs"
+by (auto dest:init_filefd_valid)
+
+lemma init_filefd_prop3: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto dest:init_filefd_valid)
+
+lemma init_filefd_prop4: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<exists> flags. init_oflags_of_proc_fd p fd = Some flags"
+by (auto dest:init_filefd_valid)
+
+lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"
+by (auto dest:init_filefd_valid simp:is_init_file_def)
+
+lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1)
+
+lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)"
+by (auto dest!:init_filefd_valid is_init_udp_sock_prop1)
+
+lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets"
+by (auto dest!:init_filefd_valid)
+
+lemmas init_file_of_proc_fd_props = init_filefd_prop1 init_filefd_prop2 init_filefd_prop3 init_filefd_prop4 init_filefd_prop5 init_filefd_prop6 init_filefd_prop7 init_filefd_prop8
+
+lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"
+by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
+
+lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p"
+by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)
+
+lemmas init_oflags_of_proc_fd_props = init_oflags_prop1 init_oflags_prop2 init_fileflag_valid
+
+(*
+lemma init_socketstate_prop1: "s \<in> init_sockets \<Longrightarrow> init_socket_state s \<noteq> None"
+using init_socket_has_state
+by (case_tac s, simp add:bidirect_in_init_def)
+
+lemma init_socketstate_prop2: "s \<in> init_sockets \<Longrightarrow> \<exists> t. init_socket_state s = Some t"
+using init_socket_has_state
+by (case_tac s, simp add:bidirect_in_init_def)
+
+lemma init_socketstate_prop3: "init_socket_state s = Some t \<Longrightarrow> s \<in> init_sockets"
+using init_socket_has_state
+by (case_tac s, simp add:bidirect_in_init_def)
+
+lemmas init_socket_state_props = init_socketstate_prop1 init_socketstate_prop2 init_socketstate_prop3
+*)
+
+lemma init_inum_sock_file_noninter: "\<lbrakk>init_inum_of_socket s = Some im; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> False"
+apply (frule init_inumof_prop1, erule exE, drule init_inumof_prop3, simp)
+apply (frule init_inumos_prop2)
+apply (case_tac tag, simp+)
+done
+
+lemma init_parent_file_has_inum: "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> \<exists> im. init_inum_of_file pf = Some im"
+by (drule init_files_prop1, drule parent_file_in_init, simp, simp add:init_files_props)
+
+lemma init_file_has_no_son': "\<lbrakk>init_itag_of_inum im = Some Tag_FILE; init_inum_of_file f = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> init_inum_of_file f' = None"
+apply (drule init_file_no_son, simp)
+by (case_tac "init_inum_of_file f'", auto dest:init_files_prop1)
+
+lemma init_parent_file_is_dir': "\<lbrakk>parent f = Some pf; init_inum_of_file f = Some im; init_inum_of_file pf = Some ipm\<rbrakk> \<Longrightarrow> init_itag_of_inum ipm = Some Tag_DIR"
+by (drule init_parentf_is_dir, auto dest:init_files_prop1)
+
+lemma init_file_hung_has_no_son: "\<lbrakk>f \<in> init_files_hung_by_del; parent f' = Some f; init_inum_of_file f' = Some im\<rbrakk> \<Longrightarrow> False"
+apply (frule init_files_hung_prop1, drule init_file_has_inum, erule exE)
+apply (drule init_files_hung_valid', simp)
+apply (frule init_parent_file_is_dir', simp+)
+apply (drule init_files_prop1)
+apply (erule_tac x = f' in allE, simp)
+by (case_tac f', simp_all add:no_junior_def)
+
+(*
+lemma same_inode_nil_prop:
+  "same_inode_files [] f = init_same_inode_files f"
+by (simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
+
+lemma init_same_inode_prop1:
+  "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
+apply (simp add:init_same_inode_files_def)
+apply (drule init_files_prop3)
+apply (auto simp:init_files_prop1)
+done
+
+lemma init_same_inode_prop2:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f \<in> init_files\<rbrakk> \<Longrightarrow> f' \<in> init_files"
+by (drule init_same_inode_prop1, simp)
+
+lemma init_same_inode_prop3:
+  "f' \<in> init_same_inode_files f \<Longrightarrow> f \<in> init_same_inode_files f'"
+by (auto simp add:init_same_inode_files_def is_init_file_def split:if_splits)
+
+lemma init_same_inode_prop4:
+  "\<lbrakk>f' \<in> init_same_inode_files f; f' \<in> init_files\<rbrakk> \<Longrightarrow> f \<in> init_files"
+apply (drule init_same_inode_prop3)
+by (simp add:init_same_inode_prop2)
+*)
+
+end
+
+context flask begin
+
+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_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
+lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp
+lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp
+lemma init_alive_fd: "fd \<in> init_fds_of_proc p \<Longrightarrow> init_alive (O_fd p fd)" by simp
+lemma init_alive_tcp: "is_init_tcp_sock s \<Longrightarrow> init_alive (O_tcp_sock s)" by simp
+lemma init_alive_udp: "is_init_udp_sock s \<Longrightarrow> init_alive (O_udp_sock s)" by simp
+lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp
+lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp
+lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>
+  \<Longrightarrow> init_alive (O_msg q m)" by simp
+
+lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 
+  init_alive_tcp init_alive_udp init_alive_node init_alive_msgq init_alive_msg
+
+lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"
+using init_obj_has_type
+by (auto simp:is_init_file_def split:option.splits)
+
+lemma init_file_type_prop2: "is_init_file f \<Longrightarrow> init_type_of_obj (O_file f) \<noteq> None"
+by (simp add:init_file_type_prop1)
+
+lemma init_file_type_prop3: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"
+apply (drule init_type_has_obj) 
+by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+
+lemma init_file_type_prop4: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"
+apply (drule init_type_has_obj) 
+by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+
+lemmas init_file_types_props = init_file_type_prop1 init_file_type_prop2 init_file_type_prop3 init_file_type_prop4
+
+lemma init_dir_type_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_type_of_obj (O_dir f) = Some t"
+using init_obj_has_type
+by (auto simp:is_init_dir_def split:option.splits)
+
+lemma init_dir_type_prop2: "is_init_dir f \<Longrightarrow> init_type_of_obj (O_dir f) \<noteq> None"
+by (simp add:init_dir_type_prop1)
+
+lemma init_dir_type_prop3: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"
+apply (drule init_type_has_obj) 
+by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+
+lemma init_dir_type_prop4: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"
+apply (drule init_type_has_obj) 
+by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+
+lemmas init_dir_types_props = init_dir_type_prop1 init_dir_type_prop2 init_dir_type_prop3 init_dir_type_prop4
+
+lemma init_procrole_prop1: "init_role_of_proc p = Some r \<Longrightarrow> p \<in> init_procs"
+using init_proc_has_role
+by (auto simp:bidirect_in_init_def)
+
+lemma init_procrole_prop2: "p \<in> init_procs \<Longrightarrow> \<exists> r. init_role_of_proc p = Some r"
+using init_proc_has_role
+by (auto simp:bidirect_in_init_def)
+
+lemma init_procrole_prop3: "p \<in> init_procs \<Longrightarrow> init_role_of_proc p \<noteq> None"
+using init_proc_has_role
+by (auto simp:bidirect_in_init_def)
+
+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 (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"
+by (simp add:init_file_user_prop1)
+
+lemma init_file_user_prop3: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"
+apply (drule init_user_has_obj) 
+by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+
+lemma init_file_user_prop4: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"
+apply (drule init_user_has_obj) 
+by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)
+
+lemma init_file_user_prop5: "init_user_of_obj (O_file f) = Some u \<Longrightarrow> u \<in> init_users"
+by (simp add:init_user_has_obj)
+
+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 (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"
+by (simp add:init_dir_user_prop1)
+
+lemma init_dir_user_prop3: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"
+apply (drule init_user_has_obj) 
+by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+
+lemma init_dir_user_prop4: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"
+apply (drule init_user_has_obj) 
+by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)
+
+lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users"
+by (simp add:init_user_has_obj)
+
+lemmas init_dir_users_props = init_dir_user_prop1 init_dir_user_prop2 init_dir_user_prop3 init_dir_user_prop4 init_dir_user_prop5
+
+lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+end
+
+context tainting begin
+
+lemma tainted_nil_prop:
+  "(x \<in> tainted []) = (x \<in> seeds)"
+by auto
+
+end
+
+context tainting_s begin
+
+lemma init_file_has_ctxt:
+  "is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_file_props)
+by (simp add:init_file_types_props)
+
+lemma init_file_has_ctxt':
+  "init_sectxt_of_obj (O_file f) = None \<Longrightarrow> \<not> is_init_file f"
+by (rule notI, drule init_file_has_ctxt, simp)
+
+lemma init_dir_has_ctxt:
+  "is_init_dir f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_dir f) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+by (simp add:init_dir_types_props)
+
+lemma init_dir_has_ctxt':
+  "init_sectxt_of_obj (O_dir f) = None \<Longrightarrow> \<not> is_init_dir f"
+by (rule notI, drule init_dir_has_ctxt, simp)
+
+lemma init_proc_has_ctxt:
+  "p \<in> init_procs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_proc p) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp)
+apply (frule init_alive_proc, drule init_obj_has_type)
+by (drule init_procrole_prop2, auto)
+
+lemma init_proc_has_ctxt':
+  "init_sectxt_of_obj (O_proc p) = None \<Longrightarrow> p \<notin> init_procs"
+by (rule notI, drule init_proc_has_ctxt, simp)
+
+lemma init_fd_has_ctxt:
+  "fd \<in> init_fds_of_proc p \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_fd p fd) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+apply (drule init_alive_intros)
+apply (drule init_obj_has_type, clarsimp)
+done
+
+lemma init_fd_has_ctxt':
+  "init_sectxt_of_obj (O_fd p fd) = None \<Longrightarrow> fd \<notin> init_fds_of_proc p"
+by (rule notI, drule init_fd_has_ctxt, simp)
+
+lemma init_node_has_ctxt:
+  "n \<in> init_nodes \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_node n) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+apply (drule init_alive_intros)
+apply (drule init_obj_has_type, clarsimp)
+done
+
+lemma init_node_has_ctxt':
+  "init_sectxt_of_obj (O_node n) = None \<Longrightarrow> n \<notin> init_nodes"
+by (rule notI, drule init_node_has_ctxt, simp)
+
+lemma init_tcp_has_ctxt:
+  "is_init_tcp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_tcp_sock s) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+apply (drule init_alive_intros)
+apply (drule init_obj_has_type, clarsimp)
+done
+
+lemma init_tcp_has_ctxt':
+  "init_sectxt_of_obj (O_tcp_sock s) = None \<Longrightarrow> \<not> is_init_tcp_sock s"
+by (rule notI, drule init_tcp_has_ctxt, simp)
+
+lemma init_udp_has_ctxt:
+  "is_init_udp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_udp_sock s) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+by (drule init_alive_intros, drule init_obj_has_type, clarsimp)
+
+lemma init_udp_has_ctxt':
+  "init_sectxt_of_obj (O_udp_sock s) = None \<Longrightarrow> \<not> is_init_udp_sock s"
+by (rule notI, drule init_udp_has_ctxt, simp)
+
+lemma init_msgq_has_ctxt:
+  "q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+by (drule init_alive_intros, drule init_obj_has_type, clarsimp)
+
+lemma init_msgq_has_ctxt':
+  "init_sectxt_of_obj (O_msgq q) = None \<Longrightarrow> q \<notin> init_msgqs"
+by (rule notI, drule init_msgq_has_ctxt, simp)
+
+lemma init_msg_has_ctxt:
+  "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msg q m) = Some sec"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)
+by (drule init_alive_intros, simp, drule init_obj_has_type, clarsimp)
+
+lemma init_msg_has_ctxt':
+  "init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"
+by (auto dest:init_msg_has_ctxt)
+
+lemma init_rootf_has_ctxt:
+  "\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"
+apply (rule init_dir_has_ctxt, simp add:is_init_dir_def split:option.splits)
+using root_is_dir by auto
+
+lemma init_rootf_has_ctxt':
+  "init_sectxt_of_obj (O_dir []) = None \<Longrightarrow> False" 
+using init_rootf_has_ctxt by auto
+
+lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt
+  init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt init_msgq_has_ctxt
+  init_msg_has_ctxt init_rootf_has_ctxt
+
+lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'
+  init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' init_msgq_has_ctxt'
+  init_msg_has_ctxt' init_rootf_has_ctxt'
+
+lemma sec_of_root_valid:
+  "init_sectxt_of_obj (O_dir []) = Some sec_of_root"
+using init_rootf_has_ctxt
+by (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)
+
+lemma sec_of_root_is_tuple:
+  "\<exists> u t. sec_of_root = (u, R_object, t)"
+using sec_of_root_valid
+by (auto simp:sec_of_root_def init_sectxt_of_obj_def split:option.splits)
+
+lemma sroot_valid:
+  "init_cf2sfile [] = Some sroot"
+by (simp add:init_cf2sfile_def)
+
+lemma sroot_valid':
+  "cf2sfile s [] = Some sroot"
+by (simp add:cf2sfile_def)  
+
+lemma init_sectxt_prop:
+  "sectxt_of_obj [] obj = init_sectxt_of_obj obj"
+apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)
+apply (case_tac [!] obj, simp+)
+done
+
+lemma init_sectxt_prop2:
+  "init_sectxt_of_obj obj = Some sec \<Longrightarrow> init_alive obj"
+by (case_tac obj, auto simp:init_sectxt_of_obj_def split:option.splits dest:init_type_has_obj)
+
+lemma init_dir_has_seclist:
+  "is_init_dir f \<Longrightarrow> \<exists> seclist. get_parentfs_ctxts [] f = Some seclist"
+apply (induct f)
+apply (simp only:get_parentfs_ctxts.simps init_sectxt_prop)
+using init_rootf_has_ctxt apply (auto)[1]
+apply (frule init_parent_file_prop3', simp del:get_parentfs_ctxts.simps)
+apply (erule exE, drule init_dir_has_ctxt)
+by (auto simp add:init_sectxt_prop)
+
+lemma is_init_file_dir_prop1:
+  "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+
+lemma is_init_file_dir_prop2:
+  "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+
+lemma is_init_file_dir_prop3:
+  "\<lbrakk>is_init_dir f; is_init_file f\<rbrakk> \<Longrightarrow> False"
+by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+
+lemma is_init_file_dir_prop4:
+  "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"
+by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
+
+lemmas is_init_file_dir_props = is_init_file_dir_prop1 is_init_file_dir_prop2 is_init_file_dir_prop3 is_init_file_dir_prop4
+
+lemma init_dir_has_sfile:
+  "is_init_dir f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"
+apply (case_tac f)
+using init_rootf_has_ctxt apply (auto)[1]
+apply (simp add:sec_of_root_valid sroot_valid sroot_def)
+apply (simp, frule init_parent_file_prop3')
+apply (frule_tac f = list in init_dir_has_seclist)
+apply (frule_tac f = list in init_dir_has_ctxt)
+apply (frule_tac f = "a # list" in init_dir_has_ctxt)
+apply ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def split:option.splits)
+by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
+
+lemma init_file_has_sfile:
+  "is_init_file f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"
+apply (case_tac f)
+apply (simp, drule root_is_init_dir', simp)
+apply (simp, frule init_parent_file_prop2')
+apply (frule_tac f = list in init_dir_has_seclist)
+apply (frule_tac f = list in init_dir_has_ctxt)
+apply (frule_tac f = "a # list" in init_file_has_ctxt)
+by ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def)
+
+lemma init_proc_has_sproc:
+  "p \<in> init_procs \<Longrightarrow> \<exists> sp. init_cp2sproc p = Some sp"
+apply (frule init_proc_has_ctxt, erule exE)
+apply (simp add:init_cp2sproc_def)
+by (case_tac sec, simp+)
+
+lemma init_cqm2sms_has_sms_aux:
+  "\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"
+by (induct ms, auto split:option.splits simp:init_cm2smsg_def)
+
+lemma init_cqm2sms_has_sms: 
+  "q \<in> init_msgqs \<Longrightarrow> \<exists> sms. init_cqm2sms q (init_msgs_of_queue q) = Some sms"
+apply (rule init_cqm2sms_has_sms_aux)
+using init_msg_has_ctxt by auto
+
+lemma init_msgq_has_smsgq:
+  "q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"
+apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
+apply (simp add:init_cq2smsgq_def)
+by (case_tac sec, simp+)
+
+lemma cf2sfile_nil_prop:
+  "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
+apply (case_tac f)
+apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
+apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
+apply (auto simp:is_init_file_def is_init_dir_def is_file_nil split:option.splits t_inode_tag.splits 
+            dest:init_file_has_inum inof_has_file_tag)
+done
+
+lemma init_sec_file_dir:
+  "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
+apply (drule init_sectxt_prop2)+
+apply (auto intro:init_file_dir_conflict)
+done
+
+lemma cf2sfile_nil_prop3:
+  "is_init_file f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
+by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
+
+lemma cf2sfile_nil_prop4:
+  "is_init_dir f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
+apply (frule init_file_dir_conflict2)
+by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
+
+lemma cfd2sfd_nil_prop:
+  "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"
+apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)
+apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop)
+by (auto split:option.splits)
+
+lemma cpfd2sfds_nil_prop:
+  "cpfd2sfds [] p = init_cfds2sfds p"
+apply (simp only:cpfd2sfds_def init_cfds2sfds_def proc_file_fds_def init_proc_file_fds_def)
+apply (rule set_eqI, rule iffI)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI, simp)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI)
+using cfd2sfd_nil_prop 
+by auto
+
+lemma cp2sproc_nil_prop:
+  "p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p"
+by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cpfd2sfds_nil_prop
+         split:option.splits)
+
+lemma msg_has_sec_imp_init: 
+  "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+by (drule init_type_has_obj, simp)
+
+lemma msgq_has_sec_imp_init:
+  "init_sectxt_of_obj (O_msgq q) = Some sec \<Longrightarrow> q \<in> init_msgqs"
+apply (simp add:init_sectxt_of_obj_def split:option.splits)
+by (drule init_type_has_obj, simp)
+
+lemma cm2smsg_nil_prop:
+  "cm2smsg [] q m = init_cm2smsg q m"
+by (auto simp add:init_sectxt_prop cm2smsg_def init_cm2smsg_def split:option.splits
+             dest: msg_has_sec_imp_init elim:tainted.cases)
+
+lemma cqm2sms_nil_prop:
+  "cqm2sms [] q ms = init_cqm2sms q ms"
+apply (induct ms, simp)
+by (auto simp add:cm2smsg_def init_sectxt_prop tainted_nil_prop msg_has_sec_imp_init init_cm2smsg_def
+         split:option.splits)
+
+lemma cq2smsga_nil_prop:
+  "cq2smsgq [] q = init_cq2smsgq q"
+by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
+            intro:msgq_has_sec_imp_init split:option.splits)
+
+lemma co2sobj_nil_prop:
+  "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
+apply (case_tac obj)
+apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 
+                     cp2sproc_nil_prop is_init_dir_prop1 is_init_file_prop1
+                     is_init_udp_sock_prop1 is_init_tcp_sock_prop1 
+                       cm2smsg_nil_prop 
+               split:option.splits)
+done
+
+lemma s2ss_nil_prop:
+  "s2ss [] = init_static_state"
+using co2sobj_nil_prop init_alive_prop
+by (auto simp add:s2ss_def init_static_state_def)
+
+end
+
+(*<*)
+end
+(*>*)
\ No newline at end of file