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 deleted_cons_I: "deleted obj s \<Longrightarrow> deleted obj (e # s)"

     8 by (case_tac e, auto)

     9 

    10 lemma not_deleted_cons_D: "\<not> deleted obj (e # s) \<Longrightarrow> \<not> deleted obj s" 

    11 by (auto dest:deleted_cons_I)

    12 

    13 lemma cons_app_simp_aux:

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

    15 

    16 lemma not_deleted_app_I:

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

    18 apply (induct s', simp)

    19 by (simp add:cons_app_simp_aux deleted_cons_I)

    20 

    21 lemma not_deleted_app_D:

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

    23 apply (rule notI)

    24 by (simp add:not_deleted_app_I)

    25 

    26 lemma not_deleted_init_file:

    27   "\<lbrakk>\<not> deleted (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_deleted_init_dir:

    35   "\<lbrakk>\<not> deleted (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_deleted_init_proc:

    43   "\<lbrakk>\<not> deleted (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 (**** ???*)

    48 lemma current_fd_imp_current_proc:

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

    50 apply (induct s)

    51 apply (simp add:init_fds_of_proc_prop1)

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

    53 by (auto split:if_splits option.splits)

    54 

    55 lemma not_deleted_init_fd_aux:

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

    57    \<Longrightarrow> fd \<in> current_proc_fds s p \<and> \<not> deleted (O_proc p) s"

    58 apply (induct s arbitrary: p, simp)

    59 apply (frule vd_cons, drule vt_grant_os)

    60 apply (case_tac a, auto dest:current_fd_imp_current_proc)

    61 done

    62 

    63 lemma not_deleted_init_fd2:

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

    65 by (auto dest:not_deleted_init_fd_aux)

    66 

    67 lemma not_deleted_init_fd1:

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

    69 by (auto dest:not_deleted_init_fd_aux)

    70 

    71 lemma not_deleted_init_tcp_aux:

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

    73    \<Longrightarrow> is_tcp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"

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

    75 apply (frule vd_cons, frule vt_grant_os)

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

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

    78          dest:is_tcp_sock_imp_curernt_proc)

    79 

    80 lemma not_deleted_init_tcp1:

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

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

    83 by (auto dest:not_deleted_init_tcp_aux)

    84 

    85 lemma not_deleted_init_tcp2:

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

    87    \<Longrightarrow> \<not> deleted (O_proc p) s"

    88 by (auto dest:not_deleted_init_tcp_aux)

    89 

    90 lemma not_deleted_init_udp_aux:

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

    92    \<Longrightarrow> is_udp_sock s (p,fd) \<and> \<not> deleted (O_proc p) s"

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

    94 apply (frule vd_cons, frule vt_grant_os)

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

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

    97          dest:is_udp_sock_imp_curernt_proc)

    98 

    99 lemma not_deleted_init_udp1:

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

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

   102 by (auto dest:not_deleted_init_udp_aux)

   103 

   104 lemma not_deleted_init_udp2:

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

   106    \<Longrightarrow> \<not> deleted (O_proc p) s"

   107 by (auto dest:not_deleted_init_udp_aux)

   108 

   109 lemma not_deleted_init_shm:

   110   "\<lbrakk>\<not> deleted (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 lemma not_deleted_init_msgq:

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

   116 apply (induct s, simp)

   117 by (case_tac a, auto)

   118 

   119 lemma current_msg_imp_current_msgq:

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

   121 apply (induct s)

   122 apply (simp add:init_msgs_valid)

   123 apply (frule vd_cons, drule vt_grant_os)

   124 apply (case_tac a, auto split:if_splits)

   125 done

   126 

   127 lemma not_deleted_init_msg:

   128   "\<lbrakk>\<not> deleted (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)"

   129 apply (induct s, simp)

   130 apply (frule vd_cons, frule vt_grant_os)

   131 apply (case_tac a, auto dest:current_msg_imp_current_msgq)

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

   133 done

   134 

   135 lemma not_deleted_imp_alive:

   136   "\<lbrakk>\<not> deleted obj s; valid s; init_alive obj\<rbrakk> \<Longrightarrow> alive s obj"

   137 apply (case_tac obj)

   138 apply (auto dest!:not_deleted_init_msg not_deleted_init_file not_deleted_init_dir not_deleted_init_proc

   139   not_deleted_init_fd1 not_deleted_init_tcp1 not_deleted_init_udp1 not_deleted_init_shm 

   140   not_deleted_init_msgq 

   141            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 

   142   current_msg_imp_current_msgq)

   143 done

   144 

   145 lemma not_deleted_cur_file_app:

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

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

   148 apply (frule vd_cons, frule vt_grant_os, simp)

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

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

   151 done

   152 

   153 lemma not_deleted_cur_dir_app:

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

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

   156 apply (frule vd_cons, frule vt_grant_os, simp)

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

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

   159 done

   160 

   161 lemma not_deleted_cur_proc_app:

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

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

   164 by (case_tac a, auto)

   165 

   166 lemma not_deleted_cur_fd_app:

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

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

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

   170 apply (frule vd_cons, drule vt_grant_os)

   171 apply (case_tac a, auto dest:current_fd_imp_current_proc)

   172 done

   173 

   174 lemma not_deleted_cur_tcp_app:

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

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

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

   178 apply (frule vd_cons, frule vt_grant_os)

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

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

   181          dest:is_tcp_sock_imp_curernt_proc)

   182 

   183 lemma not_deleted_cur_udp_app:

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

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

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

   187 apply (frule vd_cons, frule vt_grant_os)

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

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

   190          dest:is_udp_sock_imp_curernt_proc)

   191 

   192 lemma not_deleted_cur_shm_app:

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

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

   195 by (case_tac a, auto)

   196 

   197 lemma not_deleted_cur_msgq_app:

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

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

   200 by (case_tac a, auto)

   201 

   202 lemma not_deleted_cur_msg_app:

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

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

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

   206 apply (frule vd_cons, frule vt_grant_os)

   207 apply (case_tac a, auto dest:current_msg_imp_current_msgq)

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

   209 done

   210 

   211 lemma not_deleted_imp_alive_app:

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

   213 apply (case_tac obj)

   214 apply (auto dest!:not_deleted_cur_msg_app not_deleted_cur_file_app not_deleted_cur_dir_app

   215   not_deleted_cur_proc_app not_deleted_cur_fd_app not_deleted_cur_tcp_app 

   216   not_deleted_cur_udp_app not_deleted_cur_shm_app not_deleted_cur_msgq_app

   217            intro:is_file_in_current is_dir_in_current is_tcp_in_current is_udp_in_current 

   218   current_msg_imp_current_msgq)

   219 done

   220 

   221 lemma not_deleted_imp_alive_cons:

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

   223 using not_deleted_imp_alive_app[where s = s and s' = "[e]" and obj = obj]

   224 by auto

   225 

   226 (*

   227 

   228 lemma nodel_imp_un_deleted:

   229   "no_del_event s \<Longrightarrow> \<not> deleted obj s"

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

   231 

   232 lemma nodel_exists_remains:

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

   234 apply (drule_tac obj = obj in nodel_imp_un_deleted)

   235 by (simp add:not_deleted_imp_exists')

   236 

   237 lemma nodel_imp_exists:

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

   239 apply (drule_tac obj = obj in nodel_imp_un_deleted)

   240 by (simp add:not_deleted_imp_exists)

   241 

   242 lemma no_del_event_cons_D:

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

   244 by (case_tac e, auto)

   245 *)

   246 end

   247 

   248 end