3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop

     3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop

   380  split:if_splits option.splits)

   391            split:if_splits option.splits)

   381 

   392 done

   393 

   394 lemma cf2sfile_rmdir:

   395   "\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>

   396    \<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"

   397 apply (frule vd_cons, frule vt_grant_os)

   398 apply (simp add:current_files_simps split:if_splits)

   399 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

   400            split:if_splits option.splits)

   401 done

   402 

   403 lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"

   404 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   405 by (simp add:pfdof_simp2, simp)

   406 

   407 lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"

   408 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   409 by (simp add:pfdof_simp2, simp)

   410 

   411 lemma cf2sfile_closefd:

   412   "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>

   413    \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"

   414 apply (frule vd_cons, frule vt_grant_os)

   415 apply (simp add:current_files_simps split:if_splits option.splits) 

   416 (* costs too much time, but solved

   417 

   418 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 

   419            split:if_splits option.splits  

   420             dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file

   421                  not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file

   422             dest!:current_has_sec')

   423 done

   424 *)

   425 sorry

   385 

   430 (*********** cfd2sfd simpset *********)

   386 

   431 

   387 

   432 lemma cfd2sfd_open1:

   388 

   433   "valid (Open p f flags fd opt # s)

   389 

   434    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 

   390 

   435      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   391 

   436         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   392 

   437       | _ \<Rightarrow> None)"

   393 

   438 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)

   394 

   439 

   395 

   440 lemma cfd2sfd_open_some2:

   396 

   441   "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   397 

   442   \<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"

   398 

   443 apply (frule vd_cons, frule vt_grant_os)

   399 lemma cf2sfile_keep_path: "\<lbrakk>f \<preceq> f'; \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"

   444 apply (frule proc_fd_in_fds, simp)

   400 apply (induct f', simp add:no_junior_def)

   445 apply (frule file_of_proc_fd_in_curf, simp)

   401 apply (case_tac "f = a # f'", simp add:cf2sfile.simps)

   446 apply (case_tac "f = f'", simp)

   402 apply (drule no_junior_noteq, simp, simp add:cf2sfile.simps)

   447 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)

   403 done

   448 apply (case_tac "p = p'", simp)

   404 

   449 apply (rule conjI, rule impI, simp)

   405 lemma ckp'_aux: "\<not> f \<preceq> a # f' \<Longrightarrow> \<not> f \<preceq> f'"

   450 apply (drule cf2sfile_open_some1, simp)

   406 by (auto simp:no_junior_def)

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

   407 

   452 apply simp

   408 lemma cf2sfile_keep_path': "\<lbrakk>\<not> f \<preceq> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'"

   453 apply (drule cf2sfile_open_some1, simp)

   409 apply (induct f', simp add:no_junior_def cf2sfile.simps, rule notI, drule cf2sfile_root_file, simp)

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

   410 apply (case_tac "f = a # f'", simp add:cf2sfile.simps)

   455 done

   411 apply (rule notI)

   456 

   412 apply (frule ckp'_aux, simp, frule parentf_in_current', simp+)

   457 lemma cfd2sfd_open_none2:

   413 apply (case_tac "cf2sfile \<tau> f = cf2sfile \<tau> (a # f')", drule cf2sfile_inj, simp+)

   458   "\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   414 apply (simp add:cf2sfile.simps)

   459   \<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"

   415 by (drule no_junior_noteq, simp+)

   460 apply (frule vd_cons, frule vt_grant_os)

   416 

   461 apply (frule proc_fd_in_fds, simp)

   417 lemma cf2sfile_keep_path'': "\<lbrakk>cf2sfile \<tau> f \<preceq> cf2sfile \<tau> f'; \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; f' \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<preceq> f'"

   462 apply (frule file_of_proc_fd_in_curf, simp)

   418 using cf2sfile_keep_path'

   463 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)

   419 by (auto)

   464 apply (case_tac "p = p'", simp)

   420 

   465 apply (rule conjI, rule impI, simp)

   421 lemma cf2sfile_open_some': "\<lbrakk>f \<in> current_files \<tau>; Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"

   466 apply (drule cf2sfile_open_none)

   422 apply (frule vt_cons')

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

   423 apply (drule vt_grant_os)

   468 apply simp

   424 apply (induct f)

   469 apply (drule cf2sfile_open_none)

   425 apply (simp add:cf2sfile.simps)+

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

   426 apply (frule parentf_in_current', simp)

   471 done

   427 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   472   

   428 done

   473 lemma cfd2sfd_open2:

   429 

   474   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   430 lemma cf2sfile_open_some: "\<lbrakk>Open p f flags fd (Some inum) # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk> 

   475   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"

   431                            \<Longrightarrow> cf2sfile (Open p f flags fd (Some inum) # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"

   476 apply (case_tac opt)

   432 apply (case_tac f, simp)

   477 apply (simp add:cfd2sfd_open_none2)

   433 apply (frule vt_grant_os)

   478 apply (simp add:cfd2sfd_open_some2)

   434 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_open_some')

   479 done

   435 done

   480 

   436 

   481 lemma cfd2sfd_open:

   437 lemma cf2sfile_open_none: "cf2sfile (Open p f flags fd None # \<tau>) f' = cf2sfile \<tau> f'"

   482   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>

   438 apply (induct f')

   483    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 

   439 by (simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)+

   484      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   440 

   485         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   441 lemma cf2sfile_open: "\<lbrakk>Open p f flags fd opt # \<tau> \<in> vt rc_cs; f' \<in> current_files (Open p f flags fd opt # \<tau>)\<rbrakk> \<Longrightarrow> 

   486       | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"

   442                        cf2sfile (Open p f flags fd opt # \<tau>) f' = (

   487 apply (simp split:if_splits)

   443                          if (opt = None) then cf2sfile \<tau> f'

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

   444                          else if (f' = f) then (case (parent f) of

   489 apply (simp add:cfd2sfd_open2)

   445                                                   Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))

   490 apply (rule impI, simp)

   446                                                 | _       \<Rightarrow> [])

   491 done

   447                               else cf2sfile \<tau> f'                                                          )"

   492 

   448 apply (frule vt_grant_os)

   493 lemma cfd2sfd_closefd:

   449 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_open_none cf2sfile_open_some cf2sfile_open_some' split:if_splits option.splits)

   494   "\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>

   450 

   495    \<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd  s p' fd'"

   451 lemma cf2sfile_mkdir_some': "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"

   496 apply (frule vd_cons, frule vt_grant_os)

   452 apply (frule vt_cons', drule vt_grant_os)

   497 apply (frule proc_fd_in_fds, simp)

   453 apply (induct f, (simp add:cf2sfile.simps)+)

   498 apply (frule file_of_proc_fd_in_curf, simp)

   454 apply (frule parentf_in_current', simp)

   499 apply (frule cf2sfile_closefd, simp)

   455 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   500 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   456 done

   501 apply (auto split:option.splits if_splits)

   457 

   502 done

   458 lemma cf2sfile_mkdir_some: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; parent f = Some pf\<rbrakk>

   503 

   459                              \<Longrightarrow> cf2sfile (Mkdir p f inum # \<tau>) f = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))"

   504 lemma cfd2sfd_clone:

   460 apply (case_tac f, simp)

   505   "\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>

   461 apply (frule vt_grant_os)

   506    \<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (

   462 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_mkdir_some')

   507      if (p'' = p') then cfd2sfd s p fd'

   463 done

   508      else cfd2sfd s p'' fd')"

   464 

   509 apply (frule vd_cons, frule vt_grant_os)

   465 lemma cf2sfile_mkdir: "\<lbrakk>Mkdir p f inum # \<tau> \<in> vt rc_cs; f' \<in> current_files (Mkdir p f inum # \<tau>)\<rbrakk> \<Longrightarrow>

   510 apply (frule proc_fd_in_fds, simp)

   466                         cf2sfile (Mkdir p f inum # \<tau>) f' = (

   511 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   467                           if (f' = f) then (case (parent f) of

   512 apply (frule_tac cf2sfile_other', simp+)

   468                                               Some pf \<Rightarrow> (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf))

   513 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   469                                             | _       \<Rightarrow> [])

   514 apply (case_tac "p'' = p'", simp)

   470                           else cf2sfile \<tau> f'               ) "

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

   471 apply (frule vt_grant_os)

   516 apply (simp)

   472 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_mkdir_some cf2sfile_mkdir_some' split:if_splits option.splits)

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

   473 

   518 done

   474 lemma cf2sfile_linkhard_none: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"

   519 

   475 apply (frule vt_cons')

   520 lemma cfd2sfd_execve:

   476 apply (drule vt_grant_os)

   521   "\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>

   477 apply (induct f)

   522    \<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"

   478 apply (simp add:cf2sfile.simps)+

   523 apply (frule vd_cons, frule vt_grant_os)

   479 apply (frule parentf_in_current', simp)

   524 apply (frule proc_fd_in_fds, simp)

   480 apply (auto simp:os_grant.simps index_of_file.simps split:option.splits)

   525 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   481 done

   526 apply (frule_tac cf2sfile_other', simp+)

   482 

   527 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   483 lemma cf2sfile_linkhard_some: 

   528 apply (case_tac "p' = p", simp)

   484   "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; parent f\<^isub>2 = Some pf\<^isub>2\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f\<^isub>2 = (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2))"

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

   485 apply (case_tac f\<^isub>2, simp)

   530 apply (simp)

   486 apply (frule vt_grant_os)

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

   487 apply (simp add:cf2sfile.simps os_grant.simps current_files_simps index_of_file.simps cf2sfile_linkhard_none)

   532 done

   488 done

   533 

   489 

   534 lemma cfd2sfd_kill:

   490 lemma cf2sfile_linkhard: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; f \<in> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>)\<rbrakk> \<Longrightarrow>

   535   "\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>

   491                            cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = (

   536    \<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"

   492                              if (f = f\<^isub>2) then (case (parent f\<^isub>2) of

   537 apply (frule vd_cons, frule vt_grant_os)

   493                                                  Some pf\<^isub>2 \<Rightarrow> SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>2)

   538 apply (frule proc_fd_in_fds, simp)

   494                                                | _        \<Rightarrow> [])

   539 apply (frule proc_fd_in_procs, simp)

   495                              else cf2sfile \<tau> f                 )"

   540 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   496 apply (frule vt_grant_os)

   541 apply (frule_tac cf2sfile_other', simp+)

   497 by (auto simp:os_grant.simps current_files_simps intro:cf2sfile_linkhard_none cf2sfile_linkhard_some split:if_splits option.splits)

   542 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   498 

   543 apply (auto split:option.splits if_splits)

   499 

   544 done

   500 lemma no_junior_aux: "\<not> f\<^isub>2 \<preceq> a # f \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"

   545 

   501 by (auto simp:no_junior_def)

   546 lemma cfd2sfd_exit:

   502 

   547   "\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>

   503 lemma cf2sfile_rename_aux: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f \<noteq> f\<^isub>3 \<and> \<not> f\<^isub>3 \<preceq> f"

   548    \<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"

   504 apply (frule vt_grant_os, simp add:os_grant.simps, (erule exE|erule conjE)+)

   549 apply (frule vd_cons, frule vt_grant_os)

   505 apply (rule conjI, rule notI, simp)

   550 apply (frule proc_fd_in_fds, simp)

   506 apply (rule notI, drule vt_cons', simp add:ancenf_in_current)

   551 apply (frule proc_fd_in_procs, simp)

   507 done

   552 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   508 

   553 apply (frule_tac cf2sfile_other', simp+)

   509 lemma cf2sfile_rename'1: 

   554 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   510   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   555 apply (auto split:option.splits if_splits)

   511 apply (frule vt_cons',frule vt_grant_os,  induct f)

   556 done

   512 apply (simp add:cf2sfile.simps)

   557 

   513 apply (frule parentf_in_current', simp, simp)

   558 lemma cfd2sfd_other:

   514 apply (frule no_junior_aux, simp)

   559   "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';

   515 apply (simp add:os_grant.simps, (erule exE|erule conjE)+)

   560     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   516 apply (drule cf2sfile_rename_aux, simp, erule conjE)

   561     \<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>

   517 apply (auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   562    \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"

   518 done

   563 apply (frule vd_cons, frule vt_grant_os)

   519 

   564 apply (frule proc_fd_in_fds, simp)

   520 lemma cf2sfile_rename'2: 

   565 apply (frule proc_fd_in_procs, simp)

   521   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; \<not> (f\<^isub>3 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   566 apply (frule file_of_proc_fd_in_curf, simp)

   522 apply (frule vt_cons', induct f)

   567 apply (case_tac e)

   523 by (auto simp add:index_of_file.simps cf2sfile.simps no_junior_def split:option.splits nat.splits)

   568 apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)

   524 

   569 apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)

   525 lemma cf2sfile_rename1:

   570 apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)

   526   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f\<^isub>3 = SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)"

   571 done

   527 apply (case_tac f\<^isub>3, simp add:cf2sfile.simps)

   572 

   528 apply (auto dest!:cf2sfile_rename'2 simp add:no_junior_def cf2sfile.simps index_of_file.simps split:option.splits)

   573 lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other

   529 done

   574 

   530 

   575 (********** cpfd2sfds simpset **********)

   531 lemma index_of_file_rename1: "\<lbrakk>f\<^isub>2 \<preceq> f; f \<noteq> f\<^isub>2\<rbrakk> \<Longrightarrow> index_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = index_of_file \<tau> f"

   576 

   532 apply (clarsimp simp add:index_of_file.simps split:option.splits)

   577 lemma current_filefd_has_flags:

   533 by (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop3, simp, erule conjE, simp add:file_renaming_prop5)

   578   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"

   534 

   579 apply (induct s arbitrary:p)

   535 lemma cf2sfile_rename2: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; (file_before_rename f\<^isub>2 f\<^isub>3 f) \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 

   580 apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)

   536    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"

   581 apply (frule vd_cons, frule vt_grant_os, case_tac a)

   537 apply (induct f, simp add:no_junior_def)

   582 apply (auto split:if_splits option.splits dest:proc_fd_in_fds)

   538 apply (case_tac "a # f = f\<^isub>3", simp)

   583 done

   539 apply (drule cf2sfile_rename1, simp, simp add:file_renaming_prop0' file_renaming_prop0)

   584 

   540 

   585 lemma current_filefd_has_flags':

   541 apply (frule no_junior_noteq, simp, simp)

   586   "\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   542 apply (frule_tac file_renaming_prop1')

   587 apply (case_tac "file_of_proc_fd s p fd")

   543 apply (frule_tac f = f\<^isub>2 and \<tau> = \<tau> in cf2sfile_keep_path, simp add:vt_cons')

   588 apply (simp, drule current_filefd_has_flags, simp+)

   544 apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop8')

   589 done

   545 apply (frule_tac f\<^isub>2 = f\<^isub>2 and a = a in file_renaming_prop6')

   590 

   546 apply (frule_tac f = "file_before_rename f\<^isub>2 f\<^isub>3 (a # f)" and \<tau> = \<tau> and f\<^isub>2 = f\<^isub>2 and f\<^isub>3 = f\<^isub>3 and p = p in index_of_file_rename1, simp add:file_before_rename_def)

   591 lemma current_file_has_sfile':

   547 apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = f and a = a and f\<^isub>2 = f\<^isub>2 in file_renaming_prop9', simp)

   592   "\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   548 apply (drule parentf_in_current', simp add:vt_cons')

   593 by (rule notI, drule current_file_has_sfile, simp+)

   549 apply (simp add:cf2sfile.simps)

   594 

   550 apply (erule file_renaming_prop6[THEN sym])

   595 lemma current_filefd_has_sfd:

   551 done

   596   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"

   552 

   597 by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile' 

   553 lemma cf2sfile_rename2': "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 

   598          dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)

   554    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   599 

   555 apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop5)

   600 lemma current_filefd_has_sfd':

   556 apply (frule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1)

   601   "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   557 apply (drule_tac f = "file_after_rename f\<^isub>2 f\<^isub>3 f" in cf2sfile_rename2, simp+)

   602 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)

   558 done

   603 

   559 

   604 definition cpfd2sfds' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"

   560 lemma cf2sfile_rename3: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files \<tau>; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 

   605 where

   561    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   606   "cpfd2sfds' s p \<equiv> {sfd. \<exists> fd f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}"

   562 apply (case_tac "f\<^isub>2 \<preceq> f")

   607 

   563 apply (rule cf2sfile_rename2', simp+)

   608 definition cph2spshs' :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"

   564 apply (frule vt_grant_os)

   609 where

   565 apply (frule_tac \<tau> = \<tau> in cf2sfile_keep_path', simp add:vt_cons', simp add:os_grant.simps, simp)

   610   "cph2spshs' s p \<equiv> {(sh, flag). \<exists> h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"

   566 apply (simp add:file_after_rename_def)

   611 

   567 by (rule cf2sfile_rename'1, simp+)

   612 lemma "x \<in> cph2spshs' s p \<Longrightarrow> False"

   568 

   613 apply (simp add:cph2spshs'_def)

   569 lemma cf2sfile_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow>

   614 apply (case_tac x, simp)

   570                          cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (

   615 

   571                            if (f\<^isub>3 \<preceq> f) then (case (parent f\<^isub>3) of 

   616 

   572                                                Some pf\<^isub>3 \<Rightarrow> file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))

   617 lemma cpfd2sfds_open_some1:

   573                                              | _        \<Rightarrow> [])

   618   "valid (Open p f flags fd (Some inum) # s) \<Longrightarrow>

   574                            else cf2sfile \<tau> f               )"

   619    cpfd2sfds (Open p f flags fd (Some inum) # s) p = (

   575 apply (frule vt_grant_os)

   620     case (cfd2sfd (Open p f flags fd (Some inum) # s) p fd) of

   576 apply (case_tac "f = f\<^isub>3", clarsimp simp:os_grant.simps, drule cf2sfile_rename1, simp+, simp add:file_renaming_prop0' file_renaming_prop0)

   621         Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}

   577 

   622       | _ \<Rightarrow> cpfd2sfds s p)"

   578 apply (auto simp:os_grant.simps current_files_simps intro:cf2sfile_rename'2 cf2sfile_rename1 split:if_splits option.splits) 

   623 apply (frule vd_cons, frule vt_grant_os)

   579 apply (rule cf2sfile_rename2, simp, drule rename_renaming_decom, simp+)

   624 apply (split option.splits)

   580 apply (drule_tac f\<^isub>2 = f\<^isub>2 and f\<^isub>1 = f\<^isub>1 and f\<^isub>3 = f\<^isub>3 in file_renaming_prop5, simp+)

   625 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)

   581 done

   626 apply (rule allI, rule impI)

   582 

   627 apply (rule set_eqI, rule iffI)

   583 lemma cf2sfile_other: "\<lbrakk>

   628 unfolding cpfd2sfds_def

   584                         \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   629 thm CollectE

   585                         \<forall> p f im. e \<noteq> Mkdir p f im;

   630 apply (erule CollectE)

   586                         \<forall> p f\<^isub>1 f\<^isub>2. e \<noteq> LinkHard p f\<^isub>1 f\<^isub>2;

   631 apply (erule CollectE, (erule conjE|erule exE)+)

   587                         \<forall> p f\<^isub>2 f\<^isub>3. e \<noteq> Rename p f\<^isub>2 f\<^isub>3\<rbrakk> \<Longrightarrow> cf2sfile (e # \<tau>) f' = cf2sfile \<tau> f'"

   632 apply (simp only:file_of_proc_fd.simps split:if_splits)

   588 apply (induct f', simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   633 apply (simp add:cpfd2sfds_def)

   589 apply (case_tac e, auto simp add:cf2sfile.simps index_of_file.simps split:option.splits nat.splits)

   634 

   590 done

   635 apply (auto simp:cpfd2sfds_def split:option.splits if_splits dest:file_of_proc_fd_in_curf proc_fd_in_fds proc_fd_in_procs)

   591 

   636 

   592 lemmas cf2sfile_nil = init_cf2sfile

   637 lemma cpfd2sfds_open1:

   593 

   638   "valid (Open p f flags fd opt # s) \<Longrightarrow>

   594 lemma cf2sfile_nil': "f \<in> current_files [] \<Longrightarrow> cf2sfile [] f = map SInit f"

   639    cpfd2sfds (Open p f flags fd opt # s) p = (

   595 by (simp add:cf2sfile_nil current_files_simps)

   640     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   596 

   641         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

   597 lemmas cf2sfile_simps = cf2sfile_nil cf2sfile_nil' cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_rename cf2sfile_other

   642       | _ \<Rightarrow> cpfd2sfds s p)"

   598 

   643 apply (frule vd_cons, frule vt_grant_os)

   599 lemmas cf2sfile_simpss = cf2sfile_nil cf2sfile_nil' cf2sfile_open_some' cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some' cf2sfile_mkdir_some

   644 apply (case_tac opt)

   600                          cf2sfile_mkdir cf2sfile_linkhard_none cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1 cf2sfile_rename'2 cf2sfile_rename1

   645 apply (auto simp:sectxt_of_obj_simps current_files_simps dest!:current_has_sec' current_file_has_sfile'

   601                          cf2sfile_rename2 cf2sfile_rename2' cf2sfile_rename3 cf2sfile_rename cf2sfile_other

   646   split:option.splits)

   602 

   647 apply (auto simp:cpfd2sfds_def split:if_splits)

   603 lemma cf2sfile_open_some'_inum: "\<lbrakk>Open p f' flags fd (Some inum) # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Open p f' flags fd (Some inum) # \<tau>) f = cf2sfile \<tau> f"

   648 apply (auto simp:cfd2sfd_open cf2sfile_open sectxt_of_obj_simps current_files_simps split:option.splits if_splits dest!:current_has_sec' current_file_has_sfile')

   604 by (simp add:cf2sfile_open_some' current_files_def)

   649 apply (frule cfd2sfd_open1)

   605 

   650 apply (

   606 lemma cf2sfile_mkdir_some'_inum: "\<lbrakk>Mkdir p f' inum # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (Mkdir p f' inum # \<tau>) f = cf2sfile \<tau> f"

   651 apply (simp add:cpfd2sfds_def)

   607 by (simp add:cf2sfile_mkdir_some' current_files_def)

   652 apply (auto simp add:cpfd2sfds_def split:option.splits)

   608 

   653 apply (auto dest!:current_has_sec')

   609 lemma cf2sfile_linkhard_none_inum: "\<lbrakk>LinkHard p f\<^isub>1 f\<^isub>2 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> cf2sfile (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) f = cf2sfile \<tau> f"

   654 

   610 by (simp add:cf2sfile_linkhard_none current_files_def)

   655 lemma cpfd2sfds_open:

   611 

   656   "valid (Open p f flags fd opt # s)

   612 lemma cf2sfile_rename'1_inum: 

   657    \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (

   613   "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im ; \<not> (f\<^isub>2 \<preceq> f)\<rbrakk> \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = cf2sfile \<tau> f"

   658     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   614 by (simp add:cf2sfile_rename'1 current_files_def)

   659         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

   615 

   660       | _ \<Rightarrow> cpfd2sfds s p))"

   616 lemma cf2sfile_rename2_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>3 \<preceq> f\<rbrakk> 

   661 apply (frule cfd2sfd_open1)

   617    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f))"

   662 apply (rule ext)

   618 by (simp add:cf2sfile_rename2 current_files_def)

   663 apply (simp add:cpfd2sfds_def)

   619 

   664 apply (auto simp add:cpfd2sfds_def split:option.splits)

   620 lemma cf2sfile_rename2'_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3; f\<^isub>2 \<preceq> f\<rbrakk> 

   665 

   621    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   666 lemma cpfd2sfds_simps = 

   622 by (simp add:cf2sfile_rename2' current_files_def)

   667 

   623 

   668 (******** cp2sproc simpset *********)

   624 lemma cf2sfile_rename3_inum: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # \<tau> \<in> vt rc_cs; inum_of_file \<tau> f = Some im; parent f\<^isub>3 = Some pf\<^isub>3\<rbrakk> 

   625    \<Longrightarrow> cf2sfile (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) (file_after_rename f\<^isub>2 f\<^isub>3 f) = file_after_rename (cf2sfile \<tau> f\<^isub>2) (SCrea (Suc (length \<tau>)) # (cf2sfile \<tau> pf\<^isub>3)) (cf2sfile \<tau> f)"

   626 by (simp add:cf2sfile_rename3 current_files_def)

   627 

   628 lemma cf2sfile_nil'_inum: "inum_of_file [] f = Some im \<Longrightarrow> cf2sfile [] f = map SInit f"

   629 by (simp add:cf2sfile_nil' current_files_def)

   630 

   631 lemmas cf2sfile_simps_inum = cf2sfile_nil cf2sfile_nil'_inum cf2sfile_open_some'_inum cf2sfile_open_some cf2sfile_open_none cf2sfile_open cf2sfile_mkdir_some'_inum cf2sfile_mkdir_some

   632                          cf2sfile_mkdir cf2sfile_linkhard_none_inum cf2sfile_linkhard_some cf2sfile_linkhard cf2sfile_rename'1_inum cf2sfile_rename'2 cf2sfile_rename1

   633                          cf2sfile_rename2_inum cf2sfile_rename2'_inum cf2sfile_rename3_inum cf2sfile_rename cf2sfile_other

   634 

   635 (*************** cp2sproc simpset *********************)