# HG changeset patch
# User chunhan
# Date 1380171292 -28800
# Node ID b718662f61fa138f624c70d27fc6e31e209d9e69
# Parent  ed90f7d5e6d735087b1bf53aad3ee6eb4ea74c71
s2ss_rmdir

diff -r ed90f7d5e6d7 -r b718662f61fa S2ss_prop.thy
--- a/S2ss_prop.thy	Thu Sep 26 11:50:01 2013 +0800
+++ b/S2ss_prop.thy	Thu Sep 26 12:54:52 2013 +0800
@@ -1583,7 +1583,142 @@
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
 apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
 
+apply (rule impI)
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (subgoal_tac "alive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
 
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (rule_tac x =obj in exI)
+apply (subgoal_tac "alive (UnLink p f # s) obj")
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (auto simp add:co2sobj_unlink alive_simps split:t_object.splits)[1]
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (auto simp add:co2sobj_unlink is_file_simps is_dir_simps same_inode_files_prop9 split:t_object.splits)[1]
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (simp add:alive_simps co2sobj.simps)
+apply (rule conjI, rule notI, simp add:same_inode_files_prop9)
+apply (rule impI, frule_tac f' = f' in cf2sfiles_unlink)
+apply (simp add:current_files_simps is_file_simps is_file_in_current)
+apply (simp add:tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (case_tac "obj = O_file f", simp add:alive_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps is_dir_simps split:t_object.splits if_splits)
+apply (simp add:co2sobj.simps)
+apply (simp add:co2sobj.simps)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_file f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (simp split:if_splits option.splits add:is_file_simps)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (auto split:t_sobject.splits)[1]
+apply (simp add:is_file_simps same_inode_files_prop11)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (case_tac "fa \<in> same_inode_files s f")
+apply (rule_tac x = "O_file f'" in exI)
+apply (subgoal_tac "alive (UnLink p f # s) (O_file f')")
+apply (frule same_inode_files_prop11, frule_tac f = f' in is_file_has_sfile', simp add:vd_cons, erule exE)
+apply (frule_tac obj = "O_file f'" in co2sobj_unlink, simp)
+apply (simp split:if_splits option.splits add:is_file_simps)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (auto split:t_sobject.splits)[1]
+apply (simp add:is_file_simps same_inode_files_prop11)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_unlink)
+done
+
+definition del_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
+where
+  "del_s2ss_obj s ss obj sobj \<equiv> 
+     if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
+     then ss
+     else ss - {sobj}"
+
+lemma del_update_s2ss_obj:
+  "update_s2ss_obj s ss obj sobj sobj' = del_s2ss_obj s ss obj sobj \<union> {sobj'}"
+by (auto simp:update_s2ss_obj_def del_s2ss_obj_def split:if_splits)
+
+lemma s2ss_rmdir: "valid (Rmdir p f # s) \<Longrightarrow> s2ss (Rmdir p f # s) = (
+  case (co2sobj s (O_dir f)) of
+    Some sdir \<Rightarrow> del_s2ss_obj s (s2ss s) (O_dir f) sdir
+  | _         \<Rightarrow> {})"
+apply (frule vd_cons, frule vt_grant_os)
+apply (clarsimp simp:dir_is_empty_def)
+apply (frule is_dir_has_sdir', simp, erule exE)
+apply (simp split:option.splits, rule conjI, rule impI, simp add:co2sobj.simps)
+apply (rule allI, rule impI)
+
+apply (simp add:del_s2ss_obj_def)
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_rmdir is_file_simps is_dir_simps alive_simps split:t_object.splits if_splits)
+apply (tactic {*my_setiff_tac 1*})
+apply (case_tac "obj = O_dir f")
+apply (rule_tac x = obj' in exI)
+apply (subgoal_tac "alive (Rmdir p f # s) obj'")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:alive_rmdir)
+apply (rule_tac x = obj in exI)
+apply (subgoal_tac "alive (Rmdir p f # s) obj")
+apply (auto simp add:co2sobj_rmdir is_file_simps is_dir_simps split:t_object.splits)[1]
+apply (simp add:alive_rmdir)
+
+apply (rule conjI|rule impI|erule exE|erule conjE)+
+apply (simp add:s2ss_def)
+apply (tactic {*my_seteq_tac 1*})
+apply simp
+apply (case_tac "obj = O_dir f", simp add:alive_rmdir)
+apply (rule conjI)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+apply (simp add:co2sobj_rmdir)
+apply (simp add:alive_rmdir, erule_tac x = obj in allE, simp)
+apply (tactic {*my_setiff_tac 1*}, simp)
+apply (case_tac "obj = O_dir f", simp)
+apply (rule_tac x = obj in exI, simp add:co2sobj_rmdir alive_rmdir)
+done
 
 
 
@@ -1591,5 +1726,5 @@
 
 
 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
-  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink
+  s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir