29 |
29 |
30 lemma finite_cfd: "valid \<tau> \<Longrightarrow> finite (current_proc_fds \<tau> p)" |
30 lemma finite_cfd: "valid \<tau> \<Longrightarrow> finite (current_proc_fds \<tau> p)" |
31 apply (induct \<tau> arbitrary:p) |
31 apply (induct \<tau> arbitrary:p) |
32 apply (simp add:current_proc_fds.simps init_finite_sets) |
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) |
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) |
34 apply (erule finite_subset) |
35 by (metis double_diff finite_Diff subset_refl) |
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 |
36 |
41 |
37 lemma finite_pair: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> A \<and> y \<in> B}" |
42 lemma finite_pair: "\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> finite {(x, y). x \<in> A \<and> y \<in> B}" |
38 by auto |
43 by auto |
39 |
44 |
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}" |
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}" |