theory IpcCancel_C

lemma cendpoint_relation_ep_queue:
  fixes ep :: "endpoint"
  assumes   ep: "cendpoint_relation mp ep' b"
  and     mpeq: "(mp' |` (- S)) = (mp |` (- S))"
  and      epq: "ep' \<noteq> IdleEP \<Longrightarrow>
                     set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}"
  shows  "cendpoint_relation mp' ep' b" proof - have rl: "\<And>p list. \<lbrakk> ctcb_ptr_to_tcb_ptr p \<in> set list;
                          ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk>
                         \<Longrightarrow> mp' p = mp p" using epq apply (cut_tac x=p in fun_cong[OF mpeq]) apply (cases ep', auto simp: restrict_map_def split: if_split_asm) done have rl': "\<And>p list. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set list;
                          ep' = RecvEP list \<or> ep' = SendEP list \<rbrakk>
                         \<Longrightarrow> mp' p = mp p" by (clarsimp elim!: rl[rotated]) show ?thesis using ep rl' mpeq unfolding cendpoint_relation_def by (simp add: Let_def
            cong: Structures_H.endpoint.case_cong tcb_queue_relation'_cong) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (state)
goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (prove)
goal (1 subgoal):
 1. \<And>p list. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<in> set list; ep' = Structures_H.endpoint.RecvEP list \<or> ep' = Structures_H.endpoint.SendEP list\<rbrakk> \<Longrightarrow> mp' p = mp p proof (prove)
using this:
ep' \<noteq> Structures_H.endpoint.IdleEP \<Longrightarrow> set (epQueue ep') \<inter> ctcb_ptr_to_tcb_ptr ` S = {}

goal (1 subgoal):
 1. \<And>p list. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<in> set list; ep' = Structures_H.endpoint.RecvEP list \<or> ep' = Structures_H.endpoint.SendEP list\<rbrakk> \<Longrightarrow> mp' p = mp p proof (prove)
goal (1 subgoal):
 1. \<And>p list. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<in> set list; ep' = Structures_H.endpoint.RecvEP list \<or> ep' = Structures_H.endpoint.SendEP list; ep' \<noteq> Structures_H.endpoint.IdleEP \<Longrightarrow> set (epQueue ep') \<inter> ctcb_ptr_to_tcb_ptr ` S = {}; (mp'|\<^bsub>(- S)\<^esub>) p = (mp|\<^bsub>(- S)\<^esub>) p\<rbrakk> \<Longrightarrow> mp' p = mp p proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>ctcb_ptr_to_tcb_ptr ?p1 \<in> set ?list1; ep' = Structures_H.endpoint.RecvEP ?list1 \<or> ep' = Structures_H.endpoint.SendEP ?list1\<rbrakk> \<Longrightarrow> mp' ?p1 = mp ?p1

goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (prove)
goal (1 subgoal):
 1. \<And>p list. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set list; ep' = Structures_H.endpoint.RecvEP list \<or> ep' = Structures_H.endpoint.SendEP list\<rbrakk> \<Longrightarrow> mp' p = mp p proof (state)
this:
\<lbrakk>?p1 \<in> tcb_ptr_to_ctcb_ptr ` set ?list1; ep' = Structures_H.endpoint.RecvEP ?list1 \<or> ep' = Structures_H.endpoint.SendEP ?list1\<rbrakk> \<Longrightarrow> mp' ?p1 = mp ?p1

goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (prove)
goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (prove)
using this:
cendpoint_relation mp ep' b
\<lbrakk>?p1 \<in> tcb_ptr_to_ctcb_ptr ` set ?list1; ep' = Structures_H.endpoint.RecvEP ?list1 \<or> ep' = Structures_H.endpoint.SendEP ?list1\<rbrakk> \<Longrightarrow> mp' ?p1 = mp ?p1
mp'|\<^bsub>(- S)\<^esub> = mp|\<^bsub>(- S)\<^esub>

goal (1 subgoal):
 1. cendpoint_relation mp' ep' b proof (prove)
using this:
let cstate = endpoint_CL.state_CL (endpoint_lift b); chead = (tcb_Ptr \<circ> epQueue_head_CL \<circ> endpoint_lift) b; cend = (tcb_Ptr \<circ> epQueue_tail_CL \<circ> endpoint_lift) b in case ep' of Structures_H.endpoint.RecvEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q chead cend | Structures_H.endpoint.IdleEP \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] chead cend | Structures_H.endpoint.SendEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q chead cend
\<lbrakk>?p1 \<in> tcb_ptr_to_ctcb_ptr ` set ?list1; ep' = Structures_H.endpoint.RecvEP ?list1 \<or> ep' = Structures_H.endpoint.SendEP ?list1\<rbrakk> \<Longrightarrow> mp' ?p1 = mp ?p1
mp'|\<^bsub>(- S)\<^esub> = mp|\<^bsub>(- S)\<^esub>

goal (1 subgoal):
 1. let cstate = endpoint_CL.state_CL (endpoint_lift b); chead = (tcb_Ptr \<circ> epQueue_head_CL \<circ> endpoint_lift) b; cend = (tcb_Ptr \<circ> epQueue_tail_CL \<circ> endpoint_lift) b in case ep' of Structures_H.endpoint.RecvEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q chead cend | Structures_H.endpoint.IdleEP \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] chead cend | Structures_H.endpoint.SendEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q chead cend proof (state)
this:
cendpoint_relation mp' ep' b

goal:
No subgoals!