equal
deleted
inserted
replaced
2103 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir) |
2103 apply (frule is_dir_in_current, rule impI, simp add:current_files_mkdir) |
2104 apply (frule current_file_has_sfile, simp, erule exE, simp) |
2104 apply (frule current_file_has_sfile, simp, erule exE, simp) |
2105 apply (drule cf2sfile_mkdir1, simp+) |
2105 apply (drule cf2sfile_mkdir1, simp+) |
2106 done |
2106 done |
2107 |
2107 |
2108 lemma same_inodes_Tainted: |
|
2109 "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)" |
|
2110 apply (frule same_inode_files_prop8, frule same_inode_files_prop7) |
|
2111 apply (auto intro:has_same_inode_Tainted) |
|
2112 done |
|
2113 |
2108 |
2114 lemma co2sobj_linkhard: |
2109 lemma co2sobj_linkhard: |
2115 "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> |
2110 "\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk> |
2116 \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = ( |
2111 \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = ( |
2117 case obj of |
2112 case obj of |
2149 |
2144 |
2150 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
2145 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp' |
2151 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
2146 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps tainted_eq_Tainted |
2152 same_inode_files_prop6 |
2147 same_inode_files_prop6 |
2153 dest:is_file_in_current is_dir_in_current) |
2148 dest:is_file_in_current is_dir_in_current) |
2154 |
2149 done |
2155 (* should delete has_same_inode !?!?*) |
|
2156 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits) |
|
2157 |
2150 |
2158 lemma co2sobj_kill: |
2151 lemma co2sobj_kill: |
2159 "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj" |
2152 "\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj" |
2160 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2153 apply (frule vt_grant_os, frule vd_cons, case_tac obj) |
2161 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |
2154 apply (simp_all add:current_files_simps is_dir_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted) |