--- a/Dynamic_static.thy	Thu Oct 24 09:42:35 2013 +0800
+++ b/Dynamic_static.thy	Wed Oct 30 08:18:40 2013 +0800
@@ -1,32 +1,10 @@
 theory Dynamic_static
 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2
+ Temp
 begin
 
 context tainting_s begin
 
-definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100)
-where
-  "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss"
-
-lemma [simp]: "ss \<doteq> ss"
-by (auto simp:init_ss_eq_def)
-
-definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101)
-where
-  "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'"
-
-lemma s2ss_included_sobj:
-  "\<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 init_ss_in_prop:
-  "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk>
-   \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss"
-apply (simp add:init_ss_in_def init_ss_eq_def)
-apply (erule bexE, erule conjE)
-apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj)
-done
-
 
 
 
@@ -55,17 +33,6 @@
   "is_inited s obj = (\<not> is_created s obj)"
 by (auto simp:is_created_def is_inited_def)
 
-(* recorded in our static world *)
-fun recorded :: "t_object \<Rightarrow> bool"
-where
-  "recorded (O_proc p)     = True"
-| "recorded (O_file f)     = True"
-| "recorded (O_dir  f)     = True"
-| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
-| "recorded (O_shm  h)     = True"
-| "recorded (O_msgq q)     = True"
-| "recorded _              = False"
-
 
 
 
@@ -95,6 +62,16 @@
 sorry
 
 
+(* recorded in our static world *)
+fun recorded :: "t_object \<Rightarrow> bool"
+where
+  "recorded (O_proc p)     = True"
+| "recorded (O_file f)     = True"
+| "recorded (O_dir  f)     = True"
+| "recorded (O_node n)     = False" (* cause socket is temperary not considered *)
+| "recorded (O_shm  h)     = True"
+| "recorded (O_msgq q)     = True"
+| "recorded _              = False"
 
 lemma enrichability: 
   "\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>