equal
deleted
inserted
replaced
117 by (case_tac a, simp) |
117 by (case_tac a, simp) |
118 qed |
118 qed |
119 |
119 |
120 lemma enrich_inherit_fds_check: |
120 lemma enrich_inherit_fds_check: |
121 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
121 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
122 and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
122 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
123 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
123 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
124 and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p" |
124 and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p" |
125 shows "inherit_fds_check s' (up, nr, nt) p fds" |
125 shows "inherit_fds_check s' (up, nr, nt) p fds" |
126 proof- |
126 proof- |
127 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
127 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |