diff -r e832378a2ff2 -r ded3f83f6cb9 no_shm_selinux/Enrich2.thy
--- a/no_shm_selinux/Enrich2.thy	Wed Jan 01 23:00:24 2014 +0800
+++ b/no_shm_selinux/Enrich2.thy	Mon Jan 06 23:07:51 2014 +0800
@@ -39,7 +39,7 @@
 done
 
 lemma enrich_msgq_cur_inof:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_file (enrich_msgq s q q') f = inum_of_file s f"
 apply (induct s arbitrary:f, simp)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -47,7 +47,7 @@
 done
 
 lemma enrich_msgq_cur_inos:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') = inum_of_socket s"
 apply (rule ext)
 apply (induct s, simp)
@@ -56,20 +56,20 @@
 done
 
 lemma enrich_msgq_cur_inos':
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> inum_of_socket (enrich_msgq s q q') sock = inum_of_socket s sock"
 apply (simp add:enrich_msgq_cur_inos)
 done
 
 lemma enrich_msgq_cur_inums:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_inode_nums (enrich_msgq s q q') = current_inode_nums s"
 apply (auto simp:current_inode_nums_def current_file_inums_def 
   current_sock_inums_def enrich_msgq_cur_inof enrich_msgq_cur_inos)
 done
 
 lemma enrich_msgq_cur_itag:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> itag_of_inum (enrich_msgq s q q') = itag_of_inum s"
 apply (rule ext)
 apply (induct s, simp)
@@ -78,7 +78,7 @@
 done
 
 lemma enrich_msgq_cur_tcps:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_tcp_sock (enrich_msgq s q q') = is_tcp_sock s"
 apply (rule ext)
 apply (auto simp:is_tcp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -86,7 +86,7 @@
 done
 
 lemma enrich_msgq_cur_udps:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_udp_sock (enrich_msgq s q q') = is_udp_sock s"
 apply (rule ext)
 apply (auto simp:is_udp_sock_def enrich_msgq_cur_itag enrich_msgq_cur_inos
@@ -94,7 +94,7 @@
 done
 
 lemma enrich_msgq_cur_msgqs:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_msgqs (enrich_msgq s q q') = current_msgqs s \<union> {q'}"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
@@ -103,17 +103,17 @@
 
 lemma enrich_msgq_cur_msgs:
   "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)"
+   \<Longrightarrow> msgs_of_queue (enrich_msgq s q q') =  (msgs_of_queue s) (q' := msgs_of_queue s q)" 
 apply (rule ext, simp, rule conjI, rule impI)
 apply (simp add:enrich_msgq_duq_sms)
-apply (rule impI)
+apply (rule impI) 
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
 apply (case_tac a, auto)
 done
 
 lemma enrich_msgq_cur_procs:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_procs (enrich_msgq s q q') = current_procs s"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
@@ -121,14 +121,14 @@
 done
   
 lemma enrich_msgq_cur_files:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_files (enrich_msgq s q q') = current_files s"
 apply (auto simp:current_files_def)
 apply (simp add:enrich_msgq_cur_inof)+
 done
 
 lemma enrich_msgq_cur_fds:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> current_proc_fds (enrich_msgq s q q') = current_proc_fds s"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons, case_tac a)
@@ -136,7 +136,7 @@
 done
 
 lemma enrich_msgq_filefd:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> file_of_proc_fd (enrich_msgq s q q') = file_of_proc_fd s"
 apply (rule ext, rule ext)
 apply (induct s, simp)
@@ -145,7 +145,7 @@
 done
 
 lemma enrich_msgq_flagfd:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> flags_of_proc_fd (enrich_msgq s q q') = flags_of_proc_fd s"
 apply (rule ext, rule ext)
 apply (induct s, simp)
@@ -154,7 +154,7 @@
 done
 
 lemma enrich_msgq_proc_fds:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> proc_file_fds (enrich_msgq s q q') = proc_file_fds s"
 apply (auto simp:proc_file_fds_def enrich_msgq_filefd)
 done
@@ -168,7 +168,7 @@
 done
   
 lemma enrich_msgq_is_file:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_file (enrich_msgq s q q') = is_file s"
 apply (rule ext)
 apply (auto simp add:is_file_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -176,7 +176,7 @@
 done
 
 lemma enrich_msgq_is_dir:
-  "\<lbrakk>q' \<notin> current_msgqs s; q \<in> current_msgqs s; no_del_event s; valid s\<rbrakk>
+  "\<lbrakk>no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> is_dir (enrich_msgq s q q') = is_dir s"
 apply (rule ext)
 apply (auto simp add:is_dir_def enrich_msgq_cur_itag enrich_msgq_cur_inof
@@ -204,30 +204,29 @@
 done
 
 (* enrich s target_proc duplicated_pro *)
-fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> nat \<Rightarrow> t_state"
 where 
-  "enrich_proc [] tp dp = []"
-| "enrich_proc (Execve p f fds # s) tp dp = (
+  "enrich_proc [] tp dp n = []"
+| "enrich_proc (Execve p f fds # s) tp dp n = (
      if (tp = p) 
-     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
-     else Execve p f fds # (enrich_proc s tp dp))"
-| "enrich_proc (Clone p p' fds # s) tp dp = (
+     then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp n)
+     else Execve p f fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Clone p p' fds # s) tp dp n = (
      if (tp = p') 
      then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
-     else Clone p p' fds # (enrich_proc s tp dp))"
-| "enrich_proc (Open p f flags fd opt # s) tp dp = (
+     else Clone p p' fds # (enrich_proc s tp dp n))"
+| "enrich_proc (Open p f flags fd opt # s) tp dp n= (
      if (tp = p)
-     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
-     else Open p f flags fd opt # (enrich_proc s tp dp))"
-| "enrich_proc (ReadFile p fd # s) tp dp = (
+     then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp n)
+     else Open p f flags fd opt # (enrich_proc s tp dp n))"
+| "enrich_proc (ReadFile p fd # s) tp dp n = (
      if (tp = p) 
-     then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
-     else ReadFile p fd # (enrich_proc s tp dp))"
-| "enrich_proc (RecvMsg p q m # s) tp dp = (
+     then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp n)
+     else ReadFile p fd # (enrich_proc s tp dp n))"
+| "enrich_proc (RecvMsg p q m # s) tp dp n = (
      if (tp = p) 
-     then let dq = new_msgq (enrich_proc s tp dp) in
-          RecvMsg dp dq m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp) q dq)
-     else RecvMsg p q m # (enrich_proc s tp dp))"
+     then RecvMsg dp n m # RecvMsg p q m # (enrich_msgq (enrich_proc s tp dp (n+1)) q n)
+     else RecvMsg p q m # (enrich_proc s tp dp n))"
 (*
 | "enrich_proc (CloseFd p fd # s) tp dp = (
      if (tp = p \<and> fd \<in> proc_file_fds s p)
@@ -252,7 +251,7 @@
      if (tp = p) then Exit p # s
      else Exit p # (enrich_proc s tp dp))"
 *)
-| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
+| "enrich_proc (e # s) tp dp n = e # (enrich_proc s tp dp n)"
 
 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
 where
@@ -304,47 +303,74 @@
 done
 
 lemma enrich_proc_dup_in:
-  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+  "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p' i)"
 apply (induct s, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
-done
+apply (case_tac a)
+apply ( auto simp:is_created_proc_def Let_def enrich_msgq_cur_procs
+  dest:not_all_procs_prop3)
+sorry
 
 lemma enrich_proc_dup_ffd:
   "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
-   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+   \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f"
 apply (induct s, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-done 
+sorry
 
 lemma enrich_proc_dup_ffd':
-  "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
+  "\<lbrakk>file_of_proc_fd (enrich_proc s p p' i) p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
     no_del_event s; valid s\<rbrakk>
    \<Longrightarrow> file_of_proc_fd s p fd = Some f"
 apply (induct s, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-done 
-
-lemma enrich_proc_dup_ffds':
-  "\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
-   \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
-apply (auto simp:enrich_proc_dup_ffds_eq_fds)
-apply (simp add:proc_file_fds_def)
-done
+sorry
 
 lemma enrich_proc_dup_ffd_eq:
   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
-  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
+  \<Longrightarrow> file_of_proc_fd (enrich_proc s p p' i) p' fd = file_of_proc_fd s p fd"
 apply (case_tac "file_of_proc_fd s p fd")
-apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
+apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p' i) p' fd")
 apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
+apply (drule_tac i = i in enrich_proc_dup_ffd, simp+)
 done
 
+lemma enrich_proc_cur_msgqs:
+  "\<lbrakk>valid s\<rbrakk> \<Longrightarrow> current_msgqs (enrich_proc s p p' i) = current_msgqs s \<union> {q'. q' \<ge> new_msgq s \<and> q' \<le> new_msgq s + (nums_of_recvmsg s p) - 1}"
+apply (induct s, simp)
+apply (auto)[1]
+apply (drule new_msgq_1, simp, simp)
+apply (frule vt_grant_os, frule vd_cons)
+sorry
+
+lemma enrich_proc_not_alive:
+  "\<lbrakk>enrich_not_alive s (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj; 
+    is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+  \<Longrightarrow> enrich_not_alive (enrich_proc s p p' (new_msgq s)) (E_proc p' (new_msgq s) (new_msgq s + (nums_of_recvmsg s p) - 1)) obj"
+apply (case_tac obj, simp_all)
+prefer 5
+apply (simp add:enrich_proc_cur_msgqs)
+apply (rule impI, rule notI)
+apply simp
+apply (auto)[1]
+defer
+apply simp
+apply (rule impI, rule notI)
+defer
+apply (subgoal_tac "new_msgq s \<noteq> 0")
+apply simp
+apply arith
+apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
+  enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
+defer
+apply (rule impI, rule notI)
+sorry
+
 
 lemma enrich_proc_dup_fflags:
   "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
@@ -352,9 +378,9 @@
        flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
 apply (induct s arbitrary:p, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def Let_def
   dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+sorry
 
 lemma enrich_proc_dup_ffds:
   "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -374,7 +400,14 @@
 apply (frule not_all_procs_prop3)
 apply (frule vd_cons, frule vt_grant_os, case_tac a)
 apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3 
-  simp:proc_file_fds_def is_created_proc_def)
+  simp:proc_file_fds_def is_created_proc_def Let_def)
+sorry
+
+lemma enrich_proc_dup_ffds':
+  "\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+   \<Longrightarrow> fd \<notin> proc_file_fds s p \<and> file_of_proc_fd s p fd = None"
+apply (auto simp:enrich_proc_dup_ffds_eq_fds)
+apply (simp add:proc_file_fds_def)
 done
 
 lemma enrich_proc_cur_inof:
@@ -383,8 +416,8 @@
 apply simp
 apply (frule vd_cons, frule vt_grant_os, frule vt_grant)
 apply (case_tac a, auto)
-apply (auto split:option.splits simp del:grant.simps)
-done
+apply (auto split:option.splits simp del:grant.simps simp add:Let_def)
+sorry
 
 lemma not_all_procs_sock:
   "\<lbrakk>p' \<notin> all_procs s; valid s\<rbrakk> \<Longrightarrow> inum_of_socket s (p', fd) = None"
@@ -399,11 +432,11 @@
 apply (induct s arbitrary:tp)
 apply simp
 apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:option.splits simp:not_all_procs_sock)
+apply (case_tac a, auto split:option.splits simp:not_all_procs_sock Let_def)
 apply (simp add:proc_file_fds_def, erule exE)
 apply (case_tac "inum_of_socket s (nat1, fd)", simp_all)
 apply (drule filefd_socket_conflict, simp_all add:current_sockets_def)
-done
+sorry
 
 lemma enrich_proc_cur_inums:
   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -418,8 +451,8 @@
 apply (induct s)
 apply simp
 apply (frule vd_cons, frule vt_grant_os)
-apply (case_tac a, auto split:option.splits t_socket_type.splits)
-done
+apply (case_tac a, auto split:option.splits t_socket_type.splits simp:Let_def)
+sorry
 
 lemma enrich_proc_cur_tcps:
   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
@@ -433,31 +466,32 @@
   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk> 
    \<Longrightarrow> is_udp_sock (enrich_proc s p p') = is_udp_sock s"
 apply (rule ext, case_tac x)
-apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos
+apply (auto simp add:is_udp_sock_def enrich_proc_cur_itag enrich_proc_cur_inos 
   split:option.splits t_inode_tag.splits)
 done
 
 lemma enrich_proc_cur_msgqs:
-  "valid s \<Longrightarrow> current_msgqs (enrich_proc s p p') = current_msgqs s"
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> q \<in> current_msgqs (enrich_proc s p p')"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
 
 lemma enrich_proc_cur_msgs:
-  "valid s \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q "
+  "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> msgs_of_queue (enrich_proc s p p') q = msgs_of_queue s q"
 apply (induct s, simp)
+apply (frule_tac p = p and p' = p' in enrich_proc_cur_msgqs, simp)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto)
-done
+apply (case_tac a, auto simp:Let_def)
+sorry
 
 lemma enrich_proc_cur_procs:
   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk> 
    \<Longrightarrow> current_procs (enrich_proc s p p') = current_procs s \<union> {p'}"
 apply (induct s, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_simps)
-done
+apply (case_tac a, auto simp:is_created_proc_simps Let_def)
+sorry
 
 lemma enrich_proc_cur_files:
   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> current_files (enrich_proc s p p') = current_files s"
@@ -472,18 +506,22 @@
 apply (frule vt_grant_os, frule vd_cons)
 apply (frule not_all_procs_prop3)
 apply (case_tac a)
+sorry
+(*
 apply (auto simp:is_created_proc_simps)
 done
+*)
 
 lemma enrich_proc_cur_fds1':
   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s; tp \<noteq> p'\<rbrakk>
    \<Longrightarrow> current_proc_fds (enrich_proc s p p') tp = current_proc_fds s tp"
 apply (induct s, simp add:is_created_proc_def)
 apply (frule vt_grant_os, frule vd_cons)
-apply (frule not_all_procs_prop3)
+apply (frule not_all_procs_prop3) sorry  (*
 apply (case_tac a)
 apply (auto simp:is_created_proc_simps)
 done
+*)
 
 lemma enrich_proc_cur_fds:
   "\<lbrakk>p' \<notin> all_procs s; no_del_event s; is_created_proc s p; valid s\<rbrakk>
@@ -497,7 +535,9 @@
 apply (case_tac obj)
 apply (simp_all add:enrich_proc_cur_procs enrich_proc_cur_files enrich_proc_cur_inums 
   enrich_proc_cur_msgqs enrich_proc_cur_msgs enrich_proc_cur_fds)
-done
+defer
+apply (rule impI, rule notI)
+sorry
 
 lemma enrich_proc_filefd:
   "\<lbrakk>file_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -507,7 +547,7 @@
 apply (frule not_all_procs_prop3)
 apply (case_tac a)
 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs split:if_splits)
-done
+sorry
 
 lemma enrich_proc_flagfd:
   "\<lbrakk>flags_of_proc_fd s tp fd = Some f; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -517,14 +557,14 @@
 apply (frule not_all_procs_prop3)
 apply (case_tac a)
 apply (auto simp:is_created_proc_simps dest:proc_fd_in_procs current_fflag_has_ffd split:if_splits option.splits)
-done
+sorry
 
 lemma enrich_proc_hungs:
   "\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> files_hung_by_del (enrich_proc s p p') = files_hung_by_del s"
 apply (induct s, simp)
 apply (frule vt_grant_os, frule vd_cons)
 apply (case_tac a, auto simp:files_hung_by_del.simps)
-done
+sorry
 
 lemma enrich_proc_is_file:
   "\<lbrakk>valid s; no_del_event s; p' \<notin> all_procs s\<rbrakk>