332 lemma init_alive_tcp: "is_init_tcp_sock s \<Longrightarrow> init_alive (O_tcp_sock s)" 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

   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

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

   335 (*

   335 (*

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

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

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

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

   338 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

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

   341 

   341 

   342 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 

   342 lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd 

   344 

   344 

   345 

   345 

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

   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

   347 using init_obj_has_type

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

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

   539 lemma init_shm_has_ctxt':

   539 lemma init_shm_has_ctxt':

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

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

   541 by (rule notI, drule init_shm_has_ctxt, simp)

   541 by (rule notI, drule init_shm_has_ctxt, simp)

   542 *)

   542 *)

   543 

   543 

   544 lemma init_msgq_has_ctxt:

   545 lemma init_msgq_has_ctxt:

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

   546   "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 (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 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 by (drule init_alive_intros, drule init_obj_has_type, clarsimp)

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

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

   559 

   560 

   560 lemma init_msg_has_ctxt':

   561 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   "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 by (auto dest:init_msg_has_ctxt)

   563 

   565 

   564 lemma init_rootf_has_ctxt:

   566 lemma init_rootf_has_ctxt:

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

   567   "\<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)

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

   567 using root_is_dir by auto

   569 using root_is_dir by auto

   569 lemma init_rootf_has_ctxt':

   571 lemma init_rootf_has_ctxt':

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

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

   571 using init_rootf_has_ctxt by auto

   573 using init_rootf_has_ctxt by auto

   572 

   574 

   573 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt

   575 lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt

   576 

   578 

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

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

   580 

   582 

   581 lemma sec_of_root_valid:

   583 lemma sec_of_root_valid:

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

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

   583 using init_rootf_has_ctxt

   585 using init_rootf_has_ctxt

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

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

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

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

   667 apply (frule init_proc_has_ctxt, erule exE)

   669 apply (frule init_proc_has_ctxt, erule exE)

   668 apply (simp add:init_cp2sproc_def)

   670 apply (simp add:init_cp2sproc_def)

   669 by (case_tac sec, simp+)

   671 by (case_tac sec, simp+)

   670 

   672 

   671 lemma init_cqm2sms_has_sms_aux:

   674 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)"

   675   "\<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)

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

   674 

   677 

   675 lemma init_cqm2sms_has_sms: 

   678 lemma init_cqm2sms_has_sms: 

   680 lemma init_msgq_has_smsgq:

   683 lemma init_msgq_has_smsgq:

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

   684   "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)

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

   683 apply (simp add:init_cq2smsgq_def)

   686 apply (simp add:init_cq2smsgq_def)

   684 by (case_tac sec, simp+)

   687 by (case_tac sec, simp+)

   685 

   689 

   686 lemma cf2sfile_nil_prop:

   690 lemma cf2sfile_nil_prop:

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

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

   688 apply (case_tac f)

   692 apply (case_tac f)

   689 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)

   693 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)

   756 lemma cp2sproc_nil_prop:

   760 lemma cp2sproc_nil_prop:

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

   761   "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*)

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

   759          split:option.splits)

   763          split:option.splits)

   760 

   764 

   761 lemma msg_has_sec_imp_init: 

   766 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)"

   767   "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)

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

   764 by (drule init_type_has_obj, simp)

   769 by (drule init_type_has_obj, simp)

   765 

   770 

   781 

   786 

   782 lemma cq2smsga_nil_prop:

   787 lemma cq2smsga_nil_prop:

   783   "cq2smsgq [] q = init_cq2smsgq q"

   788   "cq2smsgq [] q = init_cq2smsgq q"

   784 by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop

   789 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)

   790             intro:msgq_has_sec_imp_init split:option.splits)

   786 

   792 

   787 lemma co2sobj_nil_prop:

   793 lemma co2sobj_nil_prop:

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

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

   789 apply (case_tac obj)

   795 apply (case_tac obj)

   791                      cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1

   797                      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 *)

   798                      is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *)

   794             dest:init_same_inode_prop1 

   800             dest:init_same_inode_prop1 

   795                split:option.splits)

   801                split:option.splits)

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

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

   797 done

   803 done

   798 

   804