theory Invariants_H

lemma sym_refs_st_tcb_atD':
  "\<lbrakk> st_tcb_at' P t s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow>
     \<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
        \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_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 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 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_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 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 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_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 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 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_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>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 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_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. ko_wp_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> ko_wp_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>obj. tcb_ntfn_is_bound' ntfnptr obj \<and> state_refs_of' s t = refs_of' (injectKO obj)\<rbrakk> \<Longrightarrow> ko_wp_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>obj. tcb_ntfn_is_bound' ntfnptr obj \<and> state_refs_of' s t = refs_of' (injectKO obj); \<exists>obj. tcb_ntfn_is_bound' ntfnptr obj \<and> state_refs_of' s t = refs_of' (injectKO obj) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO obj). ko_wp_at' (\<lambda>ko. (t, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. (t, symreftype b) \<in> refs_of' ko) a s proof (prove)
goal:
No subgoals!