theory Recycle_C

lemma cendpoint_relation_q_cong:
  "\<lbrakk> \<And>t rf. (t, rf) \<in> ep_q_refs_of' ep \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t) \<rbrakk>
      \<Longrightarrow> cendpoint_relation hp ep ep' = cendpoint_relation hp' ep ep'" apply (cases ep, simp_all add: cendpoint_relation_def Let_def) apply (rule conj_cong [OF refl]) apply (rule tcb_queue_relation'_cong[OF refl refl refl]) apply clarsimp apply (rule conj_cong [OF refl]) apply (rule tcb_queue_relation'_cong[OF refl refl refl]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>t rf. (t, rf) \<in> ep_q_refs_of' ep \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t)) \<Longrightarrow> cendpoint_relation hp ep ep' = cendpoint_relation hp' ep ep' proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<And>t. t \<in> set x1 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' hp x1 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) = (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' hp' x1 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep'))))
 2. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) = (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp' x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<And>t. t \<in> set x1 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.RecvEP x1; endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Recv\<rbrakk> \<Longrightarrow> ep_queue_relation' hp x1 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep'))) = ep_queue_relation' hp' x1 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))
 2. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) = (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp' x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) proof (prove)
goal (2 subgoals):
 1. \<And>x1 p. \<lbrakk>\<And>t. t \<in> set x1 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.RecvEP x1; endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Recv; p \<in> tcb_ptr_to_ctcb_ptr ` set x1\<rbrakk> \<Longrightarrow> hp p = hp' p
 2. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) = (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp' x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) = (endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' hp' x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep')))) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3; endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send\<rbrakk> \<Longrightarrow> ep_queue_relation' hp x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep'))) = ep_queue_relation' hp' x3 (tcb_Ptr (epQueue_head_CL (endpoint_lift ep'))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift ep'))) proof (prove)
goal (1 subgoal):
 1. \<And>x3 p. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ep = Structures_H.endpoint.SendEP x3; endpoint_CL.state_CL (endpoint_lift ep') = SCAST(32 signed \<rightarrow> 32) EPState_Send; p \<in> tcb_ptr_to_ctcb_ptr ` set x3\<rbrakk> \<Longrightarrow> hp p = hp' p proof (prove)
goal:
No subgoals!