--- a/os_rc.thy	Fri Apr 12 18:07:03 2013 +0100
+++ b/os_rc.thy	Thu Jun 13 22:12:45 2013 +0800
@@ -274,6 +274,35 @@
 apply (induct s) defer apply (case_tac a)
 using init_finite by auto
 
+end
+
+context tainting_s_complete begin
+
+lemma init_notin_curf_deleted:
+  "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curi_deleted:
+  "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curp_deleted:
+  "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
+by (induct s, simp, case_tac a, auto)
+  
+lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+by (induct f, auto split:if_splits)
+
+lemma source_proc_in_init:
+  "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
+apply (induct s arbitrary:p, simp split:if_splits)
+apply (frule valid_os, frule valid_cons, case_tac a)
+by (auto split:if_splits)
+
+end
+
+context tainting_s_sound begin
+
 (*** properties of new-proc new-ipc ... ***)
 
 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
@@ -299,22 +328,6 @@
 lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"
 by (simp add:ni_notin_curi)
 
-end
-
-context tainting_s_complete begin
-
-lemma init_notin_curf_deleted:
-  "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curi_deleted:
-  "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curp_deleted:
-  "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
-by (induct s, simp, case_tac a, auto)
-  
 lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"
 using ni_notin_curi[where \<tau> = s]
 by (drule_tac init_notin_curi_deleted, simp+)
@@ -323,18 +336,6 @@
 using np_notin_curp[where \<tau> = s]
 by (drule_tac init_notin_curp_deleted, simp+)
 
-lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
-by (induct f, auto split:if_splits)
-
-lemma source_proc_in_init:
-  "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
-apply (induct s arbitrary:p, simp split:if_splits)
-apply (frule valid_os, frule valid_cons, case_tac a)
-by (auto simp:np_notin_curp split:if_splits)
-
-end
-
-context tainting_s_sound begin
 
 lemma len_fname_all: "length (fname_all_a len) = len"
 by (induct len, auto simp:fname_all_a.simps)
@@ -366,7 +367,7 @@
 lemma clone_event_no_limit: 
   "\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"
 apply (rule vs_step)
-apply (auto intro:clone_no_limit split:option.splits
+apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp'
             dest:current_proc_has_role current_proc_has_type)
 done