|
1 theory Finite_current |
|
2 imports Main Valid_prop Flask Flask_type |
|
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) |
|
34 apply (metis double_diff equalityE finite_Diff) |
|
35 by (metis double_diff finite_Diff subset_refl) |
|
36 |
|
37 lemma finite_pair: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> A \<and> y \<in> B}" |
|
38 by auto |
|
39 |
|
40 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}" |
|
41 apply (frule_tac B = f in finite_UN_I, simp) |
|
42 apply (drule_tac finite_pair, simp) |
|
43 apply (rule_tac B = "{(x, y). x \<in> X \<and> y \<in> (\<Union>a\<in>X. f a)}" in finite_subset, auto) |
|
44 done |
|
45 |
|
46 lemma finite_init_netobjs: "finite init_sockets" |
|
47 apply (subgoal_tac "finite {(p, fd). p \<in> init_procs \<and> fd \<in> init_fds_of_proc p}") |
|
48 apply (rule_tac B = "{(p, fd). p \<in> init_procs \<and> fd \<in> init_fds_of_proc p}" in finite_subset) |
|
49 apply (clarsimp dest!:init_socket_has_inode, simp) |
|
50 using init_finite_sets finite_UN_I' |
|
51 by (metis Collect_mem_eq SetCompr_Sigma_eq internal_split_def) |
|
52 |
|
53 lemma finite_cn_aux: "valid \<tau> \<Longrightarrow> finite {s. \<exists>i. inum_of_socket \<tau> s = Some i}" |
|
54 apply (induct \<tau>) |
|
55 apply (rule_tac B = "init_sockets" in finite_subset) |
|
56 apply (clarsimp simp:inum_of_socket.simps dest!:inos_has_sock_tag, simp add:finite_init_netobjs) |
|
57 |
|
58 apply (frule vd_cons, frule vt_grant_os, simp, case_tac a) |
|
59 apply (auto split:option.splits if_splits) |
|
60 apply (rule_tac B = "{s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp split:if_splits, simp) |
|
61 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) |
|
62 apply (simp only:finite_Un, rule conjI, simp) |
|
63 apply (rule_tac B = "{(p, fd). \<exists> i. inum_of_socket \<tau> (nat1, fd) = Some i \<and> p = nat2}" in finite_subset, clarsimp) |
|
64 apply (drule_tac h = "\<lambda> (p, fd). if (p = nat1) then (nat2, fd) else (p, fd)" in finite_imageI) |
|
65 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) |
|
66 apply (rule subsetI,erule CollectE, case_tac x, simp, (erule exE|erule conjE)+) |
|
67 unfolding image_def |
|
68 apply (rule CollectI, rule_tac x = "(nat1, b)" in bexI, simp+) |
|
69 apply (rule_tac B = "{s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp split:if_splits, simp)+ |
|
70 apply (rule_tac B = "insert (nat1, nat2) {s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp, simp) |
|
71 apply (rule_tac B = "insert (nat1, nat4) {s. \<exists>i. inum_of_socket \<tau> s = Some i}" in finite_subset, clarsimp, simp) |
|
72 done |
|
73 |
|
74 lemma finite_cn: "valid \<tau> \<Longrightarrow> finite (current_sockets \<tau>)" |
|
75 apply (simp add:current_sockets_def inum_of_socket.simps) |
|
76 using finite_cn_aux[where \<tau> = \<tau>] by auto |
|
77 |
|
78 lemma finite_ch: "finite (current_shms \<tau>)" |
|
79 apply (induct \<tau>) defer |
|
80 apply (case_tac a, auto simp:current_shms.simps init_finite_sets) |
|
81 done |
|
82 |
|
83 lemma finite_cm: "finite (current_msgqs \<tau>)" |
|
84 apply (induct \<tau>) defer |
|
85 apply (case_tac a, auto simp: init_finite_sets) |
|
86 done |
|
87 |
|
88 |
|
89 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}" |
|
90 apply (drule_tac h = f in finite_imageI) |
|
91 apply (clarsimp simp only:image_def) |
|
92 apply (rule_tac f = Some in finite_imageD) |
|
93 apply (rule_tac B = "{y. \<exists>x. (\<exists>y. f x = Some y) \<and> y = f x}" in finite_subset) |
|
94 unfolding image_def |
|
95 apply auto |
|
96 done |
|
97 |
|
98 lemma finite_ci: "valid \<tau> \<Longrightarrow> finite (current_inode_nums \<tau>)" |
|
99 apply (simp add:current_inode_nums_def current_file_inums_def current_sock_inums_def) |
|
100 apply (rule conjI, drule finite_cf, simp add:current_files_def, erule finite_option) |
|
101 using finite_cn[where \<tau> = \<tau>] |
|
102 apply (simp add:current_sockets_def, drule_tac finite_option, simp) |
|
103 done |
|
104 |
|
105 end |
|
106 |
|
107 end |
|
108 |
|
109 |