1 (*<*)

     2 theory Co2sobj_prop

     3 imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop Alive_prop

     4 begin

     5 (*<*)

     6 

     7 ML {*

     8 fun print_ss ss =

     9 let

    10 val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss

    11 in

    12 simps

    13 end

    14 *}

    15 

    16 

    17 context tainting_s begin

    18 

    19 (********************* cm2smsg simpset ***********************)

    20 

    21 lemma cm2smsg_other: 

    22   "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m; \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

    23    \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"

    24 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)

    25 unfolding cm2smsg_def

    26 apply (case_tac e)

    27 apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted 

    28            split:t_object.splits option.splits if_splits 

    29             dest:not_deleted_init_msg  dest!:current_has_sec')

    30 done

    31 

    32 lemma cm2smsg_sendmsg:

    33   "valid (SendMsg p q m # s) \<Longrightarrow> cm2smsg (SendMsg p q m # s) = (\<lambda> q' m'. 

    34      if (q' = q \<and> m' = m)

    35      then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

    36              Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))

    37            | _ \<Rightarrow> None)

    38      else cm2smsg s q' m') "

    39 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)

    40 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    41   split:if_splits option.splits

    42   dest:not_deleted_init_msg  dest!:current_has_sec')

    43 done

    44 

    45 lemma cm2smsg_recvmsg1:

    46   "\<lbrakk>q' \<noteq> q; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"

    47 apply (frule vd_cons, frule vt_grant_os, rule ext)

    48 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    49   split:if_splits option.splits)

    50 done

    51 

    52 lemma cm2smsg_recvmsg2:

    53   "\<lbrakk>m' \<noteq> m; valid (RecvMsg p q m # s)\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"

    54 apply (frule vd_cons, frule vt_grant_os)

    55 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    56   split:if_splits option.splits)

    57 done

    58 

    59 lemma cm2smsg_recvmsg1':

    60   "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'"

    61 apply (frule vd_cons, frule vt_grant_os, rule ext)

    62 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    63   split:if_splits option.splits)

    64 done

    65 

    66 lemma cm2smsg_recvmsg2':

    67   "\<lbrakk>valid (RecvMsg p q m # s); m' \<noteq> m\<rbrakk> \<Longrightarrow> cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'"

    68 apply (frule vd_cons, frule vt_grant_os)

    69 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    70   split:if_splits option.splits)

    71 done

    72 

    73 lemma cm2smsg_removemsgq:

    74   "\<lbrakk>q' \<noteq> q; valid (RemoveMsgq p q # s)\<rbrakk> \<Longrightarrow> cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'"

    75 apply (frule vd_cons, frule vt_grant_os, rule ext)

    76 apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

    77   split:if_splits option.splits)

    78 done

    79 

    80 lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'

    81   cm2smsg_removemsgq cm2smsg_other

    82 

    83 lemma init_cm2smsg_has_smsg:

    84   "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"

    85 by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)

    86 

    87 lemma hd_set_prop1:

    88   "hd l \<notin> set l \<Longrightarrow> l = []"

    89 by (case_tac l, auto)

    90 

    91 lemma tl_set_prop1:

    92   "a \<in> set (tl l) \<Longrightarrow> a \<in> set l"

    93 by (case_tac l, auto)

    94 

    95 lemma current_has_smsg:

    96   "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sm. cm2smsg s q m = Some sm"

    97 apply (induct s)

    98 apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg)

    99 

   100 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   101 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits

   102   dest!:current_has_sec' hd_set_prop1 dest:not_deleted_init_msg tl_set_prop1)

   103 done 

   104 

   105 lemma current_has_smsg':

   106   "\<lbrakk>cm2smsg s q m = None; q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> m \<notin> set (msgs_of_queue s q)"

   107 by (auto dest:current_has_smsg)

   108 

   109 lemma cqm2sms_has_sms_aux:

   110   "\<forall> m \<in> set ms. sectxt_of_obj s (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. cqm2sms s q ms = Some sms)"

   111 by (induct ms, auto split:option.splits simp:cm2smsg_def)

   112 

   113 lemma current_has_sms:

   114   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sms. cqm2sms s q (msgs_of_queue s q) = Some sms"

   115 apply (rule cqm2sms_has_sms_aux)

   116 apply (auto dest:current_msg_has_sec)

   117 done

   118 

   119 lemma current_has_sms':

   120   "\<lbrakk>cqm2sms s q (msgs_of_queue s q) = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"

   121 by (auto dest:current_has_sms)

   122 

   123 (********************* cqm2sms simpset ***********************) 

   124 

   125 lemma cqm2sms_other:

   126   "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   127     \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

   128    \<Longrightarrow> cqm2sms (e # s) = cqm2sms s"

   129 apply (rule ext, rule ext)

   130 apply (induct_tac xa, simp)

   131 apply (frule vt_grant_os, frule vd_cons, case_tac e)

   132 apply (auto split:option.splits dest:cm2smsg_other) 

   133 done

   134 

   135 lemma cqm2sms_createmsgq:

   136   "valid (CreateMsgq p q # s) \<Longrightarrow> cqm2sms (CreateMsgq p q # s) = (\<lambda> q' ms'. 

   137      if (q' = q \<and> ms' = []) then Some []

   138      else cqm2sms s q' ms')"

   139 apply (rule ext, rule ext)

   140 apply (frule vt_grant_os, frule vd_cons, induct_tac ms')

   141 apply (auto split:if_splits option.splits dest:cm2smsg_other)

   142 done

   143 

   144 lemma cqm2sms_2:

   145   "cqm2sms s q (ms @ [m]) = 

   146      (case (cqm2sms s q ms, cm2smsg s q m) of 

   147        (Some sms, Some sm) \<Rightarrow> Some (sms @ [sm]) 

   148      | _ \<Rightarrow> None)"

   149 apply (induct ms, simp split:option.splits)

   150 by (auto split:option.splits)

   151 

   152 lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2

   153 

   154 declare cqm2sms.simps [simp del]

   155 

   156 lemma cqm2sms_prop1:

   157   "cqm2sms s q ms = None \<Longrightarrow> \<exists> m \<in> set ms. cm2smsg s q m = None"

   158 by (induct ms, auto simp:cqm2sms.simps split:option.splits)

   159 

   160 lemma cqm2sms_sendmsg1:

   161   "\<lbrakk>valid (SendMsg p q m # s); m \<notin> set ms\<rbrakk>

   162    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"

   163 apply (frule vt_grant_os, frule vd_cons)

   164 apply (frule cm2smsg_sendmsg)

   165 apply (induct ms rule:rev_induct)

   166 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)

   167 done

   168 

   169 lemma cqm2sms_sendmsg2:

   170   "\<lbrakk>valid (SendMsg p q m # s); q' \<noteq> q\<rbrakk>

   171    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms"

   172 apply (frule vt_grant_os, frule vd_cons)

   173 apply (frule cm2smsg_sendmsg)

   174 apply (induct ms rule:rev_induct)

   175 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2)

   176 done

   177 

   178 lemma cqm2sms_sendmsg3:

   179   "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\<rbrakk>

   180    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q ms' = 

   181      (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

   182        (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   183      | _ \<Rightarrow> None)"

   184 apply (frule vt_grant_os, frule vd_cons)

   185 apply (frule cm2smsg_sendmsg)

   186 apply (auto split:if_splits option.splits  simp:cqm2sms_simps2 cqm2sms_sendmsg1)

   187 done

   188 

   189 lemma cqm2sms_sendmsg:

   190   "\<lbrakk>valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\<rbrakk> 

   191    \<Longrightarrow> cqm2sms (SendMsg p q m # s) q' ms' = (

   192      if (q' = q) 

   193      then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of

   194              (Some sms, Some sec) \<Rightarrow> Some (sms @ [(Created, sec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   195            | _ \<Rightarrow> None)

   196      else cqm2sms s q' ms' )"

   197 apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3)

   198 done

   199 

   200 lemma cqm2sms_recvmsg1:

   201   "\<lbrakk>valid (RecvMsg p q m # s); m \<notin> set ms\<rbrakk> 

   202    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms"

   203 apply (frule vt_grant_os, frule vd_cons)

   204 apply (induct ms rule:rev_induct)

   205 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2')

   206 done

   207 

   208 lemma cqm2sms_recvmsg2:

   209   "\<lbrakk>valid (RecvMsg p q m # s); q' \<noteq> q\<rbrakk>

   210    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms"

   211 apply (frule vt_grant_os, frule vd_cons)

   212 apply (induct ms rule:rev_induct)

   213 apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1')

   214 done

   215 

   216 lemma cqm2sms_recvmsg:

   217   "\<lbrakk>valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\<rbrakk>

   218    \<Longrightarrow> cqm2sms (RecvMsg p q m # s) q' ms = (

   219      if (q' = q) 

   220      then (case (cqm2sms s q (msgs_of_queue s q)) of

   221              Some sms \<Rightarrow> Some (tl sms)

   222            | _ \<Rightarrow> None)

   223      else cqm2sms s q' ms)"

   224 apply (frule vt_grant_os, frule vd_cons)

   225 apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2 

   226      dest!:current_has_sms')

   227 apply (case_tac "msgs_of_queue s q", simp)

   228 apply (frule_tac ms = "tl (msgs_of_queue s q)" in cqm2sms_recvmsg1)

   229 apply (drule_tac q = q in distinct_queue_msgs, simp+)

   230 apply (case_tac a, auto simp:cqm2sms.simps split:option.splits if_splits)

   231 done

   232 

   233 lemma cqm2sms_removemsgq:

   234   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk> 

   235    \<Longrightarrow> cqm2sms (RemoveMsgq p q # s) q' ms = cqm2sms s q' ms"

   236 apply (frule vt_grant_os, frule vd_cons)

   237 apply (induct ms rule:rev_induct)

   238 apply (auto simp:cqm2sms_simps2 cm2smsg_removemsgq split:option.splits if_splits)

   239 done

   240   

   241 lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq

   242 

   243 (********************* cq2smsgq simpset ***********************) 

   244  

   245 lemma cq2smsgq_other: 

   246   "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<forall> p q m. e \<noteq> SendMsg p q m; 

   247     \<forall> p q m. e \<noteq> RecvMsg p q m; \<forall> p q. e \<noteq> RemoveMsgq p q\<rbrakk> 

   248    \<Longrightarrow> cq2smsgq (e # s) = cq2smsgq s" 

   249 apply (frule cqm2sms_other, simp+)

   250 apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) 

   251 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps 

   252            split:t_object.splits option.splits if_splits 

   253             dest:not_deleted_init_msg) 

   254 done

   255 

   256 lemma cq2smsg_createmsgq:

   257   "valid (CreateMsgq p q # s)

   258    \<Longrightarrow> cq2smsgq (CreateMsgq p q # s) = (cq2smsgq s) (q := 

   259      case (sectxt_of_obj s (O_proc p)) of

   260        Some psec \<Rightarrow> Some (Created, (fst psec, R_object, (snd o snd) psec), [])

   261      | None     \<Rightarrow> None)"

   262 apply (frule vd_cons, frule vt_grant_os)

   263 apply (frule cqm2sms_createmsgq)

   264 apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 

   265   split:option.splits if_splits dest:not_deleted_init_msgq)

   266 done

   267 

   268 lemma cq2smsg_sendmsg:

   269   "valid (SendMsg p q m # s) 

   270    \<Longrightarrow> cq2smsgq (SendMsg p q m # s) = (cq2smsgq s) (q := 

   271      case (cq2smsgq s q, sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of 

   272        (Some (qi, sec, sms), Some msec) \<Rightarrow> 

   273           Some (qi, sec, sms @ [(Created, msec, O_msg q m \<in> tainted (SendMsg p q m # s))])

   274      | _ \<Rightarrow> None)"

   275 apply (frule vd_cons, frule vt_grant_os)

   276 apply (rule ext)

   277 apply (frule_tac q' = x in cqm2sms_sendmsg, simp)

   278 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps  split:option.splits if_splits

   279   dest!:current_has_sms' current_has_sec')

   280 done

   281 

   282 lemma current_has_smsgq:

   283   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sq. cq2smsgq s q = Some sq"

   284 by (auto simp:cq2smsgq_def split:option.splits dest!:current_has_sec' current_has_sms')

   285 

   286 lemma current_has_smsgq':

   287   "\<lbrakk>cq2smsgq s q = None; valid s\<rbrakk> \<Longrightarrow> q \<notin> current_msgqs s"

   288 by (auto dest:current_has_smsgq)

   289 

   290 lemma cq2smsg_recvmsg:

   291   "valid (RecvMsg p q m # s) 

   292    \<Longrightarrow> cq2smsgq (RecvMsg p q m # s) = (cq2smsgq s) (q := 

   293     case (cq2smsgq s q) of

   294       Some (qi, sec, sms) \<Rightarrow> Some (qi, sec, tl sms)

   295     | _ \<Rightarrow> None)"

   296 apply (frule vd_cons, frule vt_grant_os)

   297 apply (rule ext, frule_tac q' = x in cqm2sms_recvmsg, simp)

   298 apply (auto simp add:cq2smsgq_def sectxt_of_obj_simps split:option.splits if_splits 

   299   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   300 done

   301 

   302 lemma cq2smsg_removemsgq:

   303   "\<lbrakk>valid (RemoveMsgq p q # s); q' \<noteq> q; q' \<in> current_msgqs s\<rbrakk>

   304    \<Longrightarrow> cq2smsgq (RemoveMsgq p q # s) q' = cq2smsgq s q'"

   305 apply (frule vd_cons, frule vt_grant_os)

   306 apply (auto simp:cq2smsgq_def sectxt_of_obj_simps cqm2sms_removemsgq split:if_splits option.splits 

   307   dest!:current_has_sec' current_has_sms' current_has_smsgq')

   308 done

   309 

   310 lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq

   311 

   312 lemma sm_in_sqsms_init_aux:

   313   "\<lbrakk>m \<in> set ms; init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   314     init_cqm2sms q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   315 apply (induct ms arbitrary:m sm sms)

   316 by (auto split:if_splits option.splits)

   317 

   318 lemma sm_in_sqsms_init:

   319   "\<lbrakk>m \<in> set (init_msgs_of_queue q); init_cm2smsg q m = Some sm; q \<in> init_msgqs; 

   320     init_cqm2sms q (init_msgs_of_queue q) = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   321 by (simp add:sm_in_sqsms_init_aux)

   322 

   323 lemma cqm2sms_prop0:

   324   "\<lbrakk>m \<in> set ms; cm2smsg s q m = Some sm; cqm2sms s q ms = Some sms\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   325 apply (induct ms arbitrary:m sm sms)

   326 apply (auto simp:cqm2sms.simps split:option.splits)

   327 done

   328 

   329 lemma sm_in_sqsms:

   330   "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms);

   331     cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms"

   332 proof (induct s arbitrary:m q qi qsec sms sm)

   333   case Nil

   334   thus ?case 

   335     by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 

   336            split:option.splits)

   337 next

   338   case (Cons e s)

   339   hence p1:"\<And> m q qi qsec sms sm. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; 

   340     cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   341     \<Longrightarrow> sm \<in> set sms" and p2: "m \<in> set (msgs_of_queue (e # s) q)" 

   342     and p3: "q \<in> current_msgqs (e # s)" and p4: "valid (e # s)"

   343     and p5: "cq2smsgq (e # s) q = Some (qi, qsec, sms)"

   344     and p6: "cm2smsg (e # s) q m = Some sm" by auto

   345   from p4 have os: "os_grant s e" and vd: "valid s" by (auto dest:vd_cons vt_grant_os)

   346 (*

   347   from p1 have p1':

   348     "\<And> m q qi qsec sms sm ms. \<lbrakk>m \<in> set ms; set ms \<subseteq> set (msgs_of_queue s q); q \<in> current_msgqs s;

   349     valid s; cq2smsgq s q = Some (qi, qsec, sms); cm2smsg s q m = Some sm\<rbrakk>

   350     \<Longrightarrow> sm \<in> set "

   351 *)

   352   show ?case using p2 p3 p4 p5 p6 vd os

   353     apply (case_tac e)

   354     apply (auto simp:cq2smsgq_simps cm2smsg_simps split:if_splits option.splits intro:p1)

   355 

   356     apply (rule_tac m = m and q = q and qi = qi and qsec = qsec in p1, simp+)

   357     apply (case_tac "q = nat2", simp)

   358     apply (drule cq2smsg_createmsgq, simp, simp)

   359 

   360     apply (drule_tac m = m and q = q and qi = qi and qsec = "(aa,ab,b)" in p1, simp+)

   361 

   362     apply (simp add:cq2smsgq_def split:option.splits)

   363     apply (rule_tac m = m and sm = sm in cqm2sms_prop0, simp+)

   364     apply (simp add:cqm2sms_recvmsg)

   365     done

   366 qed

   367 

   368 (****************** cf2sfile path simpset ***************)

   369 

   370 lemma sroot_only:

   371   "cf2sfile s [] = Some sroot"

   372 by (simp add:cf2sfile_def)

   373 

   374 lemma not_file_is_dir:

   375   "\<lbrakk>\<not> is_file s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_dir s f"

   376 by (auto simp:is_file_def current_files_def is_dir_def 

   377          dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

   378 

   379 lemma not_dir_is_file:

   380   "\<lbrakk>\<not> is_dir s f; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f"

   381 by (auto simp:is_file_def current_files_def is_dir_def 

   382          dest:finum_has_itag finum_has_ftag' split:t_inode_tag.splits option.splits)

   383 

   384 lemma is_file_or_dir:

   385   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> is_file s f \<or> is_dir s f"

   386 by (auto dest:not_dir_is_file)

   387 

   388 lemma current_file_has_sfile:

   389   "\<lbrakk>f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   390 apply (induct f)

   391 apply (rule_tac x = "sroot" in exI, simp add:sroot_only)

   392 apply (frule parentf_in_current', simp, clarsimp)

   393 apply (frule parentf_is_dir'', simp)

   394 apply (frule is_file_or_dir, simp)

   395 apply (auto dest!:current_has_sec'

   396             simp:cf2sfile_def split:option.splits if_splits dest!:get_pfs_secs_prop')

   397 done

   398 

   399 definition sectxt_of_pf :: "t_state \<Rightarrow> t_file \<Rightarrow> security_context_t option"

   400 where

   401   "sectxt_of_pf s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> sectxt_of_obj s (O_dir pf))"

   402 

   403 definition get_parentfs_ctxts' :: "t_state \<Rightarrow> t_file \<Rightarrow> (security_context_t list) option"

   404 where

   405   "get_parentfs_ctxts' s f = (case f of [] \<Rightarrow> None | (a # pf) \<Rightarrow> get_parentfs_ctxts s pf)"

   406 

   407 lemma is_file_has_sfile:

   408   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sec psec asecs. cf2sfile s f = Some 

   409       (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created,

   410        sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_file f) = Some sec) \<and>

   411        (sectxt_of_pf s f = Some psec) \<and> (get_parentfs_ctxts' s f = Some asecs)"

   412 apply (case_tac f, simp, drule root_is_dir', simp, simp)

   413 apply (frule is_file_in_current)

   414 apply (drule current_file_has_sfile, simp)

   415 apply (auto simp:cf2sfile_def sectxt_of_pf_def get_parentfs_ctxts'_def split:if_splits option.splits)

   416 done

   417 

   418 lemma is_file_has_sfile':

   419   "\<lbrakk>is_file s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   420 by (drule is_file_has_sfile, auto)

   421 

   422 lemma is_dir_has_sfile:

   423   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> (case f of

   424       [] \<Rightarrow> cf2sfile s f = Some sroot

   425     | a # pf \<Rightarrow> (\<exists> sec psec asecs. cf2sfile s f = Some 

   426       (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created,

   427        sec, Some psec, set asecs) \<and> (sectxt_of_obj s (O_dir f) = Some sec) \<and>

   428        (sectxt_of_obj s (O_dir pf) = Some psec) \<and> (get_parentfs_ctxts s pf = Some asecs)))"

   429 apply (case_tac f, simp add:sroot_only)

   430 apply (frule is_dir_in_current, frule is_dir_not_file)

   431 apply (drule current_file_has_sfile, simp)

   432 apply (auto simp:cf2sfile_def split:if_splits option.splits)

   433 done

   434 

   435 lemma is_dir_has_sdir':

   436   "\<lbrakk>is_dir s f; valid s\<rbrakk> \<Longrightarrow> \<exists> sf. cf2sfile s f = Some sf"

   437 apply (case_tac f)

   438 apply (rule_tac x = sroot in exI)

   439 apply (simp add:sroot_only)

   440 apply (drule is_dir_has_sfile, auto)

   441 done

   442 

   443 lemma sroot_set:

   444   "valid s \<Longrightarrow> \<exists> sec. sroot = (Init [], sec, None, {}) \<and> sectxt_of_obj s (O_dir []) = Some sec"

   445 apply (frule root_is_dir)

   446 apply (drule is_dir_has_sec, simp)

   447 apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 

   448                  root_type_remains root_user_remains

   449            dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'

   450            split:option.splits)

   451 done

   452 

   453 lemma cf2sfile_path_file:

   454   "\<lbrakk>is_file s (f # pf); valid s\<rbrakk>

   455    \<Longrightarrow> cf2sfile s (f # pf) = (

   456      case (cf2sfile s pf) of

   457        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

   458           (case (sectxt_of_obj s (O_file (f # pf))) of

   459               Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   460                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   461            | None \<Rightarrow> None)

   462      | _ \<Rightarrow> None)"

   463 apply (frule is_file_in_current, drule parentf_is_dir'', simp)

   464 apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp)

   465 apply (frule sroot_set)

   466 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

   467 done

   468 

   469 lemma cf2sfile_path_dir:

   470   "\<lbrakk>is_dir s (f # pf); valid s\<rbrakk>

   471    \<Longrightarrow> cf2sfile s (f # pf) = (

   472      case (cf2sfile s pf) of

   473        Some (pfi, pfsec, psec, asecs) \<Rightarrow> 

   474           (case (sectxt_of_obj s (O_dir (f # pf))) of

   475               Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   476                                 else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   477            | None \<Rightarrow> None)

   478      | _ \<Rightarrow> None)"

   479 apply (frule is_dir_in_current, drule parentf_is_dir'', simp)

   480 apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp)

   481 apply (frule_tac f = "pf" in is_dir_has_sfile, simp)

   482 apply (frule sroot_set)

   483 apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) 

   484 done  

   485 

   486 lemma cf2sfile_path:

   487   "\<lbrakk>f # pf \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = (

   488      case (cf2sfile s pf) of

   489        Some (pfi, pfsec, psec, asecs) \<Rightarrow> (if (is_file s (f # pf))

   490          then (case (sectxt_of_obj s (O_file (f # pf))) of

   491                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   492                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   493                | None \<Rightarrow> None)

   494          else (case (sectxt_of_obj s (O_dir (f # pf))) of

   495                  Some fsec \<Rightarrow> Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   496                                    else Created, fsec, Some pfsec, asecs \<union> {pfsec})

   497                | None \<Rightarrow> None)           )

   498      | None \<Rightarrow> None)"

   499 apply (drule is_file_or_dir, simp)

   500 apply (erule disjE)

   501 apply (frule cf2sfile_path_file, simp) defer

   502 apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file)

   503 apply (auto split:option.splits)

   504 done

   505 

   506 lemma cf2sfile_path_file_prop1:

   507   "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   508    \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

   509                  Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   510                        else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

   511                sectxt_of_obj s (O_file (f # pf)) = Some fsec"

   512 apply (frule is_file_has_sfile, simp)

   513 by (auto simp:cf2sfile_path_file)

   514 

   515 lemma cf2sfile_path_file_prop2:

   516   "\<lbrakk>is_file s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

   517     sectxt_of_obj s (O_file (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

   518       Some (if (\<not> deleted (O_file (f # pf)) s \<and> is_init_file (f # pf)) then Init (f # pf)

   519             else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

   520 by (drule cf2sfile_path_file_prop1, auto)

   521 

   522 lemma cf2sfile_path_dir_prop1:

   523   "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); valid s\<rbrakk>

   524    \<Longrightarrow> \<exists> fsec. cf2sfile s (f # pf) = 

   525                  Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   526                        else Created, fsec, Some pfsec, asecs \<union> {pfsec}) \<and> 

   527                sectxt_of_obj s (O_dir (f # pf)) = Some fsec"

   528 apply (frule is_dir_has_sfile, simp)

   529 by (auto simp:cf2sfile_path_dir)

   530 

   531 lemma cf2sfile_path_dir_prop2:

   532   "\<lbrakk>is_dir s (f # pf); cf2sfile s pf = Some (pfi, pfsec, psec, asecs); 

   533     sectxt_of_obj s (O_dir (f # pf)) = Some fsec; valid s\<rbrakk> \<Longrightarrow> cf2sfile s (f # pf) = 

   534       Some (if (\<not> deleted (O_dir (f # pf)) s \<and> is_init_dir (f # pf)) then Init (f # pf)

   535             else Created, fsec, Some pfsec, asecs \<union> {pfsec})"

   536 by (drule cf2sfile_path_dir_prop1, auto)

   537 

   538 (**************** cf2sfile event list simpset ****************)

   539 

   540 lemma cf2sfile_open_none':

   541   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) f'= cf2sfile s f'"

   542 apply (frule vd_cons, frule vt_grant_os)

   543 apply (induct f', simp add:cf2sfile_def)

   544 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   545                get_parentfs_ctxts_simps)

   546 done

   547 

   548 lemma cf2sfile_open_none:

   549   "valid (Open p f flag fd None # s) \<Longrightarrow> cf2sfile (Open p f flag fd None # s) = cf2sfile s"

   550 apply (rule ext)

   551 by (simp add:cf2sfile_open_none')

   552 

   553 lemma cf2sfile_open_some1:

   554   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); f' \<in> current_files s\<rbrakk>

   555    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   556 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   557 apply (case_tac "f = f'", simp)

   558 apply (induct f', simp add:sroot_only, simp)

   559 apply (frule parentf_in_current', simp+)

   560 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   561                get_parentfs_ctxts_simps)

   562 done

   563 

   564 lemma cf2sfile_open_some2:

   565   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_file s f'\<rbrakk>

   566    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   567 apply (frule vd_cons, drule is_file_in_current)

   568 by (simp add:cf2sfile_open_some1)

   569 

   570 lemma cf2sfile_open_some3:

   571   "\<lbrakk>valid (Open p f flag fd (Some inum) # s); is_dir s f'\<rbrakk>

   572    \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f' = cf2sfile s f'"

   573 apply (frule vd_cons, drule is_dir_in_current)

   574 by (simp add:cf2sfile_open_some1)

   575 

   576 lemma cf2sfile_open_some4:

   577   "valid (Open p f flag fd (Some inum) # s) \<Longrightarrow> cf2sfile (Open p f flag fd (Some inum) # s) f = (

   578      case (parent f) of

   579        Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd (Some inum) # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   580                          get_parentfs_ctxts s pf) of

   581                     (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   582                   | _ \<Rightarrow> None)

   583      | None \<Rightarrow> None)"

   584 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   585 apply (case_tac f, simp)

   586 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   587                get_parentfs_ctxts_simps)

   588 apply (rule impI, (erule conjE)+)

   589 apply (drule not_deleted_init_file, simp+)

   590 apply (simp add:is_file_in_current)

   591 done

   592 

   593 lemma cf2sfile_open:

   594   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>

   595    \<Longrightarrow> cf2sfile (Open p f flag fd opt # s) f' = (

   596      if (opt = None) then cf2sfile s f'

   597      else if (f' = f) 

   598      then (case (parent f) of

   599              Some pf \<Rightarrow> (case (sectxt_of_obj (Open p f flag fd opt # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   600                  get_parentfs_ctxts s pf) of

   601                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   602                         | _ \<Rightarrow> None)

   603            | None \<Rightarrow> None)

   604      else cf2sfile s f')"

   605 apply (case_tac opt)

   606 apply (simp add:cf2sfile_open_none)

   607 apply (case_tac "f = f'")

   608 apply (simp add:cf2sfile_open_some4 split:option.splits)

   609 apply (simp add:cf2sfile_open_some1 current_files_simps)

   610 done

   611 

   612 lemma cf2sfile_mkdir1:

   613   "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files s\<rbrakk>

   614    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   615 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   616 apply (case_tac "f = f'", simp)

   617 apply (induct f', simp add:sroot_only, simp)

   618 apply (frule parentf_in_current', simp+)

   619 apply (case_tac "f = f'", simp)

   620 apply (simp add:cf2sfile_path is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   621                get_parentfs_ctxts_simps split:if_splits option.splits)

   622 done

   623 

   624 lemma cf2sfile_mkdir2:

   625   "\<lbrakk>valid (Mkdir p f i # s); is_file s f'\<rbrakk>

   626    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   627 apply (frule vd_cons, drule is_file_in_current)

   628 by (simp add:cf2sfile_mkdir1)

   629 

   630 lemma cf2sfile_mkdir3:

   631   "\<lbrakk>valid (Mkdir p f i # s); is_dir s f'\<rbrakk>

   632    \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = cf2sfile s f'"

   633 apply (frule vd_cons, drule is_dir_in_current)

   634 by (simp add:cf2sfile_mkdir1)

   635 

   636 lemma cf2sfile_mkdir4:

   637   "valid (Mkdir p f i # s)

   638   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f = (case (parent f) of

   639          Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 

   640                            get_parentfs_ctxts s pf) of

   641                       (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   642                     | _ \<Rightarrow> None)

   643        | None \<Rightarrow> None)"

   644 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   645 apply (case_tac f, simp)

   646 apply (clarsimp simp:os_grant.simps)

   647 apply (simp add:sectxt_of_obj_simps)

   648 apply (frule current_proc_has_sec, simp)

   649 apply (frule is_dir_has_sec, simp)

   650 apply (frule get_pfs_secs_prop, simp)

   651 apply (frule is_dir_not_file)

   652 apply (auto simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   653                get_parentfs_ctxts_simps split:option.splits if_splits 

   654             dest:not_deleted_init_dir is_dir_in_current not_deleted_init_file is_file_in_current)

   655 done

   656 

   657 lemma cf2sfile_mkdir:

   658   "\<lbrakk>valid (Mkdir p f i # s); f' \<in> current_files (Mkdir p f i # s)\<rbrakk>

   659   \<Longrightarrow> cf2sfile (Mkdir p f i # s) f' = (

   660     if (f' = f) 

   661     then (case (parent f) of

   662              Some pf \<Rightarrow> (case (sectxt_of_obj (Mkdir p f i # s) (O_dir f), sectxt_of_obj s (O_dir pf), 

   663                  get_parentfs_ctxts s pf) of

   664                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   665                         | _ \<Rightarrow> None)

   666            | None \<Rightarrow> None)

   667      else cf2sfile s f')"

   668 apply (case_tac "f = f'")

   669 apply (simp add:cf2sfile_mkdir4 split:option.splits)

   670 apply (simp add:cf2sfile_mkdir1 current_files_simps)

   671 done

   672 

   673 lemma cf2sfile_linkhard1:

   674   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files s\<rbrakk>

   675    \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"

   676 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   677 apply (case_tac "f = f'", simp)

   678 apply (induct f', simp add:sroot_only, simp)

   679 apply (frule parentf_in_current', simp+)

   680 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   681                get_parentfs_ctxts_simps split:if_splits option.splits)

   682 done

   683 

   684 lemma cf2sfile_linkhard2:

   685   "\<lbrakk>valid (LinkHard p oldf f # s); is_file s f'\<rbrakk>

   686    \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

   687 apply (frule vd_cons, drule is_file_in_current)

   688 by (simp add:cf2sfile_linkhard1)

   689 

   690 lemma cf2sfile_linkhard3:

   691   "\<lbrakk>valid (LinkHard p oldf f # s); is_dir s f'\<rbrakk>

   692    \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = cf2sfile s f'"

   693 apply (frule vd_cons, drule is_dir_in_current)

   694 by (simp add:cf2sfile_linkhard1)

   695 

   696 lemma cf2sfile_linkhard4:

   697   "valid (LinkHard p oldf f # s)

   698   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f = (case (parent f) of

   699          Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   700                            get_parentfs_ctxts s pf) of

   701                       (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   702                     | _ \<Rightarrow> None)

   703        | None \<Rightarrow> None)"

   704 apply (frule vd_cons, frule vt_grant_os, frule noroot_events)

   705 apply (case_tac f, simp)

   706 apply (simp add:cf2sfile_def is_file_simps is_dir_simps current_files_simps sectxt_of_obj_simps 

   707                get_parentfs_ctxts_simps)

   708 apply (rule impI, (erule conjE)+)

   709 apply (drule not_deleted_init_file, simp+)

   710 apply (simp add:is_file_in_current)

   711 done

   712 

   713 lemma cf2sfile_linkhard:

   714   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> current_files (LinkHard p oldf f # s)\<rbrakk>

   715   \<Longrightarrow> cf2sfile (LinkHard p oldf f # s) f' = (

   716     if (f' = f) 

   717     then (case (parent f) of

   718              Some pf \<Rightarrow> (case (sectxt_of_obj (LinkHard p oldf f # s) (O_file f), sectxt_of_obj s (O_dir pf), 

   719                  get_parentfs_ctxts s pf) of

   720                           (Some sec, Some psec, Some asecs) \<Rightarrow> Some (Created, sec, Some psec, set asecs)

   721                         | _ \<Rightarrow> None)

   722            | None \<Rightarrow> None)

   723      else cf2sfile s f')"

   724 apply (case_tac "f = f'")

   725 apply (simp add:cf2sfile_linkhard4 split:option.splits)

   726 apply (simp add:cf2sfile_linkhard1 current_files_simps)

   727 done

   728 

   729 lemma cf2sfile_other:

   730   "\<lbrakk>ff \<in> current_files s;

   731     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   732     \<forall> p fd. e \<noteq> CloseFd p fd;

   733     \<forall> p f. e \<noteq> UnLink p f;

   734     \<forall> p f. e \<noteq> Rmdir p f;

   735     \<forall> p f i. e \<noteq> Mkdir p f i;

   736     \<forall> p f f'. e \<noteq> LinkHard p f f'; 

   737     valid (e # s)\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"

   738 apply (frule vd_cons, frule vt_grant_os)

   739 apply (induct ff, simp add:sroot_only)

   740 apply (frule parentf_in_current', simp+, case_tac e)

   741 apply (auto simp:current_files_simps is_file_simps is_dir_simps sectxt_of_obj_simps cf2sfile_path 

   742            split:if_splits option.splits)                     

   743 done     

   744 

   745 lemma cf2sfile_other':

   746   "\<lbrakk>valid (e # s); 

   747     \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;

   748     \<forall> p fd. e \<noteq> CloseFd p fd;

   749     \<forall> p f. e \<noteq> UnLink p f;

   750     \<forall> p f. e \<noteq> Rmdir p f;

   751     \<forall> p f i. e \<noteq> Mkdir p f i;

   752     \<forall> p f f'. e \<noteq> LinkHard p f f'; 

   753     ff \<in> current_files s\<rbrakk> \<Longrightarrow> cf2sfile (e # s) ff = cf2sfile s ff"

   754 by (auto intro!:cf2sfile_other)

   755   

   756 lemma cf2sfile_unlink:

   757   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk>

   758    \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"

   759 apply (frule vd_cons, frule vt_grant_os)

   760 apply (simp add:current_files_simps split:if_splits)

   761 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

   762            split:if_splits option.splits)

   763 done

   764 

   765 lemma cf2sfile_rmdir:

   766   "\<lbrakk>valid (Rmdir p f # s); f' \<in> current_files (Rmdir p f # s)\<rbrakk>

   767    \<Longrightarrow> cf2sfile (Rmdir p f # s) f' = cf2sfile s f'"

   768 apply (frule vd_cons, frule vt_grant_os)

   769 apply (simp add:current_files_simps split:if_splits)

   770 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps

   771            split:if_splits option.splits)

   772 done

   773 

   774 lemma pfdof_simp5: "\<lbrakk>proc_fd_of_file s f = {(p, fd)}; file_of_proc_fd s p fd = None\<rbrakk> \<Longrightarrow> False"

   775 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   776 by (simp add:pfdof_simp2, simp)

   777 

   778 lemma pfdof_simp6: "proc_fd_of_file s f = {(p, fd)} \<Longrightarrow> file_of_proc_fd s p fd = Some f"

   779 apply (subgoal_tac "(p, fd) \<in> proc_fd_of_file s f")

   780 by (simp add:pfdof_simp2, simp)

   781 

   782 lemma cf2sfile_closefd:

   783   "\<lbrakk>valid (CloseFd p fd # s); f \<in> current_files (CloseFd p fd # s)\<rbrakk>

   784    \<Longrightarrow> cf2sfile (CloseFd p fd # s) f = cf2sfile s f"

   785 apply (frule vd_cons, frule vt_grant_os)

   786 apply (simp add:current_files_simps split:if_splits option.splits) 

   787 (* costs too much time, but solved *)

   788 

   789 apply (auto simp:cf2sfile_def sectxt_of_obj_simps get_parentfs_ctxts_simps is_file_simps is_dir_simps 

   790            split:if_splits option.splits  

   791             dest:init_file_dir_conflict pfdof_simp5 pfdof_simp6 file_of_pfd_is_file

   792                  not_deleted_init_file not_deleted_init_dir is_file_not_dir is_dir_not_file

   793             dest!:current_has_sec')

   794 done

   795 

   796 lemmas cf2sfile_simps = cf2sfile_open cf2sfile_mkdir cf2sfile_linkhard cf2sfile_other

   797   cf2sfile_unlink cf2sfile_rmdir cf2sfile_closefd

   798   

   799 (*********** cfd2sfd simpset *********)

   800 

   801 lemma cfd2sfd_open1:

   802   "valid (Open p f flags fd opt # s)

   803    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p fd = 

   804      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   805         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   806       | _ \<Rightarrow> None)"

   807 by (simp add:cfd2sfd_def sectxt_of_obj_simps split:if_splits)

   808 

   809 lemma cfd2sfd_open_some2:

   810   "\<lbrakk>valid (Open p f flags fd (Some inum) # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   811   \<Longrightarrow> cfd2sfd (Open p f flags fd (Some inum) # s) p' fd' = cfd2sfd s p' fd'"

   812 apply (frule vd_cons, frule vt_grant_os)

   813 apply (frule proc_fd_in_fds, simp)

   814 apply (frule file_of_proc_fd_in_curf, simp)

   815 apply (case_tac "f = f'", simp)

   816 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_some1)

   817 apply (case_tac "p = p'", simp)

   818 apply (rule conjI, rule impI, simp)

   819 apply (drule cf2sfile_open_some1, simp)

   820 apply (auto split:option.splits)[1]

   821 apply simp

   822 apply (drule cf2sfile_open_some1, simp)

   823 apply (auto split:option.splits)[1]

   824 done

   825 

   826 lemma cfd2sfd_open_none2:

   827   "\<lbrakk>valid (Open p f flags fd None # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   828   \<Longrightarrow> cfd2sfd (Open p f flags fd None # s) p' fd' = cfd2sfd s p' fd'"

   829 apply (frule vd_cons, frule vt_grant_os)

   830 apply (frule proc_fd_in_fds, simp)

   831 apply (frule file_of_proc_fd_in_curf, simp)

   832 apply (simp add:cfd2sfd_def sectxt_of_obj_simps cf2sfile_open_none)

   833 apply (case_tac "p = p'", simp)

   834 apply (rule conjI, rule impI, simp)

   835 apply (drule cf2sfile_open_none)

   836 apply (auto split:option.splits)[1]

   837 apply simp

   838 apply (drule cf2sfile_open_none)

   839 apply (auto split:option.splits)[1]

   840 done

   841   

   842 lemma cfd2sfd_open2:

   843   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd s p' fd' = Some f'\<rbrakk>

   844   \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = cfd2sfd s p' fd'"

   845 apply (case_tac opt)

   846 apply (simp add:cfd2sfd_open_none2)

   847 apply (simp add:cfd2sfd_open_some2)

   848 done

   849 

   850 lemma cfd2sfd_open:

   851   "\<lbrakk>valid (Open p f flags fd opt # s); file_of_proc_fd (Open p f flags fd opt # s) p' fd' = Some f'\<rbrakk>

   852    \<Longrightarrow> cfd2sfd (Open p f flags fd opt # s) p' fd' = (if (p' = p \<and> fd' = fd) then 

   853      (case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

   854         (Some sec, Some sf) \<Rightarrow> Some (sec, flags, sf)

   855       | _ \<Rightarrow> None)         else cfd2sfd s p' fd')"

   856 apply (simp split:if_splits)

   857 apply (simp add:cfd2sfd_open1 split:option.splits)

   858 apply (simp add:cfd2sfd_open2)

   859 apply (rule impI, simp)

   860 done

   861 

   862 lemma cfd2sfd_closefd:

   863   "\<lbrakk>valid (CloseFd p fd # s); file_of_proc_fd (CloseFd p fd # s) p' fd' = Some f\<rbrakk>

   864    \<Longrightarrow> cfd2sfd (CloseFd p fd # s) p' fd' = cfd2sfd  s p' fd'"

   865 apply (frule vd_cons, frule vt_grant_os)

   866 apply (frule proc_fd_in_fds, simp)

   867 apply (frule file_of_proc_fd_in_curf, simp)

   868 apply (frule cf2sfile_closefd, simp)

   869 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   870 apply (auto split:option.splits if_splits)

   871 done

   872 

   873 lemma cfd2sfd_clone:

   874   "\<lbrakk>valid (Clone p p' fds shms # s); file_of_proc_fd (Clone p p' fds shms # s) p'' fd' = Some f\<rbrakk>

   875    \<Longrightarrow> cfd2sfd (Clone p p' fds shms # s) p'' fd' = (

   876      if (p'' = p') then cfd2sfd s p fd'

   877      else cfd2sfd s p'' fd')"

   878 apply (frule vd_cons, frule vt_grant_os)

   879 apply (frule proc_fd_in_fds, simp)

   880 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   881 apply (frule_tac cf2sfile_other', simp+)

   882 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   883 apply (case_tac "p'' = p'", simp)

   884 apply (auto split:option.splits if_splits)[1]

   885 apply (simp)

   886 apply (auto split:option.splits if_splits)[1]

   887 done

   888 

   889 lemma cfd2sfd_execve:

   890   "\<lbrakk>valid (Execve p f fds # s); file_of_proc_fd (Execve p f fds # s) p' fd' = Some f'\<rbrakk>

   891    \<Longrightarrow> cfd2sfd (Execve p f fds # s) p' fd' = cfd2sfd s p' fd'"

   892 apply (frule vd_cons, frule vt_grant_os)

   893 apply (frule proc_fd_in_fds, simp)

   894 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   895 apply (frule_tac cf2sfile_other', simp+)

   896 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   897 apply (case_tac "p' = p", simp)

   898 apply (auto split:option.splits if_splits)[1]

   899 apply (simp)

   900 apply (auto split:option.splits if_splits)[1]

   901 done

   902 

   903 lemma cfd2sfd_kill:

   904   "\<lbrakk>valid (Kill p p'' # s); file_of_proc_fd (Kill p p'' # s) p' fd' = Some f'\<rbrakk>

   905    \<Longrightarrow> cfd2sfd (Kill p p'' # s) p' fd' = cfd2sfd s p' fd'"

   906 apply (frule vd_cons, frule vt_grant_os)

   907 apply (frule proc_fd_in_fds, simp)

   908 apply (frule proc_fd_in_procs, simp)

   909 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   910 apply (frule_tac cf2sfile_other', simp+)

   911 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   912 apply (auto split:option.splits if_splits)

   913 done

   914 

   915 lemma cfd2sfd_exit:

   916   "\<lbrakk>valid (Exit p # s); file_of_proc_fd (Exit p # s) p' fd' = Some f'\<rbrakk>

   917    \<Longrightarrow> cfd2sfd (Exit p # s) p' fd' = cfd2sfd s p' fd'"

   918 apply (frule vd_cons, frule vt_grant_os)

   919 apply (frule proc_fd_in_fds, simp)

   920 apply (frule proc_fd_in_procs, simp)

   921 apply (frule file_of_proc_fd_in_curf, simp, simp add:current_files_simps)

   922 apply (frule_tac cf2sfile_other', simp+)

   923 apply (simp add:cfd2sfd_def sectxt_of_obj_simps)

   924 apply (auto split:option.splits if_splits)

   925 done

   926 

   927 lemma cfd2sfd_other:

   928   "\<lbrakk>valid (e # s); file_of_proc_fd (e # s) p' fd' = Some f';

   929     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

   930     \<forall> p p'' fds shms. e \<noteq> Clone p p'' fds shms\<rbrakk>

   931    \<Longrightarrow> cfd2sfd (e # s) p' fd' = cfd2sfd s p' fd'"

   932 apply (frule vd_cons, frule vt_grant_os)

   933 apply (frule proc_fd_in_fds, simp)

   934 apply (frule proc_fd_in_procs, simp)

   935 apply (frule file_of_proc_fd_in_curf, simp)

   936 apply (case_tac e)

   937 apply (auto intro!:cfd2sfd_execve cfd2sfd_closefd cfd2sfd_kill cfd2sfd_exit)

   938 apply (auto simp:cfd2sfd_def sectxt_of_obj_simps current_files_simps cf2sfile_simps split:option.splits)

   939 apply (auto dest!:current_has_sec' dest:file_of_proc_fd_in_curf proc_fd_in_fds)

   940 done

   941 

   942 lemmas cfd2sfd_simps = cfd2sfd_open cfd2sfd_clone cfd2sfd_other

   943 

   944 (********** cpfd2sfds simpset **********)

   945 

   946 lemma current_filefd_has_flags:

   947   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists> flags. flags_of_proc_fd s p fd = Some flags"

   948 apply (induct s arbitrary:p)

   949 apply (simp only:flags_of_proc_fd.simps file_of_proc_fd.simps init_filefd_prop4)

   950 apply (frule vd_cons, frule vt_grant_os, case_tac a)

   951 apply (auto split:if_splits option.splits dest:proc_fd_in_fds)

   952 done

   953 

   954 lemma current_filefd_has_flags':

   955   "\<lbrakk>flags_of_proc_fd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   956 apply (case_tac "file_of_proc_fd s p fd")

   957 apply (simp, drule current_filefd_has_flags, simp+)

   958 done

   959 

   960 lemma current_file_has_sfile':

   961   "\<lbrakk>cf2sfile s f = None; valid s\<rbrakk> \<Longrightarrow> f \<notin> current_files s"

   962 by (rule notI, drule current_file_has_sfile, simp+)

   963 

   964 lemma current_filefd_has_sfd:

   965   "\<lbrakk>file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> \<exists>sfd. cfd2sfd s p fd = Some sfd"

   966 by (auto simp:cfd2sfd_def split:option.splits dest!:current_has_sec' current_file_has_sfile' 

   967          dest:file_of_proc_fd_in_curf proc_fd_in_fds current_filefd_has_flags)

   968 

   969 lemma current_filefd_has_sfd':

   970   "\<lbrakk>cfd2sfd s p fd = None; valid s\<rbrakk> \<Longrightarrow> file_of_proc_fd s p fd = None"

   971 by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd)

   972 

   973 lemma cpfd2sfds_open1:

   974   "valid (Open p f flags fd opt # s) \<Longrightarrow>

   975    cpfd2sfds (Open p f flags fd opt # s) p = (

   976     case (cfd2sfd (Open p f flags fd opt # s) p fd) of

   977         Some sfd \<Rightarrow> (cpfd2sfds s p) \<union> {sfd}

   978       | _ \<Rightarrow> cpfd2sfds s p)"

   979 apply (frule vd_cons, frule vt_grant_os)

   980 apply (split option.splits)

   981 apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp)

   982 apply (rule allI, rule impI)

   983 apply (rule set_eqI, rule iffI)

   984 apply (case_tac "x = a", simp)

   985 unfolding cpfd2sfds_def

   986 apply (erule CollectE, (erule conjE|erule bexE)+)

   987 apply (simp add:proc_file_fds_def split:if_splits)

   988 apply (erule exE, rule_tac x = fda in exI)

   989 apply (simp add:cfd2sfd_open2)

   990 apply (case_tac "x = a", simp add:proc_file_fds_def)

   991 apply (rule_tac x = fd in exI, simp+)

   992 apply (erule conjE|erule bexE)+

   993 apply (rule_tac x = fda in bexI)

   994 apply (simp add:proc_file_fds_def, erule exE)

   995 apply (simp add:cfd2sfd_open2)

   996 apply (simp add:proc_file_fds_def)

   997 done

   998 

   999 lemma cpfd2sfds_open1':

  1000   "valid (Open p f flags fd opt # s) \<Longrightarrow>

  1001    cpfd2sfds (Open p f flags fd opt # s) p = (

  1002     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

  1003         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

  1004       | _ \<Rightarrow> cpfd2sfds s p)"

  1005 apply (frule cfd2sfd_open1)

  1006 apply (auto dest:cpfd2sfds_open1 split:option.splits)

  1007 done

  1008 

  1009 lemma cpfd2sfds_open2:

  1010   "\<lbrakk>valid (Open p f flags fd opt # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'"

  1011 apply (frule vt_grant_os, frule vd_cons)

  1012 unfolding cpfd2sfds_def

  1013 apply (rule set_eqI, rule iffI)

  1014 apply (simp add:proc_file_fds_def)

  1015 apply (erule exE|erule conjE)+

  1016 apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits)

  1017 apply (rule_tac x = fda in exI, simp)

  1018 apply (simp add:proc_file_fds_def)

  1019 apply (erule exE|erule conjE)+

  1020 apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2)

  1021 done

  1022 

  1023 lemma cpfd2sfds_open:

  1024   "valid (Open p f flags fd opt # s)

  1025    \<Longrightarrow> cpfd2sfds (Open p f flags fd opt # s) = (cpfd2sfds s) (p := (

  1026     case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of

  1027         (Some sec, Some sf) \<Rightarrow> (cpfd2sfds s p) \<union> {(sec, flags, sf)}

  1028       | _ \<Rightarrow> cpfd2sfds s p))"

  1029 apply (rule ext)

  1030 apply (case_tac "x \<noteq> p")

  1031 apply (simp add:cpfd2sfds_open2)

  1032 apply (simp add:cpfd2sfds_open1')

  1033 done

  1034 

  1035 lemma cpfd2sfds_execve:

  1036   "valid (Execve p f fds # s) 

  1037    \<Longrightarrow> cpfd2sfds (Execve p f fds # s) = (cpfd2sfds s) (p := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"

  1038 apply (frule vd_cons, frule vt_grant_os)

  1039 apply (rule ext)

  1040 apply (rule set_eqI, rule iffI)

  1041 unfolding cpfd2sfds_def proc_file_fds_def

  1042 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1043 apply (simp split:if_splits)

  1044 apply (frule_tac p' = p and fd' = fd in cfd2sfd_other, simp+)

  1045 apply (rule_tac x = fd in bexI, simp+)

  1046 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1047 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1048 apply (rule_tac x = fd in exI, simp)

  1049 apply (simp split:if_splits)

  1050 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1051 apply (rule_tac x = fd in exI, simp)

  1052 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1053 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1054 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1055 apply (rule_tac x = fd in exI, simp)

  1056 apply (frule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1057 done

  1058 

  1059 lemma cpfd2sfds_clone:

  1060   "valid (Clone p p' fds shms # s) 

  1061    \<Longrightarrow> cpfd2sfds (Clone p p' fds shms # s) = (cpfd2sfds s) (p' := {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd})"

  1062 apply (frule vd_cons, frule vt_grant_os)

  1063 apply (rule ext)

  1064 apply (rule set_eqI, rule iffI)

  1065 unfolding cpfd2sfds_def proc_file_fds_def

  1066 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1067 apply (simp split:if_splits)

  1068 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

  1069 apply (rule_tac x = fd in bexI, simp+)

  1070 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1071 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

  1072 apply (rule_tac x = fd in exI, simp)

  1073 apply (simp split:if_splits)

  1074 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1075 apply (rule_tac x = fd in exI, simp)

  1076 apply (frule_tac p'' = p' and fd' = fd in cfd2sfd_clone, simp+)

  1077 apply (simp add:cpfd2sfds_def proc_file_fds_def)

  1078 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1079 apply (rule_tac x = fd in exI, simp)

  1080 apply (frule_tac p'' = x and fd' = fd in cfd2sfd_clone, simp+)

  1081 done

  1082 

  1083 lemma cpfd2sfds_other:

  1084   "\<lbrakk>valid (e # s);

  1085     \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;

  1086     \<forall> p f fds. e \<noteq> Execve p f fds;

  1087     \<forall> p p'. e \<noteq> Kill p p';

  1088     \<forall> p. e \<noteq> Exit p;

  1089     \<forall> p fd. e \<noteq> CloseFd p fd;

  1090     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms\<rbrakk> \<Longrightarrow> cpfd2sfds (e # s) = cpfd2sfds s"

  1091 apply (frule vd_cons, frule vt_grant_os)

  1092 apply (rule ext)

  1093 unfolding cpfd2sfds_def proc_file_fds_def

  1094 apply (case_tac e)

  1095 using cfd2sfd_other

  1096 by auto

  1097 

  1098 lemma cpfd2sfds_kill:

  1099   "valid (Kill p p' # s) \<Longrightarrow> cpfd2sfds (Kill p p' # s) = (cpfd2sfds s) (p' := {})"

  1100 apply (frule vd_cons, frule vt_grant_os)

  1101 apply (rule ext, rule set_eqI)

  1102 unfolding cpfd2sfds_def proc_file_fds_def

  1103 apply (rule iffI)

  1104 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1105 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1106 apply (rule_tac x = fd in exI, simp)

  1107 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1108 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1109 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1110 apply (rule_tac x = fd in exI, simp)

  1111 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1112 done

  1113 

  1114 lemma cpfd2sfds_exit:

  1115   "valid (Exit p # s) \<Longrightarrow> cpfd2sfds (Exit p # s) = (cpfd2sfds s) (p := {})"

  1116 apply (frule vd_cons, frule vt_grant_os)

  1117 apply (rule ext, rule set_eqI)

  1118 unfolding cpfd2sfds_def proc_file_fds_def

  1119 apply (rule iffI)

  1120 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1121 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1122 apply (rule_tac x = fd in exI, simp)

  1123 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1124 apply (simp split:if_splits add: cpfd2sfds_def proc_file_fds_def)

  1125 apply (erule CollectE| erule bexE| erule conjE| erule exE| rule conjI)+

  1126 apply (rule_tac x = fd in exI, simp)

  1127 apply (drule_tac p' = x and fd' = fd in cfd2sfd_other, simp+)

  1128 done

  1129 

  1130 lemma cpfd2sfds_closefd:

  1131   "valid (CloseFd p fd # s) \<Longrightarrow> cpfd2sfds (CloseFd p fd # s) = (cpfd2sfds s) (p := 

  1132      if (fd \<in> proc_file_fds s p)

  1133      then (case (cfd2sfd s p fd) of 

  1134              Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd)

  1135                           then cpfd2sfds s p else cpfd2sfds s p - {sfd})