diff -r b992684e9ff6 -r dcde836219bc del_vs_del_s.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/del_vs_del_s.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,277 @@
+theory del_vs_del_s
+imports Main rc_theory os_rc obj2sobj_prop all_sobj_prop 
+begin
+
+context tainting_s_complete begin
+
+lemma deleted_has_del_event_proc:
+  "\<lbrakk>deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p'. Kill p' p # s' \<preceq> s \<and> \<not> deleted (Proc p) s'"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os)
+by (case_tac a, auto simp:no_junior_def)
+
+lemma deleted_has_del_event_ipc:
+  "\<lbrakk>deleted (IPC i) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteIPC p i # s' \<preceq> s \<and> \<not> deleted (IPC i) s'"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os)
+by (case_tac a, auto simp:no_junior_def)
+
+lemma deleted_has_del_event_file:
+  "\<lbrakk>deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteFile p f # s' \<preceq> s \<and> \<not> deleted (File f) s'"
+apply (induct s, simp)
+apply (frule valid_cons, frule valid_os)
+by (case_tac a, auto simp:no_junior_def)
+
+(*
+lemma noJ_Anc: "x \<prec> y = (x \<preceq> y \<and> x \<noteq> y)"
+apply (simp add: no_junior_expand)
+by (auto simp:is_ancestor_def)
+
+lemma noJ_Anc': "x \<prec> y \<Longrightarrow> (x \<preceq> y \<and> x \<noteq> y)"
+by (simp add:noJ_Anc)
+
+lemma noJ_Anc'': "\<lbrakk>x \<preceq> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<prec> y"
+by (simp add:noJ_Anc)
+
+lemma deled_imp_no_childfs:
+  "\<lbrakk>valid (DeleteFile p f # s); f \<prec> childf\<rbrakk> \<Longrightarrow> childf \<notin> current_files s"
+apply (frule valid_cons, drule valid_os, rule notI, clarsimp dest!:noJ_Anc')
+apply (drule ancient_has_parent, simp, clarsimp)
+apply (drule_tac af = sonf and f = childf in ancient_file_in_current, simp+)
+apply (case_tac sonf, simp)
+apply (erule_tac x = a in allE, simp)
+done
+
+lemma deled_imp_childfs_deleted:
+  "\<lbrakk>valid (DeleteFile p f # s); f \<prec> childf; childf \<in> init_files\<rbrakk>
+  \<Longrightarrow> deleted (File childf) s"
+apply (drule deled_imp_no_childfs, simp+)
+apply (erule_tac P = "childf \<in> current_files s" in swap)
+by (drule not_deleted_imp_exists, simp+)
+
+lemma initf_deled_imp_childf_deled:
+  "\<lbrakk>deleted (File f) s; valid s\<rbrakk> \<Longrightarrow> \<exists> s' p. DeleteFile p f # s' \<preceq> s \<and> \<not> deleted (File f) s' \<and> (\<forall> childf \<in> init_files. f \<prec> childf \<longrightarrow> deleted (File childf) s')"
+apply (drule deleted_has_del_event_file, simp, clarify)
+apply (rule_tac x = s' in exI, rule_tac x = p in exI, simp)
+apply (rule ballI, rule impI, frule vs_history, simp)
+by (erule deled_imp_childfs_deleted, simp+)
+
+lemma initf_deled_imp_childf_deled:
+  "\<lbrakk>deleted (File f) s; valid s; f \<prec> childf; childf \<in> init_files\<rbrakk> 
+  \<Longrightarrow> \<exists> s'. s' \<preceq> s \<and> valid s' \<and> deleted (File childf) s'"
+apply (drule deleted_has_del_event_file, simp, clarify)
+apply (frule vs_history, simp, frule valid_cons)
+apply (drule deled_imp_childfs_deleted, simp, simp)
+apply (rule_tac x = s' in exI, auto elim:no_juniorE)
+done
+
+lemma deleted_has_del_event_allchildf:
+  "\<lbrakk>deleted (File f) s; valid s; f \<preceq> childf; childf \<in> init_files\<rbrakk>
+  \<Longrightarrow> \<exists> s' p. DeleteFile p childf # s' \<preceq> s \<and> \<not> deleted (File childf) s'"
+apply (case_tac "f = childf")
+apply (drule deleted_has_del_event_file, simp, simp)
+apply (drule noJ_Anc'', simp)
+apply (drule initf_deled_imp_childf_deled, simp+, clarify)
+apply (drule deleted_has_del_event_file, simp+, clarify)
+apply (rule_tac x = s'a in exI, rule conjI, rule_tac x = p in exI)
+apply (erule no_junior_trans, simp+)
+done
+*)
+
+lemma del_imp_del_s_file:
+  assumes initf: "f \<in> init_files"
+  and deled: "deleted (File f) s"
+  and vs: "valid s"
+  shows "file_deletable_s f"
+proof -
+  from deled vs obtain s' p' where
+    his: "DeleteFile p' f # s' \<preceq> s" and fstdel: "\<not> deleted (File f) s'"
+    by (drule_tac deleted_has_del_event_file, auto)
+  from his vs have "valid (DeleteFile p' f # s')" by (simp add:vs_history)
+  hence exp': "p' \<in> current_procs s'" and exf: "f \<in> current_files s'"
+    and rc: "rc_grant s' (DeleteFile p' f)" and vs': "valid s'"
+    by (auto dest:valid_os valid_rc valid_cons)
+
+  from initf obtain t where etype: "etype_of_file [] f = Some t"
+    by (drule_tac init_file_has_etype, simp add:etype_of_file_def, blast)
+  from initf have sd: "source_dir [] f = Some f"
+    by (simp add:source_dir_of_init') 
+  hence "obj2sobj [] (File f) = SFile (t, f) (Some f)"
+    using etype initf by (auto simp:obj2sobj.simps)
+  with fstdel vs' initf exf etype
+  have SF: "obj2sobj s' (File f) = SFile (t, f) (Some f)"
+    using obj2sobj_file_remains'''[where s = "[]" and s' = s']
+    by (auto simp:obj2sobj.simps)
+
+  from exp' vs' obtain r' fr' pt' u' srp' where
+    SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"
+    by (frule_tac current_proc_has_sobj, simp, blast)
+  with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]
+  have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp
+
+  show ?thesis unfolding file_deletable_s_def
+    apply (rule_tac x = t in exI, 
+           rule_tac x = "(r',fr',pt',u')" in exI,
+           rule_tac x = srp' in exI)
+    apply (simp add:SP'_in) 
+    using rc SP' SF etype
+    by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits if_splits)
+qed
+
+lemma del_imp_del_s_proc:
+  assumes initp: "p \<in> init_processes"
+  and deled: "deleted (Proc p) s"
+  and vs: "valid s"
+  shows "proc_deletable_s p"
+proof-
+  from deled vs obtain s' p' where
+    his: "Kill p' p # s' \<preceq> s" and fstdel: "\<not> deleted (Proc p) s'"
+    by (drule_tac deleted_has_del_event_proc, auto)
+  from his vs have "valid (Kill p' p # s')" by (simp add:vs_history)
+  hence exp': "p' \<in> current_procs s'" and exp: "p \<in> current_procs s'"
+    and rc: "rc_grant s' (Kill p' p)" and vs': "valid s'"
+    by (auto dest:valid_os valid_rc valid_cons)
+
+  from initp fstdel vs' have "source_proc s' p = Some p"
+    apply (induct s', simp)
+    apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
+    by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp)
+  with exp initp vs' obtain r fr pt u 
+    where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"
+    apply (frule_tac current_proc_has_sobj, simp)
+    by (simp add:obj2sobj.simps split:option.splits, blast)
+  with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"]
+  have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp
+
+  from exp' vs' obtain r' fr' pt' u' srp' where
+    SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"
+    by (frule_tac current_proc_has_sobj, simp, blast)
+  with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]
+  have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp
+
+  show ?thesis unfolding proc_deletable_s_def
+    apply (rule_tac x = r in exI, rule_tac x = fr in exI,
+           rule_tac x = pt in exI, rule_tac x = u in exI,
+           rule_tac x = "(r',fr',pt',u')" in exI,
+           rule_tac x = srp' in exI)
+    apply (simp add:SP_in SP'_in) 
+    using rc SP SP'
+    by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits)
+qed
+    
+lemma del_imp_del_s_ipc:
+  assumes initi: "i \<in> init_ipcs"
+  and deled: "deleted (IPC i) s"
+  and vs: "valid s"
+  shows "ipc_deletable_s i"
+proof-
+  from deled vs obtain s' p' where
+    his: "DeleteIPC p' i # s' \<preceq> s" and fstdel: "\<not> deleted (IPC i) s'"
+    by (drule_tac deleted_has_del_event_ipc, auto)
+  from his vs have "valid (DeleteIPC p' i # s')" by (simp add:vs_history)
+  hence exp': "p' \<in> current_procs s'" and exi: "i \<in> current_ipcs s'"
+    and rc: "rc_grant s' (DeleteIPC p' i)" and vs': "valid s'"
+    by (auto dest:valid_os valid_rc valid_cons)
+
+  from initi obtain t where type: "init_ipc_type i = Some t" 
+    using init_ipc_has_type by (auto simp:bidirect_in_init_def)
+  with fstdel vs' initi exi have SI: "obj2sobj s' (IPC i) = SIPC t (Some i)"
+    using obj2sobj_ipc_remains'''[where s = "[]" and s' = s']
+    by (auto simp:obj2sobj.simps)
+
+  from exp' vs' obtain r' fr' pt' u' srp' where
+    SP': "obj2sobj s' (Proc p') = SProc (r',fr',pt',u') srp'"
+    by (frule_tac current_proc_has_sobj, simp, blast)
+  with exp' vs' all_sobjs_I[where s = s' and obj = "Proc p'"]
+  have SP'_in: "SProc (r',fr',pt',u') srp' \<in> all_sobjs" by simp
+
+  show ?thesis unfolding ipc_deletable_s_def
+    apply (rule_tac x = t in exI, 
+           rule_tac x = "(r',fr',pt',u')" in exI,
+           rule_tac x = srp' in exI)
+    apply (simp add: SP'_in) 
+    using rc SP' SI type
+    by (auto simp:obj2sobj.simps cp2sproc.simps split:option.splits if_splits)
+qed
+
+lemma deleted_imp_deletable_s:
+  "\<lbrakk>deleted obj s; exists [] obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
+apply (case_tac obj)  
+apply (simp add:del_imp_del_s_proc)  
+apply (simp add:del_imp_del_s_file) 
+apply (simp add:del_imp_del_s_ipc)
+done
+
+(*
+lemma all_sobjs_E3:
+  assumes prem: "sobj \<in> all_sobjs" 
+  shows "\<exists> s obj. valid s \<and> obj2sobj s obj = sobj \<and> sobj_source_eq_obj sobj obj \<and> 
+                  initp_intact_but s sobj \<and> exists s obj \<and> no_del_event s"
+proof-
+  obtain t where "etype_of_file [] [] = Some t" 
+    using root_in_filesystem current_file_has_etype[of "[]" "[]"] vs_nil 
+    by auto
+  with root_in_filesystem
+  have "obj2sobj [] (File []) = SFile (t,[]) (Some [])"
+    by (auto simp:obj2sobj.simps source_dir_of_init' 
+            split:option.splits if_splits)
+  moreover have "initp_intact []"
+    by (auto simp:initp_intact_def cp2sproc.simps obj2sobj.simps 
+            split:option.splits)
+  ultimately show ?thesis
+    using prem vs_nil root_in_filesystem 
+    apply (drule_tac s' = "[]" and obj' = "File []" in all_sobjs_E2)
+    apply (simp+, (erule exE|erule conjE)+)
+    by (rule_tac x = s in exI, simp, rule_tac x = obj in exI, simp+)
+qed
+
+lemma del_s_imp_del_proc:
+  assumes initp: "p \<in> init_processes"
+  and del_s: "proc_deletable_s p"
+  shows "\<exists> s. valid s \<and> deleted (Proc p) s"
+proof-
+  from del_s obtain r fr pt u sp' srp' 
+    where Target: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" 
+    and Killer: "SProc sp' srp' \<in> all_sobjs"
+    and rc: "(role_of_sproc sp', Proc_type pt, DELETE) \<in> compatible"
+    using proc_deletable_s_def by auto
+  
+  from Target obtain s where vs: "valid s" 
+    and "obj2sobj s (Proc p) = SProc (r,fr,pt,u) (Some p)" 
+    and "exists s (Proc p)"  and "no_del_event s"
+    and "initp_intact_but s (SProc (r,fr,pt,u) (Some p))"
+    apply (drule_tac all_sobjs_E3, clarsimp)
+    by (frule obj2sobj_proc, clarsimp)
+  with Killer obtain s' p' where vs': "valid (s' @ s)" and
+    SP : "obj2sobj (s' @ s) (Proc p) = SProc (r,fr,pt,u) (Some p)" and
+    exp: "exists (s' @ s) (Proc p)"  and
+    SP': "obj2sobj (s' @ s) (Proc p') = SProc sp' srp'" and
+    exp': "exists (s' @ s) (Proc p')"
+    apply (drule_tac obj' = "Proc p" and s' = s in all_sobjs_E1, auto)
+    apply (frule_tac obj = obj in obj2sobj_proc, erule exE)
+    apply (auto intro:nodel_exists_remains)
+    apply blast
+    apply (frule_tac obj = "Proc p" in nodel_exists_remains)
+
+
+lemma deletable_s_imp_deleted:
+  "deletable_s obj \<Longrightarrow> \<exists> s. valid s \<and> deleted obj s"
+apply (case_tac obj)
+apply (simp add:deletable_s.simps)
+
+
+lemma valid_kill_imp_proc_del_s:
+  "\<lbrakk>valid (Kill p' p # s); p \<in> init_processes; \<not> deleted (Proc p) s\<rbrakk> \<Longrightarrow> proc_deletable_s p"
+apply (frule valid_os, frule valid_
+
+
+lemma build_phase: "f \<in> init_files \<and> file_deletable_s f \<longrightarrow> (\<exists> s. \<forall> childf. valids s \<and> f \<preceq> childf \<and> childf \<in> init_files \<and> etype_of_file [] f = Some t \<longrightarrow> (\<exists> p. p \<in> current_procs s \<and> currentrole s p = Some r \<and> (r, File_type t, DELETE) \<in> compatible))"
+ thm all_sobjs_E0
+
+lemma del_phase: "f \<in> init_files \<and> file_deletable_s f \<and> (\<forall> childf. f \<preceq> childf \<and> childf \<notin> current_files s \<and> valid s"
+
+*)
+
+end
+
+end
\ No newline at end of file