--- a/S2ss_prop.thy	Sat Aug 31 00:35:36 2013 +0800
+++ b/S2ss_prop.thy	Mon Sep 02 11:12:42 2013 +0800
@@ -129,6 +129,14 @@
           split:if_splits option.splits t_inode_tag.splits)
 done
 
+lemma same_inode_files_prop4:
+  "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
+by (auto simp:same_inode_files_def split:if_splits)
+
+lemma same_inode_files_prop5:
+  "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
+by (auto simp:same_inode_files_def is_file_def split:if_splits)
+
 (* simpset for cf2sfiles *)
 
 lemma cf2sfiles_open:
@@ -167,6 +175,12 @@
 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
 done
 
+lemma cf2sfile_linkhard1':
+  "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>
+   \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
+apply (drule same_inode_files_prop1)
+by (simp add:cf2sfile_linkhard1)
+
 lemma cf2sfiles_linkhard:
   "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 
      if (f' = f \<or> f' \<in> same_inode_files s oldf)
@@ -175,13 +189,157 @@
            | _       \<Rightarrow> {})
      else cf2sfiles s f')"
 apply (frule vt_grant_os, frule vd_cons, rule ext)
-apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
-  split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1)
-apply (simp add:cf2sfiles_def)
+apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard 
+  split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)
+done
+
+lemma cf2sfile_unlink':
+  "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>
+   \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
+apply (drule same_inode_files_prop1)
+by (simp add:cf2sfile_unlink)
 
 lemma cf2sfiles_unlink:
+  "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( 
+     if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
+         (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then 
+        (case (cf2sfile s f) of 
+           Some sf \<Rightarrow> cf2sfiles s f' - {sf}
+         | _       \<Rightarrow> {})
+     else cf2sfiles s f')"
+apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)
+apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
+apply (simp add:current_files_unlink, simp, erule conjE)
+apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)
+apply (simp add:current_files_unlink same_inode_files_prop1, simp)
+apply (rule_tac x = f'a in bexI, simp, simp)
+apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
+apply (erule conjE|erule exE|erule bexE)+
+apply (case_tac "f'a = f", simp)
+apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)
+apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
+apply (rule_tac x = f'a in bexI, simp, simp)
+
+apply (rule impI)+
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
+apply (simp add:current_files_unlink, simp, (erule conjE)+)
+apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)
+apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
+apply (simp add:current_files_unlink, simp)
+apply (case_tac "f'a = f", simp)
+apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)
+apply (erule bexE, erule conjE)
+apply (rule_tac x = f'' in bexI)
+apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
+apply (simp, simp, erule same_inode_files_prop4, simp)
+apply (rule_tac x = f'a in bexI)
+apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
+apply (simp, simp)
+
+
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
+apply (simp add:current_files_unlink, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f' = f'a in cf2sfile_unlink)
+apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
+apply (simp add:current_files_unlink, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f' = f'a in cf2sfile_unlink)
+apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
+done
 
 lemma cf2sfiles_closefd:
+  "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (
+     case (file_of_proc_fd s p fd) of
+       Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> 
+                    (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) 
+                 then (case (cf2sfile s f) of 
+                         Some sf \<Rightarrow> cf2sfiles s f' - {sf}
+                       | _       \<Rightarrow> {})
+                 else cf2sfiles s f'
+     | _       \<Rightarrow> cf2sfiles s f')"
+
+apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")
+apply (simp_all add:current_files_simps split:if_splits)
+
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+
+apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)
+apply (frule is_file_has_sfile', simp, erule exE, simp)
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp, erule conjE)
+apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)
+apply (simp add:current_files_closefd same_inode_files_prop1, simp)
+apply (rule_tac x = f'a in bexI, simp, simp)
+apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
+apply (erule conjE|erule exE|erule bexE)+
+apply (case_tac "f'a = a", simp)
+apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)
+apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
+apply (rule_tac x = f'a in bexI, simp, simp)
+
+apply (rule impI)+
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp, (erule conjE)+)
+apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (case_tac "f'a = a", simp)
+apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)
+apply (erule bexE, erule conjE)
+apply (rule_tac x = f'' in bexI)
+apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
+apply (simp, simp, erule same_inode_files_prop4, simp)
+apply (rule_tac x = f'a in bexI)
+apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
+apply (simp, simp)
+
+apply (rule conjI, clarify)
+
+apply (rule impI)
+apply (case_tac "a \<in> files_hung_by_del s", simp_all)
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
+apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
+apply (simp add:current_files_closefd, simp)
+apply (rule_tac x = f'a in bexI)
+apply (frule_tac f = f'a in cf2sfile_closefd)
+apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
+done
 
 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
   cf2sfiles_unlink cf2sfiles_closefd
@@ -201,14 +359,15 @@
 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 apply (drule current_proc_has_sp', simp, simp)
 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
-
-apply (rule impI, simp add:cf2sfiles_def) defer
-
+apply (rule impI, simp add:cf2sfiles_other) 
 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 
+lemma co2sobj_
+
+
 end
 
 (* simpset for s2ss*)