643 lemma same_inode_files_prop9:

   644   "is_file s f \<Longrightarrow> f \<in> same_inode_files s f"

   645 by (simp add:same_inode_files_def)

   646 

   647 lemma cf2sfiles_prop:

   648   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> cf2sfiles s f = cf2sfiles s f'"

   649 apply (auto simp:cf2sfiles_def)

   650 apply (rule_tac x = f'a in bexI, simp)

   651 apply (erule same_inode_files_prop4, simp)

   652 apply (rule_tac x = f'a in bexI, simp)

   653 apply (drule same_inode_files_prop5)

   654 apply (erule same_inode_files_prop4, simp)

   655 done

   656 

   657 lemma co2sobj_writefile_unchange:

   658   "\<lbrakk>valid (WriteFile p fd # s); alive s obj; file_of_proc_fd s p fd = Some f;

   659     O_proc p \<in> Tainted s \<longrightarrow> O_file f \<in> Tainted s\<rbrakk> 

   660    \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = co2sobj s obj"

   661 apply (frule vd_cons, frule co2sobj_writefile, simp, simp split:t_object.splits if_splits)

   662 apply (simp add:co2sobj.simps)

   663 apply (case_tac "O_proc p \<in> Tainted s")

   664 apply (simp add:tainted_eq_Tainted same_inodes_Tainted)+

   665 done

   666 

   667 lemma s2ss_writefile:

   668   "valid (WriteFile p fd # s) \<Longrightarrow> s2ss (WriteFile p fd # s) = (

   669      case (file_of_proc_fd s p fd) of

   670        Some f \<Rightarrow> if (O_proc p \<in> Tainted s \<and> O_file f \<notin> Tainted s)

   671                  then (if (\<exists> f'. f' \<notin> same_inode_files s f \<and> is_file s f' \<and>

   672                                  co2sobj s (O_file f') = co2sobj s (O_file f))

   673                        then s2ss s \<union> {S_file (cf2sfiles s f) True}

   674                        else s2ss s - {S_file (cf2sfiles s f) False} 

   675                                    \<union> {S_file (cf2sfiles s f) True})

   676                  else s2ss s

   677      | _      \<Rightarrow> {})"

   678 apply (frule vd_cons, frule vt_grant_os)

   679 apply (clarsimp split:option.splits)

   680 unfolding s2ss_def

   681 apply (rule conjI|rule impI|erule exE|erule conjE)+

   682 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   683 apply (frule_tac obj =  obj in co2sobj_writefile, simp add:alive_other)

   684 apply (simp split:t_object.splits if_splits)

   685 apply (rule disjI2, rule_tac x= "O_proc nat" in exI, simp)

   686 apply (rule disjI1, simp add:cf2sfiles_prop)

   687 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_file_simps)

   688 apply (simp add:co2sobj.simps)

   689 apply (rule disjI2, rule_tac x = obj in exI, simp add:is_dir_simps)

   690 apply (simp add:co2sobj.simps)

   691 apply (simp add:co2sobj.simps)

   692 apply (simp add:co2sobj.simps)

   693 apply (rule disjI2, rule_tac x = obj in exI, simp)

   694 apply (rule disjI2, rule_tac x = obj in exI, simp)

   695 apply (simp add:co2sobj.simps)

   696 

   697 apply (simp, erule disjE)

   698 apply (rule_tac x = "O_file aa" in exI, simp add:is_file_simps file_of_pfd_is_file)

   699 apply (frule_tac obj = "O_file aa" in co2sobj_writefile, simp add:file_of_pfd_is_file)

   700 apply (simp split:if_splits add:same_inode_files_def file_of_pfd_is_file)

   701 apply (erule exE, erule conjE)

   702 apply (erule_tac obj = obj in co2sobj_some_caseD)

   703 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   704 apply (case_tac "fa \<in> same_inode_files s aa")

   705 apply (frule_tac f = fa and f' = aa in cf2sfiles_prop, simp)

   706 apply (rule_tac x = "O_file f'" in exI, simp add:co2sobj_writefile is_file_simps)

   707 apply (rule conjI, rule impI, simp add:same_inode_files_prop5)

   708 apply (rule impI, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   709 apply (rule_tac x = "O_file fa" in exI, simp add:co2sobj_writefile is_file_simps)

   710 apply (rule impI, simp add:same_inode_files_prop5)

   711 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   712 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   713 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   714 

   715 apply (rule impI, rule impI, simp, rule set_eqI, rule iffI, erule CollectE, (erule conjE|erule exE)+)

   716 apply (rule CollectI, rule_tac x = obj in exI, simp add:alive_simps)

   717 apply (simp add:co2sobj_writefile split:t_object.splits if_splits)

   718 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   719 apply (case_tac "O_proc p \<in> Tainted s", simp, simp)

   720 apply (erule CollectE, (erule conjE|erule exE)+, rule CollectI)

   721 apply (rule_tac x = obj in exI)

   722 apply (simp add:co2sobj_writefile_unchange alive_simps)

   723 

   724 apply (rule impI| rule conjI|erule conjE)+

   725 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE)

   726 apply (simp add:alive_simps co2sobj_writefile split:t_object.splits)

   727 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   728   rule notI, simp add:co2sobj.simps split:option.splits)

   729 apply (simp split:if_splits)

   730 apply (rule disjI1, simp add:cf2sfiles_prop)

   731 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp)

   732 apply (rule notI, simp add:co2sobj.simps split:option.splits)

   733 apply (erule_tac x = list in allE, simp add:tainted_eq_Tainted same_inode_files_prop5)

   734 apply (simp add:co2sobj.simps)

   735 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   736   rule notI, simp add:co2sobj.simps split:option.splits)

   737 apply (simp add:co2sobj.simps)

   738 apply (simp add:co2sobj.simps)

   739 apply (simp add:co2sobj.simps)

   740 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   741   rule notI, simp add:co2sobj.simps split:option.splits)

   742 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp,

   743   rule notI, simp add:co2sobj.simps split:option.splits)

   744 apply (simp add:co2sobj.simps)

   745 apply (simp)

   746 apply (erule disjE)

   747 apply (rule_tac x= "O_file aa" in exI, simp add:co2sobj_writefile alive_simps file_of_pfd_is_file)

   748 apply (rule impI, simp add:same_inode_files_def file_of_pfd_is_file)

   749 apply (erule exE|erule conjE)+

   750 apply (erule co2sobj_some_caseD)

   751 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   752 apply (case_tac "fa \<in> same_inode_files s aa")

   753 apply (frule cf2sfiles_prop, simp, simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)

   754 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_file_simps)

   755 apply (rule impI, simp add:same_inode_files_prop5)

   756 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   757 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile is_dir_simps)

   758 apply (rule_tac x = obj in exI, simp add:co2sobj_writefile)

   759 apply (rule impI, rule impI)

   760 

   761 apply (rule set_eqI, rule iffI, erule CollectE,erule exE,erule conjE,rule CollectI)

   762 apply (rule_tac x = obj in exI)

   763 apply (simp add:co2sobj_writefile_unchange alive_simps)

   764 apply (erule CollectE, erule exE, erule conjE)

   765 apply (rule CollectI, rule_tac x = obj in exI)

   766 apply (simp add:co2sobj_writefile_unchange alive_simps)

   767 done

   768 

   769