equal
deleted
inserted
replaced
37 \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
37 \<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
38 show ?case using a5 a2 a4 a3 |
38 show ?case using a5 a2 a4 a3 |
39 apply (case_tac e) |
39 apply (case_tac e) |
40 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
40 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
41 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) |
41 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) |
|
42 apply (frule_tac p = nat1 in file_fds_subset_pfds) |
|
43 apply (rule a1, auto) |
42 done |
44 done |
43 qed |
45 qed |
44 |
46 |
45 lemma alive_obj_has_user: |
47 lemma alive_obj_has_user: |
46 assumes alive: "alive s obj" and vs: "valid s" |
48 assumes alive: "alive s obj" and vs: "valid s" |
75 \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
77 \<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1) |
76 show ?case using a5 a2 a4 a3 |
78 show ?case using a5 a2 a4 a3 |
77 apply (case_tac e) |
79 apply (case_tac e) |
78 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
80 apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits |
79 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) |
81 dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps) |
|
82 apply (frule_tac p = nat1 in file_fds_subset_pfds) |
|
83 apply (rule a1, auto) |
80 done |
84 done |
81 qed |
85 qed |
82 |
86 |
83 lemma alive_obj_has_type': "\<lbrakk>type_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
87 lemma alive_obj_has_type': "\<lbrakk>type_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj" |
84 by (rule_tac notI, auto dest:alive_obj_has_type) |
88 by (rule_tac notI, auto dest:alive_obj_has_type) |