theory Invariants_AI

lemma sym_refs_bound_tcb_atD:
  "\<lbrakk>bound_tcb_at P t s; sym_refs (state_refs_of s)\<rbrakk>
    \<Longrightarrow> \<exists>ts ntfnptr.
        P ntfnptr \<and>
        obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and>
        state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and>
        (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr.
            obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s)" apply (drule bound_tcb_at_state_refs_ofD) apply (erule exE)+ apply (rule_tac x=ts in exI) apply (rule_tac x=ntfnptr in exI) apply clarsimp apply (frule obj_at_state_refs_ofD) apply (drule (1)sym_refs_obj_atD) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound_tcb_at P t s; sym_refs (state_refs_of s)\<rbrakk> \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_refs_of s); \<exists>ts ntfnptr. P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr. \<lbrakk>sym_refs (state_refs_of s); P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr. \<lbrakk>sym_refs (state_refs_of s); P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> \<exists>ntfnptr. P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr. \<lbrakk>sym_refs (state_refs_of s); P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> P ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr a b. \<lbrakk>sym_refs (state_refs_of s); (a, b) \<in> tcb_st_refs_of ts \<or> (a, b) \<in> tcb_bound_refs ntfnptr; P ntfnptr; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (t, symreftype b) \<in> refs_of ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr a b. \<lbrakk>sym_refs (state_refs_of s); (a, b) \<in> tcb_st_refs_of ts \<or> (a, b) \<in> tcb_bound_refs ntfnptr; P ntfnptr; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; \<exists>ko. tcb_ntfn_is_bound ntfnptr ko \<and> state_refs_of s t = refs_of ko\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (t, symreftype b) \<in> refs_of ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr a b. \<lbrakk>sym_refs (state_refs_of s); (a, b) \<in> tcb_st_refs_of ts \<or> (a, b) \<in> tcb_bound_refs ntfnptr; P ntfnptr; state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; \<exists>ko. tcb_ntfn_is_bound ntfnptr ko \<and> state_refs_of s t = refs_of ko; \<exists>ko. tcb_ntfn_is_bound ntfnptr ko \<and> state_refs_of s t = refs_of ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (t, symreftype b) \<in> refs_of ko) a s proof (prove)
goal:
No subgoals!