615 |
615 |
616 lemma parentf_is_dir_prop3: "\<lbrakk>(x # pf) \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s pf" |
616 lemma parentf_is_dir_prop3: "\<lbrakk>(x # pf) \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s pf" |
617 apply (rule_tac f = "x # pf" in parentf_is_dir) |
617 apply (rule_tac f = "x # pf" in parentf_is_dir) |
618 by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits) |
618 by (auto simp:is_dir_def current_files_def split:option.splits t_inode_tag.splits) |
619 |
619 |
620 lemma get_pfs_secs_prop: |
620 lemma get_pfs_secs_prop': |
621 "\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
621 "\<lbrakk>get_parentfs_ctxts s f = None; valid s\<rbrakk> \<Longrightarrow> \<not> is_dir s f" |
622 apply (induct f) |
622 apply (induct f) |
623 by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1) |
623 by (auto split:option.splits dest:current_has_sec' parentf_is_dir_prop1) |
|
624 |
|
625 lemma get_pfs_secs_prop: |
|
626 "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> asecs. get_parentfs_ctxts s f = Some asecs" |
|
627 using get_pfs_secs_prop' |
|
628 by (auto) |
624 |
629 |
625 lemma get_pfs_secs_open: |
630 lemma get_pfs_secs_open: |
626 "valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s" |
631 "valid (Open p f flags fd opt # s) \<Longrightarrow> get_parentfs_ctxts (Open p f flags fd opt # s) = get_parentfs_ctxts s" |
627 apply (frule noroot_events, frule vd_cons, frule vt_grant_os) |
632 apply (frule noroot_events, frule vd_cons, frule vt_grant_os) |
628 apply (rule ext, induct_tac x) |
633 apply (rule ext, induct_tac x) |
654 from Cons p1 have p3: "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'" by simp |
659 from Cons p1 have p3: "get_parentfs_ctxts (Mkdir p f inum # s) f' = get_parentfs_ctxts s f'" by simp |
655 from p2 os have p4: "a # f' \<noteq> f" by (auto simp:is_dir_in_current) |
660 from p2 os have p4: "a # f' \<noteq> f" by (auto simp:is_dir_in_current) |
656 from p1 os have p5: "f' \<noteq> f" by (auto simp:is_dir_in_current) |
661 from p1 os have p5: "f' \<noteq> f" by (auto simp:is_dir_in_current) |
657 show ?case using mkdir vd os p4 p5 p1 |
662 show ?case using mkdir vd os p4 p5 p1 |
658 by (auto simp:sectxt_of_obj_simps is_dir_simps p3 |
663 by (auto simp:sectxt_of_obj_simps is_dir_simps p3 |
659 split:option.splits dest:current_has_sec' get_pfs_secs_prop) |
664 split:option.splits dest:current_has_sec' get_pfs_secs_prop') |
660 qed |
665 qed |
661 qed |
666 qed |
662 |
667 |
663 lemma get_pfs_secs_mkdir2: |
668 lemma get_pfs_secs_mkdir2: |
664 "valid (Mkdir p f inum # s) \<Longrightarrow> get_parentfs_ctxts (Mkdir p f inum # s) f = ( |
669 "valid (Mkdir p f inum # s) \<Longrightarrow> get_parentfs_ctxts (Mkdir p f inum # s) f = ( |
667 | x#pf \<Rightarrow> (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
672 | x#pf \<Rightarrow> (case (get_parentfs_ctxts s pf, sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of |
668 (Some pfsecs, Some psec, Some pfsec) \<Rightarrow> Some ((fst psec, R_object, type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True) # pfsecs) |
673 (Some pfsecs, Some psec, Some pfsec) \<Rightarrow> Some ((fst psec, R_object, type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_dir True) # pfsecs) |
669 | _ \<Rightarrow> None))" |
674 | _ \<Rightarrow> None))" |
670 apply (frule vd_cons, frule vt_grant_os) |
675 apply (frule vd_cons, frule vt_grant_os) |
671 apply (frule noroot_events, case_tac f) |
676 apply (frule noroot_events, case_tac f) |
672 by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop get_pfs_secs_mkdir1 |
677 by (auto split:option.splits dest:current_has_sec' get_pfs_secs_prop' get_pfs_secs_mkdir1 |
673 simp:sectxt_of_obj_simps is_dir_simps) |
678 simp:sectxt_of_obj_simps is_dir_simps) |
674 |
679 |
675 lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2 |
680 lemmas get_parentfs_ctxts_simps = get_pfs_secs_other get_pfs_secs_mkdir1 get_pfs_secs_mkdir2 |
676 |
681 |
677 end |
682 end |