1 (*<*)

     2 theory Init_prop

     3 imports Main OS_type_def Flask Flask_type Static_type Static

     4 begin

     5 (*>*)

     6 

     7 context init begin

     8 

     9 lemma init_files_prop1: "init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files"

    10 by (simp add:inof_has_file_tag)

    11 

    12 lemma init_files_prop2: "finite init_files" 

    13 by (simp add:init_finite_sets)

    14 

    15 lemma init_files_prop3: "f \<in> init_files \<Longrightarrow> init_inum_of_file f \<noteq> None"

    16 by (auto dest:init_file_has_inum)

    17 

    18 lemma init_files_prop4: "(f \<in> init_files) = (f \<in> current_files [])"

    19 apply (simp add:current_files_def, rule iffI)

    20 using init_files_prop1 init_files_prop3 by auto

    21 

    22 lemmas init_files_props = init_file_has_inum init_files_prop1 init_files_prop2 init_files_prop3 init_files_prop4

    23 

    24 lemma init_inumof_prop1: "init_inum_of_file f = Some im \<Longrightarrow> \<exists> tag. init_itag_of_inum im = Some tag"

    25 by (auto dest:inof_has_file_tag)

    26 

    27 lemma init_inumof_prop2:  "init_inum_of_file f = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"

    28 by (auto dest:inof_has_file_tag)

    29 

    30 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"

    31 by (auto dest:inof_has_file_tag)

    32 

    33 lemmas init_inum_of_file_props = init_files_prop1 init_inumof_prop1 init_inumof_prop2 init_inumof_prop3

    34 

    35 lemma init_inumos_prop1: "init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets"

    36 by (auto dest:inos_has_sock_tag)

    37 

    38 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"

    39 apply (auto dest!:inos_has_sock_tag) 

    40 apply (case_tac tag, simp+)

    41 done

    42 

    43 lemma init_inumos_prop3: "init_inum_of_socket s = Some im \<Longrightarrow> init_itag_of_inum im \<noteq> None"

    44 by (auto dest:inos_has_sock_tag)

    45 

    46 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"

    47 by (auto dest!:inos_has_sock_tag) 

    48 

    49 lemmas init_inum_of_socket_props = init_inumos_prop1 init_inumos_prop2 init_inumos_prop3 init_inumos_prop4

    50 

    51 lemma init_sockets_prop1: "(p, fd) \<in> init_sockets \<Longrightarrow> p \<in> init_procs"

    52 by (auto dest: init_socket_has_inode)

    53 

    54 lemma init_sockets_prop2: "(p, fd) \<in> init_sockets \<Longrightarrow> fd \<in> init_fds_of_proc p"

    55 by (auto dest:init_socket_has_inode)

    56 

    57 lemma init_sockets_prop3: "s \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket s = Some im"

    58 by (case_tac s, auto dest:init_socket_has_inode)

    59 

    60 lemma init_sockets_prop4: "s \<in> init_sockets \<Longrightarrow> init_inum_of_socket s \<noteq> None"

    61 by (simp add:init_sockets_prop3)

    62 

    63 lemma init_sockets_prop5: "s \<in> init_sockets = (s \<in> current_sockets [])"

    64 apply (simp add:current_sockets_def, rule iffI)

    65 using init_sockets_prop4 inos_has_sock_tag apply auto

    66 apply (case_tac s, auto)

    67 done

    68 

    69 lemma init_socket_prop6: "(p, fd) \<in> init_sockets \<Longrightarrow> init_file_of_proc_fd p fd = None"

    70 by (auto dest: init_socket_has_inode)

    71 

    72 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5

    73 

    74 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"

    75 by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits)

    76 

    77 lemma is_init_file_prop2: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"

    78 by (auto simp add:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

    79 

    80 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2

    81 

    82 lemma is_init_dir_prop1: "is_init_dir f \<Longrightarrow> f \<in> init_files"

    83 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)

    84 

    85 lemma is_init_dir_prop2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"

    86 by (auto simp add:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

    87 

    88 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2

    89 

    90 lemma is_file_nil: "is_file [] = is_init_file"

    91 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits)

    92 

    93 lemma is_dir_nil: "is_dir [] = is_init_dir"

    94 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits)

    95 

    96 lemma is_udp_sock_nil:

    97   "is_udp_sock [] k = is_init_udp_sock k"

    98 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits)

    99 

   100 lemma is_init_udp_sock_prop1: "is_init_udp_sock s \<Longrightarrow> s \<in> init_sockets"

   101 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 

   102                 dest:init_socket_has_inode split:option.splits)       

   103 done

   104 

   105 lemma is_init_udp_sock_prop2: "is_init_udp_sock s \<Longrightarrow> \<not> is_init_tcp_sock s"

   106 apply (auto simp add:is_init_udp_sock_def is_init_tcp_sock_def  

   107                 dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       

   108 done

   109 

   110 lemma is_init_udp_sock_prop3:

   111   "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"

   112 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits

   113          dest:init_socket_has_inode inos_has_sock_tag)

   114 

   115 lemma is_init_udp_sock_prop4:

   116   "is_init_udp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"

   117 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits

   118          dest:init_socket_has_inode inos_has_sock_tag)

   119 

   120 lemma is_init_udp_sock_prop5:

   121   "is_init_udp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"

   122 by (auto dest:is_init_udp_sock_prop1 intro:init_socket_prop6)

   123 

   124 lemmas is_init_udp_sock_props = is_init_udp_sock_prop1 is_init_udp_sock_prop2 is_init_udp_sock_prop3

   125   is_init_udp_sock_prop4 is_init_udp_sock_prop5

   126 

   127 lemma is_tcp_sock_nil:

   128   "is_tcp_sock [] k = is_init_tcp_sock k"

   129 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits)

   130 

   131 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s \<Longrightarrow> s \<in> init_sockets"

   132 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 

   133                 dest:init_socket_has_inode split:option.splits)       

   134 done

   135 

   136 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s \<Longrightarrow> \<not> is_init_udp_sock s"

   137 apply (auto simp add:is_init_tcp_sock_def is_init_udp_sock_def  

   138                 dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       

   139 done

   140 

   141 lemma is_init_tcp_sock_prop3:

   142   "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs"

   143 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits

   144          dest:init_socket_has_inode inos_has_sock_tag)

   145 

   146 lemma is_init_tcp_sock_prop4:

   147   "is_init_tcp_sock (p, fd) \<Longrightarrow> fd \<in> init_fds_of_proc p"

   148 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits

   149          dest:init_socket_has_inode inos_has_sock_tag)

   150 

   151 lemma is_init_tcp_sock_prop5:

   152   "is_init_tcp_sock (p, fd) \<Longrightarrow> init_file_of_proc_fd p fd = None"

   153 by (auto dest:is_init_tcp_sock_prop1 intro:init_socket_prop6)

   154 

   155 lemmas is_init_tcp_sock_props = is_init_tcp_sock_prop1 is_init_tcp_sock_prop2 is_init_tcp_sock_prop3

   156   is_init_tcp_sock_prop4 is_init_tcp_sock_prop5

   157 

   158 lemma init_parent_file_prop1: 

   159   "\<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> is_init_dir pf"

   160 apply (frule parent_file_in_init, simp, frule_tac f = pf in init_files_prop3)

   161 apply (clarsimp, drule_tac im = y in init_parentf_is_dir, simp+)

   162 by (simp add:is_init_dir_def)

   163 

   164 lemma init_parent_file_prop1': 

   165   "a # f \<in> init_files \<Longrightarrow> is_init_dir f"

   166 by (rule_tac pf = f in init_parent_file_prop1, auto)

   167 

   168 lemma init_parent_file_prop2:

   169   "\<lbrakk>parent f = Some pf; is_init_file f\<rbrakk> \<Longrightarrow> is_init_dir pf"

   170 by (rule init_parent_file_prop1, simp, simp add: is_init_file_props)

   171 

   172 lemma init_parent_file_prop2':

   173   "is_init_file (f#pf) \<Longrightarrow> is_init_dir pf"

   174 apply (rule init_parent_file_prop2)

   175 by auto

   176 

   177 lemma init_parent_file_prop3:

   178   "\<lbrakk>parent f = Some pf; is_init_dir f\<rbrakk> \<Longrightarrow> is_init_dir pf"

   179 by (rule init_parent_file_prop1, simp, simp add: is_init_dir_props)

   180 

   181 lemma init_parent_file_prop3':

   182   "is_init_dir (f#pf) \<Longrightarrow> is_init_dir pf"

   183 apply (rule init_parent_file_prop3)

   184 by auto

   185 

   186 lemma parent_file_in_init': "a # f \<in> init_files \<Longrightarrow> f \<in> init_files"

   187 by (subgoal_tac "parent (a # f) = Some f", drule parent_file_in_init, auto)

   188 

   189 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'

   190 

   191 lemma root_in_filesystem:  "[] \<in> init_files" 

   192 using init_files_prop1 root_is_dir by auto

   193 

   194 lemma root_is_init_dir: "is_init_dir []"

   195 using root_is_dir

   196 by (auto simp add:is_init_dir_def split:option.splits)

   197 

   198 lemma root_is_init_dir': "is_init_file [] \<Longrightarrow> False"

   199 using root_is_dir

   200 by (auto simp:is_init_file_def split:option.splits)

   201 

   202 

   203 lemma init_files_hung_prop1: "f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files"

   204 by (auto dest:init_files_hung_valid)

   205 

   206 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"

   207 by (auto dest:init_files_hung_valid)

   208 

   209 lemmas init_files_hung_by_del_props = init_files_hung_prop1 init_files_hung_prop2 init_files_hung_valid'

   210 

   211 

   212 lemma init_fds_of_proc_prop1: "fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs"

   213 by (auto dest!:init_procfds_valid)

   214 

   215 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"

   216 by (auto dest:init_procfds_valid)

   217 

   218 lemmas init_fds_of_proc_props = init_fds_of_proc_prop1 init_fds_of_proc_prop2

   219 

   220 lemma init_filefd_prop1: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> f \<in> init_files"

   221 by (auto dest!:init_filefd_valid intro:init_files_prop1)

   222 

   223 lemma init_filefd_prop2: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> p \<in> init_procs"

   224 by (auto dest:init_filefd_valid)

   225 

   226 lemma init_filefd_prop3: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p"

   227 by (auto dest:init_filefd_valid)

   228 

   229 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"

   230 by (auto dest:init_filefd_valid)

   231 

   232 lemma init_filefd_prop5: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> is_init_file f"

   233 by (auto dest:init_filefd_valid simp:is_init_file_def)

   234 

   235 lemma init_filefd_prop6: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_tcp_sock (p, fd)"

   236 by (auto dest!:init_filefd_valid is_init_tcp_sock_prop1)

   237 

   238 lemma init_filefd_prop7: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> \<not> is_init_udp_sock (p, fd)"

   239 by (auto dest!:init_filefd_valid is_init_udp_sock_prop1)

   240 

   241 lemma init_filefd_prop8: "init_file_of_proc_fd p fd = Some f \<Longrightarrow> (p, fd) \<notin> init_sockets"

   242 by (auto dest!:init_filefd_valid)

   243 

   244 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

   245 

   246 lemma init_oflags_prop1: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> p \<in> init_procs"

   247 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)

   248 

   249 lemma init_oflags_prop2: "init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> fd \<in> init_fds_of_proc p"

   250 by (auto dest:init_fileflag_valid init_file_of_proc_fd_props)

   251 

   252 lemmas init_oflags_of_proc_fd_props = init_oflags_prop1 init_oflags_prop2 init_fileflag_valid

   253 

   254 (*

   255 lemma init_socketstate_prop1: "s \<in> init_sockets \<Longrightarrow> init_socket_state s \<noteq> None"

   256 using init_socket_has_state

   257 by (case_tac s, simp add:bidirect_in_init_def)

   258 

   259 lemma init_socketstate_prop2: "s \<in> init_sockets \<Longrightarrow> \<exists> t. init_socket_state s = Some t"

   260 using init_socket_has_state

   261 by (case_tac s, simp add:bidirect_in_init_def)

   262 

   263 lemma init_socketstate_prop3: "init_socket_state s = Some t \<Longrightarrow> s \<in> init_sockets"

   264 using init_socket_has_state

   265 by (case_tac s, simp add:bidirect_in_init_def)

   266 

   267 lemmas init_socket_state_props = init_socketstate_prop1 init_socketstate_prop2 init_socketstate_prop3

   268 *)

   269 

   270 lemma init_inum_sock_file_noninter: "\<lbrakk>init_inum_of_socket s = Some im; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> False"

   271 apply (frule init_inumof_prop1, erule exE, drule init_inumof_prop3, simp)

   272 apply (frule init_inumos_prop2)

   273 apply (case_tac tag, simp+)

   274 done

   275 

   276 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"

   277 by (drule init_files_prop1, drule parent_file_in_init, simp, simp add:init_files_props)

   278 

   279 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"

   280 apply (drule init_file_no_son, simp)

   281 by (case_tac "init_inum_of_file f'", auto dest:init_files_prop1)

   282 

   283 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"

   284 by (drule init_parentf_is_dir, auto dest:init_files_prop1)

   285 

   286 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"

   287 apply (frule init_files_hung_prop1, drule init_file_has_inum, erule exE)

   288 apply (drule init_files_hung_valid', simp)

   289 apply (frule init_parent_file_is_dir', simp+)

   290 apply (drule init_files_prop1)

   291 apply (erule_tac x = f' in allE, simp)

   292 by (case_tac f', simp_all add:no_junior_def)

   293 

   294 lemma same_inode_nil_prop:

   295   "same_inode_files [] f = init_same_inode_files f"

   296 by (simp add:same_inode_files_def init_same_inode_files_def is_file_nil)

   297 

   298 lemma init_same_inode_prop1:

   299   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"

   300 apply (simp add:init_same_inode_files_def)

   301 apply (drule init_files_prop3)

   302 apply (auto simp:init_files_prop1)

   303 done

   304 

   305 lemma init_same_inode_prop2:

   306   "\<lbrakk>f' \<in> init_same_inode_files f; f \<in> init_files\<rbrakk> \<Longrightarrow> f' \<in> init_files"

   307 by (drule init_same_inode_prop1, simp)

   308 

   309 lemma init_same_inode_prop3:

   310   "f' \<in> init_same_inode_files f \<Longrightarrow> f \<in> init_same_inode_files f'"

   311 by (auto simp add:init_same_inode_files_def is_init_file_def split:if_splits)

   312 

   313 lemma init_same_inode_prop4:

   314   "\<lbrakk>f' \<in> init_same_inode_files f; f' \<in> init_files\<rbrakk> \<Longrightarrow> f \<in> init_files"

   315 apply (drule init_same_inode_prop3)

   316 by (simp add:init_same_inode_prop2)

   317 

   318 end

   319 

   320 context flask begin

   321 

   322 lemma init_alive_prop: "init_alive obj = alive [] obj"

   323 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props

   324          is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil

   325          is_tcp_sock_nil is_udp_sock_nil)

   326 done

   327 

   328 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp

   329 lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp

   330 lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp

   331 lemma init_alive_fd: "fd \<in> init_fds_of_proc p \<Longrightarrow> init_alive (O_fd p fd)" by simp

   332 lemma init_alive_tcp: "is_init_tcp_sock s \<Longrightarrow> init_alive (O_tcp_sock s)" by simp

   333 lemma init_alive_udp: "is_init_udp_sock s \<Longrightarrow> init_alive (O_udp_sock s)" by simp

   334 lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp

   335 (*

   336 lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp

   337 *)

   338 lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp

   339 lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>

   340   \<Longrightarrow> init_alive (O_msg q m)" by simp

   341 

   342 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 

   343   init_alive_tcp init_alive_udp init_alive_node  init_alive_msgq init_alive_msg (*init_alive_shm*)

   344 

   345 

   346 lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"

   347 using init_obj_has_type

   348 by (auto simp:is_init_file_def split:option.splits)

   349 

   350 lemma init_file_type_prop2: "is_init_file f \<Longrightarrow> init_type_of_obj (O_file f) \<noteq> None"

   351 by (simp add:init_file_type_prop1)

   352 

   353 lemma init_file_type_prop3: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"

   354 apply (drule init_type_has_obj) 

   355 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   356 

   357 lemma init_file_type_prop4: "init_type_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"

   358 apply (drule init_type_has_obj) 

   359 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   360 

   361 lemmas init_file_types_props = init_file_type_prop1 init_file_type_prop2 init_file_type_prop3 init_file_type_prop4

   362 

   363 lemma init_dir_type_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_type_of_obj (O_dir f) = Some t"

   364 using init_obj_has_type

   365 by (auto simp:is_init_dir_def split:option.splits)

   366 

   367 lemma init_dir_type_prop2: "is_init_dir f \<Longrightarrow> init_type_of_obj (O_dir f) \<noteq> None"

   368 by (simp add:init_dir_type_prop1)

   369 

   370 lemma init_dir_type_prop3: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"

   371 apply (drule init_type_has_obj) 

   372 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   373 

   374 lemma init_dir_type_prop4: "init_type_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"

   375 apply (drule init_type_has_obj) 

   376 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   377 

   378 lemmas init_dir_types_props = init_dir_type_prop1 init_dir_type_prop2 init_dir_type_prop3 init_dir_type_prop4

   379 

   380 lemma init_procrole_prop1: "init_role_of_proc p = Some r \<Longrightarrow> p \<in> init_procs"

   381 using init_proc_has_role

   382 by (auto simp:bidirect_in_init_def)

   383 

   384 lemma init_procrole_prop2: "p \<in> init_procs \<Longrightarrow> \<exists> r. init_role_of_proc p = Some r"

   385 using init_proc_has_role

   386 by (auto simp:bidirect_in_init_def)

   387 

   388 lemma init_procrole_prop3: "p \<in> init_procs \<Longrightarrow> init_role_of_proc p \<noteq> None"

   389 using init_proc_has_role

   390 by (auto simp:bidirect_in_init_def)

   391 

   392 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3

   393 

   394 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t"

   395 apply (drule init_alive_file)

   396 by (drule init_obj_has_user, auto)

   397 

   398 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None"

   399 by (simp add:init_file_user_prop1)

   400 

   401 lemma init_file_user_prop3: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> f \<in> init_files"

   402 apply (drule init_user_has_obj) 

   403 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   404 

   405 lemma init_file_user_prop4: "init_user_of_obj (O_file f) = Some t \<Longrightarrow> is_init_file f"

   406 apply (drule init_user_has_obj) 

   407 by (simp add:is_init_file_def init_inum_of_file_props split:option.splits)

   408 

   409 lemma init_file_user_prop5: "init_user_of_obj (O_file f) = Some u \<Longrightarrow> u \<in> init_users"

   410 by (simp add:init_user_has_obj)

   411 

   412 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

   413 

   414 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t"

   415 apply (drule init_alive_dir)

   416 by (drule init_obj_has_user, auto)

   417 

   418 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None"

   419 by (simp add:init_dir_user_prop1)

   420 

   421 lemma init_dir_user_prop3: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> f \<in> init_files"

   422 apply (drule init_user_has_obj) 

   423 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   424 

   425 lemma init_dir_user_prop4: "init_user_of_obj (O_dir f) = Some t \<Longrightarrow> is_init_dir f"

   426 apply (drule init_user_has_obj) 

   427 by (simp add:is_init_dir_def init_inum_of_file_props split:option.splits)

   428 

   429 lemma init_dir_user_prop5: "init_user_of_obj (O_dir f) = Some u \<Longrightarrow> u \<in> init_users"

   430 by (simp add:init_user_has_obj)

   431 

   432 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

   433 

   434 lemma init_file_dir_conflict: "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"

   435 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   436 

   437 lemma init_file_dir_conflict1: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"

   438 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   439 

   440 lemma init_file_dir_conflict2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"

   441 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   442 

   443 end

   444 

   445 context tainting begin

   446 

   447 lemma tainted_nil_prop:

   448   "(x \<in> tainted []) = (x \<in> seeds)"

   449 by auto

   450 

   451 end

   452 

   453 context tainting_s begin

   454 

   455 lemma init_file_has_ctxt:

   456   "is_init_file f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_file f) = Some sec"

   457 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   458 apply (rule conjI, rule init_obj_has_user, simp add:is_init_file_props)

   459 by (simp add:init_file_types_props)

   460 

   461 lemma init_file_has_ctxt':

   462   "init_sectxt_of_obj (O_file f) = None \<Longrightarrow> \<not> is_init_file f"

   463 by (rule notI, drule init_file_has_ctxt, simp)

   464 

   465 lemma init_dir_has_ctxt:

   466   "is_init_dir f \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_dir f) = Some sec"

   467 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   468 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   469 by (simp add:init_dir_types_props)

   470 

   471 lemma init_dir_has_ctxt':

   472   "init_sectxt_of_obj (O_dir f) = None \<Longrightarrow> \<not> is_init_dir f"

   473 by (rule notI, drule init_dir_has_ctxt, simp)

   474 

   475 lemma init_proc_has_ctxt:

   476   "p \<in> init_procs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_proc p) = Some sec"

   477 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   478 apply (rule conjI, rule init_obj_has_user, simp)

   479 apply (frule init_alive_proc, drule init_obj_has_type)

   480 by (drule init_procrole_prop2, auto)

   481 

   482 lemma init_proc_has_ctxt':

   483   "init_sectxt_of_obj (O_proc p) = None \<Longrightarrow> p \<notin> init_procs"

   484 by (rule notI, drule init_proc_has_ctxt, simp)

   485 

   486 lemma init_fd_has_ctxt:

   487   "fd \<in> init_fds_of_proc p \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_fd p fd) = Some sec"

   488 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   489 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   490 apply (drule init_alive_intros)

   491 apply (drule init_obj_has_type, clarsimp)

   492 done

   493 

   494 lemma init_fd_has_ctxt':

   495   "init_sectxt_of_obj (O_fd p fd) = None \<Longrightarrow> fd \<notin> init_fds_of_proc p"

   496 by (rule notI, drule init_fd_has_ctxt, simp)

   497 

   498 lemma init_node_has_ctxt:

   499   "n \<in> init_nodes \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_node n) = Some sec"

   500 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   501 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   502 apply (drule init_alive_intros)

   503 apply (drule init_obj_has_type, clarsimp)

   504 done

   505 

   506 lemma init_node_has_ctxt':

   507   "init_sectxt_of_obj (O_node n) = None \<Longrightarrow> n \<notin> init_nodes"

   508 by (rule notI, drule init_node_has_ctxt, simp)

   509 

   510 lemma init_tcp_has_ctxt:

   511   "is_init_tcp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_tcp_sock s) = Some sec"

   512 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   513 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   514 apply (drule init_alive_intros)

   515 apply (drule init_obj_has_type, clarsimp)

   516 done

   517 

   518 lemma init_tcp_has_ctxt':

   519   "init_sectxt_of_obj (O_tcp_sock s) = None \<Longrightarrow> \<not> is_init_tcp_sock s"

   520 by (rule notI, drule init_tcp_has_ctxt, simp)

   521 

   522 lemma init_udp_has_ctxt:

   523   "is_init_udp_sock s \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_udp_sock s) = Some sec"

   524 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   525 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   526 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   527 

   528 lemma init_udp_has_ctxt':

   529   "init_sectxt_of_obj (O_udp_sock s) = None \<Longrightarrow> \<not> is_init_udp_sock s"

   530 by (rule notI, drule init_udp_has_ctxt, simp)

   531 

   532 (*

   533 lemma init_shm_has_ctxt:

   534   "h \<in> init_shms \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_shm h) = Some sec"

   535 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   536 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   537 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   538 

   539 lemma init_shm_has_ctxt':

   540   "init_sectxt_of_obj (O_shm h) = None \<Longrightarrow> h \<notin> init_shms"

   541 by (rule notI, drule init_shm_has_ctxt, simp)

   542 *)

   543 

   544 lemma init_msgq_has_ctxt:

   545   "q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"

   546 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   547 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   548 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

   549 

   550 lemma init_msgq_has_ctxt':

   551   "init_sectxt_of_obj (O_msgq q) = None \<Longrightarrow> q \<notin> init_msgqs"

   552 by (rule notI, drule init_msgq_has_ctxt, simp)

   553 

   554 lemma init_msg_has_ctxt:

   555   "\<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"

   556 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   557 apply (rule conjI, rule init_obj_has_user, simp add:is_init_dir_props)

   558 by (drule init_alive_intros, simp, drule init_obj_has_type, clarsimp)

   559 

   560 lemma init_msg_has_ctxt':

   561   "init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"

   562 by (auto dest:init_msg_has_ctxt)

   563 

   564 lemma init_rootf_has_ctxt:

   565   "\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"

   566 apply (rule init_dir_has_ctxt, simp add:is_init_dir_def split:option.splits)

   567 using root_is_dir by auto

   568 

   569 lemma init_rootf_has_ctxt':

   570   "init_sectxt_of_obj (O_dir []) = None \<Longrightarrow> False" 

   571 using init_rootf_has_ctxt by auto

   572 

   573 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt

   574   init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) init_msgq_has_ctxt

   575   init_msg_has_ctxt init_rootf_has_ctxt

   576 

   577 lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'

   578   init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) init_msgq_has_ctxt'

   579   init_msg_has_ctxt' init_rootf_has_ctxt'

   580 

   581 lemma sec_of_root_valid:

   582   "init_sectxt_of_obj (O_dir []) = Some sec_of_root"

   583 using init_rootf_has_ctxt

   584 by (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits)

   585 

   586 lemma sec_of_root_is_tuple:

   587   "\<exists> u t. sec_of_root = (u, R_object, t)"

   588 using sec_of_root_valid

   589 by (auto simp:sec_of_root_def init_sectxt_of_obj_def split:option.splits)

   590 

   591 lemma sroot_valid:

   592   "init_cf2sfile [] = Some sroot"

   593 by (simp add:init_cf2sfile_def)

   594 

   595 lemma sroot_valid':

   596   "cf2sfile s [] = Some sroot"

   597 by (simp add:cf2sfile_def)  

   598 

   599 lemma init_sectxt_prop:

   600   "sectxt_of_obj [] obj = init_sectxt_of_obj obj"

   601 apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)

   602 apply (case_tac [!] obj, simp+)

   603 done

   604 

   605 lemma init_sectxt_prop2:

   606   "init_sectxt_of_obj obj = Some sec \<Longrightarrow> init_alive obj"

   607 by (case_tac obj, auto simp:init_sectxt_of_obj_def split:option.splits dest:init_type_has_obj)

   608 

   609 lemma init_dir_has_seclist:

   610   "is_init_dir f \<Longrightarrow> \<exists> seclist. get_parentfs_ctxts [] f = Some seclist"

   611 apply (induct f)

   612 apply (simp only:get_parentfs_ctxts.simps init_sectxt_prop)

   613 using init_rootf_has_ctxt apply (auto)[1]

   614 apply (frule init_parent_file_prop3', simp del:get_parentfs_ctxts.simps)

   615 apply (erule exE, drule init_dir_has_ctxt)

   616 by (auto simp add:init_sectxt_prop)

   617 

   618 lemma is_init_file_dir_prop1:

   619   "is_init_dir f \<Longrightarrow> \<not> is_init_file f"

   620 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   621 

   622 lemma is_init_file_dir_prop2:

   623   "is_init_file f \<Longrightarrow> \<not> is_init_dir f"

   624 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   625 

   626 lemma is_init_file_dir_prop3:

   627   "\<lbrakk>is_init_dir f; is_init_file f\<rbrakk> \<Longrightarrow> False"

   628 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   629 

   630 lemma is_init_file_dir_prop4:

   631   "\<lbrakk>is_init_file f; is_init_dir f\<rbrakk> \<Longrightarrow> False"

   632 by (auto simp:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)

   633 

   634 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

   635 

   636 lemma init_dir_has_sfile:

   637   "is_init_dir f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"

   638 apply (case_tac f)

   639 using init_rootf_has_ctxt apply (auto)[1]

   640 apply (simp add:sec_of_root_valid sroot_valid sroot_def)

   641 apply (simp, frule init_parent_file_prop3')

   642 apply (frule_tac f = list in init_dir_has_seclist)

   643 apply (frule_tac f = list in init_dir_has_ctxt)

   644 apply (frule_tac f = "a # list" in init_dir_has_ctxt)

   645 apply ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def split:option.splits)

   646 by (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)

   647 

   648 lemma init_file_has_sfile:

   649   "is_init_file f \<Longrightarrow> \<exists> sf. init_cf2sfile f = Some sf"

   650 apply (case_tac f)

   651 apply (simp, drule root_is_init_dir', simp)

   652 apply (simp, frule init_parent_file_prop2')

   653 apply (frule_tac f = list in init_dir_has_seclist)

   654 apply (frule_tac f = list in init_dir_has_ctxt)

   655 apply (frule_tac f = "a # list" in init_file_has_ctxt)

   656 by ((erule exE)+, case_tac sec, auto simp:init_cf2sfile_def)

   657   

   658 (*

   659 lemma init_shm_has_sshm:

   660   "h \<in> init_shms \<Longrightarrow> \<exists> sh. init_ch2sshm h = Some sh"

   661 apply (drule init_shm_has_ctxt)

   662 by (auto simp add:init_ch2sshm_def)

   663 *)

   664 

   665 lemma init_proc_has_sproc:

   666   "p \<in> init_procs \<Longrightarrow> \<exists> sp. init_cp2sproc p = Some sp"

   667 apply (frule init_proc_has_ctxt, erule exE)

   668 apply (simp add:init_cp2sproc_def)

   669 by (case_tac sec, simp+)

   670 

   671 lemma init_cqm2sms_has_sms_aux:

   672   "\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"

   673 by (induct ms, auto split:option.splits simp:init_cm2smsg_def)

   674 

   675 lemma init_cqm2sms_has_sms: 

   676   "q \<in> init_msgqs \<Longrightarrow> \<exists> sms. init_cqm2sms q (init_msgs_of_queue q) = Some sms"

   677 apply (rule init_cqm2sms_has_sms_aux)

   678 using init_msg_has_ctxt by auto

   679 

   680 lemma init_msgq_has_smsgq:

   681   "q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"

   682 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)

   683 apply (simp add:init_cq2smsgq_def)

   684 by (case_tac sec, simp+)

   685 

   686 lemma cf2sfile_nil_prop:

   687   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"

   688 apply (case_tac f)

   689 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)

   690 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')

   691 apply (auto simp:is_init_file_def is_init_dir_def is_file_nil split:option.splits t_inode_tag.splits 

   692             dest:init_file_has_inum inof_has_file_tag)

   693 done

   694 

   695 lemma init_sec_file_dir:

   696   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"

   697 apply (drule init_sectxt_prop2)+

   698 apply (auto intro:init_file_dir_conflict)

   699 done

   700 

   701 lemma cf2sfile_nil_prop3:

   702   "is_init_file f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"

   703 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)

   704 

   705 lemma cf2sfile_nil_prop4:

   706   "is_init_dir f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"

   707 apply (frule init_file_dir_conflict2)

   708 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)

   709 

   710 lemma cfs2sfiles_nil_prop:

   711   "f \<in> init_files \<Longrightarrow> cf2sfiles [] f = init_cf2sfiles f"

   712 apply (simp add:cf2sfiles_def init_cf2sfiles_def)

   713 apply (rule set_eqI, rule iffI, auto split:if_splits)

   714 apply (rule_tac x = f' in bexI, simp add:same_inode_nil_prop cf2sfile_nil_prop)

   715 apply (drule init_same_inode_prop2, simp)

   716 apply (simp add:cf2sfile_nil_prop)

   717 apply (simp add:same_inode_nil_prop)

   718 apply (rule_tac x = f' in bexI)

   719 apply (drule init_same_inode_prop2, simp)

   720 apply ( simp add:same_inode_nil_prop cf2sfile_nil_prop)

   721 apply (simp add:same_inode_nil_prop)

   722 done

   723 

   724 lemma cfd2sfd_nil_prop:

   725   "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"

   726 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)

   727 apply (frule init_filefd_prop5, drule init_filefd_prop1, drule cf2sfile_nil_prop)

   728 by (auto split:option.splits)

   729 

   730 lemma cpfd2sfds_nil_prop:

   731   "cpfd2sfds [] p = init_cfds2sfds p"

   732 apply (simp only:cpfd2sfds_def init_cfds2sfds_def proc_file_fds_def init_proc_file_fds_def)

   733 apply (rule set_eqI, rule iffI)

   734 apply (drule CollectD, erule bexE, drule CollectD, erule exE)

   735 apply (rule CollectI, rule_tac x = fd in bexI) defer

   736 apply (rule CollectI, rule_tac x = f in exI, simp)

   737 apply (drule CollectD, erule bexE, drule CollectD, erule exE)

   738 apply (rule CollectI, rule_tac x = fd in bexI) defer

   739 apply (rule CollectI, rule_tac x = f in exI)

   740 using cfd2sfd_nil_prop 

   741 by auto

   742 

   743 (*

   744 lemma ch2sshm_nil_prop:

   745   "h \<in> init_shms \<Longrightarrow> ch2sshm [] h = init_ch2sshm h"

   746 by (simp add:ch2sshm_def init_sectxt_prop init_ch2sshm_def)

   747 

   748 lemma cph2spshs_nil_prop:

   749   "cph2spshs [] p = init_cph2spshs p"

   750 apply (auto simp add:init_cph2spshs_def cph2spshs_def init_sectxt_prop)

   751 apply (rule_tac x = h in exI, simp) defer

   752 apply (rule_tac x = h in exI, simp)

   753 by (auto simp:ch2sshm_nil_prop dest:init_procs_has_shm)

   754 *)

   755 

   756 lemma cp2sproc_nil_prop:

   757   "p \<in> init_procs \<Longrightarrow> cp2sproc [] p = init_cp2sproc p"

   758 by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cpfd2sfds_nil_prop (*cph2spshs_nil_prop*)

   759          split:option.splits)

   760 

   761 lemma msg_has_sec_imp_init: 

   762   "init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"

   763 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   764 by (drule init_type_has_obj, simp)

   765 

   766 lemma msgq_has_sec_imp_init:

   767   "init_sectxt_of_obj (O_msgq q) = Some sec \<Longrightarrow> q \<in> init_msgqs"

   768 apply (simp add:init_sectxt_of_obj_def split:option.splits)

   769 by (drule init_type_has_obj, simp)

   770 

   771 lemma cm2smsg_nil_prop:

   772   "cm2smsg [] q m = init_cm2smsg q m"

   773 by (auto simp add:init_sectxt_prop cm2smsg_def init_cm2smsg_def split:option.splits

   774              dest: msg_has_sec_imp_init elim:tainted.cases)

   775 

   776 lemma cqm2sms_nil_prop:

   777   "cqm2sms [] q ms = init_cqm2sms q ms"

   778 apply (induct ms, simp)

   779 by (auto simp add:cm2smsg_def init_sectxt_prop tainted_nil_prop msg_has_sec_imp_init init_cm2smsg_def

   780          split:option.splits)

   781 

   782 lemma cq2smsga_nil_prop:

   783   "cq2smsgq [] q = init_cq2smsgq q"

   784 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop

   785             intro:msgq_has_sec_imp_init split:option.splits)

   786 

   787 lemma co2sobj_nil_prop:

   788   "init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"

   789 apply (case_tac obj)

   790 apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop 

   791                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1

   792                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *)

   793                      same_inode_nil_prop  cm2smsg_nil_prop 

   794             dest:init_same_inode_prop1 

   795                split:option.splits)

   796 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)

   797 done

   798 

   799 lemma s2ss_nil_prop:

   800   "s2ss [] = init_static_state"

   801 using co2sobj_nil_prop init_alive_prop

   802 by (auto simp add:s2ss_def init_static_state_def)

   803 

   804 end

   805 

   806 (*<*)

   807 end

   808 (*>*)