theory Proc_fd_of_file_prop
imports Main Flask Flask_type Valid_prop Current_files_prop
begin

context flask begin

lemma proc_fd_in_procs: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk>  \<Longrightarrow> p \<in> current_procs \<tau>"
apply (induct \<tau> arbitrary: f) defer
apply (frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:file_of_proc_fd.simps current_procs.simps os_grant.simps split:if_splits option.splits)
by (drule init_filefd_valid, simp)

lemma proc_fd_in_fds_aux: "\<forall> p f. file_of_proc_fd \<tau> p fd = Some f \<and> valid \<tau> \<longrightarrow> fd \<in> current_proc_fds \<tau> p"
apply (induct \<tau>)
apply (simp add:file_of_proc_fd.simps current_proc_fds.simps)
apply (clarify, drule init_filefd_valid, simp)
apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
apply (auto simp:file_of_proc_fd.simps current_proc_fds.simps split:if_splits option.splits t_sock_addr.splits)
done

lemma proc_fd_in_fds: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds \<tau> p"
by (rule proc_fd_in_fds_aux[rule_format], simp+)

lemma proc_fd_file_in_cur: "\<lbrakk>(p, fd) \<in> proc_fd_of_file \<tau> f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current)

lemma proc_fd_file_in_cur': "\<lbrakk>proc_fd_of_file \<tau> f \<noteq> {}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (auto simp:proc_fd_file_in_cur)

lemma proc_fd_file_in_cur'': "\<lbrakk>proc_fd_of_file \<tau> f = {(p,fd)}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (auto simp:proc_fd_file_in_cur')

lemma procfd_of_file_imp_fpfd: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_imp_fpfd': "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd \<noteq> None"
by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_eq_fpfd'': "(p, fd) \<in> proc_fd_of_file \<tau> f = (file_of_proc_fd \<tau> p fd = Some f)"
by (auto simp:proc_fd_of_file_def)

lemma procfd_of_file_non_empty: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> proc_fd_of_file \<tau> f \<noteq> {}"
by (auto simp:proc_fd_of_file_def)

lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')


(******************* rebuild proc_fd_of_file simpset ***********************)
(*
lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow> 
  proc_fd_of_file (Open p f flags fd iopt # \<tau>) f' = (if (f' = f) then insert (p, fd) (proc_fd_of_file \<tau> f') else proc_fd_of_file \<tau> f')"
apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)
apply (frule vd_cons, drule vt_grant_os, case_tac iopt)
apply (drule proc_fd_in_fds, simp, simp add:os_grant.simps nfd_notin_curfd)+
done

lemma proc_fd_of_file_closefd: "proc_fd_of_file (CloseFd p fd # \<tau>) f = (if (file_of_proc_fd \<tau> p fd = Some f) then (proc_fd_of_file \<tau> f - {(p,fd)}) else proc_fd_of_file \<tau> f) "
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)

lemma proc_fd_of_file_rename: "\<lbrakk>Rename p f\<^isub>2 f\<^isub>3 # valid \<tau>; f \<in> current_files (Rename p f\<^isub>2 f\<^isub>3 # \<tau>)\<rbrakk> \<Longrightarrow> 
  proc_fd_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (if (f\<^isub>3 \<preceq> f) then proc_fd_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f) else proc_fd_of_file \<tau> f)"
apply (frule vt_grant_os, frule vd_cons)
apply (case_tac "f\<^isub>3 \<preceq> f")
apply (subgoal_tac "f \<notin> current_files \<tau>") prefer 2 apply (rule notI)
apply (clarsimp simp:os_grant.simps, drule_tac f = f\<^isub>3 and f' = f in ancenf_in_current, simp, simp, simp)
apply (auto simp add:proc_fd_of_file_def)[1]

apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>1 = aa and f\<^isub>2 = f\<^isub>2 in file_renaming_prop5, simp)
apply (drule file_of_pfd_in_current, simp+)
apply (simp add:file_of_proc_fd.simps)
apply (rule conjI, rule impI, simp add:file_renaming_prop5')
apply (rule impI, simp add:file_before_rename_def)

apply (simp add:proc_fd_of_file_def split:if_splits)
apply auto
apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>2 = f\<^isub>2 and f = aa in file_renaming_prop1, simp)
apply (simp add:current_files_simps)
apply (erule exE| erule conjE)+
apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
apply (drule_tac f = f\<^isub>1 in rename_renaming_decom', simp+)
apply (simp add:file_after_rename_def)
done


lemma proc_fd_of_file_kill: "proc_fd_of_file (Kill p\<^isub>1 p\<^isub>2 # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p\<^isub>2}"
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

lemma proc_fd_of_file_exit: "proc_fd_of_file (Exit p' # \<tau>) f = {(p, fd). (p, fd) \<in> proc_fd_of_file \<tau> f \<and> p \<noteq> p'}"
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)

lemma proc_fd_of_file_clone: "Clone p\<^isub>1 p\<^isub>2 # valid \<tau> \<Longrightarrow> proc_fd_of_file (Clone p\<^isub>1 p\<^isub>2 # \<tau>) f = proc_fd_of_file \<tau> f \<union> {(p\<^isub>2, fd)| fd. (p\<^isub>1, fd) \<in> proc_fd_of_file \<tau> f}" 
apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
apply (frule vd_cons, drule vt_grant_os)
apply (drule proc_fd_in_procs, (simp add:os_grant.simps np_notin_curp)+)
done

lemma proc_fd_of_file_other: "\<lbrakk>e # valid \<tau>;
                               \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
                               \<forall> p fd. e \<noteq> CloseFd p fd;
                               \<forall> p f f'. e \<noteq> Rename p f f';
                               \<forall> p p'. e \<noteq> Kill p p';
                               \<forall> p. e \<noteq> Exit p;
                               \<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> proc_fd_of_file (e # \<tau>) f = proc_fd_of_file \<tau> f"
apply (case_tac e, auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
done

lemmas proc_fd_of_file_simps = proc_fd_of_file_open proc_fd_of_file_closefd proc_fd_of_file_rename proc_fd_of_file_kill proc_fd_of_file_exit proc_fd_of_file_clone proc_fd_of_file_other
*)
end


end