equal
deleted
inserted
replaced
537 current_files_mkdir current_files_linkhard current_files_other |
537 current_files_mkdir current_files_linkhard current_files_other |
538 |
538 |
539 |
539 |
540 (******************** is_file simpset *********************) |
540 (******************** is_file simpset *********************) |
541 |
541 |
542 lemma is_file_nil: "is_file [] = is_init_file" |
|
543 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
|
544 |
|
545 lemma is_file_open: |
542 lemma is_file_open: |
546 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
543 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
547 is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))" |
544 is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))" |
548 apply (frule vd_cons, drule vt_grant_os, rule ext) |
545 apply (frule vd_cons, drule vt_grant_os, rule ext) |
549 apply (auto dest:finum_has_itag iof's_im_in_cim |
546 apply (auto dest:finum_has_itag iof's_im_in_cim |
604 |
601 |
605 lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other |
602 lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other |
606 |
603 |
607 (********* is_dir simpset **********) |
604 (********* is_dir simpset **********) |
608 |
605 |
609 lemma is_dir_nil: "is_dir [] = is_init_dir" |
|
610 by (auto simp:is_init_dir_def is_dir_def init_inum_of_file_props intro!:ext split:option.splits) |
|
611 |
|
612 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)" |
606 lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)" |
613 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
607 apply (frule vd_cons, drule vt_grant_os, rule_tac ext) |
614 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
608 apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext |
615 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
609 split:if_splits option.splits t_inode_tag.split t_socket_type.splits |
616 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |
610 simp:is_dir_def dir_is_empty_def is_dir_def current_files_def) |