theory KHeap_DR

lemma transform_full_intent_same_cap:
  "\<lbrakk> transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<rbrakk>
  \<Longrightarrow> transform_full_intent ms p' (tcb\<lparr>tcb_ipcframe := cap'\<rparr>) =
     transform_full_intent ms p' tcb" apply (rule transform_full_intent_caps_cong) apply simp apply simp apply (simp add: is_cap_simps) apply (cases "tcb_ipcframe tcb", simp_all) by (simp add:transform_cap_def is_cap_simps
                     split:cap.splits if_split_asm arch_cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> transform_full_intent ms p' (tcb\<lparr>tcb_ipcframe := cap'\<rparr>) = transform_full_intent ms p' tcb proof (prove)
goal (4 subgoals):
 1. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> arch_tcb_context_get (tcb_arch (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = arch_tcb_context_get (tcb_arch tcb)
 2. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> tcb_ipc_buffer (tcb\<lparr>tcb_ipcframe := cap'\<rparr>) = tcb_ipc_buffer tcb
 3. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = is_pg_cap (tcb_ipcframe tcb)
 4. \<lbrakk>transform_cap (tcb_ipcframe tcb) = transform_cap cap'; is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)); is_pg_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = obj_ref_of (tcb_ipcframe tcb) \<and> cap_bits (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = cap_bits (tcb_ipcframe tcb) \<and> Structures_A.cap_rights (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = Structures_A.cap_rights (tcb_ipcframe tcb) proof (prove)
goal (3 subgoals):
 1. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> tcb_ipc_buffer (tcb\<lparr>tcb_ipcframe := cap'\<rparr>) = tcb_ipc_buffer tcb
 2. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = is_pg_cap (tcb_ipcframe tcb)
 3. \<lbrakk>transform_cap (tcb_ipcframe tcb) = transform_cap cap'; is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)); is_pg_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = obj_ref_of (tcb_ipcframe tcb) \<and> cap_bits (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = cap_bits (tcb_ipcframe tcb) \<and> Structures_A.cap_rights (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = Structures_A.cap_rights (tcb_ipcframe tcb) proof (prove)
goal (2 subgoals):
 1. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = is_pg_cap (tcb_ipcframe tcb)
 2. \<lbrakk>transform_cap (tcb_ipcframe tcb) = transform_cap cap'; is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)); is_pg_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = obj_ref_of (tcb_ipcframe tcb) \<and> cap_bits (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = cap_bits (tcb_ipcframe tcb) \<and> Structures_A.cap_rights (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = Structures_A.cap_rights (tcb_ipcframe tcb) proof (prove)
goal (2 subgoals):
 1. transform_cap (tcb_ipcframe tcb) = transform_cap cap' \<Longrightarrow> (\<exists>dev p R sz m. cap' = ArchObjectCap (PageCap dev p R sz m)) = (\<exists>dev p R sz m. tcb_ipcframe tcb = ArchObjectCap (PageCap dev p R sz m))
 2. \<lbrakk>transform_cap (tcb_ipcframe tcb) = transform_cap cap'; is_pg_cap (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)); is_pg_cap (tcb_ipcframe tcb)\<rbrakk> \<Longrightarrow> obj_ref_of (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = obj_ref_of (tcb_ipcframe tcb) \<and> cap_bits (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = cap_bits (tcb_ipcframe tcb) \<and> Structures_A.cap_rights (tcb_ipcframe (tcb\<lparr>tcb_ipcframe := cap'\<rparr>)) = Structures_A.cap_rights (tcb_ipcframe tcb) proof (prove)
goal (13 subgoals):
 1. \<lbrakk>cdl_cap.NullCap = transform_cap cap'; tcb_ipcframe tcb = cap.NullCap\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 2. \<And>x21 x22 x23 x24. \<lbrakk>cdl_cap.UntypedCap x21 {x22..x22 + 2 ^ x23 - 1} (free_range_of_untyped x24 x23 x22) = transform_cap cap'; tcb_ipcframe tcb = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 3. \<And>x31 x32 x33. \<lbrakk>cdl_cap.EndpointCap x31 x32 x33 = transform_cap cap'; tcb_ipcframe tcb = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 4. \<And>x41 x42 x43. \<lbrakk>cdl_cap.NotificationCap x41 x42 x43 = transform_cap cap'; tcb_ipcframe tcb = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 5. \<And>x51 x52 x53. \<lbrakk>(if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = transform_cap cap'; tcb_ipcframe tcb = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 6. \<And>x61 x62 x63. \<lbrakk>cdl_cap.CNodeCap x61 (of_bl x63) (length x63) x62 = transform_cap cap'; tcb_ipcframe tcb = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 7. \<And>x7. \<lbrakk>TcbCap x7 = transform_cap cap'; tcb_ipcframe tcb = ThreadCap x7\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 8. \<lbrakk>cdl_cap.DomainCap = transform_cap cap'; tcb_ipcframe tcb = cap.DomainCap\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 9. \<lbrakk>IrqControlCap = transform_cap cap'; tcb_ipcframe tcb = IRQControlCap\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
 10. \<And>x10. \<lbrakk>IrqHandlerCap x10 = transform_cap cap'; tcb_ipcframe tcb = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<forall>dev p R sz m. cap' \<noteq> ArchObjectCap (PageCap dev p R sz m)
A total of 13 subgoals...