theory SR_lemmas_C

lemma cap_get_tag_isCap:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_thread_cap) = (isThreadCap cap)"
  and "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)"
  and "(cap_get_tag cap' = scast cap_notification_cap) = (isNotificationCap cap)"
  and "(cap_get_tag cap' = scast cap_endpoint_cap) = (isEndpointCap cap)"
  and "(cap_get_tag cap' = scast cap_irq_handler_cap) = (isIRQHandlerCap cap)"
  and "(cap_get_tag cap' = scast cap_irq_control_cap) = (isIRQControlCap cap)"
  and "(cap_get_tag cap' = scast cap_zombie_cap) = (isZombie cap)"
  and "(cap_get_tag cap' = scast cap_reply_cap) = isReplyCap cap"
  and "(cap_get_tag cap' = scast cap_untyped_cap) = (isUntypedCap cap)"
  and "(cap_get_tag cap' = scast cap_cnode_cap) = (isCNodeCap cap)"
  and "isArchCap_tag (cap_get_tag cap') = isArchCap \<top> cap"
  and "(cap_get_tag cap' = scast cap_small_frame_cap) = (isArchPageCap cap \<and> pageSize cap = ARMSmallPage)"
  and "(cap_get_tag cap' = scast cap_frame_cap) = (isArchPageCap cap \<and> pageSize cap \<noteq> ARMSmallPage)"
  and "(cap_get_tag cap' = scast cap_domain_cap) = isDomainCap cap" using cap_get_tag_isCap0 [OF cr] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap) = isNotificationCap cap) &&& ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap) = isEndpointCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap) = isIRQHandlerCap cap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = isIRQControlCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = isZombie cap) &&& ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) = isReplyCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap) = isUntypedCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap) = isCNodeCap cap) &&& (isArchCap_tag (cap_get_tag cap') = isArchCap (\<lambda>_. True) cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isArchPageCap cap \<and> pageSize cap = Wellformed_C.ARMSmallPage)) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isArchPageCap cap \<and> pageSize cap \<noteq> Wellformed_C.ARMSmallPage) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = isDomainCap cap proof (prove)
using this:
(cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap) = isNotificationCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap) = isEndpointCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap) = isIRQHandlerCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = isIRQControlCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = isZombie cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) = isReplyCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap) = isUntypedCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap) = isCNodeCap cap \<and> isArchCap_tag (cap_get_tag cap') = isArchCap (\<lambda>_. True) cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isArchPageCap cap \<and> pageSize cap = Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isArchPageCap cap \<and> pageSize cap \<noteq> Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = isDomainCap cap

goal (1 subgoal):
 1. (((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) = (cap = capability.NullCap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_notification_cap) = isNotificationCap cap) &&& ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap) = isEndpointCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_handler_cap) = isIRQHandlerCap cap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_irq_control_cap) = isIRQControlCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap) = isZombie cap) &&& ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap) = isReplyCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap) = isUntypedCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap) = isCNodeCap cap) &&& (isArchCap_tag (cap_get_tag cap') = isArchCap (\<lambda>_. True) cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isArchPageCap cap \<and> pageSize cap = Wellformed_C.ARMSmallPage)) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isArchPageCap cap \<and> pageSize cap \<noteq> Wellformed_C.ARMSmallPage) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_domain_cap) = isDomainCap cap