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