theory KHeap_DP

lemma reset_cap_asid_simps2:
  "reset_cap_asid cap = NullCap \<Longrightarrow> cap = NullCap"
  "reset_cap_asid cap = RunningCap \<Longrightarrow> cap = RunningCap"
  "reset_cap_asid cap = (UntypedCap dev a ra) \<Longrightarrow> cap = UntypedCap dev a ra"
  "reset_cap_asid cap = (EndpointCap b c d) \<Longrightarrow> cap = EndpointCap b c d"
  "reset_cap_asid cap = (NotificationCap e f g) \<Longrightarrow> cap = NotificationCap e f g"
  "reset_cap_asid cap = (ReplyCap h R) \<Longrightarrow> cap = ReplyCap h R"
  "reset_cap_asid cap = (MasterReplyCap i) \<Longrightarrow> cap = MasterReplyCap i"
  "reset_cap_asid cap = (CNodeCap j k l sz) \<Longrightarrow> cap = CNodeCap j k l sz"
  "reset_cap_asid cap = (TcbCap m) \<Longrightarrow> cap = TcbCap m"
  "reset_cap_asid cap = DomainCap \<Longrightarrow> cap = DomainCap"
  "reset_cap_asid cap = RestartCap \<Longrightarrow> cap = RestartCap"
  "reset_cap_asid cap = (PendingSyncSendCap n p q r s rp) \<Longrightarrow> cap = (PendingSyncSendCap n p q r s rp)"
  "reset_cap_asid cap = (PendingSyncRecvCap t isf rp) \<Longrightarrow> cap = (PendingSyncRecvCap t isf rp)"
  "reset_cap_asid cap = (PendingNtfnRecvCap u) \<Longrightarrow> cap = (PendingNtfnRecvCap u)"
  "reset_cap_asid cap = IrqControlCap \<Longrightarrow> cap = IrqControlCap"
  "reset_cap_asid cap = (IrqHandlerCap v) \<Longrightarrow> cap = (IrqHandlerCap v)"
  "reset_cap_asid cap = AsidControlCap \<Longrightarrow> cap = AsidControlCap"
  "reset_cap_asid cap = (AsidPoolCap w x) \<Longrightarrow> cap = (AsidPoolCap w x)"
  "reset_cap_asid cap = (IOPortsCap y z) \<Longrightarrow> cap = (IOPortsCap y z)"
  "reset_cap_asid cap = IOSpaceMasterCap \<Longrightarrow> cap = IOSpaceMasterCap"
  "reset_cap_asid cap = (IOSpaceCap a1) \<Longrightarrow> cap = (IOSpaceCap a1)"
  "reset_cap_asid cap = (IOPageTableCap a2) \<Longrightarrow> cap = (IOPageTableCap a2)"
  "reset_cap_asid cap = (ZombieCap a3) \<Longrightarrow> cap = (ZombieCap a3)"
  "reset_cap_asid cap = (BoundNotificationCap a4) \<Longrightarrow> cap = (BoundNotificationCap a4)"
  "reset_cap_asid cap = (FrameCap dev aa rghts sz rset ma) \<Longrightarrow> \<exists>asid. cap = FrameCap dev aa rghts sz rset asid"
  "reset_cap_asid cap = (PageTableCap aa rights ma) \<Longrightarrow> \<exists>asid. cap = PageTableCap aa rights asid"
  "reset_cap_asid cap = (PageDirectoryCap aa rights as) \<Longrightarrow> \<exists>asid. cap = PageDirectoryCap aa rights asid" by (clarsimp simp: reset_cap_asid_def split: cdl_cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((reset_cap_asid cap = NullCap \<Longrightarrow> cap = NullCap) &&& (reset_cap_asid cap = RunningCap \<Longrightarrow> cap = RunningCap) &&& (reset_cap_asid cap = UntypedCap dev a ra \<Longrightarrow> cap = UntypedCap dev a ra)) &&& (reset_cap_asid cap = EndpointCap b c d \<Longrightarrow> cap = EndpointCap b c d) &&& (reset_cap_asid cap = NotificationCap e f g \<Longrightarrow> cap = NotificationCap e f g) &&& (reset_cap_asid cap = ReplyCap h R \<Longrightarrow> cap = ReplyCap h R)) &&& ((reset_cap_asid cap = MasterReplyCap i \<Longrightarrow> cap = MasterReplyCap i) &&& (reset_cap_asid cap = CNodeCap j k l sz \<Longrightarrow> cap = CNodeCap j k l sz) &&& (reset_cap_asid cap = TcbCap m \<Longrightarrow> cap = TcbCap m)) &&& ((reset_cap_asid cap = DomainCap \<Longrightarrow> cap = DomainCap) &&& (reset_cap_asid cap = RestartCap \<Longrightarrow> cap = RestartCap)) &&& (reset_cap_asid cap = PendingSyncSendCap n p q r s rp \<Longrightarrow> cap = PendingSyncSendCap n p q r s rp) &&& (reset_cap_asid cap = PendingSyncRecvCap t isf rp \<Longrightarrow> cap = PendingSyncRecvCap t isf rp)) &&& (((reset_cap_asid cap = PendingNtfnRecvCap u \<Longrightarrow> cap = PendingNtfnRecvCap u) &&& (reset_cap_asid cap = IrqControlCap \<Longrightarrow> cap = IrqControlCap) &&& (reset_cap_asid cap = IrqHandlerCap v \<Longrightarrow> cap = IrqHandlerCap v)) &&& ((reset_cap_asid cap = AsidControlCap \<Longrightarrow> cap = AsidControlCap) &&& (reset_cap_asid cap = AsidPoolCap w x \<Longrightarrow> cap = AsidPoolCap w x)) &&& (reset_cap_asid cap = IOPortsCap y z \<Longrightarrow> cap = IOPortsCap y z) &&& (reset_cap_asid cap = IOSpaceMasterCap \<Longrightarrow> cap = IOSpaceMasterCap)) &&& ((reset_cap_asid cap = IOSpaceCap a1 \<Longrightarrow> cap = IOSpaceCap a1) &&& (reset_cap_asid cap = IOPageTableCap a2 \<Longrightarrow> cap = IOPageTableCap a2) &&& (reset_cap_asid cap = ZombieCap a3 \<Longrightarrow> cap = ZombieCap a3)) &&& ((reset_cap_asid cap = BoundNotificationCap a4 \<Longrightarrow> cap = BoundNotificationCap a4) &&& (reset_cap_asid cap = FrameCap dev aa rghts sz rset ma \<Longrightarrow> \<exists>asid. cap = FrameCap dev aa rghts sz rset asid)) &&& (reset_cap_asid cap = PageTableCap aa rights ma \<Longrightarrow> \<exists>asid. cap = PageTableCap aa rights asid) &&& (reset_cap_asid cap = PageDirectoryCap aa rights as \<Longrightarrow> \<exists>asid. cap = PageDirectoryCap aa rights asid)