1
+ − 1
theory Finite_current
72
+ − 2
imports Main Valid_prop Flask Flask_type Proc_fd_of_file_prop
1
+ − 3
begin
+ − 4
+ − 5
context flask begin
+ − 6
+ − 7
lemma finite_cf: "valid \<tau> \<Longrightarrow> finite (current_files \<tau>)"
+ − 8
apply (induct \<tau>)
+ − 9
apply (simp add:current_files_def inum_of_file.simps)
+ − 10
apply (rule_tac B = "init_files" in finite_subset)
+ − 11
apply (clarsimp dest!:inof_has_file_tag, simp add:init_finite_sets)
+ − 12
+ − 13
apply (frule vt_grant_os, frule vd_cons, simp, case_tac a)
+ − 14
+ − 15
apply (auto simp:current_files_def os_grant.simps inum_of_file.simps split:if_splits option.splits)
+ − 16
apply (rule_tac B = "insert list {f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 17
apply (rule_tac B = "{f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 18
apply (rule_tac B = "{f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 19
apply (rule_tac B = "{f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 20
apply (rule_tac B = "insert list {f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 21
apply (rule_tac B = "insert list2 {f. \<exists>i. inum_of_file \<tau> f = Some i}" in finite_subset, clarsimp, simp)
+ − 22
done
+ − 23
+ − 24
lemma finite_cp: "finite (current_procs \<tau>)"
+ − 25
apply (induct \<tau>)
+ − 26
apply (simp add:current_procs.simps init_finite_sets)
+ − 27
apply (case_tac a, auto simp:current_procs.simps)
+ − 28
done
+ − 29
+ − 30
lemma finite_cfd: "valid \<tau> \<Longrightarrow> finite (current_proc_fds \<tau> p)"
+ − 31
apply (induct \<tau> arbitrary:p)
+ − 32
apply (simp add:current_proc_fds.simps init_finite_sets)
+ − 33
apply (frule vd_cons, frule vt_grant_os, case_tac a, auto simp:current_proc_fds.simps)
72
+ − 34
apply (erule finite_subset)
+ − 35
apply (frule_tac s = \<tau> and p = nat in file_fds_subset_pfds)
+ − 36
apply (erule finite_subset, simp)
+ − 37
apply (erule finite_subset)
+ − 38
apply (frule_tac s = \<tau> and p = nat1 in file_fds_subset_pfds)
+ − 39
apply (erule finite_subset, simp)
+ − 40
done
1
+ − 41
+ − 42
lemma finite_pair: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> A \<and> y \<in> B}"
+ − 43
by auto
+ − 44
+ − 45
lemma finite_UN_I': "\<lbrakk>finite X; \<forall> x. x \<in> X \<longrightarrow> finite (f x)\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> X \<and> y \<in> f x}"
+ − 46
apply (frule_tac B = f in finite_UN_I, simp)
+ − 47
apply (drule_tac finite_pair, simp)
+ − 48
apply (rule_tac B = "{(x, y). x \<in> X \<and> y \<in> (\<Union>a\<in>X. f a)}" in finite_subset, auto)
+ − 49
done
+ − 50
+ − 51
lemma finite_init_netobjs: "finite init_sockets"
+ − 52
apply (subgoal_tac "finite {(p, fd). p \<in> init_procs \<and> fd \<in> init_fds_of_proc p}")
+ − 53
apply (rule_tac B = "{(p, fd). p \<in> init_procs \<and> fd \<in> init_fds_of_proc p}" in finite_subset)
+ − 54
apply (clarsimp dest!:init_socket_has_inode, simp)
+ − 55
using init_finite_sets finite_UN_I'
+ − 56
by (metis Collect_mem_eq SetCompr_Sigma_eq internal_split_def)
+ − 57
+ − 58
lemma finite_cn_aux: "valid \<tau> \<Longrightarrow> finite {s. \<exists>i. inum_of_socket \<tau> s = Some i}"
+ − 59
apply (induct \<tau>)
+ − 60
apply (rule_tac B = "init_sockets" in finite_subset)
+ − 61
apply (clarsimp simp:inum_of_socket.simps dest!:inos_has_sock_tag, simp add:finite_init_netobjs)
+ − 62
+ − 63
apply (frule vd_cons, frule vt_grant_os, simp, case_tac a)
+ − 64
apply (auto split:option.splits if_splits)
+ − 65
apply (rule_tac B = "{s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp split:if_splits, simp)
+ − 66
apply (rule_tac B = "{s. \<exists>i. inum_of_socket \<tau> s = Some i} \<union> {(p, fd). \<exists> i. inum_of_socket \<tau> (nat1, fd) = Some i \<and> p = nat2 \<and> fd \<in> set1}" in finite_subset, clarsimp split:if_splits)
+ − 67
apply (simp only:finite_Un, rule conjI, simp)
+ − 68
apply (rule_tac B = "{(p, fd). \<exists> i. inum_of_socket \<tau> (nat1, fd) = Some i \<and> p = nat2}" in finite_subset, clarsimp)
+ − 69
apply (drule_tac h = "\<lambda> (p, fd). if (p = nat1) then (nat2, fd) else (p, fd)" in finite_imageI)
+ − 70
apply (rule_tac B = "((\<lambda>(p, fd). if p = nat1 then (nat2, fd) else (p, fd)) ` {a. \<exists>i. inum_of_socket \<tau> a = Some i})" in finite_subset)
+ − 71
apply (rule subsetI,erule CollectE, case_tac x, simp, (erule exE|erule conjE)+)
+ − 72
unfolding image_def
+ − 73
apply (rule CollectI, rule_tac x = "(nat1, b)" in bexI, simp+)
+ − 74
apply (rule_tac B = "{s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp split:if_splits, simp)+
+ − 75
apply (rule_tac B = "insert (nat1, nat2) {s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp, simp)
+ − 76
apply (rule_tac B = "insert (nat1, nat4) {s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp, simp)
+ − 77
done
+ − 78
+ − 79
lemma finite_cn: "valid \<tau> \<Longrightarrow> finite (current_sockets \<tau>)"
+ − 80
apply (simp add:current_sockets_def inum_of_socket.simps)
+ − 81
using finite_cn_aux[where \<tau> = \<tau>] by auto
+ − 82
+ − 83
lemma finite_ch: "finite (current_shms \<tau>)"
+ − 84
apply (induct \<tau>) defer
+ − 85
apply (case_tac a, auto simp:current_shms.simps init_finite_sets)
+ − 86
done
+ − 87
+ − 88
lemma finite_cm: "finite (current_msgqs \<tau>)"
+ − 89
apply (induct \<tau>) defer
+ − 90
apply (case_tac a, auto simp: init_finite_sets)
+ − 91
done
+ − 92
+ − 93
+ − 94
lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"
+ − 95
apply (drule_tac h = f in finite_imageI)
+ − 96
apply (clarsimp simp only:image_def)
+ − 97
apply (rule_tac f = Some in finite_imageD)
+ − 98
apply (rule_tac B = "{y. \<exists>x. (\<exists>y. f x = Some y) \<and> y = f x}" in finite_subset)
+ − 99
unfolding image_def
+ − 100
apply auto
+ − 101
done
+ − 102
+ − 103
lemma finite_ci: "valid \<tau> \<Longrightarrow> finite (current_inode_nums \<tau>)"
+ − 104
apply (simp add:current_inode_nums_def current_file_inums_def current_sock_inums_def)
+ − 105
apply (rule conjI, drule finite_cf, simp add:current_files_def, erule finite_option)
+ − 106
using finite_cn[where \<tau> = \<tau>]
+ − 107
apply (simp add:current_sockets_def, drule_tac finite_option, simp)
+ − 108
done
+ − 109
+ − 110
end
+ − 111
+ − 112
end
+ − 113
+ − 114