110 "\<lbrakk>\<not> died (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
110 "\<lbrakk>\<not> died (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
111 apply (induct s, simp) |
111 apply (induct s, simp) |
112 by (case_tac a, auto) |
112 by (case_tac a, auto) |
113 *) |
113 *) |
114 |
114 |
|
115 (* |
115 lemma not_died_init_msgq: |
116 lemma not_died_init_msgq: |
116 "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
117 "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
117 apply (induct s, simp) |
118 apply (induct s, simp) |
118 by (case_tac a, auto) |
119 by (case_tac a, auto) |
|
120 *) |
119 |
121 |
120 lemma current_msg_imp_current_msgq: |
122 lemma current_msg_imp_current_msgq: |
121 "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
123 "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
122 apply (induct s) |
124 apply (induct s, simp) |
123 apply (simp add:init_msgs_valid) |
|
124 apply (frule vd_cons, drule vt_grant_os) |
125 apply (frule vd_cons, drule vt_grant_os) |
125 apply (case_tac a, auto split:if_splits) |
126 apply (case_tac a, auto split:if_splits) |
126 done |
127 done |
127 |
128 |
|
129 (* |
128 lemma not_died_init_msg: |
130 lemma not_died_init_msg: |
129 "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)" |
131 "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)" |
130 apply (induct s, simp) |
132 apply (induct s, simp) |
131 apply (frule vd_cons, frule vt_grant_os) |
133 apply (frule vd_cons, frule vt_grant_os) |
132 apply (case_tac a, auto dest:current_msg_imp_current_msgq) |
134 apply (case_tac a, auto dest:current_msg_imp_current_msgq) |
133 apply (case_tac "msgs_of_queue s q", simp+) |
135 apply (case_tac "msgs_of_queue s q", simp+) |
134 done |
136 done |
|
137 *) |
135 |
138 |
136 lemma not_died_imp_alive: (* init_alive obj; *) |
139 lemma not_died_imp_alive: (* init_alive obj; *) |
137 "\<lbrakk>\<not> died obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
140 "\<lbrakk>\<not> died obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
138 apply (case_tac obj) |
141 apply (case_tac obj) |
139 apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc |
142 apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc |
140 not_died_init_msg not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 (* not_died_init_shm *) |
143 not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 |
141 not_died_init_msgq |
144 (* not_died_init_shm not_died_init_msg not_died_init_msgq*) |
142 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
145 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
143 current_msg_imp_current_msgq) |
146 current_msg_imp_current_msgq) |
144 done |
147 done |
145 |
148 |
146 lemma not_died_cur_file_app: |
149 lemma not_died_cur_file_app: |