diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/New_obj_prop.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/New_obj_prop.thy	Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,86 @@
+theory New_obj_prop
+imports Main Finite_current Flask_type Flask Static
+begin
+
+context tainting_s begin
+
+lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
+apply (erule finite.induct, simp)
+apply (rule ballI)
+apply (case_tac "aa = a", simp+)
+done
+
+lemma nn_notin: "finite s \<Longrightarrow> next_nat s \<notin> s"
+apply (drule nn_notin_aux)
+apply (simp add:next_nat_def)
+by (auto)
+
+
+(* lemmas of new created obj *)
+
+lemma np_notin_curp: "valid \<tau> \<Longrightarrow> new_proc \<tau> \<notin> current_procs \<tau>" using finite_cp
+by (simp add:new_proc_def nn_notin)
+
+lemma np_notin_curp': "\<lbrakk>new_proc \<tau> \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+apply (drule np_notin_curp, simp)
+done
+
+lemma ni_notin_curi: "valid \<tau> \<Longrightarrow> new_inode_num \<tau> \<notin> current_inode_nums \<tau>"
+apply (drule finite_ci)
+by (simp add:new_inode_num_def nn_notin)
+
+lemma ni_notin_curi': "\<lbrakk>new_inode_num \<tau> \<in> current_inode_nums \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule ni_notin_curi, simp)
+
+lemma nm_notin_curm: "valid \<tau> \<Longrightarrow> new_msgq \<tau> \<notin> current_msgqs \<tau>" using finite_cm
+by (simp add:new_msgq_def nn_notin)
+
+lemma nm_notin_curm': "\<lbrakk>new_msgq \<tau> \<in> current_msgqs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule nm_notin_curm, simp)
+
+lemma nfd_notin_curfd: "valid \<tau> \<Longrightarrow> new_proc_fd \<tau> p \<notin> current_proc_fds \<tau> p" 
+using finite_cfd[where p = p]
+apply (simp add:new_proc_fd_def nn_notin)
+done
+
+lemma nfd_notin_curfd': "\<lbrakk>new_proc_fd \<tau> p \<in> current_proc_fds \<tau> p; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule nfd_notin_curfd[where p = p], simp)
+
+lemma nim_notin_curim: "valid \<tau> \<Longrightarrow> new_inode_num \<tau> \<notin> current_inode_nums \<tau>"
+by (drule finite_ci, simp add:new_inode_num_def nn_notin)
+
+lemma nim_notin_curim': "\<lbrakk>new_inode_num \<tau> \<in> current_inode_nums \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
+by (drule nim_notin_curim, simp)
+
+lemma len_fname_all: "length (fname_all_a len) = len"
+by (induct len, auto simp:fname_all_a.simps)
+
+lemma ncf_notin_curf: "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> current_files \<tau>"
+apply (drule finite_cf)
+apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)
+apply (rule notI)
+apply (subgoal_tac "(CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> {fn. fn # f \<in> current_files \<tau>}")
+defer apply simp
+apply (subgoal_tac "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>}))) \<in> fname_length_set {fn. fn # f \<in> current_files \<tau>}")
+defer apply (auto simp:fname_length_set_def image_def)[1]
+apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files \<tau>})")  
+defer
+apply (simp add:fname_length_set_def) 
+apply (rule finite_imageI)
+apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
+apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files \<tau>)" in finite_subset)
+unfolding image_def
+apply (clarsimp  split:if_splits)
+apply (rule_tac x = "x # f" in bexI, simp+)
+
+apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files \<tau>})" in nn_notin_aux)
+apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>})))" in ballE)
+apply (simp add:len_fname_all, simp)
+done
+
+lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"
+by (simp add:new_childf_def)
+
+end
+
+end