1 theory sound_defs_prop

     2 imports rc_theory Main os_rc obj2sobj_prop

     3 begin

     4 

     5 context tainting_s_sound begin

     6 

     7 lemma not_both_I:

     8   "not_both_sproc (SProc sp srp) sobj \<Longrightarrow> not_both_sproc sobj' sobj"

     9 by (case_tac sobj, auto)

    10 

    11 lemma not_both_I_file:

    12   "not_both_sproc (SFile sf srf) sobj \<Longrightarrow> not_both_sproc (SFile sf' srf') sobj"

    13 by (case_tac sobj, auto)

    14 

    15 lemma not_both_I_ipc:

    16   "not_both_sproc (SIPC si sri) sobj \<Longrightarrow> not_both_sproc (SIPC si' sri') sobj"

    17 by (case_tac sobj, auto)

    18 

    19 lemma intact_imp_butp:

    20   "\<lbrakk>p \<in> init_processes; initp_intact s\<rbrakk> \<Longrightarrow> initp_intact_butp s p "

    21 by (auto simp:initp_intact_def initp_intact_butp_def initp_alter_def)

    22 

    23 lemma no_sproc_imp_intact:

    24   "\<lbrakk>not_both_sproc (SProc sp srp) sobj; initp_intact_but s sobj\<rbrakk> \<Longrightarrow> initp_intact s"

    25 by (case_tac sobj, simp_all)

    26 

    27 lemma initp_intact_but_nil:"initp_intact_but [] (init_obj2sobj obj)"  

    28 apply (case_tac obj)

    29 apply (auto simp:initp_intact_def initp_intact_butp_def initp_alter_def split:option.splits)

    30 apply (rule_tac x = nat in exI) using init_proc_has_role 

    31 by (auto simp:bidirect_in_init_def)

    32 

    33 lemma init_alterp_exec:

    34   "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (Execute p f # Clone p (new_proc s) # s)\<rbrakk>

    35   \<Longrightarrow> initp_alter (Execute p f # Clone p (new_proc s) # s) p"

    36 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)

    37 apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)

    38 apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

    39 apply (case_tac "p' = p")

    40 apply (rule_tac x = "new_proc s" in exI) defer

    41 apply (rule_tac x = p' in exI)

    42 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

    43            split:option.splits dest!:current_proc_has_sproc')

    44 done

    45 

    46 lemma init_alterp_chown:

    47   "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (ChangeOwner p u # Clone p (new_proc s) # s)\<rbrakk>

    48   \<Longrightarrow> initp_alter (ChangeOwner p u # Clone p (new_proc s) # s) p"

    49 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)

    50 apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)

    51 apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

    52 apply (case_tac "p' = p")

    53 apply (rule_tac x = "new_proc s" in exI) defer

    54 apply (rule_tac x = p' in exI)

    55 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

    56            split:option.splits dest!:current_proc_has_sproc')

    57 done

    58 

    59 lemma init_alterp_crole:

    60   "\<lbrakk>initp_alter s p; p \<in> init_processes; valid (ChangeRole p r # Clone p (new_proc s) # s)\<rbrakk>

    61   \<Longrightarrow> initp_alter (ChangeRole p r # Clone p (new_proc s) # s) p"

    62 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons, frule_tac \<tau> = s in valid_os)

    63 apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)

    64 apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

    65 apply (case_tac "p' = p")

    66 apply (rule_tac x = "new_proc s" in exI) defer

    67 apply (rule_tac x = p' in exI)

    68 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

    69            split:option.splits dest!:current_proc_has_sproc')

    70 done

    71 

    72 lemma init_alterp_other:

    73   "\<lbrakk>initp_alter s p; valid (e # s); \<forall> p f. e \<noteq> Execute p f;

    74     \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>

    75   \<Longrightarrow> initp_alter (e # s) p"

    76 apply (frule valid_cons, frule valid_os)

    77 apply (clarsimp simp add:initp_alter_def simp del:obj2sobj.simps init_obj2sobj.simps)

    78 apply (subgoal_tac "p' \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

    79 apply (rule_tac x = p' in exI, case_tac e)

    80 apply (auto simp add: cp2sproc_simps' simp del:cp2sproc.simps split:option.splits)

    81 done

    82 

    83 lemma initp_intact_butp_I_exec:

    84   "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; valid (Execute p f # Clone p (new_proc s) # s); 

    85     no_del_event s\<rbrakk>

    86   \<Longrightarrow> initp_intact_butp (Execute p f # Clone p (new_proc s) # s) p"

    87 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

    88 apply (auto simp add:initp_intact_def initp_intact_butp_def 

    89             simp del:obj2sobj.simps init_obj2sobj.simps 

    90                intro:init_alterp_exec)

    91 apply (erule_tac x = pa in allE)

    92 apply (subgoal_tac "pa \<noteq> (new_proc s)")

    93 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

    94            split:option.splits dest!:current_proc_has_sproc')[1]

    95 apply (rule notI, simp add:np_notin_curp)

    96 done

    97 

    98 lemma initp_intact_butp_I_chown:

    99   "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; no_del_event s;

   100    valid (ChangeOwner p u # Clone p (new_proc s) # s)\<rbrakk>

   101   \<Longrightarrow> initp_intact_butp (ChangeOwner p u # Clone p (new_proc s) # s) p"

   102 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

   103 apply (auto simp add:initp_intact_def initp_intact_butp_def 

   104             simp del:obj2sobj.simps init_obj2sobj.simps 

   105                intro:init_alterp_chown)

   106 apply (erule_tac x = pa in allE)

   107 apply (subgoal_tac "pa \<noteq> (new_proc s)")

   108 apply (auto simp:cp2sproc_simps simp del:cp2sproc.simps 

   109            split:option.splits dest!:current_proc_has_sproc')[1]

   110 apply (rule notI, simp add:np_notin_curp)

   111 done

   112 

   113 lemma initp_intact_butp_I_crole:

   114   "\<lbrakk>initp_intact_butp s p; p \<in> init_processes; 

   115     valid (ChangeRole p r # Clone p (new_proc s) # s); no_del_event s\<rbrakk>

   116   \<Longrightarrow> initp_intact_butp (ChangeRole p r # Clone p (new_proc s) # s) p"

   117 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

   118 apply (auto simp add:initp_intact_def initp_intact_butp_def 

   119             simp del:obj2sobj.simps init_obj2sobj.simps 

   120                intro:init_alterp_crole)

   121 apply (erule_tac x = pa in allE)

   122 apply (subgoal_tac "pa \<noteq> (new_proc s)")

   123 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

   124            split:option.splits dest!:current_proc_has_sproc')[1]

   125 apply (rule notI, simp add:np_notin_curp)

   126 done

   127 

   128 lemma initp_intact_butp_I_others:

   129   "\<lbrakk>initp_intact_butp s p; valid (e # s); \<forall> p f. e \<noteq> Execute p f;

   130     \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>

   131   \<Longrightarrow> initp_intact_butp (e # s) p"

   132 apply (frule valid_os, frule valid_cons)

   133 apply (simp add:initp_intact_butp_def init_alterp_other 

   134             del:obj2sobj.simps init_obj2sobj.simps)

   135 apply (rule impI|rule allI|erule conjE|rule conjI)+

   136 apply (drule_tac obj = "Proc pa" in nodel_imp_exists, simp, simp)

   137 apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp)

   138 apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

   139 apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e)

   140 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

   141            split:option.splits dest!:current_proc_has_sproc')

   142 done

   143 

   144 lemma initp_intact_I_exec:

   145   "\<lbrakk>initp_intact s; valid (Execute (new_proc s) f # Clone p (new_proc s) # s)\<rbrakk>

   146   \<Longrightarrow> initp_intact (Execute (new_proc s) f # Clone p (new_proc s) # s)"

   147 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

   148 apply (auto simp add:initp_intact_def 

   149             simp del:obj2sobj.simps init_obj2sobj.simps)

   150 apply (erule_tac x = pa in allE)

   151 apply (subgoal_tac "pa \<noteq> (new_proc s)")

   152 apply (auto simp:cp2sproc_simps' cp2sproc.simps 

   153            split:option.splits dest!:current_proc_has_sproc')[1]

   154 apply (rule notI, simp add:np_notin_curp)

   155 done

   156 

   157 lemma initp_intact_I_chown:

   158   "\<lbrakk>initp_intact s; valid (ChangeOwner (new_proc s) u # Clone p (new_proc s) # s)\<rbrakk>

   159   \<Longrightarrow> initp_intact (ChangeOwner (new_proc s) u # Clone p (new_proc s) # s)"

   160 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

   161 apply (auto simp add:initp_intact_def 

   162             simp del:obj2sobj.simps init_obj2sobj.simps)

   163 apply (erule_tac x = pa in allE)

   164 apply (subgoal_tac "pa \<noteq> (new_proc s)")

   165 apply (auto simp:cp2sproc_simps cp2sproc.simps 

   166            split:option.splits dest!:current_proc_has_sproc')[1]

   167 apply (rule notI, simp add:np_notin_curp)

   168 done

   169 

   170 lemma initp_intact_I_crole:

   171   "\<lbrakk>initp_intact s; valid (ChangeRole (new_proc s) r # Clone p (new_proc s) # s)\<rbrakk>

   172   \<Longrightarrow> initp_intact (ChangeRole (new_proc s) r # Clone p (new_proc s) # s)"

   173 apply (frule valid_cons, frule_tac \<tau> = s in valid_cons)

   174 apply (auto simp add:initp_intact_def initp_intact_butp_def 

   175             simp del:obj2sobj.simps init_obj2sobj.simps)

   176 apply (erule_tac x = pa in allE)

   177 apply (subgoal_tac "pa \<noteq> (new_proc s)")

   178 apply (auto simp:cp2sproc_simps' cp2sproc.simps 

   179            split:option.splits dest!:current_proc_has_sproc')[1]

   180 apply (rule notI, simp add:np_notin_curp)

   181 done

   182 

   183 lemma initp_intact_I_others:

   184   "\<lbrakk>initp_intact s; valid (e # s); \<forall> p f. e \<noteq> Execute p f;

   185     \<forall> p u. e \<noteq> ChangeOwner p u; \<forall> p r. e \<noteq> ChangeRole p r; no_del_event (e # s)\<rbrakk>

   186   \<Longrightarrow> initp_intact (e # s)"

   187 apply (frule valid_os, frule valid_cons)

   188 apply (clarsimp simp add:initp_intact_def simp del:obj2sobj.simps init_obj2sobj.simps)

   189 apply (frule no_del_event_cons_D, drule_tac obj = "Proc p" and s = s in nodel_imp_exists, simp)

   190 apply (subgoal_tac "p \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)

   191 apply (erule_tac x = p in allE, case_tac e)

   192 apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps 

   193            split:option.splits dest!:current_proc_has_sproc')

   194 done

   195 

   196 end

   197 

   198 end