--- a/Dynamic2static.thy	Mon Oct 21 16:18:19 2013 +0800
+++ b/Dynamic2static.thy	Tue Oct 22 10:08:27 2013 +0800
@@ -55,16 +55,10 @@
 sorry
 
 
-lemma tainted_has_sobj:
-  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
-apply (frule tainted_in_current, case_tac obj)
-apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits)
-oops
-
 lemma t2ts:
   "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
 apply (frule tainted_in_current, frule tainted_is_valid)
-apply (frule d2s_main', simp)
+apply (frule s2ss_included_sobj, simp)
 apply (case_tac sobj, simp_all)
 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits)
 apply (drule dir_not_tainted, simp)
@@ -91,9 +85,12 @@
     by (auto simp:taintable_def)
   hence vs: "valid s" by (simp add:tainted_is_valid)
   hence static: "s2ss s \<propto> static" using d2s_main by auto
-  from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry 
-(* should constrain undeletable with file/dir/process only, while msg and fd are excluded 
-    using vs tainted_has_sobj by blast *)
+  from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj" 
+    apply (clarsimp simp add:taintable_def)
+    apply (frule tainted_in_current)
+    apply (case_tac obj, simp_all add:co2sobj.simps)
+    apply (frule current_proc_has_sp, simp, auto)
+    done
   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"
@@ -182,6 +179,12 @@
 apply auto
 done
 
+lemma init_related_imp_init_sobj:
+  "init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj"
+apply (case_tac sobj, case_tac [!] obj, auto)
+apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto)
+done
+
 theorem undeletable_s_complete:
   assumes undel_s: "undeletable_s obj"
   shows "undeletable obj"
@@ -195,7 +198,11 @@
     then obtain s where vs: "valid s" and del: "deleted obj s" by auto
     from vs have vss: "s2ss s \<propto> static" by (rule d2s_main) 
     with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" 
-      and related: "init_obj_related sobj obj" apply auto
+      and related: "init_obj_related sobj obj" 
+      apply (simp add:init_ss_in_def init_ss_eq_def)
+      apply (erule bexE, erule_tac x= ss' in ballE)
+      apply (auto dest:init_related_imp_init_sobj)
+      done
     from init_alive del vs have "deletable_s obj" 
       by (auto elim:deleted_imp_deletable_s)
     with alive_s
@@ -210,14 +217,8 @@
 apply (erule swap)
 by (simp add:static_complete undeletable_s_complete)
 
-
-
 (************** static \<rightarrow> dynamic ***************)
 
-lemma created_can_have_many:
-  "\<lbrakk>valid s; alive s obj; \<not> init_alive obj\<rbrakk> \<Longrightarrow> \<exists> s'. valid s' \<and> alive s' obj \<and> alive s' obj' \<and> s2ss s = s2ss s'"
-sorry
-
 lemma s2d_main:
   "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
 apply (erule static.induct)
@@ -227,15 +228,6 @@
 
 sorry
 
-lemma tainted_s_in_ss:
-  "tainted_s ss sobj \<Longrightarrow> sobj \<in> ss"
-apply (case_tac sobj, simp_all)
-apply (case_tac bool, simp+)
-apply (case_tac bool, simp+)
-apply (case_tac prod1, case_tac prod2, simp)
-thm tainted_s.simps
-oops
-
 lemma set_eq_D:
   "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
 by auto
@@ -251,6 +243,8 @@
    \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
 by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)
 
+declare co2sobj.simps [simp add]
+
 lemma tainted_s_imp_tainted:
   "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
 apply (drule s2d_main)
@@ -264,29 +258,11 @@
 apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
 apply (rule_tac x = obj in exI, simp)
 apply (case_tac obj, (simp split:option.splits if_splits)+)
-
-apply (case_tac prod1, case_tac prod2, simp)
-apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) 
-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 (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:
-  "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"
-apply (erule tainted.induct)
-apply (auto intro:tainted.intros simp:has_same_inode_def)
-(*?? need simpset for tainted *)
-sorry
-
-lemma has_same_inode_tainted:
-  "\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s"
-by (drule has_inode_tainted_aux, auto simp:has_same_inode_def)
+lemma has_same_inode_prop3:
+  "has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f"
+by (auto simp:has_same_inode_def)
 
 theorem static_sound:
   assumes tbl_s: "taintable_s obj"
@@ -306,19 +282,14 @@
     apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def
                split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
     done
-  with tainted' have tainted: "obj \<in> tainted s"
-    by (auto intro:has_same_inode_tainted)
-  with vs init_alive
+  with tainted' vs have tainted: "obj \<in> tainted s"
+    by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted)
+  from sobj related init_alive have "appropriate obj"
+    by (case_tac obj, case_tac [!] sobj, auto)
+  with vs init_alive tainted
   show ?thesis by (auto simp:taintable_def)
 qed
 
-
-
-lemma ts2t:
-  "obj \<in> tainted_s ss \<Longrightarrow> \<exists> s. obj \<in> tainted s"
-  "obj \<in> tainted_s ss \<Longrightarrow> \<exists> so. so True \<in> ss \<Longrightarrow> so True \<in> ss \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<Longrightarrow> so True \<in> s2ss s \<Longrightarrow> tainted s obj. "
-
-
-
+end
 
 end
\ No newline at end of file