# HG changeset patch
# User chunhan
# Date 1370331469 -28800
# Node ID 570f90f175eec2ef94d5caa1124c42c6976e8ef7
# Parent  c8b7c24f1db6dae3dc23fc0b2755fa9b15dc8e45
updated

diff -r c8b7c24f1db6 -r 570f90f175ee Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Mon Jun 03 14:18:14 2013 +0800
+++ b/Co2sobj_prop.thy	Tue Jun 04 15:37:49 2013 +0800
@@ -1102,43 +1102,210 @@
 
 (******** cp2sproc simpset *********)
 
-lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p"
-apply (simp add:cp2sproc_def)
-by (simp add:cp2sproc_def index_of_proc.simps)
+lemma not_init_intro_proc: (*???*)
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
+using not_deleted_init_proc by auto
+
+lemma not_init_intro_proc': (*???*)
+  "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
+using not_deleted_init_proc by auto
+
+lemma cp2sproc_clone:
+  "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := 
+     case (sectxt_of_obj s (O_proc p)) of 
+       Some sec \<Rightarrow> Some (Created, sec, 
+  {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd},
+  {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag})
+     | _        \<Rightarrow> None)"
+apply (frule cph2spshs_clone, frule cpfd2sfds_clone)
+apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps)
+apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' 
+            dest:current_proc_has_sec split:option.splits if_splits)
+done
+
+lemma cp2sproc_other:
+  "\<lbrakk>valid (e # s); 
+    \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+    \<forall> p fd. e \<noteq> CloseFd p fd;
+    \<forall> p h flag. e \<noteq> Attach p h flag;
+    \<forall> p h. e \<noteq> Detach p h;
+    \<forall> p h. e \<noteq> DeleteShM p h;
+    \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+    \<forall> p f fds. e \<noteq> Execve p f fds;
+    \<forall> p p'. e \<noteq> Kill p p';
+    \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s"
+apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+)
+apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all) 
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' 
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
 
-lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p"
-by (simp add:cp2sproc_nil current_procs.simps)
+lemma cp2sproc_open:
+  "valid (Open p f flags fd opt # s) \<Longrightarrow> 
+   cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p :=      
+     case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), 
+           cf2sfile (Open p f flags fd opt # s) f) of 
+       (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
+                                               then Init p else Created, sec, 
+                                                (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p)
+     | _        \<Rightarrow> None)"
+apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
+apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p") 
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_closefd:
+  "valid (CloseFd p fd # s) \<Longrightarrow> 
+   cp2sproc (CloseFd p fd # s) = (cp2sproc s) (p := 
+     if (fd \<in> proc_file_fds s p)
+     then (case (cfd2sfd s p fd) of 
+             Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)
+                          then cp2sproc s p 
+                          else (case (sectxt_of_obj s (O_proc p)) of
+                                  Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
+                                                    then Init p else Created, 
+                                                    sec, cpfd2sfds s p - {sfd}, cph2spshs s p)
+                                | _        \<Rightarrow> None))
+           | _        \<Rightarrow> cp2sproc s p)
+     else cp2sproc s p)"
+apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p") 
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
 
-lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = (
-                         if (p'' = p') then SCrea (Suc (length \<tau>))
-                         else cp2sproc \<tau> p''           )"
-by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
+lemma cp2sproc_attach:
+  "valid (Attach p h flag # s) \<Longrightarrow> 
+   cp2sproc (Attach p h flag # s) = (cp2sproc s) (p := 
+     (case (ch2sshm s h) of 
+        Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of
+                      Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
+                                        then Init p else Created, 
+                                        sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)})
+                    | _        \<Rightarrow> None)
+      | _       \<Rightarrow> cp2sproc s p) )"
+apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p") 
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_detach:
+  "valid (Detach p h # s) \<Longrightarrow> 
+   cp2sproc (Detach p h # s) = (cp2sproc s) (p := 
+    (case (ch2sshm s h, flag_of_proc_shm s p h) of 
+       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+                              then cp2sproc s p 
+                              else (case (sectxt_of_obj s (O_proc p)) of
+                                      Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) 
+                                                       then Init p else Created, sec,
+                                                       cpfd2sfds s p, cph2spshs s p - {(sh, flag)})
+                                    | None     \<Rightarrow> None)                   
+     | _       \<Rightarrow> cp2sproc s p)             )"
+apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (case_tac "x = p") 
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
 
-lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''"
-apply (case_tac e)
-by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps)
+lemma cp2sproc_deleteshm:
+  "valid (DeleteShM p h # s) \<Longrightarrow> 
+   cp2sproc (DeleteShM p h # s) = (\<lambda> p'. 
+    (case (ch2sshm s h, flag_of_proc_shm s p' h) of 
+       (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh)
+                              then cp2sproc s p' 
+                              else (case (sectxt_of_obj s (O_proc p')) of
+                                      Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs) 
+                                                       then Init p' else Created, sec,
+                                                       cpfd2sfds s p', cph2spshs s p' - {(sh, flag)})
+                                    | None     \<Rightarrow> None)                   
+     | _       \<Rightarrow> cp2sproc s p')             )"
+apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_execve:
+  "valid (Execve p f fds # s) \<Longrightarrow> 
+   cp2sproc (Execve p f fds # s) = (cp2sproc s) (p := 
+     (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of
+        Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, 
+                         {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {})
+      | _        \<Rightarrow> None)                        )"
+apply (frule cph2spshs_execve, frule cpfd2sfds_execve)
+apply (frule vt_grant_os, frule vd_cons, rule ext)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
 
-lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other
+lemma cp2sproc_kill:
+  "\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow> 
+   cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
+apply (frule cph2spshs_kill, frule cpfd2sfds_kill)
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_kill':
+  "\<lbrakk>valid (Kill p p' # s); p'' \<in> current_procs (Kill p p' # s)\<rbrakk> \<Longrightarrow> 
+   cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''"
+by (drule_tac p'' = p'' in cp2sproc_kill, simp+)
+
+lemma cp2sproc_exit:
+  "\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> 
+   cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
+apply (frule cph2spshs_exit, frule cpfd2sfds_exit)
+apply (frule vt_grant_os, frule vd_cons)
+apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps 
+           dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current
+            dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits)
+done
+
+lemma cp2sproc_exit':
+  "\<lbrakk>valid (Exit p # s); p' \<in> current_procs (Exit p # s)\<rbrakk> \<Longrightarrow> 
+   cp2sproc (Exit p # s) p' = (cp2sproc s) p'"
+by (drule_tac p'= p' in cp2sproc_exit, simp+)
+
+lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
+  cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other 
 
 (********************* cm2smsg simpset ***********************)
 
-lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m"
-by (simp add:cm2smsg_def index_of_msg.simps)
-
-lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m"
-by (simp add:cm2smsg_nil current_msgs.simps)
-
-lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')"
-by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps)
-
-lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'"
+lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
+apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
 apply (case_tac e)
-by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps)
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits)
 
 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
 
 
 
+(********************* cq2smsgq simpset ***********************) 
+
+lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
+apply (case_tac e) 
+by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
+
+lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
+
+
+
+
 end
 
 (*<*)