diff -r 0753309adfc7 -r 6f9a588bcfc4 S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/S2ss_prop.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -1875,9 +1875,9 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 done
 
-lemma has_same_inode_prop3:
-  "is_file s f \<Longrightarrow> has_same_inode s f f"
-by (auto simp:is_file_def has_same_inode_def split:option.splits)
+lemma same_inode_files_prop12:
+  "is_file s f \<Longrightarrow> f \<in> same_inode_files s f "
+by (auto simp:is_file_def  same_inode_files_def split:option.splits)
 
 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
 where
@@ -1900,12 +1900,11 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
-apply (simp add:same_inode_files_prop7)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
 apply (rule disjI2, simp, rule_tac x = obj in exI)
@@ -1916,7 +1915,7 @@
 apply (simp add:co2sobj_truncate)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
@@ -1933,13 +1932,12 @@
 apply (simp add:s2ss_def)
 apply (tactic {*my_seteq_tac 1*})
 apply (case_tac "obj = O_file f")
-apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
+apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted same_inode_files_prop12 cf2sfiles_other)
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (case_tac "fa \<in> same_inode_files s f")
 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
-apply (simp add:same_inode_files_prop7)
 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 apply (simp add:co2sobj_truncate is_file_simps)
 apply (rule notI, simp add:co2sobj_truncate is_file_simps)
@@ -1956,7 +1954,7 @@
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (tactic {*my_setiff_tac 1*})
 apply (rule_tac x = "O_file f" in exI)
-apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
+apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other same_inode_files_prop12)
 apply (tactic {*my_setiff_tac 1*})
 apply (erule_tac obj = obj in co2sobj_some_caseD)
 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)