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:

    95 lemma maxium_queue:

    96   "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"

    96   "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"

    99 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)

    98 apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)

   100 done

    99 done

   101 

   100 

   102 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"

   101 lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"

   103 apply (drule_tac h = f in finite_imageI)

   102 apply (drule_tac h = f in finite_imageI)