diff -r 021672ec28f5 -r 137358bd4921 Dynamic2static.thy
--- a/Dynamic2static.thy	Thu Sep 05 13:23:03 2013 +0800
+++ b/Dynamic2static.thy	Thu Sep 12 13:50:22 2013 +0800
@@ -22,8 +22,8 @@
   "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
 by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
 
-lemma alive_has_sobj:
-  "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
+lemma tainted_has_sobj:
+  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
 sorry
 
 lemma t2ts:
@@ -37,12 +37,7 @@
 apply (drule dir_not_tainted, simp)
 apply (drule msgq_not_tainted, simp)
 apply (drule shm_not_tainted, simp)
-apply (case_tac prod1, simp, case_tac prod2, clarsimp)
-apply (rule conjI)
-apply (rule_tac x = "O_msgq nat1" in exI, simp)
-apply (rule conjI) defer
-apply (simp add:cm2smsg_def split:option.splits) 
-sorry
+done
 
 lemma delq_imp_delqm:
   "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
@@ -57,21 +52,28 @@
     by (auto simp:taintable_def)
   hence vs: "valid s" by (simp add:tainted_is_valid)
   hence static: "s2ss s \<in> static" using d2s_main by auto
-  from tainted have alive: "alive s obj" 
-    using tainted_in_current by auto
-  then obtain sobj where sobj: "co2sobj s obj = Some sobj"
-    using vs alive_has_sobj by blast
+  from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj"
+    using vs tainted_has_sobj by blast
   from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" 
     by (auto simp:undeletable_def)
   with vs sobj have "init_obj_related sobj obj"
     apply (case_tac obj, case_tac [!] sobj)
     apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
-    apply (frule not_deleted_init_file, simp+) (*
-apply (drule is_file_has_sfile, erule exE)
+    apply (frule not_deleted_init_file, simp+) 
+    apply (drule is_file_has_sfile', simp, erule exE)
     apply (rule_tac x = sf in bexI)
     apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]
-    apply (simp add:same_inode_files_def cfs2sfiles_def) *)  
-    sorry
+    apply (drule root_is_init_dir', simp)
+    apply (frule not_deleted_init_file, simp, simp)
+    apply (simp add:cf2sfile_def split:option.splits if_splits)
+    apply (simp add:cf2sfiles_def)
+    apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file)
+
+    apply (frule not_deleted_init_dir, simp+)
+    apply (simp add:cf2sfile_def split:option.splits if_splits)
+    apply (case_tac list, simp add:sroot_def, simp)
+    apply (drule file_dir_conflict, simp+)
+    done
   with tainted t2ts init_alive sobj static
   show ?thesis unfolding taintable_s_def
     apply (rule_tac x = "s2ss s" in bexI, simp)
@@ -189,7 +191,7 @@
 lemma cqm2sms_prop1:
   "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
 apply (induct queue arbitrary:sms)
-apply (auto split:option.splits)
+apply (auto simp:cqm2sms.simps split:option.splits)
 done
 
 lemma sq_sm_prop:
@@ -216,7 +218,11 @@
 apply (case_tac obj, simp_all split:option.splits if_splits)
 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
 apply (rule_tac x = "O_msg nat m" in exI)
-apply (simp add:cm2smsg_def split:option.splits)
+apply (rule conjI)
+apply simp
+apply (simp add
+apply (simp add:co2sobj.simps)
+apply (simp add:cm2smsg_def split:option.splits if_splits)
 done
 
 lemma has_inode_tainted_aux: