803 |
803 |
804 lemma cfd2sfd_open1: |
804 lemma cfd2sfd_open1: |
805 "valid (Open p f flags fd opt # s) |
805 "valid (Open p f flags fd opt # s) |
806 \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = |
806 \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = |
807 (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 |
807 (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 |
808 (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf) |
808 (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf) |
809 | _ \<Rightarrow> None)" |
809 | _ \<Rightarrow> None)" |
810 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits) |
810 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits) |
811 |
811 |
812 lemma cfd2sfd_open_some2: |
812 lemma cfd2sfd_open_some2: |
813 "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk> |
813 "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk> |
852 |
852 |
853 lemma cfd2sfd_open: |
853 lemma cfd2sfd_open: |
854 "\<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> |
854 "\<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> |
855 \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then |
855 \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then |
856 (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 |
856 (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 |
857 (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf) |
857 (Some sec, Some sf) \<Rightarrow> Some (sec, remove_create_flag flags, sf) |
858 | _ \<Rightarrow> None) else cfd2sfd s p' fd')" |
858 | _ \<Rightarrow> None) else cfd2sfd s p' fd')" |
859 apply (simp split:if_splits) |
859 apply (simp split:if_splits) |
860 apply (simp add:cfd2sfd_open1 split:option.splits) |
860 apply (simp add:cfd2sfd_open1 split:option.splits) |
861 apply (simp add:cfd2sfd_open2) |
861 apply (simp add:cfd2sfd_open2) |
862 apply (rule impI, simp) |
862 apply (rule impI, simp) |
1001 |
1001 |
1002 lemma cpfd2sfds_open1': |
1002 lemma cpfd2sfds_open1': |
1003 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
1003 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
1004 cpfd2sfds (Open p f flags fd opt # s) p = ( |
1004 cpfd2sfds (Open p f flags fd opt # s) p = ( |
1005 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 |
1005 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 |
1006 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
1006 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)} |
1007 | _ \<Rightarrow> cpfd2sfds s p)" |
1007 | _ \<Rightarrow> cpfd2sfds s p)" |
1008 apply (frule cfd2sfd_open1) |
1008 apply (frule cfd2sfd_open1) |
1009 apply (auto dest:cpfd2sfds_open1 split:option.splits) |
1009 apply (auto dest:cpfd2sfds_open1 split:option.splits) |
1010 done |
1010 done |
1011 |
1011 |
1025 |
1025 |
1026 lemma cpfd2sfds_open: |
1026 lemma cpfd2sfds_open: |
1027 "valid (Open p f flags fd opt # s) |
1027 "valid (Open p f flags fd opt # s) |
1028 \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := ( |
1028 \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := ( |
1029 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 |
1029 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 |
1030 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)} |
1030 (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, remove_create_flag flags, sf)} |
1031 | _ \<Rightarrow> cpfd2sfds s p))" |
1031 | _ \<Rightarrow> cpfd2sfds s p))" |
1032 apply (rule ext) |
1032 apply (rule ext) |
1033 apply (case_tac "x \<noteq> p") |
1033 apply (case_tac "x \<noteq> p") |
1034 apply (simp add:cpfd2sfds_open2) |
1034 apply (simp add:cpfd2sfds_open2) |
1035 apply (simp add:cpfd2sfds_open1') |
1035 apply (simp add:cpfd2sfds_open1') |
1477 cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p := |
1477 cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p := |
1478 case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), |
1478 case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), |
1479 cf2sfile (Open p f flags fd opt # s) f) of |
1479 cf2sfile (Open p f flags fd opt # s) f) of |
1480 (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) |
1480 (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> died (O_proc p) s \<and> p \<in> init_procs) |
1481 then Init p else Created, sec, |
1481 then Init p else Created, sec, |
1482 (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}) |
1482 (cpfd2sfds s p) \<union> {(fdsec, remove_create_flag flags, sf)}) |
1483 | _ \<Rightarrow> None)" (*, cph2spshs s p |
1483 | _ \<Rightarrow> None)" (*, cph2spshs s p |
1484 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) *) |
1484 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) *) |
1485 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext) |
1485 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext) |
1486 apply (case_tac "x = p") |
1486 apply (case_tac "x = p") |
1487 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
1487 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |