357 qed |
357 qed |
358 |
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" |
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) |
360 by (rule hung_file_no_des_aux[rule_format], blast) |
361 |
361 |
|
362 (* current version, dir can not be opened, so hung_files are all files |
362 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" |
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" |
363 apply (frule hung_file_has_inum', simp, erule exE) |
364 apply (frule hung_file_has_inum', simp, erule exE) |
364 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) |
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) |
365 by (simp add: noJ_Anc, auto dest:hung_file_no_des) |
366 by (simp add: noJ_Anc, auto dest:hung_file_no_des) |
366 |
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 |
367 |
425 |
368 |
426 |
369 (************** file_of_proc_fd in current ********************) |
427 (************** file_of_proc_fd in current ********************) |
370 |
428 |
371 lemma file_of_pfd_imp_inode_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" |
|
372 apply (induct \<tau>) |
|
373 apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum) |
|
374 apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a) |
|
375 apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def is_file_def |
|
376 split:if_splits option.splits) |
|
377 apply (simp add:pfdof_simp3)+ |
|
378 apply (simp add:proc_fd_of_file_def)+ |
|
379 done |
|
380 |
|
381 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" |
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" |
382 by (rule file_of_pfd_imp_inode_aux[rule_format], blast) |
430 by (drule file_of_pfd_2in1, blast) |
383 |
431 |
384 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" |
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" |
385 by (auto dest!:file_of_pfd_imp_inode') |
433 by (auto dest!:file_of_pfd_imp_inode') |
386 |
434 |
387 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>" |
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>" |
388 by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def) |
436 by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def) |
389 |
437 |
390 |
438 |
391 (*************** file_of_proc_fd is file *********************) |
439 (*************** file_of_proc_fd is file *********************) |
392 |
440 |
393 lemma file_of_pfd_is_file_tag: |
|
394 "\<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" |
|
395 apply (induct \<tau> arbitrary:p, simp) |
|
396 apply (drule init_filefd_prop5, simp add:is_init_file_def split:option.splits t_inode_tag.splits) |
|
397 apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) |
|
398 by (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits |
|
399 dest:file_of_pfd_imp_inode' iof's_im_in_cim |
|
400 simp:is_file_def is_dir_def dir_is_empty_def current_files_def) |
|
401 |
|
402 lemma file_of_pfd_is_file: |
441 lemma file_of_pfd_is_file: |
403 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
442 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f" |
404 apply (frule file_of_pfd_imp_inode, simp, erule exE) |
443 by (drule file_of_pfd_2in1, auto simp:is_file_def) |
405 apply (drule file_of_pfd_is_file_tag, simp+) |
|
406 by (simp add:is_file_def) |
|
407 |
444 |
408 lemma file_of_pfd_is_file': |
445 lemma file_of_pfd_is_file': |
409 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
446 "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False" |
410 by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits) |
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) |
411 |
452 |
412 (************** parent file / ancestral file is dir *******************) |
453 (************** parent file / ancestral file is dir *******************) |
413 |
454 |
414 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" |
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" |
415 apply (induct \<tau>) |
456 apply (induct \<tau>) |