205 

   206 lemma enrich_msgq_not_alive:

   207   "\<lbrakk>enrich_not_alive s (E_msgq q') obj; q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   208    \<Longrightarrow> enrich_not_alive (enrich_msgq s q q') (E_msgq q') obj"

   209 apply (case_tac obj)

   210 apply (auto simp:enrich_msgq_cur_fds enrich_msgq_cur_files 

   211   enrich_msgq_cur_procs enrich_msgq_cur_inums enrich_msgq_cur_msgqs enrich_msgq_cur_msgs)

   212 done

   213 

   214 lemma enrich_msgq_no_del:

   215   "\<lbrakk>no_del_event s\<rbrakk> \<Longrightarrow> no_del_event (enrich_msgq s q q')"

   216 apply (induct s, simp)

   217 by (case_tac a, auto)

   218 

   219 lemma nodel_died_proc:

   220   "no_del_event s \<Longrightarrow> \<not> died (O_proc p) s"

   221 apply (induct s, simp)

   222 by (case_tac a, auto)

   223 

   224 lemma cf2sfile_execve:

   225   "\<lbrakk>ff \<in> current_files (Execve p f fds # s); valid (Execve p f fds # s)\<rbrakk>

   226    \<Longrightarrow> cf2sfile (Execve p f fds # s) ff= cf2sfile s ff"

   227 by (auto dest:cf2sfile_other' simp:current_files_simps)

   228 lemma cf2sfile_clone:

   229   "\<lbrakk>ff \<in> current_files (Clone p p' fds # s); valid (Clone p p' fds # s)\<rbrakk>

   230    \<Longrightarrow> cf2sfile (Clone p p' fds # s) ff= cf2sfile s ff"

   231 by (auto dest:cf2sfile_other' simp:current_files_simps)

   232 lemma cf2sfile_ptrace:

   233   "\<lbrakk>ff \<in> current_files (Ptrace p p' # s); valid (Ptrace p p' # s)\<rbrakk>

   234    \<Longrightarrow> cf2sfile (Ptrace p p' # s) ff= cf2sfile s ff"

   235 by (auto dest:cf2sfile_other' simp:current_files_simps)

   236 lemma cf2sfile_readfile:

   237   "\<lbrakk>ff \<in> current_files (ReadFile p fd # s); valid (ReadFile p fd # s)\<rbrakk>

   238    \<Longrightarrow> cf2sfile (ReadFile p fd # s) ff= cf2sfile s ff"

   239 by (auto dest:cf2sfile_other' simp:current_files_simps)

   240 lemma cf2sfile_writefile:

   241   "\<lbrakk>ff \<in> current_files (WriteFile p fd # s); valid (WriteFile p fd # s)\<rbrakk>

   242    \<Longrightarrow> cf2sfile (WriteFile p fd # s) ff= cf2sfile s ff"

   243 by (auto dest:cf2sfile_other' simp:current_files_simps)

   244 lemma cf2sfile_truncate:

   245   "\<lbrakk>ff \<in> current_files (Truncate p f len # s); valid (Truncate p f len # s)\<rbrakk>

   246    \<Longrightarrow> cf2sfile (Truncate p f len # s) ff= cf2sfile s ff"

   247 by (auto dest:cf2sfile_other' simp:current_files_simps)

   248 lemma cf2sfile_createmsgq:

   249   "\<lbrakk>ff \<in> current_files (CreateMsgq p q # s); valid (CreateMsgq p q # s)\<rbrakk>

   250    \<Longrightarrow> cf2sfile (CreateMsgq p q # s) ff= cf2sfile s ff"

   251 by (auto dest:cf2sfile_other' simp:current_files_simps)

   252 lemma cf2sfile_sendmsg:

   253   "\<lbrakk>ff \<in> current_files (SendMsg p q m # s); valid (SendMsg p q m # s)\<rbrakk>

   254    \<Longrightarrow> cf2sfile (SendMsg p q m # s) ff = cf2sfile s ff"

   255 by (auto dest:cf2sfile_other' simp:current_files_simps)

   256 lemma cf2sfile_recvmsg:

   257   "\<lbrakk>ff \<in> current_files (RecvMsg p q m # s); valid (RecvMsg p q m # s)\<rbrakk>

   258    \<Longrightarrow> cf2sfile (RecvMsg p q m # s) ff = cf2sfile s ff"

   259 by (auto dest:cf2sfile_other' simp:current_files_simps)

   260 lemmas cf2sfile_other'' = cf2sfile_recvmsg cf2sfile_sendmsg cf2sfile_createmsgq cf2sfile_truncate

   261   cf2sfile_writefile cf2sfile_readfile cf2sfile_ptrace cf2sfile_clone cf2sfile_execve

   262 

   263 lemma enrich_msgq_prop:

   264   "\<lbrakk>valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>

   265    \<Longrightarrow> valid (enrich_msgq s q q') \<and>

   266        (\<forall> tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and>

   267        (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and> 

   268        (\<forall> tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and> 

   269        (\<forall> tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>

   270        (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"

   271 proof (induct s)

   272   case Nil

   273   thus ?case by (auto)

   274 next

   275   case (Cons e s)

   276   hence vd_cons': "valid (e # s)" and curq_cons: "q \<in> current_msgqs (e # s)"

   277     and curq'_cons: "q' \<notin> current_msgqs (e # s)" and nodel_cons: "no_del_event (e # s)"

   278     and os: "os_grant s e" and grant: "grant s e"  and vd: "valid s"

   279     by (auto dest:vd_cons vt_grant_os vt_grant)

   280   from curq'_cons nodel_cons have curq': "q' \<notin> current_msgqs s" by (case_tac e, auto)

   281   from nodel_cons have nodel: "no_del_event s" by (case_tac e, auto)

   282   from nodel curq' vd Cons

   283   have pre: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q') \<and>

   284      (\<forall>tp. tp \<in> current_procs s \<longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp) \<and>

   285      (\<forall>f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f) \<and>

   286      (\<forall>tq. tq \<in> current_msgqs s \<longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq) \<and>

   287      (\<forall>tp fd. fd \<in> proc_file_fds s tp \<longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd) \<and>

   288      (cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q)"

   289     by auto

   290   

   291   from pre have pre_vd: "q \<in> current_msgqs s \<Longrightarrow> valid (enrich_msgq s q q')" by simp

   292   from pre have pre_sp: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk>

   293     \<Longrightarrow> cp2sproc (enrich_msgq s q q') tp = cp2sproc s tp" by auto

   294   from pre have pre_sf: "\<And> f. \<lbrakk>f \<in> current_files s; q \<in> current_msgqs s\<rbrakk>

   295     \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f" by auto

   296   from pre have pre_sq: "\<And> tq. \<lbrakk>tq \<in> current_msgqs s; q \<in> current_msgqs s\<rbrakk>

   297     \<Longrightarrow> cq2smsgq (enrich_msgq s q q') tq = cq2smsgq s tq" by auto

   298   from pre have pre_sfd: "\<And> tp fd. \<lbrakk>fd \<in> proc_file_fds s tp; q \<in> current_msgqs s\<rbrakk>

   299     \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by auto

   300   hence pre_sfd': "\<And> tp fd f. \<lbrakk>file_of_proc_fd s tp fd = Some f; q \<in> current_msgqs s\<rbrakk>

   301     \<Longrightarrow> cfd2sfd (enrich_msgq s q q') tp fd = cfd2sfd s tp fd" by (auto simp:proc_file_fds_def)

   302   from pre have pre_duq: "q \<in> current_msgqs s \<Longrightarrow> cq2smsgq (enrich_msgq s q q') q' = cq2smsgq s q"

   303     by auto

   304   have vd_enrich:"q \<in> current_msgqs s \<Longrightarrow> valid (e # enrich_msgq s q q')" 

   305     apply (frule pre_vd)

   306     apply (erule_tac s = s and obj' = "E_msgq q'" in enrich_valid_intro_cons)

   307     apply (simp_all add:pre nodel nodel_cons curq_cons vd_cons' vd enrich_msgq_hungs)

   308     apply (clarsimp simp:nodel vd curq' enrich_msgq_alive)

   309     apply (rule allI, rule impI, erule enrich_msgq_not_alive)

   310     apply (simp_all add:curq' curq'_cons nodel vd enrich_msgq_cur_msgs enrich_msgq_filefd enrich_msgq_flagfd)

   311     done

   312   

   313   have q_neq_q': "q' \<noteq> q" using curq'_cons curq_cons by auto

   314 

   315   have vd_enrich_cons: "valid (enrich_msgq (e # s) q q')"

   316   proof-

   317     have "\<And> p q''. e = CreateMsgq p q'' \<Longrightarrow> valid (enrich_msgq (e # s) q q')"

   318     proof-

   319       fix p q'' assume ev: "e = CreateMsgq p q''" 

   320       show "valid (enrich_msgq (e # s) q q')"

   321       proof (cases "q'' = q")

   322         case False with ev vd_enrich curq_cons

   323         show ?thesis by simp

   324       next

   325         case True 

   326         have "os_grant (CreateMsgq p q # s) (CreateMsgq p q')"

   327           using os ev

   328           by (simp add:q_neq_q' curq')

   329         moreover have "grant (CreateMsgq p q # s) (CreateMsgq p q')"

   330           using grant ev

   331           by (auto simp add:sectxt_of_obj_def split:option.splits)

   332         ultimately 

   333         show ?thesis using  ev vd_cons' True 

   334           by (auto intro: valid.intros(2))

   335       qed

   336     qed

   337     moreover have "\<And> p q'' m. \<lbrakk>e = SendMsg p q'' m; q \<in> current_msgqs s\<rbrakk>

   338       \<Longrightarrow> valid (enrich_msgq (e # s) q q')" 

   339     proof-

   340       fix p q'' m assume ev: "e = SendMsg p q'' m" and q_in: "q \<in> current_msgqs s"

   341       show "valid (enrich_msgq (e # s) q q')"

   342       proof (cases "q'' = q")

   343         case False with ev vd_enrich q_in

   344         show ?thesis by simp

   345       next

   346         case True

   347         from grant os ev True obtain psec qsec 

   348           where psec: "sectxt_of_obj s (O_proc p) = Some psec"

   349           and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec"

   350           by (auto split:option.splits)

   351         from psec q_in os ev 

   352         have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec"  

   353           by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits)

   354         from qsec q_in pre_duq vd

   355         have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec"

   356           by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')

   357         show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd 

   358           curq' psec psec' qsec qsec' grant os q_neq_q'

   359           apply (simp, erule_tac valid.intros(2))    

   360           apply (auto simp:q_neq_q' enrich_msgq_cur_msgqs enrich_msgq_cur_procs

   361             enrich_msgq_cur_msgs sectxt_of_obj_simps)

   362           done        

   363       qed

   364     qed

   365     moreover have "\<And> p q'' m. \<lbrakk>e = RecvMsg p q'' m; q \<in> current_msgqs s\<rbrakk>

   366            \<Longrightarrow> valid (enrich_msgq (e # s) q q')"

   367     proof-

   368       fix p q'' m assume ev: "e = RecvMsg p q'' m" and q_in: "q \<in> current_msgqs s"

   369       show "valid (enrich_msgq (e # s) q q')"

   370       proof (cases "q'' = q")

   371         case False with ev vd_enrich q_in

   372         show ?thesis by simp

   373       next

   374         case True

   375         from grant os ev True obtain psec qsec msec

   376           where psec: "sectxt_of_obj s (O_proc p) = Some psec"

   377           and qsec: "sectxt_of_obj s (O_msgq q) = Some qsec"

   378           and msec: "sectxt_of_obj s (O_msg q (hd (msgs_of_queue s q))) = Some msec"

   379           by (auto split:option.splits)

   380         from psec q_in os ev 

   381         have psec':"sectxt_of_obj (enrich_msgq s q q') (O_proc p) = Some psec"  

   382           by (auto dest!:pre_sp simp:cp2sproc_def split:option.splits)

   383         from qsec q_in pre_duq vd

   384         have qsec': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q') = Some qsec"

   385           by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')

   386         from qsec q_in vd

   387         have qsec'': "sectxt_of_obj (enrich_msgq s q q') (O_msgq q) = Some qsec"

   388           apply (frule_tac pre_sq, simp_all)          

   389           by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sms')

   390         from msec q_in pre_duq vd qsec qsec' qsec'' curq' nodel

   391         have msec': "sectxt_of_obj (enrich_msgq s q q') (O_msg q' (hd (msgs_of_queue s q))) = Some msec"

   392           apply (auto simp:cq2smsgq_def  enrich_msgq_cur_msgs

   393             split:option.splits dest!:current_has_sms')

   394           apply (case_tac "msgs_of_queue s q")

   395           using os ev True apply simp

   396           apply (simp add:cqm2sms.simps split:option.splits)

   397           apply (auto simp:cm2smsg_def split:option.splits)

   398           done          

   399         show ?thesis using ev True vd_cons' q_in vd_enrich nodel vd 

   400           curq'  grant os q_neq_q' psec psec' msec msec' qsec qsec'

   401           apply (simp, erule_tac valid.intros(2))

   402           apply (auto simp:enrich_msgq_cur_msgqs enrich_msgq_cur_procs

   403             enrich_msgq_cur_msgs sectxt_of_obj_simps)

   404           done

   405       qed

   406     qed

   407     ultimately

   408     show ?thesis using vd_enrich curq_cons vd_cons'

   409       apply (case_tac e)

   410       apply (auto simp del:enrich_msgq.simps)

   411       apply (auto split:if_splits )

   412       done

   413   qed

   414 

   415   have curpsec: "\<And> tp. \<lbrakk>tp \<in> current_procs s; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> 

   416     sectxt_of_obj (enrich_msgq s q q') (O_proc tp) = sectxt_of_obj s (O_proc tp)"

   417     using pre_vd vd

   418     apply (frule_tac pre_sp, simp)

   419     by (auto simp:cp2sproc_def split:option.splits if_splits dest!:current_has_sec')    

   420   have curfsec: "\<And> f. \<lbrakk>is_file s f; q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> 

   421     sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)"

   422   proof-

   423     fix f 

   424     assume a1: "is_file s f" and a2: "q \<in> current_msgqs s"

   425     from a2 pre_sf pre_vd

   426     have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"

   427       and vd_enrich: "valid (enrich_msgq s q q')"

   428       by auto

   429     hence csf: "cf2sfile (enrich_msgq s q q') f = cf2sfile s f"

   430       using a1 by (auto simp:is_file_in_current)

   431     from a1 obtain sf where csf_some: "cf2sfile s f = Some sf"

   432       apply (case_tac "cf2sfile s f")

   433       apply (drule current_file_has_sfile')

   434       apply (simp add:vd, simp add:is_file_in_current, simp)

   435       done

   436     from a1 have a1': "is_file (enrich_msgq s q q') f"

   437       using vd nodel by (simp add:enrich_msgq_is_file)

   438     show "sectxt_of_obj (enrich_msgq s q q') (O_file f) = sectxt_of_obj s (O_file f)"

   439       using csf csf_some vd_enrich vd a1 a1'

   440       apply (auto simp:cf2sfile_def split:option.splits if_splits)

   441       apply (case_tac f, simp_all)

   442       apply (drule root_is_dir', simp+)

   443       done

   444   qed

   445   have curdsec: "\<And> tf. \<lbrakk>is_dir s tf; q \<in> current_msgqs s\<rbrakk>

   446     \<Longrightarrow> sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)"

   447   proof-  

   448     fix tf 

   449     assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s"

   450     from a2 pre_sf pre_vd

   451     have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"

   452       and vd_enrich: "valid (enrich_msgq s q q')"

   453       by auto

   454     hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf"

   455       using a1 by (auto simp:is_dir_in_current)

   456     from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"

   457       apply (case_tac "cf2sfile s tf")

   458       apply (drule current_file_has_sfile')

   459       apply (simp add:vd, simp add:is_dir_in_current, simp)

   460       done      

   461     from a1 have a1': "is_dir (enrich_msgq s q q') tf"

   462       using enrich_msgq_is_dir vd nodel by simp

   463     from a1 have a3: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)

   464     from a1' vd have a3': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file)  

   465     show "sectxt_of_obj (enrich_msgq s q q') (O_dir tf) = sectxt_of_obj s (O_dir tf)"

   466       using csf csf_some a3 a3' vd_enrich vd

   467       apply (auto simp:cf2sfile_def split:option.splits)

   468       apply (case_tac tf)

   469       apply (simp add:root_sec_remains, simp)

   470       done

   471   qed

   472   have curpsecs: "\<And> tf ctxts'. \<lbrakk>is_dir s tf; q \<in> current_msgqs s; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>

   473     \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'"

   474   proof-

   475     fix tf ctxts'

   476     assume a1: "is_dir s tf" and a2: "q \<in> current_msgqs s" 

   477       and a4: "get_parentfs_ctxts s tf = Some ctxts'"

   478     from a2 pre

   479     have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_msgq s q q') f = cf2sfile s f"

   480       and vd_enrich': "valid (enrich_msgq s q q')"

   481       by auto

   482     hence csf: "cf2sfile (enrich_msgq s q q') tf = cf2sfile s tf"

   483       using a1 by (auto simp:is_dir_in_current)

   484     from a1 obtain sf where csf_some: "cf2sfile s tf = Some sf"

   485       apply (case_tac "cf2sfile s tf")

   486       apply (drule current_file_has_sfile')

   487       apply (simp add:vd, simp add:is_dir_in_current, simp)

   488       done      

   489     from a1 have a1': "is_dir (enrich_msgq s q q') tf"

   490       using enrich_msgq_is_dir vd nodel by simp

   491     from a1 have a5: "\<not> is_file s tf" using vd by (simp add:is_dir_not_file)

   492     from a1' vd have a5': "\<not> is_file (enrich_msgq s q q') tf" by (simp add:is_dir_not_file) 

   493     

   494     from a1' pre_vd a2 obtain ctxts 

   495       where a3: "get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts"

   496       apply (case_tac "get_parentfs_ctxts (enrich_msgq s q q') tf")

   497       apply (drule get_pfs_secs_prop', simp+)

   498       done

   499     moreover have "set ctxts = set ctxts'"

   500     proof (cases tf)

   501       case Nil          

   502       with a3 a4 vd vd_enrich'

   503       show ?thesis

   504         by (simp add:get_parentfs_ctxts.simps root_sec_remains split:option.splits)

   505     next

   506       case (Cons a ff)

   507       with csf csf_some a5 a5' vd_enrich' vd a3 a4

   508       show ?thesis

   509         apply (auto simp:cf2sfile_def split:option.splits if_splits)

   510         done

   511     qed

   512     ultimately 

   513     show "\<exists> ctxts. get_parentfs_ctxts (enrich_msgq s q q') tf = Some ctxts \<and> set ctxts = set ctxts'"

   514       by auto        

   515   qed

   516     

   517   have psec_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> 

   518     sectxt_of_obj (enrich_msgq (e # s) q q') (O_proc tp) = sectxt_of_obj (e # s) (O_proc tp)"

   519     using curq_cons vd_enrich_cons vd_cons' os pre_vd nodel_cons vd

   520     apply (case_tac e)

   521     apply (auto intro:curpsec simp:sectxt_of_obj_simps)

   522     apply (frule curpsec, simp, frule curfsec, simp)    

   523     apply (auto split:option.splits)[1]

   524     apply (frule vd_cons) defer apply (frule vd_cons)

   525     apply (auto intro:curpsec simp:sectxt_of_obj_simps)

   526     done

   527   

   528 

   529   have sf_cons: "\<And> f. f \<in> current_files (e # s) \<Longrightarrow> cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   530   proof-

   531     fix f

   532     assume a1: "f \<in> current_files (e # s)"

   533     hence a1': "f \<in> current_files (enrich_msgq (e # s) q q')"

   534       using nodel_cons os vd vd_cons' vd_enrich_cons

   535       apply (case_tac e)

   536       apply (auto simp:current_files_simps enrich_msgq_cur_files dest:is_file_in_current split:option.splits)

   537       done

   538     have b1: "\<And> p f' flags fd opt. e = Open p f' flags fd opt \<Longrightarrow> 

   539       cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   540     proof-

   541       fix p f' flags fd opt 

   542       assume ev: "e = Open p f' flags fd opt"

   543       show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   544       proof (cases opt)

   545         case None

   546         with a1 a1' ev vd_cons' vd_enrich_cons curq_cons

   547         show ?thesis

   548           apply (simp add:cf2sfile_open_none)

   549           apply (simp add:pre_sf current_files_simps)

   550           done

   551       next

   552         case (Some inum)

   553         show ?thesis

   554         proof (cases "f = f'")

   555           case False

   556           with a1 a1' ev vd_cons' vd_enrich_cons curq_cons Some

   557           show ?thesis

   558             apply (simp add:cf2sfile_open)

   559             apply (simp add:pre_sf current_files_simps)

   560             done

   561         next

   562           case True

   563           with vd_cons' ev os Some

   564           obtain pf where pf: "parent f = Some pf" by auto

   565           then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"

   566             using os vd ev Some True

   567             apply (case_tac "get_parentfs_ctxts s pf")

   568             apply (drule get_pfs_secs_prop', simp, simp)

   569             apply auto

   570             done

   571             

   572           have "sectxt_of_obj (Open p f' flags fd (Some inum) # enrich_msgq s q q') (O_file f') = 

   573                 sectxt_of_obj (Open p f' flags fd (Some inum) # s) (O_file f')"

   574             using Some vd_enrich_cons vd_cons' ev pf True os curq_cons

   575             by (simp add:sectxt_of_obj_simps curpsec curdsec)

   576           moreover 

   577           have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"

   578             using curq_cons ev pf Some True os 

   579             by (simp add:curdsec)

   580           moreover

   581           have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"

   582             using curq_cons ev pf Some True os vd psecs

   583             apply (case_tac "get_parentfs_ctxts s pf")

   584             apply (drule get_pfs_secs_prop', simp+)

   585             apply (rule curpsecs, simp+)

   586             done

   587           then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"

   588             and psecs_eq: "set ctxts' = set ctxts" by auto

   589           ultimately show ?thesis

   590             using a1 a1' ev vd_cons' vd_enrich_cons Some True pf psecs

   591             by (simp add:cf2sfile_open split:option.splits)

   592         qed

   593       qed

   594     qed

   595     have b2: "\<And> p f' inum. e = Mkdir p f' inum \<Longrightarrow> 

   596       cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   597     proof-

   598       fix p f' inum

   599       assume ev: "e = Mkdir p f' inum"

   600       show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   601       proof (cases "f' = f")

   602         case False

   603         with a1 a1' ev vd_cons' vd_enrich_cons curq_cons

   604         show ?thesis

   605           apply (simp add:cf2sfile_mkdir)

   606           apply (simp add:pre_sf current_files_simps)

   607           done

   608       next

   609         case True

   610         with vd_cons' ev os

   611         obtain pf where pf: "parent f = Some pf" by auto

   612         then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"

   613           using os vd ev True

   614           apply (case_tac "get_parentfs_ctxts s pf")

   615           apply (drule get_pfs_secs_prop', simp, simp)

   616           apply auto

   617           done

   618 

   619         have "sectxt_of_obj (Mkdir p f' inum # enrich_msgq s q q') (O_dir f') = 

   620           sectxt_of_obj (Mkdir p f' inum # s) (O_dir f')"

   621           using vd_enrich_cons vd_cons' ev pf True os curq_cons

   622           by (simp add:sectxt_of_obj_simps curpsec curdsec)

   623         moreover 

   624         have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"

   625           using curq_cons ev pf True os 

   626           by (simp add:curdsec)

   627         moreover

   628         have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"

   629           using curq_cons ev pf True os vd psecs

   630           apply (case_tac "get_parentfs_ctxts s pf")

   631           apply (drule get_pfs_secs_prop', simp+)

   632           apply (rule curpsecs, simp+)

   633           done

   634         then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"

   635           and psecs_eq: "set ctxts' = set ctxts" by auto

   636         ultimately show ?thesis

   637           using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs

   638           apply (simp add:cf2sfile_mkdir split:option.splits)

   639           done

   640       qed

   641     qed

   642     have b3: "\<And> p f' f''. e = LinkHard p f' f'' \<Longrightarrow> 

   643       cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   644     proof-

   645       fix p f' f''

   646       assume ev: "e = LinkHard p f' f''"

   647       show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   648       proof (cases "f'' = f")

   649         case False

   650         with a1 a1' ev vd_cons' vd_enrich_cons curq_cons

   651         show ?thesis

   652           apply (simp add:cf2sfile_linkhard)

   653           apply (simp add:pre_sf current_files_simps)

   654           done

   655       next

   656         case True

   657         with vd_cons' ev os

   658         obtain pf where pf: "parent f = Some pf" by auto

   659         then obtain ctxts where psecs: "get_parentfs_ctxts s pf = Some ctxts"

   660           using os vd ev True

   661           apply (case_tac "get_parentfs_ctxts s pf")

   662           apply (drule get_pfs_secs_prop', simp, simp)

   663           apply auto

   664           done

   665 

   666         have "sectxt_of_obj (LinkHard p f' f'' # enrich_msgq s q q') (O_file f) = 

   667           sectxt_of_obj (LinkHard p f' f'' # s) (O_file f)"

   668           using vd_enrich_cons vd_cons' ev pf True os curq_cons

   669           by (simp add:sectxt_of_obj_simps curpsec curdsec)

   670         moreover 

   671         have "sectxt_of_obj (enrich_msgq s q q') (O_dir pf) = sectxt_of_obj s (O_dir pf)"

   672           using curq_cons ev pf True os 

   673           by (simp add:curdsec)

   674         moreover

   675         have "\<exists> ctxts'. get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts' \<and> set ctxts' = set ctxts"

   676           using curq_cons ev pf True os vd psecs

   677           apply (case_tac "get_parentfs_ctxts s pf")

   678           apply (drule get_pfs_secs_prop', simp+)

   679           apply (rule curpsecs, simp+)

   680           done

   681         then obtain ctxts' where psecs': "get_parentfs_ctxts (enrich_msgq s q q') pf = Some ctxts'"

   682           and psecs_eq: "set ctxts' = set ctxts" by auto

   683         ultimately show ?thesis

   684           using a1 a1' ev vd_cons' vd_enrich_cons True pf psecs

   685           apply (simp add:cf2sfile_linkhard split:option.splits)

   686           done

   687       qed

   688     qed

   689     show "cf2sfile (enrich_msgq (e # s) q q') f = cf2sfile (e # s) f"

   690       apply (case_tac e)

   691       prefer 6 apply (erule b1)

   692       prefer 11 apply (erule b2)

   693       prefer 11 apply (erule b3)

   694       apply (simp_all only:b1 b2 b3)

   695       using a1' a1 vd_enrich_cons vd_cons' curq_cons nodel_cons 

   696       apply (simp_all add:cf2sfile_other'' cf2sfile_simps enrich_msgq.simps no_del_event.simps split:if_splits)

   697       apply (simp_all add:pre_sf cf2sfile_other' current_files_simps split:if_splits)

   698       apply (drule vd_cons, simp add:cf2sfile_other', drule pre_sf, simp+)+

   699       done

   700   qed

   701   

   702   have sfd_cons:"\<And> tp fd f. file_of_proc_fd (e # s) tp fd = Some f \<Longrightarrow> 

   703     cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"

   704   proof-

   705     fix tp fd f

   706     assume a1: "file_of_proc_fd (e # s) tp fd = Some f"

   707     hence a1': "file_of_proc_fd (enrich_msgq (e # s) q q') tp fd = Some f"

   708       using nodel_cons vd_enrich os vd_cons'

   709       apply (case_tac e, auto simp:enrich_msgq_filefd simp del:enrich_msgq.simps)

   710       done

   711     have b1: "\<And> p f' flags fd' opt. e = Open p f' flags fd' opt \<Longrightarrow> 

   712       cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"

   713     proof-

   714       fix p f' flags fd' opt

   715       assume ev: "e = Open p f' flags fd' opt"

   716       have c1': "file_of_proc_fd (Open p f' flags fd' opt # s) tp fd = Some f"

   717         using a1' ev a1 by (simp split:if_splits)

   718       show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"        thm cfd2sfd_open

   719       proof (cases "tp = p \<and> fd = fd'")

   720         case False

   721         show ?thesis using ev vd_enrich_cons vd_cons' a1' a1 False curq_cons

   722           apply (simp add:cfd2sfd_open split:if_splits del:file_of_proc_fd.simps)

   723           apply (rule conjI, rule impI, simp)

   724           apply (rule conjI, rule impI, simp)

   725           apply (auto simp: False  intro!:pre_sfd' split:if_splits)

   726           done

   727       next

   728         case True

   729         have "f' \<in> current_files (Open p f' flags fd' opt # s)" using ev vd_cons' os

   730           by (auto simp:current_files_simps is_file_in_current split:option.splits) 

   731         hence "cf2sfile (Open p f' flags fd' opt # enrich_msgq s q q') f' 

   732           = cf2sfile (Open p f' flags fd' opt # s) f'"

   733           using sf_cons ev by auto

   734         moreover have "sectxt_of_obj (enrich_msgq s q q') (O_proc p) = sectxt_of_obj s (O_proc p)"

   735           apply (rule curpsec)

   736           using os ev curq_cons   

   737           by (auto split:option.splits)

   738         ultimately show ?thesis

   739           using ev True a1 a1' vd_enrich_cons vd_cons'

   740           apply (simp add:cfd2sfd_open sectxt_of_obj_simps del:file_of_proc_fd.simps)

   741           done

   742       qed

   743     qed

   744     show "cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"

   745       apply (case_tac e)

   746       prefer 6 apply (erule b1)

   747       using a1' a1 vd_enrich_cons vd_cons' curq_cons

   748       apply (simp_all only:cfd2sfd_simps enrich_msgq.simps)

   749       apply (auto simp:cfd2sfd_simps pre_sfd' dest:vd_cons cfd2sfd_other split:if_splits)

   750       done

   751   qed

   752 

   753   thm psec_cons

   754   thm cp2sproc_def

   755   have pfds_cons: "\<And> tp. tp \<in> current_procs (e # s) \<Longrightarrow> 

   756     cpfd2sfds (enrich_msgq (e # s) q q') tp = cpfd2sfds (e # s) tp"

   757     apply (auto simp add:cpfd2sfds_def)

   758     sorry

   759   

   760   have "\<forall>tp fd. fd \<in> proc_file_fds (e # s) tp \<longrightarrow> cfd2sfd (enrich_msgq (e # s) q q') tp fd = cfd2sfd (e # s) tp fd"

   761     by (auto simp:proc_file_fds_def elim!:sfd_cons)

   762   moreover 

   763   have "\<forall>tp. tp \<in> current_procs (e # s) \<longrightarrow> cp2sproc (enrich_msgq (e # s) q q') tp = cp2sproc (e # s) tp"

   764     apply (auto simp:cp2sproc_def pfds_cons psec_cons split:option.splits)

   765     sorry

   766   moreover 

   767   have "\<forall>tq. tq \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_msgq (e # s) q q') tq = cq2smsgq (e # s) tq"

   768     sorry

   769   moreover 

   770   have "cq2smsgq (enrich_msgq (e # s) q q') q' = cq2smsgq (e # s) q"

   771     sorry

   772   ultimately show ?case using vd_enrich_cons sf_cons

   773     by auto

   774 qed

   775 

   776 

   777 thm cp2sproc_def