--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/source_prop.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,75 @@
+theory source_prop
+imports Main rc_theory os_rc deleted_prop obj2sobj_prop
+begin
+
+context tainting_s_complete begin
+
+lemma all_sobjs_srp_init'[rule_format]:
+  "sobj \<in> all_sobjs \<Longrightarrow> \<forall> sp srp. sobj = SProc sp (Some srp) \<longrightarrow> srp \<in> init_processes"
+apply (erule all_sobjs.induct, auto) 
+using init_proc_has_type 
+by (simp add:bidirect_in_init_def)
+
+lemma all_sobjs_srp_init:
+  "SProc sp (Some srp) \<in> all_sobjs \<Longrightarrow> srp \<in> init_processes"
+by (auto dest!:all_sobjs_srp_init')
+
+(*
+lemma tainted_sproc_srp_init:
+  "SProc sp (Some srp) \<in> tainted_s \<Longrightarrow> srp \<in> init_processes"
+by (auto dest:tainted_s_in_all_sobjs intro:all_sobjs_srp_init) *)
+
+lemma source_proc_of_init_remains:
+  "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
+apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists)
+done
+
+lemma init_proc_keeps_source:
+  "\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> 
+   \<Longrightarrow> source_of_sobj (obj2sobj s (Proc p)) = Some (Proc p)"
+apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)
+apply (frule current_proc_has_sproc, simp)
+apply (clarsimp split:option.splits simp:source_proc_of_init_remains)
+done
+
+lemma init_file_keeps_source:
+  "\<lbrakk>f \<in> init_files; \<not> deleted (File f) s; valid s\<rbrakk> 
+   \<Longrightarrow> source_of_sobj (obj2sobj s (File f)) = Some (File f)"
+apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)
+apply (frule current_file_has_sfile, auto)
+done
+
+lemma init_ipc_keeps_source:
+  "\<lbrakk>i \<in> init_ipcs; \<not> deleted (IPC i) s; valid s\<rbrakk> 
+   \<Longrightarrow> source_of_sobj (obj2sobj s (IPC i)) = Some (IPC i)"
+apply (frule not_deleted_imp_exists, simp, simp only:exists.simps)
+apply (frule current_ipc_has_sipc, auto)
+done
+ 
+lemma init_obj_keeps_source: 
+  "\<lbrakk>exists [] obj; \<not> deleted obj s; valid s\<rbrakk> \<Longrightarrow> source_of_sobj (obj2sobj s obj) = Some obj"
+apply (case_tac obj)
+by (auto intro:init_ipc_keeps_source init_proc_keeps_source init_file_keeps_source 
+      simp del:obj2sobj.simps)
+
+end
+
+context tainting_s_sound begin
+
+lemma source_eq:
+  "\<lbrakk>source_of_sobj sobj = Some obj; sobj_source_eq_obj sobj obj'\<rbrakk> \<Longrightarrow> obj = obj'"
+apply (case_tac obj, case_tac [!] sobj, case_tac [!] obj')
+by (auto split:option.splits)
+
+lemma proc_source_eq_prop:
+  "\<lbrakk>obj2sobj s (Proc p) = SProc sp srp; p \<in> current_procs s;
+    sobj_source_eq_obj (SProc sp srp) (Proc p); valid s\<rbrakk>
+  \<Longrightarrow> srp = Some p"
+apply (frule current_proc_has_srp,auto split:option.splits)
+by (case_tac "source_proc s p", simp+)
+
+end
+
+end
\ No newline at end of file