107 else alive s (O_udp_sock (p', fd))) |
107 else alive s (O_udp_sock (p', fd))) |
108 | _ \<Rightarrow> alive s obj )" |
108 | _ \<Rightarrow> alive s obj )" |
109 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
109 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
110 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
110 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
111 is_tcp_sock_simps is_udp_sock_simps |
111 is_tcp_sock_simps is_udp_sock_simps |
112 dest:is_dir_in_current split:if_splits option.splits) |
112 dest:is_dir_in_current split:if_splits option.splits |
113 apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto) |
113 dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds) |
114 |
|
115 done |
114 done |
116 |
115 |
117 lemma alive_clone: |
116 lemma alive_clone: |
118 "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = ( |
117 "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = ( |
119 \<lambda> obj. case obj of |
118 \<lambda> obj. case obj of |
120 O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj |
119 O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj |
121 | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True |
120 | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True |
122 else if (p'' = p') then False |
121 else if (p'' = p') then False |
123 else alive s obj |
122 else alive s obj |
124 | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd)) |
123 | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False |
125 else if (p'' = p') then False |
124 else alive s (O_tcp_sock (p'', fd))) |
126 else alive s (O_tcp_sock (p'', fd))) |
125 | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False |
127 | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd)) |
126 else alive s (O_udp_sock (p'', fd))) |
128 else if (p'' = p') then False |
|
129 else alive s (O_udp_sock (p'', fd))) |
|
130 | _ \<Rightarrow> alive s obj )" |
127 | _ \<Rightarrow> alive s obj )" |
131 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
128 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj) |
132 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
129 apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps |
133 is_tcp_sock_simps is_udp_sock_simps |
130 is_tcp_sock_simps is_udp_sock_simps |
134 intro:is_tcp_in_current is_udp_in_current |
131 intro:is_tcp_in_current is_udp_in_current |
135 dest:is_dir_in_current split:if_splits option.splits) |
132 dest:is_dir_in_current split:if_splits option.splits |
136 done |
133 dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds) |
137 |
134 done |
138 |
135 |
139 lemma alive_kill: |
136 lemma alive_kill: |
140 "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = ( |
137 "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = ( |
141 \<lambda> obj. case obj of |
138 \<lambda> obj. case obj of |
142 O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj |
139 O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj |