1 theory Enrich

     1 theory Enrich2

    26 

    25 lemma enrich_msgq_duq_in:

    26   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    27    \<Longrightarrow> q' \<in> current_msgqs (enrich_msgq s q q')"

    28 apply (induct s, simp)

    29 apply (frule vt_grant_os, frule vd_cons, case_tac a)

    30 apply auto

    31 done

    32 

    33 lemma enrich_msgq_duq_sms:

    34   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    35    \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') q' = msgs_of_queue s q"

    36 apply (induct s, simp)

    37 apply (frule vt_grant_os, frule vd_cons, case_tac a)

    38 apply auto

    39 done

    40 

    41 lemma enrich_msgq_cur_inof:

    42   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    43    \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"

    44 apply (induct s arbitrary:f, simp)

    45 apply (frule vt_grant_os, frule vd_cons, case_tac a)

    46 apply (auto split:option.splits)

    47 done

    48 

    49 lemma enrich_msgq_cur_inos:

    50   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    51    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"

    52 apply (rule ext)

    53 apply (induct s, simp)

    54 apply (frule vt_grant_os, frule vd_cons, case_tac a)

    55 apply (auto split:option.splits)

    56 done

    57 

    58 lemma enrich_msgq_cur_inos':

    59   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    60    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"

    61 apply (simp add:enrich_msgq_cur_inos)

    62 done

    63 

    64 lemma enrich_msgq_cur_inums:

    65   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    66    \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"

    67 apply (auto simp:current_inode_nums_def current_file_inums_def 

    68   current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)

    69 done

    70 

    71 lemma enrich_msgq_cur_itag:

    72   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    73    \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"

    74 apply (rule ext)

    75 apply (induct s, simp)

    76 apply (frule vt_grant_os, frule vd_cons, case_tac a)

    77 apply (auto split:option.splits t_socket_type.splits)

    78 done

    79 

    80 lemma enrich_msgq_cur_tcps:

    81   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    82    \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"

    83 apply (rule ext)

    84 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos

    85   split:option.splits t_inode_tag.splits)

    86 done

    87 

    88 lemma enrich_msgq_cur_udps:

    89   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    90    \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"

    91 apply (rule ext)

    92 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos

    93   split:option.splits t_inode_tag.splits)

    94 done

    95 

    96 lemma enrich_msgq_cur_msgqs:

    97   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

    98    \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"

    99 apply (induct s, simp)

   100 apply (frule vt_grant_os, frule vd_cons)

   101 apply (case_tac a, auto)

   102 done

   103 

   104 lemma enrich_msgq_cur_msgs:

   105   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   106    \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"

   107 apply (rule ext, simp, rule conjI, rule impI)

   108 apply (simp add:enrich_msgq_duq_sms)

   109 apply (rule impI)

   110 apply (induct s, simp)

   111 apply (frule vt_grant_os, frule vd_cons)

   112 apply (case_tac a, auto)

   113 done

   114 

   115 lemma enrich_msgq_cur_procs:

   116   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   117    \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"

   118 apply (induct s, simp)

   119 apply (frule vt_grant_os, frule vd_cons)

   120 apply (case_tac a, auto)

   121 done

   122   

   123 lemma enrich_msgq_cur_files:

   124   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   125    \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"

   126 apply (auto simp:current_files_def)

   127 apply (simp add:enrich_msgq_cur_inof)+

   128 done

   129 

   130 lemma enrich_msgq_cur_fds:

   131   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   132    \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"

   133 apply (induct s, simp)

   134 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   135 apply auto

   136 done

   137 

   138 lemma enrich_msgq_filefd:

   139   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   140    \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"

   141 apply (rule ext, rule ext)

   142 apply (induct s, simp)

   143 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   144 apply auto

   145 done

   146 

   147 lemma enrich_msgq_flagfd:

   148   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   149    \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"

   150 apply (rule ext, rule ext)

   151 apply (induct s, simp)

   152 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   153 apply auto

   154 done

   155 

   156 lemma enrich_msgq_proc_fds:

   157   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   158    \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"

   159 apply (auto simp:proc_file_fds_def enrich_msgq_filefd)

   160 done

   161 

   162 lemma enrich_msgq_hungs:

   163   "\<lbrakk>no_del_event s; valid s\<rbrakk>

   164    \<Longrightarrow> files_hung_by_del (enrich_msgq s q q') = files_hung_by_del s"

   165 apply (induct s, simp)

   166 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   167 apply (auto simp:files_hung_by_del.simps)

   168 done

   169   

   170 lemma enrich_msgq_is_file:

   171   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   172    \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"

   173 apply (rule ext)

   174 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof

   175   split:option.splits t_inode_tag.splits)

   176 done

   177 

   178 lemma enrich_msgq_is_dir:

   179   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>

   180    \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"

   181 apply (rule ext)

   182 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof

   183   split:option.splits t_inode_tag.splits)

   184 done

   185 

   186 lemma enrich_msgq_alive:

   187   "\<lbrakk>alive s obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>

   188    \<Longrightarrow> alive (enrich_msgq s q q') obj"

   189 apply (case_tac obj)

   190 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 

   191   enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds

   192   enrich_msgq_cur_tcps enrich_msgq_cur_udps)

   193 apply (rule impI, simp)

   194 done

   195 

   196 lemma enrich_msgq_alive':

   197   "\<lbrakk>alive (enrich_msgq s q q') obj; valid s; q \<in> current_msgqs s; q' \<notin> current_msgqs s; no_del_event s\<rbrakk>

   198    \<Longrightarrow> alive s obj \<or> obj = O_msgq q' \<or> (\<exists> m. obj = O_msg q' m \<and> alive s (O_msg q m))"

   199 apply (case_tac obj)

   200 apply (simp_all add:enrich_msgq_is_file enrich_msgq_is_dir enrich_msgq_cur_msgqs 

   201   enrich_msgq_cur_msgs enrich_msgq_cur_procs enrich_msgq_cur_fds

   202   enrich_msgq_cur_tcps enrich_msgq_cur_udps)

   203 apply (auto split:if_splits)

   204 done