1 theory New_obj_prop

     2 imports Main Finite_current Flask_type Flask Static

     3 begin

     4 

     5 context tainting_s begin

     6 

     7 lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "

     8 apply (erule finite.induct, simp)

     9 apply (rule ballI)

    10 apply (case_tac "aa = a", simp+)

    11 done

    12 

    13 lemma nn_notin: "finite s \<Longrightarrow> next_nat s \<notin> s"

    14 apply (drule nn_notin_aux)

    15 apply (simp add:next_nat_def)

    16 by (auto)

    17 

    18 

    19 (* lemmas of new created obj *)

    20 

    21 lemma np_notin_curp: "valid \<tau> \<Longrightarrow> new_proc \<tau> \<notin> current_procs \<tau>" using finite_cp

    22 by (simp add:new_proc_def nn_notin)

    23 

    24 lemma np_notin_curp': "\<lbrakk>new_proc \<tau> \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    25 apply (drule np_notin_curp, simp)

    26 done

    27 

    28 lemma ni_notin_curi: "valid \<tau> \<Longrightarrow> new_inode_num \<tau> \<notin> current_inode_nums \<tau>"

    29 apply (drule finite_ci)

    30 by (simp add:new_inode_num_def nn_notin)

    31 

    32 lemma ni_notin_curi': "\<lbrakk>new_inode_num \<tau> \<in> current_inode_nums \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    33 by (drule ni_notin_curi, simp)

    34 

    35 lemma nm_notin_curm: "valid \<tau> \<Longrightarrow> new_msgq \<tau> \<notin> current_msgqs \<tau>" using finite_cm

    36 by (simp add:new_msgq_def nn_notin)

    37 

    38 lemma nm_notin_curm': "\<lbrakk>new_msgq \<tau> \<in> current_msgqs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    39 by (drule nm_notin_curm, simp)

    40 

    41 (*

    42 lemma nh_notin_curh: "valid \<tau> \<Longrightarrow> new_shm \<tau> \<notin> current_shms \<tau>" using finite_ch

    43 by (simp add:new_shm_def nn_notin)

    44 

    45 lemma nh_notin_curh': "\<lbrakk>new_shm \<tau> \<in> current_shms \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    46 by (drule nh_notin_curh, simp)

    47 *)

    48 

    49 lemma nfd_notin_curfd: "valid \<tau> \<Longrightarrow> new_proc_fd \<tau> p \<notin> current_proc_fds \<tau> p" 

    50 using finite_cfd[where p = p]

    51 apply (simp add:new_proc_fd_def nn_notin)

    52 done

    53 

    54 lemma nfd_notin_curfd': "\<lbrakk>new_proc_fd \<tau> p \<in> current_proc_fds \<tau> p; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    55 by (drule nfd_notin_curfd[where p = p], simp)

    56 

    57 lemma nim_notin_curim: "valid \<tau> \<Longrightarrow> new_inode_num \<tau> \<notin> current_inode_nums \<tau>"

    58 by (drule finite_ci, simp add:new_inode_num_def nn_notin)

    59 

    60 lemma nim_notin_curim': "\<lbrakk>new_inode_num \<tau> \<in> current_inode_nums \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

    61 by (drule nim_notin_curim, simp)

    62 

    63 lemma len_fname_all: "length (fname_all_a len) = len"

    64 by (induct len, auto simp:fname_all_a.simps)

    65 

    66 lemma ncf_notin_curf: "valid \<tau> \<Longrightarrow> new_childf f \<tau> \<notin> current_files \<tau>"

    67 apply (drule finite_cf)

    68 apply (simp add:new_childf_def next_fname_def all_fname_under_dir_def)

    69 apply (rule notI)

    70 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>}")

    71 defer apply simp

    72 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>}")

    73 defer apply (auto simp:fname_length_set_def image_def)[1]

    74 apply (subgoal_tac "finite (fname_length_set {fn. fn # f \<in> current_files \<tau>})")  

    75 defer

    76 apply (simp add:fname_length_set_def) 

    77 apply (rule finite_imageI)

    78 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)

    79 apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files \<tau>)" in finite_subset)

    80 unfolding image_def

    81 apply (clarsimp  split:if_splits)

    82 apply (rule_tac x = "x # f" in bexI, simp+)

    83 

    84 apply (drule_tac s = "(fname_length_set {fn. fn # f \<in> current_files \<tau>})" in nn_notin_aux)

    85 apply (erule_tac x = "length (CHR ''a'' # fname_all_a (Max (fname_length_set {fn. fn # f \<in> current_files \<tau>})))" in ballE)

    86 apply (simp add:len_fname_all, simp)

    87 done

    88 

    89 lemma ncf_parent: "valid \<tau> \<Longrightarrow> parent (new_childf f \<tau>) = Some f"

    90 by (simp add:new_childf_def)

    91 

    92 end

    93 

    94 end