equal
deleted
inserted
replaced
90 lemma finite_cm: "finite (current_msgqs \<tau>)" |
90 lemma finite_cm: "finite (current_msgqs \<tau>)" |
91 apply (induct \<tau>) defer |
91 apply (induct \<tau>) defer |
92 apply (case_tac a, auto simp: init_finite_sets) |
92 apply (case_tac a, auto simp: init_finite_sets) |
93 done |
93 done |
94 |
94 |
|
95 lemma maxium_queue: |
|
96 "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue" |
|
97 apply (induct s) |
|
98 apply (simp add:init_msgq_valid) |
|
99 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto) |
|
100 done |
95 |
101 |
96 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}" |
102 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}" |
97 apply (drule_tac h = f in finite_imageI) |
103 apply (drule_tac h = f in finite_imageI) |
98 apply (clarsimp simp only:image_def) |
104 apply (clarsimp simp only:image_def) |
99 apply (rule_tac f = Some in finite_imageD) |
105 apply (rule_tac f = Some in finite_imageD) |