theory Invariants_AI

lemma sym_refs_st_tcb_atD:
  "\<lbrakk> st_tcb_at P t s; sym_refs (state_refs_of s) \<rbrakk> \<Longrightarrow>
     \<exists>ts ntfn. P ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s
        \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn
        \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. obj_at (\<lambda>ko. (t, symreftype tp) \<in> refs_of ko) x s)" apply (drule st_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>st_tcb_at P t s; sym_refs (state_refs_of s)\<rbrakk> \<Longrightarrow> \<exists>ts ntfn. P ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. 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 ts \<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 ntfn. P ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. 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 ts \<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 ntfn. P ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. 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 ts \<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>ntfn. P ts \<and> obj_at (tcb_ntfn_is_bound ntfn) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of ts \<union> tcb_bound_refs ntfn. 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 ts \<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 ts \<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 ts; 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 ts; 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 ts; 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!