no_shm_selinux/New_obj_prop.thy
author chunhan
Thu, 09 Jan 2014 22:53:45 +0800
changeset 94 042e1e7fd505
parent 93 dfde07c7cd6b
permissions -rw-r--r--
new childf new-version

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 nh_notin_curh: "valid \<tau> \<Longrightarrow> new_shm \<tau> \<notin> current_shms \<tau>" using finite_ch
by (simp add:new_shm_def nn_notin)

lemma nh_notin_curh': "\<lbrakk>new_shm \<tau> \<in> current_shms \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"
by (drule nh_notin_curh, 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 finite_fs_fnames:
  "finite (fs::t_file set) \<Longrightarrow> finite {fn. fn # f \<in> fs}"
thm 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 []) ` fs)" in finite_subset)
unfolding image_def
apply (clarsimp  split:if_splits)
apply (rule_tac x = "x # f" in bexI, simp+) 
done

lemma ncf_notin_curf_aux:
  "finite (fs::t_file set) \<Longrightarrow> Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> fname_length_set {fn. fn # f \<in> fs}"
apply (drule_tac f = f in finite_fs_fnames)
apply (drule_tac h = length in finite_imageI)
apply (simp add:fname_length_set_def)
apply (drule nn_notin_aux)
apply auto
done

lemma ncf_notin_curf_general:
  assumes fin_fs: "finite fs"
  shows "new_childf_general f fs \<notin> fs"
proof-
  have a1: "Suc (Max (fname_length_set {fn. fn # f \<in> fs})) \<notin> 
    fname_length_set {fn. fn # f \<in> fs}"
    using fin_fs
    by (erule_tac ncf_notin_curf_aux)
  have a2: "\<And> f pf fs. f # pf \<in> fs \<Longrightarrow> f \<in> {fn. fn # pf \<in> fs}" by auto
  have a3: "\<And> f pf fs. f \<in> {fn. fn # pf \<in> fs} \<Longrightarrow> length f \<in> fname_length_set {fn. fn # pf \<in> fs}"
    by (auto simp:fname_length_set_def)
  show ?thesis
    apply (simp only:new_childf_general_def next_fname_def all_fname_under_dir_def)
    apply (rule notI)
    apply (drule a2, drule a3)
    apply (simp only:len_fname_all)
    using a1 by auto
qed
  
lemma ncf_notin_curf:
 "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> (current_files \<tau>)"
apply (drule finite_cf)
apply (drule_tac fs = "current_files \<tau>" in ncf_notin_curf_general)
apply (simp add:new_childf_def)
done

lemma ncf_parent_general: "valid \<tau> \<Longrightarrow> parent (new_childf_general f fs) = Some f"
by (simp add:new_childf_general_def)

lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"
by (simp add:new_childf_def ncf_parent_general)

end

end