diff -r b992684e9ff6 -r dcde836219bc sound_defs_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sound_defs_prop.thy	Fri Apr 12 10:43:11 2013 +0100
@@ -0,0 +1,198 @@
+theory sound_defs_prop
+imports rc_theory Main os_rc obj2sobj_prop
+begin
+
+context tainting_s_sound begin
+
+lemma not_both_I:
+  "not_both_sproc (SProc sp srp) sobj \<Longrightarrow> not_both_sproc sobj' sobj"
+by (case_tac sobj, auto)
+
+lemma not_both_I_file:
+  "not_both_sproc (SFile sf srf) sobj \<Longrightarrow> not_both_sproc (SFile sf' srf') sobj"
+by (case_tac sobj, auto)
+
+lemma not_both_I_ipc:
+  "not_both_sproc (SIPC si sri) sobj \<Longrightarrow> not_both_sproc (SIPC si' sri') sobj"
+by (case_tac sobj, auto)
+
+lemma intact_imp_butp:
+  "\<lbrakk>p \<in> init_processes; initp_intact s\<rbrakk> \<Longrightarrow> initp_intact_butp s p "
+by (auto simp:initp_intact_def initp_intact_butp_def initp_alter_def)
+
+lemma no_sproc_imp_intact:
+  "\<lbrakk>not_both_sproc (SProc sp srp) sobj; initp_intact_but s sobj\<rbrakk> \<Longrightarrow> initp_intact s"
+by (case_tac sobj, simp_all)
+
+lemma initp_intact_but_nil:"initp_intact_but [] (init_obj2sobj obj)"  
+apply (case_tac obj)
+apply (auto simp:initp_intact_def initp_intact_butp_def initp_alter_def split:option.splits)
+apply (rule_tac x = nat in exI) using init_proc_has_role 
+by (auto simp:bidirect_in_init_def)
+
+lemma init_alterp_exec:
+  "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (Execute p f # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_alter (Execute p f # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)
+apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (case_tac "p' = p")
+apply (rule_tac x = "new_proc s" in exI) defer
+apply (rule_tac x = p' in exI)
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')
+done
+
+lemma init_alterp_chown:
+  "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (ChangeOwner p u # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_alter (ChangeOwner p u # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)
+apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (case_tac "p' = p")
+apply (rule_tac x = "new_proc s" in exI) defer
+apply (rule_tac x = p' in exI)
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')
+done
+
+lemma init_alterp_crole:
+  "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (ChangeRole p r # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_alter (ChangeRole p r # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)
+apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (case_tac "p' = p")
+apply (rule_tac x = "new_proc s" in exI) defer
+apply (rule_tac x = p' in exI)
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')
+done
+
+lemma init_alterp_other:
+  "\<lbrakk>initp_alter s p; valid (e # s); \<forall> p f. e \<noteq> Execute p f;
+    \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>
+  \<Longrightarrow> initp_alter (e # s) p"
+apply (frule valid_cons, frule valid_os)
+apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (rule_tac x = p' in exI, case_tac e)
+apply (auto simp add: cp2sproc_simps' simp del:cp2sproc.simps split:option.splits)
+done
+
+lemma initp_intact_butp_I_exec:
+  "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; valid (Execute p f # Clone p (new_proc s) # s); 
+    no_del_event s\<rbrakk>
+  \<Longrightarrow> initp_intact_butp (Execute p f # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def initp_intact_butp_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps 
+               intro:init_alterp_exec)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_butp_I_chown:
+  "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; no_del_event s;
+   valid (ChangeOwner p u # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_intact_butp (ChangeOwner p u # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def initp_intact_butp_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps 
+               intro:init_alterp_chown)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_butp_I_crole:
+  "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; 
+    valid (ChangeRole p r # Clone p (new_proc s) # s); no_del_event s\<rbrakk>
+  \<Longrightarrow> initp_intact_butp (ChangeRole p r # Clone p (new_proc s) # s) p"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def initp_intact_butp_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps 
+               intro:init_alterp_crole)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_butp_I_others:
+  "\<lbrakk>initp_intact_butp s p; valid (e # s); \<forall> p f. e \<noteq> Execute p f;
+    \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>
+  \<Longrightarrow> initp_intact_butp (e # s) p"
+apply (frule valid_os, frule valid_cons)
+apply (simp add:initp_intact_butp_def init_alterp_other 
+            del:obj2sobj.simps init_obj2sobj.simps)
+apply (rule impI|rule allI|erule conjE|rule conjI)+
+apply (drule_tac obj = "Proc pa" in nodel_imp_exists, simp, simp)
+apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp)
+apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e)
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')
+done
+
+lemma initp_intact_I_exec:
+  "\<lbrakk>initp_intact s; valid (Execute (new_proc s) f # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_intact (Execute (new_proc s) f # Clone p (new_proc s) # s)"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps' cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_I_chown:
+  "\<lbrakk>initp_intact s; valid (ChangeOwner (new_proc s) u # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_intact (ChangeOwner (new_proc s) u # Clone p (new_proc s) # s)"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_I_crole:
+  "\<lbrakk>initp_intact s; valid (ChangeRole (new_proc s) r # Clone p (new_proc s) # s)\<rbrakk>
+  \<Longrightarrow> initp_intact (ChangeRole (new_proc s) r # Clone p (new_proc s) # s)"
+apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)
+apply (auto simp add:initp_intact_def initp_intact_butp_def 
+            simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (erule_tac x = pa in allE)
+apply (subgoal_tac "pa \<noteq> (new_proc s)")
+apply (auto simp:cp2sproc_simps' cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')[1]
+apply (rule notI, simp add:np_notin_curp)
+done
+
+lemma initp_intact_I_others:
+  "\<lbrakk>initp_intact s; valid (e # s); \<forall> p f. e \<noteq> Execute p f;
+    \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>
+  \<Longrightarrow> initp_intact (e # s)"
+apply (frule valid_os, frule valid_cons)
+apply (clarsimp simp add:initp_intact_def simp del:obj2sobj.simps init_obj2sobj.simps)
+apply (frule no_del_event_cons_D, drule_tac obj = "Proc p" and s = s in nodel_imp_exists, simp)
+apply (subgoal_tac "p \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
+apply (erule_tac x = p in allE, case_tac e)
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 
+           split:option.splits dest!:current_proc_has_sproc')
+done
+
+end
+
+end
\ No newline at end of file