77
+ − 1
(*<*)
+ − 2
theory Current_files_prop
+ − 3
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop
+ − 4
begin
+ − 5
(*<*)
+ − 6
+ − 7
context init begin
+ − 8
+ − 9
lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None"
+ − 10
by (simp add:current_files_def)
+ − 11
+ − 12
(************** file_of_proc_fd vs proc_fd_of_file *****************)
+ − 13
lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f"
+ − 14
by (simp add:proc_fd_of_file_def)
+ − 15
+ − 16
lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
+ − 17
by (simp add:proc_fd_of_file_def)
+ − 18
+ − 19
lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')"
+ − 20
by (simp add:proc_fd_of_file_def, auto)
+ − 21
+ − 22
lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd"
+ − 23
by (drule pfdof_simp3, auto)
+ − 24
+ − 25
end
+ − 26
+ − 27
context flask begin
+ − 28
+ − 29
(***************** inode number lemmas *************************)
+ − 30
+ − 31
lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+ − 32
by (auto simp add:current_inode_nums_def current_file_inums_def)
+ − 33
+ − 34
lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+ − 35
by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def)
+ − 36
+ − 37
lemma fim_noninter_sim_aux[rule_format]:
+ − 38
"\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False"
+ − 39
apply (induct \<tau>)
+ − 40
apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps)
+ − 41
apply (drule init_inum_sock_file_noninter, simp, simp)
+ − 42
apply ((rule allI|rule impI|erule conjE)+)
+ − 43
apply (frule vd_cons, frule vt_grant_os, simp, case_tac a)
+ − 44
apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits
+ − 45
dest:ios's_im_in_cim iof's_im_in_cim)
+ − 46
done
+ − 47
+ − 48
lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+ − 49
by (auto intro:fim_noninter_sim_aux)
+ − 50
+ − 51
lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+ − 52
by (auto intro:fim_noninter_sim_aux)
+ − 53
+ − 54
lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}"
+ − 55
by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format])
+ − 56
+ − 57
(******************* file inum has inode tag ************************)
+ − 58
+ − 59
lemma finum_has_itag_aux[rule_format]:
+ − 60
"\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
+ − 61
apply (induct \<tau>)
+ − 62
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
+ − 63
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+ − 64
apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def
+ − 65
dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits)
+ − 66
done
+ − 67
+ − 68
lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
+ − 69
by (auto dest:conjI[THEN finum_has_itag_aux])
+ − 70
+ − 71
(*********************** file inum is file itag *************************)
+ − 72
+ − 73
lemma finum_has_ftag_aux[rule_format]:
+ − 74
"\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag"
+ − 75
apply (induct \<tau>)
+ − 76
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)
+ − 77
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+ − 78
apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps
+ − 79
split:if_splits option.splits t_socket_type.splits
+ − 80
dest:ios's_im_in_cim iof's_im_in_cim)
+ − 81
done
+ − 82
+ − 83
lemma finum_has_ftag:
+ − 84
"\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"
+ − 85
by (auto intro:finum_has_ftag_aux)
+ − 86
+ − 87
lemma finum_has_ftag':
+ − 88
"\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR"
+ − 89
apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+)
+ − 90
apply (case_tac tag, auto)
+ − 91
done
+ − 92
+ − 93
(******************* sock inum has inode tag ************************)
+ − 94
+ − 95
lemma sinum_has_itag_aux[rule_format]:
+ − 96
"\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"
+ − 97
apply (induct \<tau>)
+ − 98
apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
+ − 99
apply (drule init_inumos_prop4, clarsimp)
+ − 100
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+ − 101
apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
+ − 102
dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
+ − 103
split:option.splits if_splits t_socket_type.splits)
+ − 104
done
+ − 105
+ − 106
lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"
+ − 107
by (auto dest:conjI[THEN sinum_has_itag_aux])
+ − 108
+ − 109
(********************** socket inum is socket itag **********************)
+ − 110
+ − 111
lemma sinum_has_stag_aux[rule_format]:
+ − 112
"\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag"
+ − 113
apply (induct \<tau>)
+ − 114
apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)
+ − 115
apply (drule init_inumos_prop4, clarsimp)
+ − 116
apply (clarify, frule vt_grant_os, frule vd_cons, case_tac a)
+ − 117
apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps
+ − 118
dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim
+ − 119
split:option.splits if_splits t_socket_type.splits)
+ − 120
done
+ − 121
+ − 122
lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag"
+ − 123
by (auto dest:conjI[THEN sinum_has_stag_aux])
+ − 124
+ − 125
lemma sinum_has_stag':
+ − 126
"\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk>
+ − 127
\<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK"
+ − 128
apply (frule sinum_has_itag, simp, erule exE)
+ − 129
apply (drule sinum_has_stag, simp+, case_tac tag, simp+)
+ − 130
done
+ − 131
+ − 132
(************************************ 4 in 1 *************************************)
+ − 133
+ − 134
lemma file_leveling: "valid \<tau> \<longrightarrow> (
+ − 135
(\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
+ − 136
(\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
+ − 137
(\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
+ − 138
(\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )"
+ − 139
proof (induct \<tau>)
+ − 140
case Nil
+ − 141
show ?case
+ − 142
apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits)
+ − 143
apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum)
+ − 144
apply (rule init_parent_file_has_inum, simp+)
+ − 145
apply (rule init_file_has_no_son', simp+)
+ − 146
apply (rule init_file_hung_has_no_son, simp+)
+ − 147
done
+ − 148
next
+ − 149
case (Cons a \<tau>)
+ − 150
assume pre: "valid \<tau> \<longrightarrow>
+ − 151
(\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>
+ − 152
(\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>
+ − 153
(\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>
+ − 154
(\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
+ − 155
show ?case
+ − 156
proof
+ − 157
assume cons:"valid (a # \<tau>)"
+ − 158
show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and>
+ − 159
(\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None) \<and>
+ − 160
(\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False) \<and>
+ − 161
(\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"
+ − 162
proof-
+ − 163
have vt: "valid \<tau>" using cons by (auto dest:vd_cons)
+ − 164
have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os)
+ − 165
have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto
+ − 166
have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None"
+ − 167
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ − 168
have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False"
+ − 169
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ − 170
have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False"
+ − 171
using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)
+ − 172
have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 173
proof
+ − 174
fix f'
+ − 175
show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 176
proof (induct f')
+ − 177
case Nil show ?case by (auto simp: no_junior_def)
+ − 178
next
+ − 179
case (Cons a f')
+ − 180
assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 181
show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 182
proof clarify
+ − 183
fix f im
+ − 184
assume h1: "f \<preceq> a # f'"
+ − 185
and h2: "inum_of_file \<tau> (a # f') = Some im"
+ − 186
show "\<exists>y. inum_of_file \<tau> f = Some y"
+ − 187
proof-
+ − 188
have h3: "\<exists> y. inum_of_file \<tau> f' = Some y"
+ − 189
proof-
+ − 190
have "parent (a # f') = Some f'" by simp
+ − 191
hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast
+ − 192
with h1 show ?thesis by simp
+ − 193
qed
+ − 194
from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
+ − 195
moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
+ − 196
moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h3 by simp
+ − 197
moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp
+ − 198
ultimately show ?thesis by auto
+ − 199
qed
+ − 200
qed
+ − 201
qed
+ − 202
qed
+ − 203
+ − 204
have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto
+ − 205
have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
+ − 206
using pin by auto
+ − 207
have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto
+ − 208
have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False"
+ − 209
by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def)
+ − 210
have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto
+ − 211
have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto
+ − 212
have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False"
+ − 213
apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)
+ − 214
by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)
+ − 215
+ − 216
have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"
+ − 217
apply (clarify, case_tac a) using os fin
+ − 218
apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def
+ − 219
split:if_splits option.splits)
+ − 220
done
+ − 221
moreover
+ − 222
have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None"
+ − 223
apply (clarify, case_tac a)
+ − 224
using vt os pin'
+ − 225
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def
+ − 226
split:if_splits option.splits t_inode_tag.splits)
+ − 227
apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)
+ − 228
apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp)
+ − 229
apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp)
+ − 230
done
+ − 231
moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"
+ − 232
apply (clarify, case_tac a)
+ − 233
using vt os fns'' cons
+ − 234
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps
+ − 235
is_file_def is_dir_def
+ − 236
dest:ios's_im_in_cim iof's_im_in_cim
+ − 237
split:if_splits option.splits t_inode_tag.splits t_socket_type.splits)
+ − 238
apply (rule_tac im = a and f = f and f' = f' in fns'', simp+)
+ − 239
apply (drule_tac f = f' and pf = list in pin', simp, simp)
+ − 240
apply (drule_tac f = f' and pf = list2 in pin', simp, simp)
+ − 241
done
+ − 242
moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and>
+ − 243
parent f' = Some f \<longrightarrow> False"
+ − 244
apply (clarify, case_tac a)
+ − 245
using vt os hns'
+ − 246
apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps
+ − 247
split:if_splits option.splits t_sock_addr.splits)
+ − 248
apply (drule fns', simp+)
+ − 249
done
+ − 250
ultimately show ?thesis by blast
+ − 251
qed
+ − 252
qed
+ − 253
qed
+ − 254
+ − 255
(**************** hung file in current ***********************)
+ − 256
+ − 257
lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 258
by (drule file_leveling[rule_format], blast)
+ − 259
+ − 260
lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
+ − 261
by (auto dest:hung_file_has_inum)
+ − 262
+ − 263
lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+ − 264
by (clarsimp simp add:current_files_def hung_file_has_inum')
+ − 265
+ − 266
lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None"
+ − 267
by (drule file_leveling[rule_format], blast)
+ − 268
+ − 269
lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"
+ − 270
by (auto dest:parentf_has_inum)
+ − 271
+ − 272
lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
+ − 273
by (clarsimp simp add:current_files_def parentf_has_inum')
+ − 274
+ − 275
lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"
+ − 276
apply (subgoal_tac "parent (a # pf) = Some pf")
+ − 277
by (erule parentf_in_current, simp+)
+ − 278
+ − 279
lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 280
proof (induct f')
+ − 281
case Nil show ?case by (auto simp: no_junior_def)
+ − 282
next
+ − 283
case (Cons a f')
+ − 284
assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 285
show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 286
proof clarify
+ − 287
fix f im
+ − 288
assume h1: "f \<preceq> a # f'"
+ − 289
and h2: "inum_of_file \<tau> (a # f') = Some im"
+ − 290
and h3: "valid \<tau>"
+ − 291
show "\<exists>y. inum_of_file \<tau> f = Some y"
+ − 292
proof-
+ − 293
have h4: "\<exists> y. inum_of_file \<tau> f' = Some y"
+ − 294
proof-
+ − 295
have "parent (a # f') = Some f'" by simp
+ − 296
hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast
+ − 297
with h1 show ?thesis by simp
+ − 298
qed
+ − 299
from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)
+ − 300
moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp
+ − 301
moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h4 by simp
+ − 302
moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp
+ − 303
ultimately show ?thesis by auto
+ − 304
qed
+ − 305
qed
+ − 306
qed
+ − 307
+ − 308
lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 309
by (rule ancenf_has_inum_aux[rule_format], auto)
+ − 310
+ − 311
lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'"
+ − 312
by (auto dest:ancenf_has_inum)
+ − 313
+ − 314
lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+ − 315
by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum')
+ − 316
+ − 317
lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+ − 318
by (drule file_leveling[rule_format], blast)
+ − 319
+ − 320
lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+ − 321
by (simp add:current_files_def, erule exE, auto intro:file_has_no_son)
+ − 322
+ − 323
lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
+ − 324
by (drule file_leveling[rule_format], blast)
+ − 325
+ − 326
lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False"
+ − 327
by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son)
+ − 328
+ − 329
lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False"
+ − 330
proof (induct f')
+ − 331
case Nil
+ − 332
show ?case
+ − 333
by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits)
+ − 334
next
+ − 335
case (Cons a pf)
+ − 336
assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False"
+ − 337
show ?case
+ − 338
proof clarify
+ − 339
fix f
+ − 340
assume h1: "f \<in> files_hung_by_del \<tau>"
+ − 341
and h2: "valid \<tau>"
+ − 342
and h3: "a # pf \<in> current_files \<tau>"
+ − 343
and h4: "f \<preceq> a # pf"
+ − 344
and h5: "f \<noteq> a # pf"
+ − 345
have h6: "parent (a # pf) = Some pf" by simp
+ − 346
with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
+ − 347
from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
+ − 348
show False
+ − 349
proof (cases "f = pf")
+ − 350
case True with h6 h2 h3 h1
+ − 351
show False by (auto intro!:hung_file_no_son')
+ − 352
next
+ − 353
case False with pre h1 h2 h7 h8
+ − 354
show False by blast
+ − 355
qed
+ − 356
qed
+ − 357
qed
+ − 358
+ − 359
lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False"
+ − 360
by (rule hung_file_no_des_aux[rule_format], blast)
+ − 361
+ − 362
(* current version, dir can not be opened, so hung_files are all files
+ − 363
lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f"
+ − 364
apply (frule hung_file_has_inum', simp, erule exE)
+ − 365
apply (auto simp add:is_file_def dir_is_empty_def is_dir_def dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits)
+ − 366
by (simp add: noJ_Anc, auto dest:hung_file_no_des)
+ − 367
*)
+ − 368
+ − 369
lemma hung_file_has_filetag:
+ − 370
"\<lbrakk>f \<in> files_hung_by_del s; inum_of_file s f = Some im; valid s\<rbrakk> \<Longrightarrow> itag_of_inum s im = Some Tag_FILE"
+ − 371
apply (induct s)
+ − 372
apply (simp add:files_hung_by_del.simps)
+ − 373
apply (drule init_files_hung_prop2, (erule exE)+)
+ − 374
apply (drule init_filefd_prop5, clarsimp simp:is_init_file_def split:t_inode_tag.splits option.splits)
+ − 375
+ − 376
apply (frule vd_cons, frule vt_grant_os, case_tac a)
+ − 377
apply (auto simp:files_hung_by_del.simps is_file_def is_dir_def current_files_def current_inode_nums_def
+ − 378
split:if_splits option.splits t_inode_tag.splits t_socket_type.splits
+ − 379
dest:hung_file_has_inum iof's_im_in_cim)
+ − 380
done
+ − 381
+ − 382
lemma hung_file_is_file: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"
+ − 383
apply (frule hung_file_has_inum', simp, erule exE)
+ − 384
apply (drule hung_file_has_filetag, auto simp:is_file_def)
+ − 385
done
+ − 386
+ − 387
(*********************** 2 in 1 *********************)
+ − 388
+ − 389
lemma file_of_pfd_2in1: "valid s \<Longrightarrow> (
+ − 390
(\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> inum_of_file s f \<noteq> None) \<and>
+ − 391
(\<forall> p fd f. file_of_proc_fd s p fd = Some f \<longrightarrow> is_file s f) )"
+ − 392
proof (induct s)
+ − 393
case Nil
+ − 394
show ?case
+ − 395
by (auto dest:init_filefd_valid simp:is_file_def)
+ − 396
next
+ − 397
case (Cons e s)
+ − 398
hence vd_e: "valid (e # s)" and vd_s: "valid s" and os: "os_grant s e"
+ − 399
and pfd: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> inum_of_file s f \<noteq> None"
+ − 400
and isf: "\<And> p fd f. file_of_proc_fd s p fd = Some f \<Longrightarrow> is_file s f"
+ − 401
by (auto dest:vd_cons vt_grant_os)
+ − 402
from pfd have pfd': "\<And> p fd f. inum_of_file s f = None \<Longrightarrow> file_of_proc_fd s p fd \<noteq> Some f"
+ − 403
by (rule_tac notI, drule_tac pfd, simp)
+ − 404
+ − 405
have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> inum_of_file (e # s) f \<noteq> None"
+ − 406
apply (case_tac e) using os
+ − 407
apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def
+ − 408
dir_is_empty_def is_file_def is_dir_def
+ − 409
split:if_splits option.splits dest:pfd)
+ − 410
apply (simp add:pfdof_simp3)+
+ − 411
apply (simp add:proc_fd_of_file_def)
+ − 412
apply (drule isf, simp add:is_file_def split:t_inode_tag.splits)
+ − 413
done
+ − 414
moreover
+ − 415
have "\<forall>p fd f. file_of_proc_fd (e # s) p fd = Some f \<longrightarrow> is_file (e # s) f"
+ − 416
apply (case_tac e) using os
+ − 417
apply (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits
+ − 418
dest:pfd isf iof's_im_in_cim
+ − 419
simp:is_file_def is_dir_def dir_is_empty_def current_files_def)
+ − 420
apply (simp add:pfdof_simp3)+
+ − 421
apply (simp add:proc_fd_of_file_def)
+ − 422
done
+ − 423
ultimately show ?case by auto
+ − 424
qed
+ − 425
+ − 426
+ − 427
(************** file_of_proc_fd in current ********************)
+ − 428
+ − 429
lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"
+ − 430
by (drule file_of_pfd_2in1, blast)
+ − 431
+ − 432
lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"
+ − 433
by (auto dest!:file_of_pfd_imp_inode')
+ − 434
+ − 435
lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+ − 436
by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def)
+ − 437
+ − 438
+ − 439
(*************** file_of_proc_fd is file *********************)
+ − 440
+ − 441
lemma file_of_pfd_is_file:
+ − 442
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"
+ − 443
by (drule file_of_pfd_2in1, auto simp:is_file_def)
+ − 444
+ − 445
lemma file_of_pfd_is_file':
+ − 446
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+ − 447
by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
+ − 448
+ − 449
lemma file_of_pfd_is_file_tag:
+ − 450
"\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE"
+ − 451
by (drule file_of_pfd_is_file, auto simp:is_file_def split:option.splits t_inode_tag.splits)
+ − 452
+ − 453
(************** parent file / ancestral file is dir *******************)
+ − 454
+ − 455
lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
+ − 456
apply (induct \<tau>)
+ − 457
apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir')
+ − 458
apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
+ − 459
apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps
+ − 460
current_files_def is_dir_def is_file_def
+ − 461
dest: ios's_im_in_cim iof's_im_in_cim
+ − 462
split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits)
+ − 463
apply (drule parentf_has_inum', simp, simp, simp)+
+ − 464
done
+ − 465
+ − 466
lemma parentf_has_dirtag:
+ − 467
"\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk>
+ − 468
\<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"
+ − 469
by (auto intro:parentf_is_dir_aux[rule_format])
+ − 470
+ − 471
lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+ − 472
apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits)
+ − 473
by (auto dest:parentf_has_dirtag)
+ − 474
+ − 475
lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+ − 476
by (clarsimp simp:current_files_def parentf_is_dir')
+ − 477
+ − 478
lemma parentf_is_dir'': "\<lbrakk>f # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"
+ − 479
by (auto intro!:parentf_is_dir)
+ − 480
+ − 481
lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
+ − 482
proof (induct f')
+ − 483
case Nil show ?case
+ − 484
by (auto simp:current_files_def no_junior_def)
+ − 485
next
+ − 486
case (Cons a pf)
+ − 487
assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"
+ − 488
show ?case
+ − 489
proof clarify
+ − 490
fix f
+ − 491
assume h1: "f \<preceq> a # pf"
+ − 492
and h2: "f \<noteq> a # pf"
+ − 493
and h3: "a # pf \<in> current_files \<tau>"
+ − 494
and h4: "valid \<tau>"
+ − 495
have h5: "parent (a # pf) = Some pf" by simp
+ − 496
with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)
+ − 497
from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)
+ − 498
show "is_dir \<tau> f"
+ − 499
proof (cases "f = pf")
+ − 500
case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto)
+ − 501
next
+ − 502
case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast
+ − 503
qed
+ − 504
qed
+ − 505
qed
+ − 506
+ − 507
lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f"
+ − 508
by (auto intro:ancenf_is_dir_aux[rule_format])
+ − 509
+ − 510
(************* rebuild current_files simpset ***********************)
+ − 511
+ − 512
lemma current_files_nil: "current_files [] = init_files"
+ − 513
apply (simp add:current_files_def inum_of_file.simps)
+ − 514
by (auto dest:inof_has_file_tag init_file_has_inum)
+ − 515
+ − 516
lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)"
+ − 517
by (auto simp add:current_files_def inum_of_file.simps split:option.splits)
+ − 518
+ − 519
lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>"
+ − 520
by (simp add:current_files_def inum_of_file.simps split:option.splits)
+ − 521
+ − 522
lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = (
+ − 523
case (file_of_proc_fd \<tau> p fd) of
+ − 524
Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>))
+ − 525
then current_files \<tau> - {f}
+ − 526
else current_files \<tau>)
+ − 527
| _ \<Rightarrow> current_files \<tau> )"
+ − 528
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+ − 529
+ − 530
lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)"
+ − 531
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+ − 532
+ − 533
lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = current_files \<tau> - {f}"
+ − 534
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+ − 535
+ − 536
lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)"
+ − 537
by (auto simp:current_files_def inum_of_file.simps split:option.splits)
+ − 538
+ − 539
lemma current_files_linkhard:
+ − 540
"valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"
+ − 541
apply (frule vt_grant_os, frule vd_cons)
+ − 542
by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits)
+ − 543
+ − 544
(*
+ − 545
lemma rename_renaming_decom:
+ − 546
"\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f"
+ − 547
apply (case_tac "f\<^isub>2 \<preceq> f", simp)
+ − 548
apply (simp add:file_after_rename_def split:if_splits)
+ − 549
by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current)
+ − 550
+ − 551
lemma rename_renaming_decom':
+ − 552
"\<lbrakk>\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"
+ − 553
by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+)
+ − 554
+ − 555
lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}"
+ − 556
apply (frule vt_grant_os, frule vd_cons)
+ − 557
apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits)
+ − 558
apply (rule_tac x = x in exI, simp add:file_after_rename_def)
+ − 559
apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5')
+ − 560
apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp)
+ − 561
apply (rule_tac x = x in exI, simp add:file_after_rename_def)
+ − 562
apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp)
+ − 563
apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp)
+ − 564
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5)
+ − 565
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
+ − 566
apply (simp add:file_after_rename_def)
+ − 567
apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)
+ − 568
apply (simp add:file_after_rename_def)
+ − 569
done
+ − 570
*)
+ − 571
+ − 572
lemma current_files_other:
+ − 573
"\<lbrakk>\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ − 574
\<forall> p fd. e \<noteq> CloseFd p fd;
+ − 575
\<forall> p f. e \<noteq> UnLink p f;
+ − 576
\<forall> p f. e \<noteq> Rmdir p f;
+ − 577
\<forall> p f i. e \<noteq> Mkdir p f i;
+ − 578
\<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> current_files (e # \<tau>) = current_files \<tau>"
+ − 579
by (case_tac e, auto simp:current_files_def inum_of_file.simps)
+ − 580
+ − 581
lemmas current_files_simps = current_files_nil current_files_open current_files_open'
+ − 582
current_files_closefd current_files_unlink current_files_rmdir
+ − 583
current_files_mkdir current_files_linkhard current_files_other
+ − 584
+ − 585
+ − 586
(******************** is_file simpset *********************)
+ − 587
+ − 588
lemma is_file_open:
+ − 589
"valid (Open p f flags fd opt # s) \<Longrightarrow>
+ − 590
is_file (Open p f flags fd opt # s) = (if (opt = None) then is_file s else (is_file s) (f:= True))"
+ − 591
apply (frule vd_cons, drule vt_grant_os, rule ext)
+ − 592
apply (auto dest:finum_has_itag iof's_im_in_cim
+ − 593
split:if_splits option.splits t_inode_tag.splits
+ − 594
simp:is_file_def current_files_def)
+ − 595
done
+ − 596
+ − 597
lemma is_file_closefd:
+ − 598
"valid (CloseFd p fd # s) \<Longrightarrow> is_file (CloseFd p fd # s) = (
+ − 599
case (file_of_proc_fd s p fd) of
+ − 600
Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
+ − 601
then (is_file s) (f := False)
+ − 602
else is_file s)
+ − 603
| _ \<Rightarrow> is_file s )"
+ − 604
apply (frule vd_cons, drule vt_grant_os, rule ext)
+ − 605
apply (auto dest:finum_has_itag iof's_im_in_cim
+ − 606
split:if_splits option.splits t_inode_tag.splits
+ − 607
simp:is_file_def)
+ − 608
done
+ − 609
+ − 610
lemma is_file_unlink:
+ − 611
"valid (UnLink p f # s) \<Longrightarrow> is_file (UnLink p f # s) = (
+ − 612
if (proc_fd_of_file s f = {}) then (is_file s) (f := False) else is_file s)"
+ − 613
apply (frule vd_cons, drule vt_grant_os, rule ext)
+ − 614
apply (auto dest:finum_has_itag iof's_im_in_cim
+ − 615
split:if_splits option.splits t_inode_tag.splits
+ − 616
simp:is_file_def)
+ − 617
done
+ − 618
+ − 619
lemma is_file_linkhard:
+ − 620
"valid (LinkHard p f f' # s) \<Longrightarrow> is_file (LinkHard p f f' # s) = (is_file s) (f' := True)"
+ − 621
apply (frule vd_cons, drule vt_grant_os, rule ext)
+ − 622
apply (auto dest:finum_has_itag iof's_im_in_cim
+ − 623
split:if_splits option.splits t_inode_tag.splits
+ − 624
simp:is_file_def)
+ − 625
done
+ − 626
+ − 627
lemma is_file_other:
+ − 628
"\<lbrakk>valid (e # \<tau>);
+ − 629
\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ − 630
\<forall> p fd. e \<noteq> CloseFd p fd;
+ − 631
\<forall> p f. e \<noteq> UnLink p f;
+ − 632
\<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> is_file (e # \<tau>) = is_file \<tau>"
+ − 633
apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
+ − 634
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ − 635
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ − 636
simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
+ − 637
done
+ − 638
+ − 639
lemma file_dir_conflict: "\<lbrakk>is_file s f; is_dir s f\<rbrakk> \<Longrightarrow> False"
+ − 640
by (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
+ − 641
+ − 642
lemma is_file_not_dir: "is_file s f \<Longrightarrow> \<not> is_dir s f"
+ − 643
by (rule notI, erule file_dir_conflict, simp)
+ − 644
+ − 645
lemma is_dir_not_file: "is_dir s f \<Longrightarrow> \<not> is_file s f"
+ − 646
by (rule notI, erule file_dir_conflict, simp)
+ − 647
+ − 648
lemmas is_file_simps = is_file_nil is_file_open is_file_closefd is_file_unlink is_file_linkhard is_file_other
+ − 649
+ − 650
(********* is_dir simpset **********)
+ − 651
+ − 652
lemma is_dir_mkdir: "valid (Mkdir p f i # s) \<Longrightarrow> is_dir (Mkdir p f i # s) = (is_dir s) (f := True)"
+ − 653
apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
+ − 654
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ − 655
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ − 656
simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
+ − 657
done
+ − 658
+ − 659
lemma is_dir_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> is_dir (Rmdir p f # s) = (is_dir s) (f := False)"
+ − 660
apply (frule vd_cons, drule vt_grant_os, rule_tac ext)
+ − 661
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ − 662
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ − 663
simp:is_dir_def dir_is_empty_def is_dir_def current_files_def)
+ − 664
done
+ − 665
+ − 666
lemma is_dir_other:
+ − 667
"\<lbrakk>valid (e # s);
+ − 668
\<forall> p f. e \<noteq> Rmdir p f;
+ − 669
\<forall> p f i. e \<noteq> Mkdir p f i\<rbrakk> \<Longrightarrow> is_dir (e # s) = is_dir s"
+ − 670
apply (frule vd_cons, drule vt_grant_os, rule_tac ext, case_tac e)
+ − 671
apply (auto dest:finum_has_itag iof's_im_in_cim intro!:ext
+ − 672
split:if_splits option.splits t_inode_tag.split t_socket_type.splits
+ − 673
simp:is_file_def dir_is_empty_def is_dir_def current_files_def)
+ − 674
apply (drule file_of_pfd_is_file, simp)
+ − 675
apply (simp add:is_file_def split:t_inode_tag.splits option.splits)
+ − 676
done
+ − 677
+ − 678
lemmas is_dir_simps = is_dir_nil is_dir_mkdir is_dir_rmdir is_dir_other
+ − 679
+ − 680
(*********** no root dir involved ***********)
+ − 681
+ − 682
lemma root_is_dir: "valid s \<Longrightarrow> is_dir s []"
+ − 683
apply (induct s, simp add:is_dir_nil root_is_init_dir)
+ − 684
apply (frule vd_cons, frule vt_grant_os, case_tac a)
+ − 685
apply (auto simp:is_dir_simps)
+ − 686
done
+ − 687
+ − 688
lemma root_is_dir': "\<lbrakk>is_file s []; valid s\<rbrakk> \<Longrightarrow> False"
+ − 689
apply (drule root_is_dir)
+ − 690
apply (erule file_dir_conflict, simp)
+ − 691
done
+ − 692
+ − 693
lemma noroot_execve:
+ − 694
"valid (Execve p f fds # s) \<Longrightarrow> f \<noteq> []"
+ − 695
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 696
+ − 697
lemma noroot_execve':
+ − 698
"valid (Execve p [] fds # s) \<Longrightarrow> False"
+ − 699
by (drule noroot_execve, simp)
+ − 700
+ − 701
lemma noroot_open:
+ − 702
"valid (Open p f flags fd opt # s) \<Longrightarrow> f \<noteq> []"
+ − 703
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir' split:option.splits)
+ − 704
+ − 705
lemma noroot_open':
+ − 706
"valid (Open p [] flags fd opt # s) \<Longrightarrow> False"
+ − 707
by (drule noroot_open, simp)
+ − 708
+ − 709
lemma noroot_filefd':
+ − 710
"\<lbrakk>file_of_proc_fd s p fd = Some []; valid s\<rbrakk> \<Longrightarrow> False"
+ − 711
apply (induct s arbitrary:p, simp)
+ − 712
apply (drule init_filefd_prop5, erule root_is_init_dir')
+ − 713
apply (frule vd_cons, frule vt_grant_os, case_tac a)
+ − 714
apply (auto split:if_splits option.splits dest!:root_is_dir')
+ − 715
done
+ − 716
+ − 717
lemma noroot_filefd:
+ − 718
"\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> f \<noteq> []"
+ − 719
by (rule notI, simp, erule noroot_filefd', simp)
+ − 720
+ − 721
lemma noroot_unlink:
+ − 722
"valid (UnLink p f # s) \<Longrightarrow> f \<noteq> []"
+ − 723
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 724
+ − 725
lemma noroot_unlink':
+ − 726
"valid (UnLink p [] # s) \<Longrightarrow> False"
+ − 727
by (drule noroot_unlink, simp)
+ − 728
+ − 729
lemma noroot_rmdir:
+ − 730
"valid (Rmdir p f # s) \<Longrightarrow> f \<noteq> []"
+ − 731
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 732
+ − 733
lemma noroot_rmdir':
+ − 734
"valid (Rmdir p [] # s) \<Longrightarrow> False"
+ − 735
by (drule noroot_rmdir, simp)
+ − 736
+ − 737
lemma noroot_mkdir:
+ − 738
"valid (Mkdir p f inum # s) \<Longrightarrow> f \<noteq> []"
+ − 739
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 740
+ − 741
lemma noroot_mkdir':
+ − 742
"valid (Mkdir p [] inum # s) \<Longrightarrow> False"
+ − 743
by (drule noroot_mkdir, simp)
+ − 744
+ − 745
lemma noroot_linkhard:
+ − 746
"valid (LinkHard p f f' # s) \<Longrightarrow> f \<noteq> [] \<and> f' \<noteq> []"
+ − 747
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 748
+ − 749
lemma noroot_linkhard':
+ − 750
"valid (LinkHard p [] f # s) \<Longrightarrow> False"
+ − 751
by (drule noroot_linkhard, simp)
+ − 752
+ − 753
lemma noroot_linkhard'':
+ − 754
"valid (LinkHard p f [] # s) \<Longrightarrow> False"
+ − 755
by (drule noroot_linkhard, simp)
+ − 756
+ − 757
lemma noroot_truncate:
+ − 758
"valid (Truncate p f len # s) \<Longrightarrow> f \<noteq> []"
+ − 759
by (frule vd_cons, drule vt_grant_os, auto dest!:root_is_dir')
+ − 760
+ − 761
lemma noroot_truncate':
+ − 762
"valid (Truncate p [] len # s) \<Longrightarrow> False"
+ − 763
by (drule noroot_truncate, simp)
+ − 764
+ − 765
lemmas noroot_events = noroot_execve noroot_open noroot_filefd noroot_unlink noroot_rmdir
+ − 766
noroot_mkdir noroot_linkhard noroot_truncate
+ − 767
+ − 768
lemmas noroot_events' = noroot_execve' noroot_open' noroot_filefd' noroot_unlink' noroot_rmdir'
+ − 769
noroot_mkdir' noroot_linkhard' noroot_linkhard'' noroot_truncate'
+ − 770
+ − 771
+ − 772
lemma is_file_in_current:
+ − 773
"is_file s f \<Longrightarrow> f \<in> current_files s"
+ − 774
by (auto simp:is_file_def current_files_def split:option.splits)
+ − 775
+ − 776
lemma is_dir_in_current:
+ − 777
"is_dir s f \<Longrightarrow> f \<in> current_files s"
+ − 778
by (auto simp:is_dir_def current_files_def split:option.splits)
+ − 779
+ − 780
+ − 781
(* simpset for same_inode_files: Current_files_prop.thy *)
+ − 782
+ − 783
lemma same_inode_files_nil:
+ − 784
"same_inode_files [] = init_same_inode_files"
+ − 785
by (rule ext, simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
+ − 786
+ − 787
lemma iof's_im_in_cim': "Some im = inum_of_file \<tau> f \<Longrightarrow> im \<in> current_inode_nums \<tau>"
+ − 788
by (auto simp add:current_inode_nums_def current_file_inums_def)
+ − 789
+ − 790
lemma same_inode_files_open:
+ − 791
"valid (Open p f flags fd opt # s) \<Longrightarrow> same_inode_files (Open p f flags fd opt # s) = (\<lambda> f'.
+ − 792
if (f' = f \<and> opt \<noteq> None) then {f} else same_inode_files s f')"
+ − 793
apply (frule vt_grant_os, frule vd_cons, rule ext)
+ − 794
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
+ − 795
dest:iof's_im_in_cim iof's_im_in_cim')
+ − 796
apply (drule is_file_in_current)
+ − 797
apply (simp add:current_files_def)
+ − 798
done
+ − 799
+ − 800
lemma same_inode_files_linkhard:
+ − 801
"valid (LinkHard p oldf f # s) \<Longrightarrow> same_inode_files (LinkHard p oldf f # s) = (\<lambda> f'.
+ − 802
if (f' = f \<or> f' \<in> same_inode_files s oldf)
+ − 803
then same_inode_files s oldf \<union> {f}
+ − 804
else same_inode_files s f')"
+ − 805
apply (frule vt_grant_os, frule vd_cons, rule ext)
+ − 806
apply (auto simp:same_inode_files_def is_file_simps split:if_splits option.splits
+ − 807
dest:iof's_im_in_cim iof's_im_in_cim')
+ − 808
apply (drule is_file_in_current)
+ − 809
apply (simp add:current_files_def is_file_def)
+ − 810
apply (simp add:is_file_def)
+ − 811
done
+ − 812
+ − 813
lemma inum_of_file_none_prop:
+ − 814
"\<lbrakk>inum_of_file s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"
+ − 815
by (simp add:current_files_def)
+ − 816
+ − 817
lemma same_inode_files_closefd:
+ − 818
"\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow>
+ − 819
same_inode_files (CloseFd p fd # s) f' = (
+ − 820
case (file_of_proc_fd s p fd) of
+ − 821
Some f \<Rightarrow> (if ((proc_fd_of_file s f = {(p, fd)}) \<and> (f \<in> files_hung_by_del s))
+ − 822
then same_inode_files s f' - {f}
+ − 823
else same_inode_files s f' )
+ − 824
| None \<Rightarrow> same_inode_files s f' )"
+ − 825
apply (frule vt_grant_os, frule vd_cons)
+ − 826
apply (auto simp:same_inode_files_def is_file_closefd current_files_closefd
+ − 827
split:if_splits option.splits
+ − 828
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
+ − 829
done
+ − 830
+ − 831
lemma same_inode_files_unlink:
+ − 832
"\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>
+ − 833
\<Longrightarrow> same_inode_files (UnLink p f # s) f' = (
+ − 834
if (proc_fd_of_file s f = {})
+ − 835
then same_inode_files s f' - {f}
+ − 836
else same_inode_files s f')"
+ − 837
apply (frule vt_grant_os, frule vd_cons)
+ − 838
apply (auto simp:same_inode_files_def is_file_unlink current_files_unlink
+ − 839
split:if_splits option.splits
+ − 840
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop)
+ − 841
done
+ − 842
+ − 843
lemma same_inode_files_mkdir:
+ − 844
"valid (Mkdir p f inum # s) \<Longrightarrow> same_inode_files (Mkdir p f inum # s) = (same_inode_files s)"
+ − 845
apply (frule vt_grant_os, frule vd_cons, rule ext)
+ − 846
apply (auto simp:same_inode_files_def is_file_simps current_files_simps
+ − 847
split:if_splits option.splits
+ − 848
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_in_current)
+ − 849
apply (simp add:current_files_def is_file_def)
+ − 850
done
+ − 851
+ − 852
lemma same_inode_files_other:
+ − 853
"\<lbrakk>valid (e # s);
+ − 854
\<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ − 855
\<forall> p fd. e \<noteq> CloseFd p fd;
+ − 856
\<forall> p f. e \<noteq> UnLink p f;
+ − 857
\<forall> p f f'. e \<noteq> LinkHard p f f'\<rbrakk> \<Longrightarrow> same_inode_files (e # s) = same_inode_files s"
+ − 858
apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e)
+ − 859
apply (auto simp:same_inode_files_def is_file_simps current_files_simps dir_is_empty_def
+ − 860
split:if_splits option.splits
+ − 861
dest:iof's_im_in_cim iof's_im_in_cim' inum_of_file_none_prop is_file_not_dir)
+ − 862
apply (simp add:is_file_def is_dir_def current_files_def split:option.splits t_inode_tag.splits)+
+ − 863
done
+ − 864
+ − 865
lemmas same_inode_files_simps = same_inode_files_nil same_inode_files_open same_inode_files_linkhard
+ − 866
same_inode_files_closefd same_inode_files_unlink same_inode_files_mkdir same_inode_files_other
+ − 867
+ − 868
lemma same_inode_files_prop1:
+ − 869
"f \<in> same_inode_files s f' \<Longrightarrow> f \<in> current_files s"
+ − 870
by (simp add:same_inode_files_def is_file_def current_files_def split:if_splits option.splits)
+ − 871
+ − 872
lemma same_inode_files_prop2:
+ − 873
"\<lbrakk>f \<in> same_inode_files s f'; f'' \<notin> current_files s\<rbrakk> \<Longrightarrow> f \<noteq> f''"
+ − 874
by (auto dest:same_inode_files_prop1)
+ − 875
+ − 876
lemma same_inode_files_prop3:
+ − 877
"\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
+ − 878
apply (rule notI)
+ − 879
apply (simp add:same_inode_files_def is_file_def is_dir_def
+ − 880
split:if_splits option.splits t_inode_tag.splits)
+ − 881
done
+ − 882
+ − 883
lemma same_inode_files_prop4:
+ − 884
"\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
+ − 885
by (auto simp:same_inode_files_def split:if_splits)
+ − 886
+ − 887
lemma same_inode_files_prop5:
+ − 888
"f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
+ − 889
by (auto simp:same_inode_files_def is_file_def split:if_splits)
+ − 890
+ − 891
lemma same_inode_files_prop6:
+ − 892
"f' \<in> same_inode_files s f \<Longrightarrow> same_inode_files s f' = same_inode_files s f"
+ − 893
by (auto simp:same_inode_files_def is_file_def split:if_splits)
+ − 894
+ − 895
lemma same_inode_files_prop7:
+ − 896
"f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f f'"
+ − 897
by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+ − 898
+ − 899
lemma same_inode_files_prop8:
+ − 900
"f' \<in> same_inode_files s f \<Longrightarrow> has_same_inode s f' f"
+ − 901
by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
+ − 902
+ − 903
+ − 904
end
+ − 905
+ − 906
end