1 theory Deleted_prop |
1 theory Deleted_prop |
2 imports Main Flask Flask_type Init_prop Alive_prop |
2 imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop |
3 begin |
3 begin |
4 |
4 |
5 context flask begin |
5 context flask begin |
6 |
6 |
7 lemma deleted_cons_I: "deleted obj s \<Longrightarrow> deleted obj (e # s)" |
7 lemma deleted_cons_I: "deleted obj s \<Longrightarrow> deleted obj (e # s)" |
8 by (case_tac e, auto) |
8 by (case_tac e, auto) |
9 |
9 |
10 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" |
10 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" |
11 by (auto dest:deleted_cons_I) |
11 by (auto dest:deleted_cons_I) |
12 |
12 |
13 lemma not_deleted_imp_exists: |
13 lemma not_deleted_init_file: |
|
14 "\<lbrakk>\<not> deleted (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f" |
|
15 apply (induct s, simp add:is_init_file_prop1) |
|
16 apply (frule vd_cons, frule vt_grant_os) |
|
17 apply (case_tac a) prefer 6 apply (case_tac option) |
|
18 apply (auto simp:is_file_simps split:option.splits) |
|
19 done |
|
20 |
|
21 lemma not_deleted_init_dir: |
|
22 "\<lbrakk>\<not> deleted (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f" |
|
23 apply (induct s, simp add:is_init_dir_prop1) |
|
24 apply (frule vd_cons, frule vt_grant_os) |
|
25 apply (case_tac a) prefer 6 apply (case_tac option) |
|
26 apply (auto simp:is_dir_simps split:option.splits) |
|
27 done |
|
28 |
|
29 lemma not_deleted_init_proc: |
|
30 "\<lbrakk>\<not> deleted (O_proc p) s; p \<in> init_procs\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
31 apply (induct s, simp) |
|
32 by (case_tac a, auto) |
|
33 |
|
34 (**** ???*) |
|
35 lemma current_fd_imp_current_proc: |
|
36 "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
|
37 apply (induct s) |
|
38 apply (simp add:init_fds_of_proc_prop1) |
|
39 apply (frule vd_cons, drule vt_grant_os, case_tac a) |
|
40 by (auto split:if_splits option.splits) |
|
41 |
|
42 lemma not_deleted_init_fd_aux: |
|
43 "\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> |
|
44 \<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> deleted (O_proc p) s" |
|
45 apply (induct s arbitrary: p, simp) |
|
46 apply (frule vd_cons, drule vt_grant_os) |
|
47 apply (case_tac a, auto dest:current_fd_imp_current_proc) |
|
48 done |
|
49 |
|
50 lemma not_deleted_init_fd2: |
|
51 "\<lbrakk>\<not> deleted (O_fd p fd) s; fd \<in> init_fds_of_proc p; valid s\<rbrakk> \<Longrightarrow> \<not> deleted (O_proc p) s" |
|
52 by (auto dest:not_deleted_init_fd_aux) |
|
53 |
|
54 lemma not_deleted_init_fd1: |
|
55 "\<lbrakk>\<not> deleted (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p" |
|
56 by (auto dest:not_deleted_init_fd_aux) |
|
57 |
|
58 lemma not_deleted_init_tcp_aux: |
|
59 "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> |
|
60 \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
|
61 apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1) |
|
62 apply (frule vd_cons, frule vt_grant_os) |
|
63 apply (case_tac a) prefer 6 apply (case_tac option) |
|
64 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits |
|
65 dest:is_tcp_sock_imp_curernt_proc) |
|
66 |
|
67 lemma not_deleted_init_tcp1: |
|
68 "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> |
|
69 \<Longrightarrow> is_tcp_sock s (p,fd)" |
|
70 by (auto dest:not_deleted_init_tcp_aux) |
|
71 |
|
72 lemma not_deleted_init_tcp2: |
|
73 "\<lbrakk>\<not> deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> |
|
74 \<Longrightarrow> \<not> deleted (O_proc p) s" |
|
75 by (auto dest:not_deleted_init_tcp_aux) |
|
76 |
|
77 lemma not_deleted_init_udp_aux: |
|
78 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
|
79 \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s" |
|
80 apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1) |
|
81 apply (frule vd_cons, frule vt_grant_os) |
|
82 apply (case_tac a) prefer 6 apply (case_tac option) |
|
83 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits |
|
84 dest:is_udp_sock_imp_curernt_proc) |
|
85 |
|
86 lemma not_deleted_init_udp1: |
|
87 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
|
88 \<Longrightarrow> is_udp_sock s (p,fd)" |
|
89 by (auto dest:not_deleted_init_udp_aux) |
|
90 |
|
91 lemma not_deleted_init_udp2: |
|
92 "\<lbrakk>\<not> deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> |
|
93 \<Longrightarrow> \<not> deleted (O_proc p) s" |
|
94 by (auto dest:not_deleted_init_udp_aux) |
|
95 |
|
96 lemma not_deleted_init_shm: |
|
97 "\<lbrakk>\<not> deleted (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s" |
|
98 apply (induct s, simp) |
|
99 by (case_tac a, auto) |
|
100 |
|
101 lemma not_deleted_init_msgq: |
|
102 "\<lbrakk>\<not> deleted (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
|
103 apply (induct s, simp) |
|
104 by (case_tac a, auto) |
|
105 |
|
106 lemma current_msg_imp_current_msgq: |
|
107 "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s" |
|
108 apply (induct s) |
|
109 apply (simp add:init_msgs_valid) |
|
110 apply (frule vd_cons, drule vt_grant_os) |
|
111 apply (case_tac a, auto split:if_splits) |
|
112 done |
|
113 |
|
114 lemma not_deleted_init_msg: |
|
115 "\<lbrakk>\<not> deleted (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)" |
|
116 apply (induct s, simp) |
|
117 apply (frule vd_cons, frule vt_grant_os) |
|
118 apply (case_tac a, auto dest:current_msg_imp_current_msgq) |
|
119 apply (case_tac "msgs_of_queue s q", simp+) |
|
120 done |
|
121 |
|
122 lemma not_deleted_imp_alive: |
14 "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
123 "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj" |
15 apply (induct s, simp add:init_alive_prop) |
124 apply (case_tac obj) |
16 apply (frule vd_cons) |
125 apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc |
17 apply (case_tac a, auto simp:alive_simps split:t_object.splits) |
126 not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm |
18 pr 19 |
127 not_deleted_init_msgq |
|
128 intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current |
|
129 current_msg_imp_current_msgq) |
19 done |
130 done |
20 |
131 |
21 lemma cons_app_simp_aux: |
132 lemma cons_app_simp_aux: |
22 "(a # b) @ c = a # (b @ c)" by auto |
133 "(a # b) @ c = a # (b @ c)" by auto |
23 |
134 |
24 lemma not_deleted_imp_exists': |
135 lemma not_deleted_imp_alive_app: |
25 "\<lbrakk>\<not> deleted obj (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj" |
136 "\<lbrakk>\<not> deleted obj (s'@s); alive s obj\<rbrakk> \<Longrightarrow> alive (s'@s) obj" |
26 apply (induct s', simp, simp only:cons_app_simp_aux) |
137 apply (induct s', simp, simp only:cons_app_simp_aux) |
27 apply (frule not_deleted_cons_D) |
138 apply (frule not_deleted_cons_D, simp) |
28 apply (case_tac a, case_tac [!] obj, auto) |
139 apply (case_tac a, case_tac [!] obj, auto) |
29 done |
140 done |
30 |
141 |
31 (* |
142 (* |
32 |
143 |