66 apply (case_tac s, auto) |
66 apply (case_tac s, auto) |
67 done |
67 done |
68 |
68 |
69 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5 |
69 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5 |
70 |
70 |
71 lemma is_init_file_prop1: "is_init_file f = (f \<in> init_files \<and> is_file [] f)" |
71 lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files" |
72 by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits) |
72 by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits) |
73 |
73 |
74 lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))" |
74 lemma is_init_file_prop2: "is_init_file f \<Longrightarrow> \<not> is_init_dir f" |
75 by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits) |
75 by (auto simp add:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) |
76 |
76 |
77 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2 |
77 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2 |
78 |
78 |
79 lemma is_init_dir_prop1: "is_init_dir f = (f \<in> init_files \<and> is_dir [] f)" |
79 lemma is_init_dir_prop1: "is_init_dir f \<Longrightarrow> f \<in> init_files" |
80 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) |
80 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) |
81 |
81 |
82 lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))" |
82 lemma is_init_dir_prop2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f" |
83 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) |
83 by (auto simp add:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits) |
84 |
84 |
85 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2 |
85 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2 |
86 |
86 |
87 lemma is_file_nil: "is_file [] = is_init_file" |
87 lemma is_file_nil: "is_file [] = is_init_file" |
88 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
88 by (auto simp:is_init_file_def is_file_def init_inum_of_file_props intro!:ext split:option.splits) |
92 |
92 |
93 lemma is_udp_sock_nil: |
93 lemma is_udp_sock_nil: |
94 "is_udp_sock [] k = is_init_udp_sock k" |
94 "is_udp_sock [] k = is_init_udp_sock k" |
95 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits) |
95 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits) |
96 |
96 |
97 lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)" |
97 lemma is_init_udp_sock_prop1: "is_init_udp_sock s \<Longrightarrow> s \<in> init_sockets" |
98 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
98 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
99 dest:init_socket_has_inode split:option.splits) |
99 dest:init_socket_has_inode split:option.splits) |
100 done |
100 done |
101 |
101 |
102 lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))" |
102 lemma is_init_udp_sock_prop2: "is_init_udp_sock s \<Longrightarrow> \<not> is_init_tcp_sock s" |
103 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props |
103 apply (auto simp add:is_init_udp_sock_def is_init_tcp_sock_def |
104 dest:init_socket_has_inode split:option.splits) |
104 dest:init_socket_has_inode split:option.splits t_inode_tag.splits) |
105 done |
105 done |
106 |
106 |
107 lemma is_init_udp_sock_prop3: |
107 lemma is_init_udp_sock_prop3: |
108 "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
108 "is_init_udp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
109 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits |
109 by (auto simp:is_init_udp_sock_def split:option.splits t_inode_tag.splits |
119 |
119 |
120 lemma is_tcp_sock_nil: |
120 lemma is_tcp_sock_nil: |
121 "is_tcp_sock [] k = is_init_tcp_sock k" |
121 "is_tcp_sock [] k = is_init_tcp_sock k" |
122 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) |
122 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) |
123 |
123 |
124 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)" |
124 lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s \<Longrightarrow> s \<in> init_sockets" |
125 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
125 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
126 dest:init_socket_has_inode split:option.splits) |
126 dest:init_socket_has_inode split:option.splits) |
127 done |
127 done |
128 |
128 |
129 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))" |
129 lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s \<Longrightarrow> \<not> is_init_udp_sock s" |
130 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props |
130 apply (auto simp add:is_init_tcp_sock_def is_init_udp_sock_def |
131 dest:init_socket_has_inode split:option.splits) |
131 dest:init_socket_has_inode split:option.splits t_inode_tag.splits) |
132 done |
132 done |
133 |
133 |
134 lemma is_init_tcp_sock_prop3: |
134 lemma is_init_tcp_sock_prop3: |
135 "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
135 "is_init_tcp_sock (p, fd) \<Longrightarrow> p \<in> init_procs" |
136 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits |
136 by (auto simp:is_init_tcp_sock_def split:option.splits t_inode_tag.splits |
299 |
299 |
300 context flask begin |
300 context flask begin |
301 |
301 |
302 lemma init_alive_prop: "init_alive obj = alive [] obj" |
302 lemma init_alive_prop: "init_alive obj = alive [] obj" |
303 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props |
303 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props |
304 is_init_udp_sock_props init_files_props init_sockets_props) |
304 is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil |
|
305 is_tcp_sock_nil is_udp_sock_nil) |
305 done |
306 done |
306 |
307 |
307 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp |
308 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp |
308 lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp |
309 lemma init_alive_file: "is_init_file f \<Longrightarrow> init_alive (O_file f)" by simp |
309 lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp |
310 lemma init_alive_dir: "is_init_dir f \<Longrightarrow> init_alive (O_dir f)" by simp |
367 by (auto simp:bidirect_in_init_def) |
368 by (auto simp:bidirect_in_init_def) |
368 |
369 |
369 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3 |
370 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3 |
370 |
371 |
371 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t" |
372 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t" |
372 apply (simp only: is_init_file_prop2) |
373 apply (drule init_alive_file) |
373 by (drule init_obj_has_user, auto) |
374 by (drule init_obj_has_user, auto) |
374 |
375 |
375 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None" |
376 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None" |
376 by (simp add:init_file_user_prop1) |
377 by (simp add:init_file_user_prop1) |
377 |
378 |
387 by (simp add:init_user_has_obj) |
388 by (simp add:init_user_has_obj) |
388 |
389 |
389 lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5 |
390 lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5 |
390 |
391 |
391 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t" |
392 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t" |
392 apply (simp only: is_init_dir_prop2) |
393 apply (drule init_alive_dir) |
393 by (drule init_obj_has_user, auto) |
394 by (drule init_obj_has_user, auto) |
394 |
395 |
395 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None" |
396 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None" |
396 by (simp add:init_dir_user_prop1) |
397 by (simp add:init_dir_user_prop1) |
397 |
398 |
763 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
764 is_init_udp_sock_prop1 is_init_tcp_sock_prop1 ch2sshm_nil_prop |
764 same_inode_nil_prop cm2smsg_nil_prop |
765 same_inode_nil_prop cm2smsg_nil_prop |
765 dest:init_same_inode_prop1 |
766 dest:init_same_inode_prop1 |
766 split:option.splits) |
767 split:option.splits) |
767 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
768 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) |
768 apply (simp add:init_files_props) |
769 apply (drule is_init_file_prop1, simp add:init_files_props) |
769 apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict) |
|
770 done |
770 done |
771 |
771 |
772 lemma s2ss_nil_prop: |
772 lemma s2ss_nil_prop: |
773 "s2ss [] = init_static_state" |
773 "s2ss [] = init_static_state" |
774 using co2sobj_nil_prop init_alive_prop |
774 using co2sobj_nil_prop init_alive_prop |