diff -r 8779d321cc2e -r f27882976251 Init_prop.thy
--- a/Init_prop.thy	Wed May 15 11:21:39 2013 +0800
+++ b/Init_prop.thy	Wed May 15 15:42:46 2013 +0800
@@ -68,19 +68,19 @@
 
 lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5
 
-lemma is_init_file_prop1: "is_init_file f = (f \<in> init_files \<and> is_file [] f)"
-by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+lemma is_init_file_prop1: "is_init_file f \<Longrightarrow> f \<in> init_files"
+by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits)
 
-lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))"
-by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits)
+lemma is_init_file_prop2: "is_init_file f \<Longrightarrow> \<not> is_init_dir f"
+by (auto simp add:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits)
 
 lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2
 
-lemma is_init_dir_prop1: "is_init_dir f = (f \<in> init_files \<and> is_dir [] f)"
+lemma is_init_dir_prop1: "is_init_dir f \<Longrightarrow> f \<in> init_files"
 by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
 
-lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))"
-by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits)
+lemma is_init_dir_prop2: "is_init_dir f \<Longrightarrow> \<not> is_init_file f"
+by (auto simp add:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits)
 
 lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2
 
@@ -94,14 +94,14 @@
   "is_udp_sock [] k = is_init_udp_sock k"
 by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits)
 
-lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \<in> init_sockets \<and> is_udp_sock [] s)"
+lemma is_init_udp_sock_prop1: "is_init_udp_sock s \<Longrightarrow> s \<in> init_sockets"
 apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))"
-apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props 
-                dest:init_socket_has_inode split:option.splits)       
+lemma is_init_udp_sock_prop2: "is_init_udp_sock s \<Longrightarrow> \<not> is_init_tcp_sock s"
+apply (auto simp add:is_init_udp_sock_def is_init_tcp_sock_def  
+                dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       
 done
 
 lemma is_init_udp_sock_prop3:
@@ -121,14 +121,14 @@
   "is_tcp_sock [] k = is_init_tcp_sock k"
 by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits)
 
-lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \<in> init_sockets \<and> is_tcp_sock [] s)"
+lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s \<Longrightarrow> s \<in> init_sockets"
 apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
                 dest:init_socket_has_inode split:option.splits)       
 done
 
-lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))"
-apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props 
-                dest:init_socket_has_inode split:option.splits)       
+lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s \<Longrightarrow> \<not> is_init_udp_sock s"
+apply (auto simp add:is_init_tcp_sock_def is_init_udp_sock_def  
+                dest:init_socket_has_inode split:option.splits t_inode_tag.splits)       
 done
 
 lemma is_init_tcp_sock_prop3:
@@ -301,7 +301,8 @@
 
 lemma init_alive_prop: "init_alive obj = alive [] obj"
 apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props
-         is_init_udp_sock_props init_files_props init_sockets_props)
+         is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil
+         is_tcp_sock_nil is_udp_sock_nil)
 done
 
 lemma init_alive_proc: "p \<in> init_procs \<Longrightarrow> init_alive (O_proc p)" by simp
@@ -369,7 +370,7 @@
 lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3
 
 lemma init_file_user_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_user_of_obj (O_file f) = Some t"
-apply (simp only: is_init_file_prop2)
+apply (drule init_alive_file)
 by (drule init_obj_has_user, auto)
 
 lemma init_file_user_prop2: "is_init_file f \<Longrightarrow> init_user_of_obj (O_file f) \<noteq> None"
@@ -389,7 +390,7 @@
 lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5
 
 lemma init_dir_user_prop1: "is_init_dir f \<Longrightarrow> \<exists> t. init_user_of_obj (O_dir f) = Some t"
-apply (simp only: is_init_dir_prop2)
+apply (drule init_alive_dir)
 by (drule init_obj_has_user, auto)
 
 lemma init_dir_user_prop2: "is_init_dir f \<Longrightarrow> init_user_of_obj (O_dir f) \<noteq> None"
@@ -765,8 +766,7 @@
             dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
-apply (simp add:init_files_props)
-apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict)
+apply (drule is_init_file_prop1, simp add:init_files_props)
 done
 
 lemma s2ss_nil_prop: