(*<*)

theory Co2sobj_prop

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

begin

(*<*)

ML {*

fun print_ss ss =

let

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

in

simps

end

*}

context tainting_s begin

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

lemma cm2smsg_other: 

  "\<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> 

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

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

unfolding cm2smsg_def

apply (case_tac e)

apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted 

           split:t_object.splits option.splits if_splits 

            dest:not_deleted_init_msg  dest!:current_has_sec')

done

lemma cm2smsg_sendmsg:

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

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

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

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

           | _ \<Rightarrow> None)

     else cm2smsg s q' m') "

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

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits

  dest:not_deleted_init_msg  dest!:current_has_sec')

done

lemma cm2smsg_recvmsg1:

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

apply (frule vd_cons, frule vt_grant_os, rule ext)

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits)

done

lemma cm2smsg_recvmsg2:

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

apply (frule vd_cons, frule vt_grant_os)

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits)

done

lemma cm2smsg_recvmsg1':

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

apply (frule vd_cons, frule vt_grant_os, rule ext)

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits)

done

lemma cm2smsg_recvmsg2':

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

apply (frule vd_cons, frule vt_grant_os)

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits)

done

lemma cm2smsg_removemsgq:

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

apply (frule vd_cons, frule vt_grant_os, rule ext)

apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps 

  split:if_splits option.splits)

done

lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'

  cm2smsg_removemsgq cm2smsg_other

lemma init_cm2smsg_has_smsg:

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

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

lemma hd_set_prop1:

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

by (case_tac l, auto)

lemma tl_set_prop1:

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

by (case_tac l, auto)

lemma current_has_smsg:

  "\<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"

apply (induct s)

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

apply (frule vt_grant_os, frule vd_cons, case_tac a)

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

  dest!:current_has_sec' hd_set_prop1 dest:not_deleted_init_msg tl_set_prop1)

done 

lemma current_has_smsg':

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

by (auto dest:current_has_smsg)

lemma cqm2sms_has_sms_aux:

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

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

lemma current_has_sms:

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

apply (rule cqm2sms_has_sms_aux)

apply (auto dest:current_msg_has_sec)

done

lemma current_has_sms':

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

by (auto dest:current_has_sms)

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

lemma cqm2sms_other:

  "\<lbrakk>valid (e # s); \<forall> p m. e \<noteq> CreateMsgq p q; \<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> 

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

apply (rule ext, rule ext)

apply (induct_tac xa, simp)

apply (frule vt_grant_os, frule vd_cons, case_tac e)

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

done

lemma cqm2sms_createmsgq:

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

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

     else cqm2sms s q' ms')"

apply (rule ext, rule ext)

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

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

done

lemma cqm2sms_2:

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

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

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

     | _ \<Rightarrow> None)"

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

by (auto split:option.splits)

lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2

declare cqm2sms.simps [simp del]

lemma cqm2sms_prop1:

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

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

lemma cqm2sms_sendmsg1:

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

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

apply (frule vt_grant_os, frule vd_cons)

apply (frule cm2smsg_sendmsg)

apply (induct ms rule:rev_induct)

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

done

lemma cqm2sms_sendmsg2:

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

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

apply (frule vt_grant_os, frule vd_cons)

apply (frule cm2smsg_sendmsg)

apply (induct ms rule:rev_induct)

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

done

lemma cqm2sms_sendmsg3:

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

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

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

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

     | _ \<Rightarrow> None)"

apply (frule vt_grant_os, frule vd_cons)

apply (frule cm2smsg_sendmsg)

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

done

lemma cqm2sms_sendmsg:

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

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

     if (q' = q) 

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

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

           | _ \<Rightarrow> None)

     else cqm2sms s q' ms' )"

apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3)

done

lemma cqm2sms_recvmsg1:

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

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

apply (frule vt_grant_os, frule vd_cons)

apply (induct ms rule:rev_induct)

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

done

lemma cqm2sms_recvmsg2:

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

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

apply (frule vt_grant_os, frule vd_cons)

apply (induct ms rule:rev_induct)

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

done

lemma cqm2sms_recvmsg:

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

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

     if (q' = q) 

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

             Some sms \<Rightarrow> Some (tl sms)

           | _ \<Rightarrow> None)

     else cqm2sms s q' ms)"

apply (frule vt_grant_os, frule vd_cons)

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

     dest!:current_has_sms')

apply (case_tac "msgs_of_queue s q", simp)

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

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

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

done

lemma cqm2sms_removemsgq:

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

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

apply (frule vt_grant_os, frule vd_cons)

apply (induct ms rule:rev_induct)

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

done

lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg cqm2sms_removemsgq

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

lemma cq2smsgq_other: 

  "\<lbrakk>valid (e # s); \<forall> p q. e \<noteq> CreateMsgq p q; \<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> 

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

apply (frule cqm2sms_other, simp+)

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

apply (auto simp:cq2smsgq_def sectxt_of_obj_simps 

           split:t_object.splits option.splits if_splits 

            dest:not_deleted_init_msg) 

done

lemma cq2smsg_createmsgq:

  "valid (CreateMsgq p q # s)

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

     case (sectxt_of_obj s (O_proc p)) of

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

     | None     \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os)

apply (frule cqm2sms_createmsgq)

apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq 

  split:option.splits if_splits dest:not_deleted_init_msgq)

done

lemma cq2smsg_sendmsg:

  "valid (SendMsg p q m # s) 

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

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

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

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

     | _ \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os)

apply (rule ext)

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

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

  dest!:current_has_sms' current_has_sec')

done

lemma current_has_smsgq:

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

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

lemma current_has_smsgq':

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

by (auto dest:current_has_smsgq)

lemma cq2smsg_recvmsg:

  "valid (RecvMsg p q m # s) 

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

    case (cq2smsgq s q) of

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

    | _ \<Rightarrow> None)"

apply (frule vd_cons, frule vt_grant_os)

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

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

  dest!:current_has_sec' current_has_sms' current_has_smsgq')

done

lemma cq2smsg_removemsgq:

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

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

apply (frule vd_cons, frule vt_grant_os)

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

  dest!:current_has_sec' current_has_sms' current_has_smsgq')

done

lemmas cq2smsgq_simps = cq2smsgq_other cq2smsg_sendmsg cq2smsg_recvmsg cq2smsg_removemsgq

lemma sm_in_sqsms_init_aux:

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

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

apply (induct ms arbitrary:m sm sms)

by (auto split:if_splits option.splits)

lemma sm_in_sqsms_init:

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

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

by (simp add:sm_in_sqsms_init_aux)

lemma cqm2sms_prop0:

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

apply (induct ms arbitrary:m sm sms)

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

done

lemma sm_in_sqsms:

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

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

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

  case Nil

  thus ?case 

    by (simp add:cq2smsga_nil_prop cm2smsg_nil_prop init_cq2smsgq_def sm_in_sqsms_init 

           split:option.splits)

next

  case (Cons e s)

  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; 

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

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

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

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

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

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

(*

  from p1 have p1':

    "\<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;

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

    \<Longrightarrow> sm \<in> set "

*)

  show ?case using p2 p3 p4 p5 p6 vd os

    apply (case_tac e)

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

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

    apply (case_tac "q = nat2", simp)

    apply (drule cq2smsg_createmsgq, simp, simp)

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

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

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

    apply (simp add:cqm2sms_recvmsg)

    done

qed

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

lemma sroot_only:

  "cf2sfile s [] = Some sroot"

by (simp add:cf2sfile_def)

lemma not_file_is_dir:

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

by (auto simp:is_file_def current_files_def is_dir_def 

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

lemma not_dir_is_file:

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

by (auto simp:is_file_def current_files_def is_dir_def 

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

lemma is_file_or_dir:

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

by (auto dest:not_dir_is_file)

lemma current_file_has_sfile:

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

apply (induct f)

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

apply (frule parentf_in_current', simp, clarsimp)

apply (frule parentf_is_dir'', simp)

apply (frule is_file_or_dir, simp)

apply (auto dest!:current_has_sec'

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

done

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

where

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

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

where

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

lemma is_file_has_sfile:

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

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

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

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

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

apply (frule is_file_in_current)

apply (drule current_file_has_sfile, simp)

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

done

lemma is_file_has_sfile':

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

by (drule is_file_has_sfile, auto)

lemma is_dir_has_sfile:

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

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

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

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

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

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

apply (case_tac f, simp add:sroot_only)

apply (frule is_dir_in_current, frule is_dir_not_file)

apply (drule current_file_has_sfile, simp)

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

done

lemma is_dir_has_sdir':

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

apply (case_tac f)

apply (rule_tac x = sroot in exI)

apply (simp add:sroot_only)

apply (drule is_dir_has_sfile, auto)

done

lemma sroot_set:

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

apply (frule root_is_dir)

apply (drule is_dir_has_sec, simp)

apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps 

                 root_type_remains root_user_remains

           dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user'

           split:option.splits)

done

lemma cf2sfile_path_file:

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

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

     case (cf2sfile s pf) of

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

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

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

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

           | None \<Rightarrow> None)

     | _ \<Rightarrow> None)"

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

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

apply (frule sroot_set)

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

done

lemma cf2sfile_path_dir:

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

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

     case (cf2sfile s pf) of

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

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

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

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

           | None \<Rightarrow> None)

     | _ \<Rightarrow> None)"

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

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

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

apply (frule sroot_set)

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

done  

lemma cf2sfile_path:

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

     case (cf2sfile s pf) of

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

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

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

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

               | None \<Rightarrow> None)