(*<*)

theory Current_files_prop

imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop

begin

(*<*)

context init begin

lemma current_files_ndef: "f \<notin> current_files \<tau> \<Longrightarrow> inum_of_file \<tau> f = None"

by (simp add:current_files_def)

(************** file_of_proc_fd vs proc_fd_of_file *****************)

lemma pfdof_simp1: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> (p, fd) \<in> proc_fd_of_file \<tau> f"

by (simp add:proc_fd_of_file_def)

lemma pfdof_simp2: "(p, fd) \<in> proc_fd_of_file \<tau> f \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"

by (simp add:proc_fd_of_file_def)

lemma pfdof_simp3: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> \<forall> p' fd'. (file_of_proc_fd \<tau> p' fd' = Some f \<longrightarrow> p = p' \<and> fd = fd')"

by (simp add:proc_fd_of_file_def, auto)

lemma pfdof_simp4: "\<lbrakk>file_of_proc_fd \<tau> p' fd' = Some f; proc_fd_of_file \<tau> f = {(p, fd)}\<rbrakk> \<Longrightarrow> p' = p \<and> fd' = fd"

by (drule pfdof_simp3, auto)

end

context flask begin

(***************** inode number lemmas *************************)

lemma iof's_im_in_cim: "inum_of_file \<tau> f = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"

by (auto simp add:current_inode_nums_def current_file_inums_def)

lemma ios's_im_in_cim: "inum_of_socket \<tau> s = Some im \<Longrightarrow> im \<in> current_inode_nums \<tau>"

by (case_tac s, auto simp add:current_inode_nums_def current_sock_inums_def)

lemma fim_noninter_sim_aux[rule_format]:

  "\<forall> f s. inum_of_file \<tau> f = Some im \<and> inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> False"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_file.simps inum_of_socket.simps)

apply (drule init_inum_sock_file_noninter, simp, simp)

apply ((rule allI|rule impI|erule conjE)+)

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

apply (auto simp:inum_of_file.simps inum_of_socket.simps split:if_splits option.splits

            dest:ios's_im_in_cim iof's_im_in_cim)

done

lemma fim_noninter_sim':"\<lbrakk>inum_of_file \<tau> f = Some im; inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"

by (auto intro:fim_noninter_sim_aux)

lemma fim_noninter_sim'':"\<lbrakk>inum_of_socket \<tau> s = Some im; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"

by (auto intro:fim_noninter_sim_aux)

lemma fim_noninter_sim: "valid \<tau> \<Longrightarrow> (current_file_inums \<tau>) \<inter> (current_sock_inums \<tau>) = {}"

by (auto simp:current_file_inums_def current_sock_inums_def intro:fim_noninter_sim_aux[rule_format])

(******************* file inum has inode tag ************************)

lemma finum_has_itag_aux[rule_format]: 

  "\<forall> f im. inum_of_file \<tau> f = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)

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

apply (auto simp add:inum_of_file.simps itag_of_inum.simps os_grant.simps current_files_def 

                dest:fim_noninter_sim'' split:option.splits if_splits t_socket_type.splits)

done

lemma finum_has_itag: "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"

by (auto dest:conjI[THEN finum_has_itag_aux])

(*********************** file inum is file itag *************************)

lemma finum_has_ftag_aux[rule_format]: 

  "\<forall> f tag. inum_of_file \<tau> f = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_file_dir_itag tag"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_inum_of_file_props)

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

apply (auto simp:inum_of_file.simps os_grant.simps current_files_def itag_of_inum.simps 

           split:if_splits option.splits t_socket_type.splits

            dest:ios's_im_in_cim iof's_im_in_cim)

done

lemma finum_has_ftag:

  "\<lbrakk>inum_of_file \<tau> f = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_file_dir_itag tag"

by (auto intro:finum_has_ftag_aux)

lemma finum_has_ftag': 

  "\<lbrakk>inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE \<or> itag_of_inum \<tau> im = Some Tag_DIR"

apply (frule finum_has_itag, simp, erule exE, drule finum_has_ftag, simp+)

apply (case_tac tag, auto)

done

(******************* sock inum has inode tag ************************)

lemma sinum_has_itag_aux[rule_format]: 

  "\<forall> s im. inum_of_socket \<tau> s = Some im \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> im \<noteq> None"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)

apply (drule init_inumos_prop4, clarsimp)

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

apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps 

                dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim

               split:option.splits if_splits t_socket_type.splits)

done

lemma sinum_has_itag: "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> tag. itag_of_inum \<tau> im = Some tag"

by (auto dest:conjI[THEN sinum_has_itag_aux])

(********************** socket inum is socket itag **********************)

lemma sinum_has_stag_aux[rule_format]: 

  "\<forall> s tag. inum_of_socket \<tau> s = Some im \<and> itag_of_inum \<tau> im = Some tag \<and> valid \<tau> \<longrightarrow> is_sock_itag tag"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_socket.simps itag_of_inum.simps)

apply (drule init_inumos_prop4, clarsimp)

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

apply (auto simp add:inum_of_socket.simps itag_of_inum.simps os_grant.simps 

                dest:fim_noninter_sim'' ios's_im_in_cim iof's_im_in_cim

               split:option.splits if_splits t_socket_type.splits)

done

lemma sinum_has_stag: "\<lbrakk>inum_of_socket \<tau> s = Some im; itag_of_inum \<tau> im = Some tag; valid \<tau>\<rbrakk> \<Longrightarrow> is_sock_itag tag"

by (auto dest:conjI[THEN sinum_has_stag_aux])

lemma sinum_has_stag': 

  "\<lbrakk>inum_of_socket \<tau> s = Some im; valid \<tau>\<rbrakk> 

   \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_UDP_SOCK \<or> itag_of_inum \<tau> im = Some Tag_TCP_SOCK"

apply (frule sinum_has_itag, simp, erule exE)

apply (drule sinum_has_stag, simp+, case_tac tag, simp+)

done

(************************************ 4 in 1 *************************************)

lemma file_leveling: "valid \<tau> \<longrightarrow> (

                        (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>

                        (\<forall> f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>

                        (\<forall> f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and>

                        (\<forall> f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False) )"

proof (induct \<tau>)

  case Nil 

  show ?case

    apply (auto simp:inum_of_file.simps files_hung_by_del.simps is_file_def itag_of_inum.simps parent_file_in_init split:option.splits t_inode_tag.splits)

    apply (drule init_files_hung_by_del_props, simp add:init_file_has_inum)

    apply (rule init_parent_file_has_inum, simp+)

    apply (rule init_file_has_no_son', simp+)

    apply (rule init_file_hung_has_no_son, simp+)

    done   

next

  case (Cons a \<tau>)  

  assume pre: "valid \<tau> \<longrightarrow>

  (\<forall> f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None) \<and>

  (\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None) \<and>

  (\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False) \<and> 

  (\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"

  show ?case

  proof 

    assume cons:"valid (a # \<tau>)"

    show "(\<forall>f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None) \<and>

          (\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None) \<and>

          (\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False) \<and>

          (\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> parent f' = Some f \<longrightarrow> False)"

    proof-

      have vt: "valid \<tau>" using cons by (auto dest:vd_cons)

      have os: "os_grant \<tau> a" using cons by (auto dest:vt_grant_os)  

      have fin: "\<forall>f. f \<in> files_hung_by_del \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" using vt pre by auto

      have pin: "\<forall>f pf im. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<longrightarrow> inum_of_file \<tau> pf \<noteq> None" 

        using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)

      have fns: "\<forall>f f' im. is_file \<tau> f \<and> parent f' = Some f \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> False"

        using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)

      have hns: "\<forall>f f' im. f \<in> files_hung_by_del \<tau> \<and> inum_of_file \<tau> f' = Some im \<and> parent f' = Some f \<longrightarrow> False" 

        using vt pre apply (erule_tac impE, simp) by ((erule_tac conjE)+, assumption)

      have ain: "\<forall>f' f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

      proof 

        fix f' 

        show " \<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

        proof (induct f')

          case Nil show ?case by (auto simp: no_junior_def)

        next

          case (Cons a f') 

          assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

          show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

          proof clarify

            fix f im

            assume h1: "f \<preceq> a # f'"

              and  h2: "inum_of_file \<tau> (a # f') = Some im"

            show "\<exists>y. inum_of_file \<tau> f = Some y"

            proof-

              have h3: "\<exists> y. inum_of_file \<tau> f' = Some y" 

              proof-

                have "parent (a # f') = Some f'" by simp

                hence "\<exists> y. inum_of_file \<tau> f' = Some y" using pin h2 by blast

                with h1 show ?thesis by simp

              qed

              from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)

              moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp

              moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y"  using h3 by simp

              moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 by simp

              ultimately show ?thesis by auto

            qed

          qed

        qed

      qed

      have fin': "\<And> f. f \<in> files_hung_by_del \<tau> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im" using fin by auto

      have pin': "\<And> f pf im. \<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"

        using pin by auto

      have fns': "\<And> f f' im. \<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False" using fns by auto

      have fns'': "\<And> f f' im im'. \<lbrakk>itag_of_inum \<tau> im = Some Tag_FILE; inum_of_file \<tau> f = Some im; parent f' = Some f; inum_of_file \<tau> f' = Some im'\<rbrakk> \<Longrightarrow> False"

        by (rule_tac f = f and f' = f' in fns', auto simp:is_file_def)

      have hns': "\<And> f f' im. \<lbrakk>f \<in> files_hung_by_del \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False" using hns by auto

      have ain': "\<And> f f' im. \<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'" using ain by auto

      have dns': "\<And> f f' im. \<lbrakk>dir_is_empty \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im\<rbrakk> \<Longrightarrow> False"

        apply (auto simp:dir_is_empty_def current_files_def is_dir_def split:option.splits)

        by (erule_tac x = f' in allE, simp add:noJ_Anc parent_is_ancen, drule parent_is_parent, simp+)

      have "\<forall> f. f \<in> files_hung_by_del (a # \<tau>) \<longrightarrow> inum_of_file (a # \<tau>) f \<noteq> None"

        apply (clarify, case_tac a) using os fin

        apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def 

                   split:if_splits option.splits)

        done

      moreover 

      have "\<forall>f pf im. parent f = Some pf \<and> inum_of_file (a # \<tau>) f = Some im \<longrightarrow> inum_of_file (a # \<tau>) pf \<noteq> None" 

        apply (clarify, case_tac a)

        using vt os pin'

        apply (auto simp:os_grant.simps current_files_def inum_of_file.simps split:if_splits option.splits)

        apply (drule_tac f = pf and f' = f in hns', simp, simp, simp)

        apply (drule_tac f = list and f' = f in fns', simp, simp, simp)

        apply (drule_tac f = list and f' = f in dns', simp, simp, simp)

        done

      moreover have "\<forall>f f' im. is_file (a # \<tau>) f \<and> parent f' = Some f \<and> inum_of_file (a # \<tau>) f' = Some im \<longrightarrow> False"

        apply (clarify, case_tac a)    

        using vt os fns''

        apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps 

                         is_file_def is_dir_def 

                    dest:ios's_im_in_cim iof's_im_in_cim

                   split:if_splits option.splits t_inode_tag.splits t_socket_type.splits)

        apply (drule_tac f = f' and pf = list in pin', simp, simp)

        apply (drule_tac f = f' and pf = list2 in pin', simp, simp)

        done

      moreover have "\<forall>f f' im. f \<in> files_hung_by_del (a # \<tau>) \<and> inum_of_file (a # \<tau>) f' = Some im \<and> 

                               parent f' = Some f \<longrightarrow> False"

        apply (clarify, case_tac a)     

        using vt os hns'

        apply (auto simp:os_grant.simps current_files_def inum_of_file.simps files_hung_by_del.simps 

                   split:if_splits option.splits t_sock_addr.splits)

        apply (drule fns', simp+)

        done

      ultimately show ?thesis by blast

    qed

  qed

qed

(**************** hung file in current ***********************)

lemma hung_file_has_inum:"\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"

by (drule file_leveling[rule_format], blast)

lemma hung_file_has_inum': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"

by (auto dest:hung_file_has_inum)

lemma hung_file_in_current: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (clarsimp simp add:current_files_def hung_file_has_inum')

lemma parentf_has_inum: "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> pf \<noteq> None"

by (drule file_leveling[rule_format], blast)

lemma parentf_has_inum': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> pf = Some im'"

by (auto dest:parentf_has_inum)

lemma parentf_in_current: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"

by (clarsimp simp add:current_files_def parentf_has_inum')

lemma parentf_in_current': "\<lbrakk>a # pf \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> pf \<in> current_files \<tau>"

apply (subgoal_tac "parent (a # pf) = Some pf")

by (erule parentf_in_current, simp+)

lemma ancenf_has_inum_aux: "\<forall> f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

proof (induct f')

  case Nil show ?case by (auto simp: no_junior_def)

next

  case (Cons a f') 

  assume pre:"\<forall>f im. f \<preceq> f' \<and> inum_of_file \<tau> f' = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

  show "\<forall>f im. f \<preceq> a # f' \<and> inum_of_file \<tau> (a # f') = Some im \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None"

  proof clarify

    fix f im

    assume h1: "f \<preceq> a # f'"

      and  h2: "inum_of_file \<tau> (a # f') = Some im"

      and  h3: "valid \<tau>"

    show "\<exists>y. inum_of_file \<tau> f = Some y"

    proof-

      have h4: "\<exists> y. inum_of_file \<tau> f' = Some y" 

      proof-

        have "parent (a # f') = Some f'" by simp

        hence "\<exists> y. inum_of_file \<tau> f' = Some y" using parentf_has_inum' h2 h3 by blast

        with h1 show ?thesis by simp

      qed

      from h1 have "f = a # f' \<or> f = f' \<or> f \<preceq> f'" by (induct f, auto simp:no_junior_def)

      moreover have "f = a # f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using h2 by simp

      moreover have "f = f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y"  using h4 by simp

      moreover have "f \<preceq> f' \<Longrightarrow> \<exists>y. inum_of_file \<tau> f = Some y" using pre h3 h4 by simp

      ultimately show ?thesis by auto

    qed

  qed

qed

lemma ancenf_has_inum: "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"

by (rule ancenf_has_inum_aux[rule_format], auto)

lemma ancenf_has_inum': "\<lbrakk>f \<preceq> f'; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im'. inum_of_file \<tau> f = Some im'"

by (auto dest:ancenf_has_inum)

lemma ancenf_in_current: "\<lbrakk>f \<preceq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (simp add:current_files_def, erule exE, simp add:ancenf_has_inum')

lemma file_has_no_son: "\<lbrakk>is_file \<tau> f; parent f' = Some f; inum_of_file \<tau> f' = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> False"

by (drule file_leveling[rule_format], blast)

lemma file_has_no_son': "\<lbrakk>is_file \<tau> f; parent f' = Some f; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> False"

by (simp add:current_files_def, erule exE, auto intro:file_has_no_son)

lemma hung_file_no_son: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; inum_of_file \<tau> f' = Some im; parent f' = Some f\<rbrakk> \<Longrightarrow> False"

by (drule file_leveling[rule_format], blast)

lemma hung_file_no_son': "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; parent f' = Some f\<rbrakk> \<Longrightarrow> False"

by (simp add:current_files_def, erule exE, auto intro:hung_file_no_son)

lemma hung_file_no_des_aux: "\<forall> f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> f' \<in> current_files \<tau> \<and> f \<preceq> f' \<and> f \<noteq> f' \<longrightarrow> False"

proof (induct f')

  case Nil 

  show ?case

    by (auto simp:files_hung_by_del.simps current_files_def inum_of_file.simps no_junior_def split:if_splits option.splits)

next

  case (Cons a pf)

  assume pre: "\<forall>f. f \<in> files_hung_by_del \<tau> \<and> valid \<tau> \<and> pf \<in> current_files \<tau> \<and> f \<preceq> pf \<and> f \<noteq> pf\<longrightarrow> False"

  show ?case

  proof clarify

    fix f

    assume h1: "f \<in> files_hung_by_del \<tau>"

      and  h2: "valid \<tau>"

      and  h3: "a # pf \<in> current_files \<tau>"

      and  h4: "f \<preceq> a # pf"

      and  h5: "f \<noteq> a # pf"

    have h6: "parent (a # pf) = Some pf" by simp

    with h2 h3 have h7: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)

    from h4 h5 have h8: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)

    show False

    proof (cases "f = pf")

      case True with h6 h2 h3 h1

      show False by (auto intro!:hung_file_no_son')

    next

      case False with pre h1 h2 h7 h8 

      show False by blast

    qed

  qed

qed

lemma hung_file_no_des: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>; f' \<in> current_files \<tau>; f \<preceq> f'; f \<noteq> f'\<rbrakk> \<Longrightarrow> False"

by (rule hung_file_no_des_aux[rule_format], blast)

lemma hung_file_is_leaf: "\<lbrakk>f \<in> files_hung_by_del \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f \<or> dir_is_empty \<tau> f"

apply (frule hung_file_has_inum', simp, erule exE)

apply (auto simp add:is_file_def dir_is_empty_def is_dir_def  dest:finum_has_itag finum_has_ftag split:option.splits if_splits t_inode_tag.splits)

by (simp add: noJ_Anc, auto dest:hung_file_no_des)

(************** file_of_proc_fd in current ********************)

lemma file_of_pfd_imp_inode_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> inum_of_file \<tau> f \<noteq> None" 

apply (induct \<tau>)

apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum)

apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def 

           split:if_splits option.splits)

apply (simp add:pfdof_simp3)+

apply (simp add:proc_fd_of_file_def)+  

done

lemma file_of_pfd_imp_inode': "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> inum_of_file \<tau> f \<noteq> None"

by (rule file_of_pfd_imp_inode_aux[rule_format], blast)

lemma file_of_pfd_imp_inode: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> \<exists> im. inum_of_file \<tau> f = Some im"

by (auto dest!:file_of_pfd_imp_inode')

lemma file_of_pfd_in_current: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"

by (auto dest!:file_of_pfd_imp_inode' simp:current_files_def)

(*************** file_of_proc_fd is file *********************)

lemma file_of_pfd_is_file_tag:

  "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>; inum_of_file \<tau> f = Some im\<rbrakk> \<Longrightarrow> itag_of_inum \<tau> im = Some Tag_FILE"

apply (induct \<tau> arbitrary:p, simp)

apply (drule init_filefd_prop5, simp add:is_init_file_def split:option.splits t_inode_tag.splits)

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

by (auto split:option.splits t_inode_tag.splits if_splits t_socket_type.splits 

          dest:file_of_pfd_imp_inode' iof's_im_in_cim

          simp:is_file_def is_dir_def dir_is_empty_def current_files_def)

lemma file_of_pfd_is_file:

  "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> is_file \<tau> f"

apply (frule file_of_pfd_imp_inode, simp, erule exE)

apply (drule file_of_pfd_is_file_tag, simp+)

by (simp add:is_file_def)

lemma file_of_pfd_is_file':

  "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; is_dir \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> False"

by (drule file_of_pfd_is_file, auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)

(************** parent file / ancestral file is dir *******************)

lemma parentf_is_dir_aux: "\<forall> f pf. parent f = Some pf \<and> inum_of_file \<tau> f = Some im \<and> inum_of_file \<tau> pf = Some ipm \<and> valid \<tau> \<longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"

apply (induct \<tau>)

apply (clarsimp simp:inum_of_file.simps itag_of_inum.simps init_parent_file_is_dir')

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

apply (auto simp:inum_of_file.simps itag_of_inum.simps os_grant.simps 

                 current_files_def is_dir_def is_file_def 

            dest: ios's_im_in_cim iof's_im_in_cim

           split:if_splits option.splits t_sock_addr.splits t_inode_tag.splits t_socket_type.splits)

apply (drule parentf_has_inum', simp, simp, simp)+

done

lemma parentf_has_dirtag: 

  "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; inum_of_file \<tau> pf = Some ipm; valid \<tau>\<rbrakk> 

   \<Longrightarrow> itag_of_inum \<tau> ipm = Some Tag_DIR"

by (auto intro:parentf_is_dir_aux[rule_format])

lemma parentf_is_dir': "\<lbrakk>parent f = Some pf; inum_of_file \<tau> f = Some im; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"

apply (frule parentf_has_inum', simp+, erule exE, simp add:is_dir_def split:t_inode_tag.splits option.splits)

by (auto dest:parentf_has_dirtag)

lemma parentf_is_dir: "\<lbrakk>parent f = Some pf; f \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> pf"

by (clarsimp simp:current_files_def parentf_is_dir')

lemma ancenf_is_dir_aux: "\<forall> f. f \<preceq> f' \<and> f \<noteq> f' \<and> f' \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"

proof (induct f')

  case Nil show ?case

    by (auto simp:current_files_def no_junior_def)

next 

  case (Cons a pf)

  assume pre: "\<forall>f. f \<preceq> pf \<and> f \<noteq> pf \<and> pf \<in> current_files \<tau> \<and> valid \<tau> \<longrightarrow> is_dir \<tau> f"

  show ?case

  proof clarify

    fix f

    assume h1: "f \<preceq> a # pf"

      and  h2: "f \<noteq> a # pf"

      and  h3: "a # pf \<in> current_files \<tau>"

      and  h4: "valid \<tau>"

    have h5: "parent (a # pf) = Some pf" by simp

    with h3 h4 have h6: "pf \<in> current_files \<tau>" by (drule_tac parentf_in_current, auto)

    from h1 h2 have h7: "f \<preceq> pf" by (erule_tac no_juniorE, case_tac zs, auto simp:no_junior_def)

    show "is_dir \<tau> f"

    proof (cases "f = pf")

      case True with h3 h4 h5 show "is_dir \<tau> f" by (drule_tac parentf_is_dir, auto)

    next

      case False with pre h6 h7 h4 show "is_dir \<tau> f" by blast

    qed

  qed

qed

lemma ancenf_is_dir: "\<lbrakk>f \<preceq> f'; f \<noteq> f'; f' \<in> current_files \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> is_dir \<tau> f"

by (auto intro:ancenf_is_dir_aux[rule_format])

(************* rebuild current_files simpset ***********************)

lemma current_files_nil: "current_files [] = init_files"

apply (simp add:current_files_def inum_of_file.simps)

by (auto dest:inof_has_file_tag init_file_has_inum)

lemma current_files_open: "current_files (Open p f flags fd (Some i) # \<tau>) = insert f (current_files \<tau>)"

by (auto simp add:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_open': "current_files (Open p f flags fd None # \<tau>) = current_files \<tau>"

by (simp add:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_closefd: "current_files (CloseFd p fd # \<tau>) = (

     case (file_of_proc_fd \<tau> p fd) of

       Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>))

                   then current_files \<tau> - {f}

                   else current_files \<tau>)

     | _      \<Rightarrow> current_files \<tau>                                  )"

by (auto simp:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_unlink: "current_files (UnLink p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then (current_files \<tau>) - {f} else current_files \<tau>)"

by (auto simp:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_rmdir: "current_files (Rmdir p f # \<tau>) = (if (proc_fd_of_file \<tau> f = {}) then current_files \<tau> - {f} else current_files \<tau>)"

by (auto simp:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_mkdir: "current_files (Mkdir p f ino # \<tau>) = insert f (current_files \<tau>)"

by (auto simp:current_files_def inum_of_file.simps split:option.splits)

lemma current_files_linkhard: 

  "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) \<Longrightarrow> current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = insert f\<^isub>2 (current_files \<tau>)"

apply (frule vt_grant_os, frule vd_cons)

by (auto simp:current_files_def inum_of_file.simps os_grant.simps split:option.splits)

(*

lemma rename_renaming_decom:

  "\<lbrakk>f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> f\<^isub>2 \<preceq> f"

apply (case_tac "f\<^isub>2 \<preceq> f", simp)

apply (simp add:file_after_rename_def split:if_splits)

by (frule vd_cons, frule vt_grant_os, auto simp:os_grant.simps dest!:ancenf_in_current)

lemma rename_renaming_decom':

  "\<lbrakk>\<not> f\<^isub>3 \<preceq> file_after_rename f\<^isub>2 f\<^isub>3 f; Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files \<tau>\<rbrakk> \<Longrightarrow> \<not> f\<^isub>2 \<preceq> f"

by (case_tac "f\<^isub>2 \<preceq> f", drule_tac f\<^isub>3 = f\<^isub>3 in file_renaming_prop1, simp+)

lemma current_files_rename: "Rename p f\<^isub>2 f\<^isub>3 # valid \<tau> \<Longrightarrow> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> current_files \<tau>}"

apply (frule vt_grant_os, frule vd_cons)

apply (auto simp:current_files_def inum_of_file.simps os_grant.simps split:if_splits option.splits)

apply (rule_tac x = x in exI, simp add:file_after_rename_def)

apply (frule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop1', drule_tac f\<^isub>2 = f\<^isub>2 in file_renaming_prop5')

apply (erule_tac x = "file_before_rename f\<^isub>2 f\<^isub>3 x" in allE, simp)

apply (rule_tac x = x in exI, simp add:file_after_rename_def)

apply (drule_tac a = f\<^isub>3 and b = f\<^isub>2 in no_junior_conf, simp, simp)

apply (drule_tac f = f\<^isub>3 and f' = f\<^isub>2 in ancenf_has_inum', simp, simp, simp)

apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom, simp, simp add:current_files_def, simp add:file_renaming_prop5)

apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)

apply (simp add:file_after_rename_def)

apply (drule_tac f\<^isub>2 = f\<^isub>2 in rename_renaming_decom', simp, simp add:current_files_def)

apply (simp add:file_after_rename_def)

done

*)

lemma current_files_other:

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

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