1
+ − 1
theory Proc_fd_of_file_prop
+ − 2
imports Main Flask Flask_type Valid_prop Current_files_prop
+ − 3
begin
+ − 4
+ − 5
context flask begin
+ − 6
+ − 7
lemma proc_fd_in_procs: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> p \<in> current_procs \<tau>"
+ − 8
apply (induct \<tau> arbitrary: f) defer
+ − 9
apply (frule vd_cons, frule vt_grant_os, case_tac a)
+ − 10
apply (auto simp:file_of_proc_fd.simps current_procs.simps os_grant.simps split:if_splits option.splits)
+ − 11
by (drule init_filefd_valid, simp)
+ − 12
+ − 13
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"
+ − 14
apply (induct \<tau>)
+ − 15
apply (simp add:file_of_proc_fd.simps current_proc_fds.simps)
+ − 16
apply (clarify, drule init_filefd_valid, simp)
+ − 17
apply (clarify, frule vd_cons, frule vt_grant_os, case_tac a)
+ − 18
apply (auto simp:file_of_proc_fd.simps current_proc_fds.simps split:if_splits option.splits t_sock_addr.splits)
+ − 19
done
+ − 20
+ − 21
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"
+ − 22
by (rule proc_fd_in_fds_aux[rule_format], simp+)
+ − 23
+ − 24
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>"
+ − 25
by (auto simp:proc_fd_of_file_def intro:file_of_pfd_in_current)
+ − 26
+ − 27
lemma proc_fd_file_in_cur': "\<lbrakk>proc_fd_of_file \<tau> f \<noteq> {}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+ − 28
by (auto simp:proc_fd_file_in_cur)
+ − 29
+ − 30
lemma proc_fd_file_in_cur'': "\<lbrakk>proc_fd_of_file \<tau> f = {(p,fd)}; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
+ − 31
by (auto simp:proc_fd_file_in_cur')
+ − 32
+ − 33
lemma procfd_of_file_imp_fpfd: "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd = Some f"
+ − 34
by (auto simp:proc_fd_of_file_def)
+ − 35
+ − 36
lemma procfd_of_file_imp_fpfd': "proc_fd_of_file \<tau> f = {(p, fd)} \<Longrightarrow> file_of_proc_fd \<tau> p fd \<noteq> None"
+ − 37
by (auto simp:proc_fd_of_file_def)
+ − 38
+ − 39
lemma procfd_of_file_eq_fpfd'': "(p, fd) \<in> proc_fd_of_file \<tau> f = (file_of_proc_fd \<tau> p fd = Some f)"
+ − 40
by (auto simp:proc_fd_of_file_def)
+ − 41
+ − 42
lemma procfd_of_file_non_empty: "file_of_proc_fd \<tau> p fd = Some f \<Longrightarrow> proc_fd_of_file \<tau> f \<noteq> {}"
+ − 43
by (auto simp:proc_fd_of_file_def)
+ − 44
+ − 45
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>"
+ − 46
by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')
+ − 47
+ − 48
+ − 49
(******************* rebuild proc_fd_of_file simpset ***********************)
+ − 50
(*
+ − 51
lemma proc_fd_of_file_open: "Open p f flags fd iopt # valid \<tau> \<Longrightarrow>
+ − 52
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')"
+ − 53
apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)
+ − 54
apply (frule vd_cons, drule vt_grant_os, case_tac iopt)
+ − 55
apply (drule proc_fd_in_fds, simp, simp add:os_grant.simps nfd_notin_curfd)+
+ − 56
done
+ − 57
+ − 58
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) "
+ − 59
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps split:if_splits)
+ − 60
+ − 61
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>
+ − 62
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)"
+ − 63
apply (frule vt_grant_os, frule vd_cons)
+ − 64
apply (case_tac "f\<^isub>3 \<preceq> f")
+ − 65
apply (subgoal_tac "f \<notin> current_files \<tau>") prefer 2 apply (rule notI)
+ − 66
apply (clarsimp simp:os_grant.simps, drule_tac f = f\<^isub>3 and f' = f in ancenf_in_current, simp, simp, simp)
+ − 67
apply (auto simp add:proc_fd_of_file_def)[1]
+ − 68
+ − 69
apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+ − 70
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)
+ − 71
apply (drule file_of_pfd_in_current, simp+)
+ − 72
apply (simp add:file_of_proc_fd.simps)
+ − 73
apply (rule conjI, rule impI, simp add:file_renaming_prop5')
+ − 74
apply (rule impI, simp add:file_before_rename_def)
+ − 75
+ − 76
apply (simp add:proc_fd_of_file_def split:if_splits)
+ − 77
apply auto
+ − 78
apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+ − 79
apply (drule_tac f\<^isub>3 = f\<^isub>3 and f\<^isub>2 = f\<^isub>2 and f = aa in file_renaming_prop1, simp)
+ − 80
apply (simp add:current_files_simps)
+ − 81
apply (erule exE| erule conjE)+
+ − 82
apply (simp add:file_of_proc_fd.simps split:option.splits if_splits)
+ − 83
apply (drule_tac f = f\<^isub>1 in rename_renaming_decom', simp+)
+ − 84
apply (simp add:file_after_rename_def)
+ − 85
done
+ − 86
+ − 87
+ − 88
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}"
+ − 89
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+ − 90
+ − 91
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'}"
+ − 92
by (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+ − 93
+ − 94
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}"
+ − 95
apply (auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+ − 96
apply (frule vd_cons, drule vt_grant_os)
+ − 97
apply (drule proc_fd_in_procs, (simp add:os_grant.simps np_notin_curp)+)
+ − 98
done
+ − 99
+ − 100
lemma proc_fd_of_file_other: "\<lbrakk>e # valid \<tau>;
+ − 101
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
+ − 102
\<forall> p fd. e \<noteq> CloseFd p fd;
+ − 103
\<forall> p f f'. e \<noteq> Rename p f f';
+ − 104
\<forall> p p'. e \<noteq> Kill p p';
+ − 105
\<forall> p. e \<noteq> Exit p;
+ − 106
\<forall> p p'. e \<noteq> Clone p p'\<rbrakk> \<Longrightarrow> proc_fd_of_file (e # \<tau>) f = proc_fd_of_file \<tau> f"
+ − 107
apply (case_tac e, auto simp:proc_fd_of_file_def file_of_proc_fd.simps)
+ − 108
done
+ − 109
+ − 110
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
+ − 111
*)
+ − 112
end
+ − 113
+ − 114
+ − 115
end