1 theory Delete_prop

     2 imports Main Flask Flask_type Init_prop Alive_prop Current_files_prop

     3 begin

     4 

     5 context flask begin

     6 

     7 lemma died_cons_I: "died obj s \<Longrightarrow> died obj (e # s)"

     8 by (case_tac e, auto)

     9 

    10 lemma not_died_cons_D: "\<not> died obj (e # s) \<Longrightarrow> \<not> died obj s" 

    11 by (auto dest:died_cons_I)

    12 

    13 lemma cons_app_simp_aux:

    14   "(a # b) @ c = a # (b @ c)" by auto

    15 

    16 lemma not_died_app_I:

    17   "died obj s \<Longrightarrow> died obj (s' @ s)"

    18 apply (induct s', simp)

    19 by (simp add:cons_app_simp_aux died_cons_I)

    20 

    21 lemma not_died_app_D:

    22   "\<not> died obj (s' @ s) \<Longrightarrow> \<not> died obj s"

    23 apply (rule notI)

    24 by (simp add:not_died_app_I)

    25 

    26 lemma not_died_init_file:

    27   "\<lbrakk>\<not> died (O_file f) s; valid s; is_init_file f\<rbrakk> \<Longrightarrow> is_file s f"

    28 apply (induct s, simp add:is_file_nil)

    29 apply (frule vd_cons, frule vt_grant_os)

    30 apply (case_tac a) prefer 6 apply (case_tac option)

    31 apply (auto simp:is_file_simps split:option.splits)

    32 done

    33 

    34 lemma not_died_init_dir:

    35   "\<lbrakk>\<not> died (O_dir f) s; valid s; is_init_dir f\<rbrakk> \<Longrightarrow> is_dir s f"

    36 apply (induct s, simp add:is_dir_nil)

    37 apply (frule vd_cons, frule vt_grant_os)

    38 apply (case_tac a) prefer 6 apply (case_tac option)

    39 apply (auto simp:is_dir_simps split:option.splits)

    40 done

    41 

    42 lemma not_died_init_proc:

    43   "\<lbrakk>\<not> died (O_proc p) s; p \<in> init_procs\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

    44 apply (induct s, simp)

    45 by (case_tac a, auto)

    46 

    47 lemma current_fd_imp_current_proc:

    48   "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

    49 apply (induct s)

    50 apply (simp add:init_fds_of_proc_prop1)

    51 apply (frule vd_cons, drule vt_grant_os, case_tac a)

    52 by (auto split:if_splits option.splits)

    53 

    54 lemma not_died_init_fd_aux:

    55   "\<lbrakk>\<not> died (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> 

    56    \<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> died (O_proc p) s"

    57 apply (induct s arbitrary: p, simp)

    58 apply (frule vd_cons, drule vt_grant_os)

    59 apply (case_tac a, auto dest:current_fd_imp_current_proc)

    60 done

    61 

    62 lemma not_died_init_fd2:

    63   "\<lbrakk>\<not> died (O_fd p fd) s; fd \<in> init_fds_of_proc p; valid s\<rbrakk> \<Longrightarrow> \<not> died (O_proc p) s"

    64 by (auto dest:not_died_init_fd_aux)

    65 

    66 lemma not_died_init_fd1:

    67   "\<lbrakk>\<not> died (O_fd p fd) s; valid s; fd \<in> init_fds_of_proc p\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"

    68 by (auto dest:not_died_init_fd_aux)

    69 

    70 lemma not_died_init_tcp_aux:

    71   "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 

    72    \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> died (O_proc p) s"

    73 apply (induct s arbitrary:p, simp add:is_tcp_sock_nil)

    74 apply (frule vd_cons, frule vt_grant_os)

    75 apply (case_tac a) prefer 6 apply (case_tac option)

    76 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 

    77          dest:is_tcp_sock_imp_curernt_proc)

    78 

    79 lemma not_died_init_tcp1:

    80   "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 

    81    \<Longrightarrow> is_tcp_sock s (p,fd)"

    82 by (auto dest:not_died_init_tcp_aux)

    83 

    84 lemma not_died_init_tcp2:

    85   "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\<rbrakk> 

    86    \<Longrightarrow> \<not> died (O_proc p) s"

    87 by (auto dest:not_died_init_tcp_aux)

    88 

    89 lemma not_died_init_udp_aux:

    90   "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 

    91    \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> died (O_proc p) s"

    92 apply (induct s arbitrary:p, simp add:is_udp_sock_nil)

    93 apply (frule vd_cons, frule vt_grant_os)

    94 apply (case_tac a) prefer 6 apply (case_tac option)

    95 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 

    96          dest:is_udp_sock_imp_curernt_proc)

    97 

    98 lemma not_died_init_udp1:

    99   "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 

   100    \<Longrightarrow> is_udp_sock s (p,fd)"

   101 by (auto dest:not_died_init_udp_aux)

   102 

   103 lemma not_died_init_udp2:

   104   "\<lbrakk>\<not> died (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\<rbrakk> 

   105    \<Longrightarrow> \<not> died (O_proc p) s"

   106 by (auto dest:not_died_init_udp_aux)

   107 

   108 (*

   109 lemma not_died_init_shm:

   110   "\<lbrakk>\<not> died (O_shm h) s; h \<in> init_shms\<rbrakk> \<Longrightarrow> h \<in> current_shms s"

   111 apply (induct s, simp)

   112 by (case_tac a, auto)

   113 *)

   114 

   115 lemma not_died_init_msgq:

   116   "\<lbrakk>\<not> died (O_msgq q) s; q \<in> init_msgqs\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"

   117 apply (induct s, simp)

   118 by (case_tac a, auto)

   119 

   120 lemma current_msg_imp_current_msgq:

   121   "\<lbrakk>m \<in> set (msgs_of_queue s q); valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs s"

   122 apply (induct s)

   123 apply (simp add:init_msgs_valid)

   124 apply (frule vd_cons, drule vt_grant_os)

   125 apply (case_tac a, auto split:if_splits)

   126 done

   127 

   128 lemma not_died_init_msg:

   129   "\<lbrakk>\<not> died (O_msg q m) s; valid s; m \<in> set (init_msgs_of_queue q)\<rbrakk> \<Longrightarrow> m \<in> set (msgs_of_queue s q)"

   130 apply (induct s, simp)

   131 apply (frule vd_cons, frule vt_grant_os)

   132 apply (case_tac a, auto dest:current_msg_imp_current_msgq)

   133 apply (case_tac "msgs_of_queue s q", simp+)

   134 done

   135 

   136 lemma not_died_imp_alive: (* init_alive obj;  *)

   137   "\<lbrakk>\<not> died obj s;  valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"

   138 apply (case_tac obj)

   139 apply (auto dest!: not_died_init_file not_died_init_dir not_died_init_proc

   140   not_died_init_msg not_died_init_fd1 not_died_init_tcp1 not_died_init_udp1 (* not_died_init_shm *)

   141   not_died_init_msgq 

   142            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current

   143   current_msg_imp_current_msgq)

   144 done

   145 

   146 lemma not_died_cur_file_app:

   147   "\<lbrakk>\<not> died (O_file f) (s' @ s); valid (s' @ s); is_file s f\<rbrakk> \<Longrightarrow> is_file (s' @ s) f"

   148 apply (induct s', simp, simp add:cons_app_simp_aux)

   149 apply (frule vd_cons, frule vt_grant_os, simp)

   150 apply (case_tac a) prefer 6 apply (case_tac option)

   151 apply (auto simp:is_file_simps split:option.splits)

   152 done

   153 

   154 lemma not_died_cur_dir_app:

   155   "\<lbrakk>\<not> died (O_dir f) (s' @ s); valid (s' @ s); is_dir s f\<rbrakk> \<Longrightarrow> is_dir (s' @ s) f"

   156 apply (induct s', simp, simp add:cons_app_simp_aux)

   157 apply (frule vd_cons, frule vt_grant_os, simp)

   158 apply (case_tac a) prefer 6 apply (case_tac option)

   159 apply (auto simp:is_dir_simps split:option.splits)

   160 done

   161 

   162 lemma not_died_cur_proc_app:

   163   "\<lbrakk>\<not> died (O_proc p) (s' @ s); p \<in> current_procs s\<rbrakk> \<Longrightarrow> p \<in> current_procs (s' @ s)"

   164 apply (induct s', simp, simp add:cons_app_simp_aux)

   165 by (case_tac a, auto)

   166 

   167 lemma not_died_cur_fd_app:

   168   "\<lbrakk>\<not> died (O_fd p fd) (s' @ s); valid (s' @ s); fd \<in> current_proc_fds s p\<rbrakk> 

   169    \<Longrightarrow> fd \<in> current_proc_fds (s' @ s) p"

   170 apply (induct s' arbitrary: p, simp, simp add:cons_app_simp_aux)

   171 apply (frule vd_cons, drule vt_grant_os)

   172 apply (case_tac a, auto dest:current_fd_imp_current_proc)

   173 done

   174 

   175 lemma not_died_cur_tcp_app:

   176   "\<lbrakk>\<not> died (O_tcp_sock (p,fd)) (s' @ s); valid (s' @ s); is_tcp_sock s (p,fd)\<rbrakk> 

   177    \<Longrightarrow> is_tcp_sock (s' @ s) (p,fd)"

   178 apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)

   179 apply (frule vd_cons, frule vt_grant_os)

   180 apply (case_tac a) prefer 6 apply (case_tac option)

   181 by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits 

   182          dest:is_tcp_sock_imp_curernt_proc)

   183 

   184 lemma not_died_cur_udp_app:

   185   "\<lbrakk>\<not> died (O_udp_sock (p,fd)) (s' @ s); valid (s' @ s); is_udp_sock s (p,fd)\<rbrakk> 

   186    \<Longrightarrow> is_udp_sock (s' @ s) (p,fd)"

   187 apply (induct s' arbitrary:p, simp, simp add:cons_app_simp_aux)

   188 apply (frule vd_cons, frule vt_grant_os)

   189 apply (case_tac a) prefer 6 apply (case_tac option)

   190 by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits 

   191          dest:is_udp_sock_imp_curernt_proc)

   192 

   193 (*

   194 lemma not_died_cur_shm_app:

   195   "\<lbrakk>\<not> died (O_shm h) (s' @ s); h \<in> current_shms s\<rbrakk> \<Longrightarrow> h \<in> current_shms (s' @ s)"

   196 apply (induct s', simp, simp add:cons_app_simp_aux)

   197 by (case_tac a, auto)

   198 *)

   199 

   200 lemma not_died_cur_msgq_app:

   201   "\<lbrakk>\<not> died (O_msgq q) (s' @ s); q \<in> current_msgqs s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (s' @ s)"

   202 apply (induct s', simp, simp add:cons_app_simp_aux)

   203 by (case_tac a, auto)

   204 

   205 lemma not_died_cur_msg_app:

   206   "\<lbrakk>\<not> died (O_msg q m) (s' @ s); valid (s' @ s); m \<in> set (msgs_of_queue s q)\<rbrakk> 

   207    \<Longrightarrow> m \<in> set (msgs_of_queue (s' @ s) q)"

   208 apply (induct s', simp, simp add:cons_app_simp_aux)

   209 apply (frule vd_cons, frule vt_grant_os)

   210 apply (case_tac a, auto dest:current_msg_imp_current_msgq)

   211 apply (case_tac "msgs_of_queue (s' @ s) q", simp+)

   212 done

   213 

   214 lemma not_died_imp_alive_app:

   215   "\<lbrakk>\<not> died obj (s' @ s); valid (s' @ s); alive s obj\<rbrakk> \<Longrightarrow> alive (s' @ s) obj"

   216 apply (case_tac obj)

   217 apply (auto dest!: not_died_cur_file_app not_died_cur_dir_app

   218   not_died_cur_proc_app not_died_cur_fd_app not_died_cur_tcp_app not_died_cur_msg_app

   219   not_died_cur_udp_app  (* not_died_cur_shm_app *) not_died_cur_msgq_app

   220            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 

   221   current_msg_imp_current_msgq)

   222 done

   223 

   224 lemma not_died_imp_alive_cons:

   225   "\<lbrakk>\<not> died obj (e # s); valid (e # s); alive s obj\<rbrakk> \<Longrightarrow> alive (e # s) obj"

   226 using not_died_imp_alive_app[where s = s and s' = "[e]" and obj = obj] 

   227 by auto

   228 

   229 end

   230 

   231 context tainting begin

   232 

   233 lemma deleted_died:

   234   "appropriate obj \<Longrightarrow> died obj s = (deleted obj s \<or> exited obj s)"

   235 apply (induct s)

   236 apply (simp, case_tac obj, simp+)

   237 apply (case_tac a, case_tac [!] obj, auto)

   238 done

   239 

   240 end

   241 

   242 (*

   243 

   244 lemma nodel_imp_un_died:

   245   "no_del_event s \<Longrightarrow> \<not> died obj s"

   246 by (induct s, simp, case_tac a,auto)

   247 

   248 lemma nodel_exists_remains:

   249   "\<lbrakk>no_del_event (s'@s); exists s obj\<rbrakk> \<Longrightarrow> exists (s'@s) obj"

   250 apply (drule_tac obj = obj in nodel_imp_un_died)

   251 by (simp add:not_died_imp_exists')

   252 

   253 lemma nodel_imp_exists:

   254   "\<lbrakk>no_del_event s; exists [] obj\<rbrakk> \<Longrightarrow> exists s obj"

   255 apply (drule_tac obj = obj in nodel_imp_un_died)

   256 by (simp add:not_died_imp_exists)

   257 

   258 lemma no_del_event_cons_D:

   259   "no_del_event (e # s) \<Longrightarrow> no_del_event s"

   260 by (case_tac e, auto)

   261 *)

   262 

   263 end