4 

     4 

     5 context flask begin

     5 context flask begin

     6 

     6 

     7 lemma distinct_queue_msgs:

     7 lemma distinct_queue_msgs:

     8   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"

     8   "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"

    11 apply (frule vd_cons, frule vt_grant_os, case_tac a)

    10 apply (frule vd_cons, frule vt_grant_os, case_tac a)

    12 apply auto

    11 apply auto

    13 apply (case_tac "msgs_of_queue s q", simp+)

    12 apply (case_tac "msgs_of_queue s q", simp+)

    14 done

    13 done

    15 

    14