259   

   260   from pre have pre_vd: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by simp

   261   have vd_enrich:"is_created_proc s p \<Longrightarrow> valid (e # enrich_proc s p p')" 

   262     apply (frule pre_vd)

   263     apply (erule_tac s = s and obj' = "E_proc p'" in enrich_valid_intro_cons)

   264     apply (simp_all add: pre nodel_cons all_procs_cons vd_cons')

   265     apply (clarsimp simp:enrich_proc_alive nodel all_procs vd)

   266     apply (rule allI, rule impI, erule enrich_proc_not_alive)

   267     apply (simp_all add:nodel all_procs vd enrich_proc_hungs enrich_proc_cur_msgs)

   268     apply ((rule allI| rule impI)+, erule enrich_proc_filefd)

   269     apply (simp_all add:nodel all_procs vd)

   270     apply ((rule allI| rule impI)+, erule enrich_proc_flagfd)

   271     apply (simp_all add:nodel all_procs vd)

   272     done  

   521             (* create new file, grant only check pf's SEARCH permission, not newfile itself, so we make assumptions of this case in the locale *)

   653   have sec_proc:

   654     "\<And> tp. \<lbrakk>tp \<in> current_procs s; is_created_proc s p\<rbrakk> 

   655     \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_proc tp) = sectxt_of_obj s (O_proc tp)"

   656     using pre 

   657     apply (clarsimp)

   658     apply (erule_tac x = tp in allE, auto simp:cp2sproc_def split:option.splits)

   659     done

   671     from a1 have a1'': "f \<in> current_files (e # enrich_proc s p p')"

   672       using vd_cons' nodel_cons os vd vd_enrich created_cons

   673       apply (case_tac e)

   674       apply (auto simp:enrich_proc_cur_files current_files_simps is_created_proc_simps

   675         dest:is_file_in_current is_dir_in_current split:option.splits)

   676       done

   677     

   678     have sec_dir:

   679       "\<And> tf. \<lbrakk>is_dir s tf; is_created_proc s p\<rbrakk>

   680       \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"

   681     proof-

   682       fix tf 

   683       assume a1: "is_dir s tf" and a2: "is_created_proc s p"

   684       from a2 pre

   685       have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"

   686         and vd_enrich: "valid (enrich_proc s p p')"

   687         by auto

   688       hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"

   689         using a1 by (auto simp:is_dir_in_current)

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

   691         apply (case_tac "cf2sfile s tf")

   692         apply (drule current_file_has_sfile')

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

   694         done      

   695       from a1 have a1': "is_dir (enrich_proc s p p') tf"

   696         using enrich_proc_is_dir vd nodel all_procs by simp

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

   698       from a1' vd have a3': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file)  

   699       show "sectxt_of_obj (enrich_proc s p p') (O_dir tf) = sectxt_of_obj s (O_dir tf)"

   700         using csf csf_some a3 a3' vd_enrich vd

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

   702         apply (case_tac tf)

   703         apply (simp add:root_sec_remains, simp)

   704         done

   705     qed

   706     have sec_file:

   707       "\<And> tf. \<lbrakk>is_file s tf; is_created_proc s p\<rbrakk>

   708       \<Longrightarrow> sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"

   709     proof-

   710       fix tf 

   711       assume a1: "is_file s tf" and a2: "is_created_proc s p"

   712       from a2 pre

   713       have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"

   714         and vd_enrich: "valid (enrich_proc s p p')"

   715         by auto

   716       hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"

   717         using a1 by (auto simp:is_file_in_current)

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

   719         apply (case_tac "cf2sfile s tf")

   720         apply (drule current_file_has_sfile')

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

   722         done

   723       from a1 have a1': "is_file (enrich_proc s p p') tf"

   724         using vd nodel all_procs by (simp add:enrich_proc_is_file)

   725       show "sectxt_of_obj (enrich_proc s p p') (O_file tf) = sectxt_of_obj s (O_file tf)"

   726         using csf csf_some vd_enrich vd a1 a1'

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

   728         apply (case_tac tf, simp_all)

   729         apply (drule root_is_dir', simp+)

   730         done

   731     qed

   732     have secs_dir:

   733       "\<And> tf ctxts'. \<lbrakk>is_dir s tf; is_created_proc s p; get_parentfs_ctxts s tf = Some ctxts'\<rbrakk>

   734        \<Longrightarrow> \<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"

   735     proof-

   736       fix tf ctxts'

   737       assume a1: "is_dir s tf" and a2: "is_created_proc s p" 

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

   739       from a2 pre

   740       have pre': "\<And>f. f \<in> current_files s \<Longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f"

   741         and vd_enrich': "valid (enrich_proc s p p')"

   742         by auto

   743       hence csf: "cf2sfile (enrich_proc s p p') tf = cf2sfile s tf"

   744         using a1 by (auto simp:is_dir_in_current)

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

   746         apply (case_tac "cf2sfile s tf")

   747         apply (drule current_file_has_sfile')

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

   749         done      

   750       from a1 have a1': "is_dir (enrich_proc s p p') tf"

   751         using enrich_proc_is_dir vd nodel all_procs by simp

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

   753       from a1' vd have a5': "\<not> is_file (enrich_proc s p p') tf" by (simp add:is_dir_not_file) 

   755       from a1' pre_vd a2 obtain ctxts 

   756         where a3: "get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts"

   757         apply (case_tac "get_parentfs_ctxts (enrich_proc s p p') tf")

   758         apply (drule get_pfs_secs_prop', simp+)

   759         done

   760       moreover have "set ctxts = set ctxts'"

   761       proof (cases tf)

   762         case Nil          

   763         with a3 a4 vd vd_enrich'

   764         show ?thesis

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

   766       next

   767         case (Cons a ff)

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

   769         show ?thesis

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

   771           done

   772       qed

   773       ultimately 

   774       show "\<exists> ctxts. get_parentfs_ctxts (enrich_proc s p p') tf = Some ctxts \<and> set ctxts = set ctxts'"

   775         by auto        

   776     qed

   777     have b1: "\<And> proc f' flags fd' opt. e = Open proc f' flags fd' opt 

   778       \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"

   779     proof-

   780       fix proc f' flags fd' opt

   781       assume ev: "e = Open proc f' flags fd' opt"

   782       have b1': "cf2sfile (e # enrich_proc s p p') f = cf2sfile (e # s) f"

   783       proof (cases opt)

   784         case None

   785         thus ?thesis

   786           using vd_cons' vd_enrich a1 created_cons 

   787           by (simp add:cf2sfile_open_none ev pre_sf 

   788             is_created_proc_simps current_files_simps)

   789       next

   790         case (Some inum)

   791         show ?thesis

   792         proof (cases "f' = f")

   793           case True

   794           from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"

   795             apply (case_tac "cf2sfile (e # s) f")

   796             apply (drule current_file_has_sfile')

   797             apply (simp add:vd_cons', simp, simp)

   798             done

   799           from a1 ev os Some True obtain pf where parent: "parent f = Some pf"

   800             and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto

   801           have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   802             using ev True Some

   803             by (simp add:current_files_open)

   804           thus ?thesis using ev Some csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in

   805             apply (simp add:is_created_proc_simps cf2sfile_open)

   806             apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)

   807             apply (drule_tac tf = pf in secs_dir, simp+) 

   808             apply (erule exE, erule conjE, simp)

   809             apply (case_tac aa, simp)

   810             done

   811         next

   812           case False

   813           have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   814             using ev False Some vd_enrich a1 created_cons nodel vd

   815             by (simp add:current_files_open is_created_proc_simps enrich_proc_cur_files)

   816           with ev Some a1 vd_enrich vd_cons' created_cons False

   817           show ?thesis

   818             apply (simp add:is_created_proc_simps cf2sfile_open)

   819             apply (simp add:current_files_simps pre_sf)

   820             done

   821         qed

   822       qed

   823       show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f" 

   824         using ev vd_enrich_cons

   825         apply simp

   826         apply (rule conjI, rule impI)

   827         apply (simp add:cf2sfile_open_none)

   828         using b1' apply (auto dest:vd_cons)

   829         done

   830     qed

   831     have b2: "\<And> proc f' inum. e = Mkdir proc f' inum

   832       \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"

   833     proof-

   834       fix proc f' inum

   835       assume ev: "e = Mkdir proc f' inum"

   836       

   837       show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"

   838       proof (cases "f' = f")

   839         case True

   840         from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"

   841           apply (case_tac "cf2sfile (e # s) f")

   842           apply (drule current_file_has_sfile')

   843           apply (simp add:vd_cons', simp, simp)

   844           done

   845         from a1 ev os True obtain pf where parent: "parent f = Some pf"

   846           and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto

   847         have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   848           using ev True

   849           by (simp add:current_files_mkdir)

   850         thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in

   851           apply (simp add:is_created_proc_simps cf2sfile_mkdir)

   852           apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)

   853           apply (drule_tac tf = pf in secs_dir, simp+) 

   854           apply (erule exE, erule conjE, simp)

   855           apply (case_tac aa, simp)

   856           done

   857       next

   858         case False

   859         have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   860           using ev False vd_enrich a1 created_cons nodel vd

   861           by (simp add:current_files_mkdir is_created_proc_simps enrich_proc_cur_files)

   862         with ev a1 vd_enrich vd_cons' created_cons False

   863         show ?thesis

   864           apply (simp add:is_created_proc_simps cf2sfile_mkdir)

   865           apply (simp add:current_files_simps pre_sf)

   866           done

   867       qed

   868     qed

   869     have b3: "\<And> proc f' f''. e = LinkHard proc f' f''

   870       \<Longrightarrow> cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"

   871     proof-

   872       fix proc f' f'' 

   873       assume ev: "e = LinkHard proc f' f''"      

   874       show "cf2sfile (enrich_proc (e # s) p p') f = cf2sfile (e # s) f"

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

   876         case True

   877         from a1 obtain sf where csf: "cf2sfile (e # s) f = Some sf"

   878           apply (case_tac "cf2sfile (e # s) f")

   879           apply (drule current_file_has_sfile')

   880           apply (simp add:vd_cons', simp, simp)

   881           done

   882         from a1 ev os True obtain pf where parent: "parent f'' = Some pf"

   883           and pdir: "is_dir s pf" and proc_in: "proc \<in> current_procs s" by auto

   884         have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   885           using ev True vd_enrich created_cons

   886           by (simp add:current_files_simps is_created_proc_simps)

   887         thus ?thesis using ev csf vd_enrich True created_cons vd_cons' a1 parent pdir proc_in

   888           apply (simp add:is_created_proc_simps cf2sfile_linkhard)

   889           apply (simp add:sectxt_of_obj_simps sec_dir sec_proc split:option.splits)

   890           apply (drule_tac tf = pf in secs_dir, simp+) 

   891           apply (erule exE, erule conjE, simp)

   892           apply (case_tac aa, simp)

   893           done

   894       next

   895         case False

   896         have f_in: "f \<in> current_files (e # enrich_proc s p p')"

   897           using ev False vd_enrich a1 created_cons nodel vd vd_cons'

   898           by (simp add:current_files_linkhard is_created_proc_simps enrich_proc_cur_files)

   899         with ev a1 vd_enrich vd_cons' created_cons False

   900         show ?thesis

   901           apply (simp add:is_created_proc_simps cf2sfile_linkhard)

   902           apply (simp add:current_files_simps pre_sf)

   903           done

   904       qed      

   905     qed

  1044   moreover have "\<forall>q. q \<in> current_msgqs (e # s) \<longrightarrow> cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"

  1045   proof clarify

  1046     fix q

  1047     assume a1: "q \<in> current_msgqs (e # s)"

  1048     from pre have pre_smsgq: "\<And> q. \<lbrakk>q \<in> current_msgqs s; is_created_proc s p\<rbrakk>

  1049       \<Longrightarrow> cq2smsgq (enrich_proc s p p') q = cq2smsgq s q"

  1050       by auto 

  1051     show "cq2smsgq (enrich_proc (e # s) p p') q = cq2smsgq (e # s) q"

  1052       using vd_enrich_cons a1 created_cons nodel_cons vd_cons' os

  1053       apply (case_tac e) 

  1054       apply (auto simp:cq2smsgq_simps cq2smsg_createmsgq is_created_proc_simps sec_proc 

  1055         dest:cq2smsgq_other intro!:pre_smsgq split:if_splits dest:vd_cons)

  1056       

  1057       apply (simp add:sectxt_of_obj_simps split:option.splits)

  1058       

  1059       thm sec_proc

  1060       thm cq2smsgq_simps

  1061       thm cq2smsg_createmsgq

  1062     sorry