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 dest:nodel_imp_exists[where obj = "Proc pa"]

           split:option.splits dest!:current_proc_has_sproc')

apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+

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')

apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+

done

end

end