theory Delete_H

lemma isCapDs:
  "isUntypedCap cap \<Longrightarrow> \<exists>dev ptr size freeIndex. cap = UntypedCap dev ptr size freeIndex"
  "isEndpointCap cap \<Longrightarrow> \<exists>ptr bdg cans canr cang cangr. cap = EndpointCap ptr bdg cans canr cang cangr"
  "isNotificationCap cap \<Longrightarrow> \<exists>ptr bdg cans canr. cap = NotificationCap ptr bdg cans canr"
  "isCNodeCap cap \<Longrightarrow> \<exists>ptr bits grd gsize. cap = CNodeCap ptr bits grd gsize"
  "isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr"
  "isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap"
  "isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num" apply (case_tac cap, simp_all add: isUntypedCap_def) apply (case_tac cap, simp_all add: isEndpointCap_def) apply (case_tac cap, simp_all add: isNotificationCap_def) apply (case_tac cap, simp_all add: isCNodeCap_def) apply (case_tac cap, simp_all add: isThreadCap_def) apply (case_tac cap, simp_all add: isArchObjectCap_def) apply (case_tac cap, simp_all add: isZombie_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((isUntypedCap cap \<Longrightarrow> \<exists>dev ptr size freeIndex. cap = UntypedCap dev ptr size freeIndex) &&& (isEndpointCap cap \<Longrightarrow> \<exists>ptr bdg cans canr cang cangr. cap = EndpointCap ptr bdg cans canr cang cangr) &&& (isNotificationCap cap \<Longrightarrow> \<exists>ptr bdg cans canr. cap = NotificationCap ptr bdg cans canr)) &&& ((isCNodeCap cap \<Longrightarrow> \<exists>ptr bits grd gsize. cap = CNodeCap ptr bits grd gsize) &&& (isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr)) &&& (isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap) &&& (isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num) proof (prove)
goal (6 subgoals):
 1. isEndpointCap cap \<Longrightarrow> \<exists>ptr bdg cans canr cang cangr. cap = EndpointCap ptr bdg cans canr cang cangr
 2. isNotificationCap cap \<Longrightarrow> \<exists>ptr bdg cans canr. cap = NotificationCap ptr bdg cans canr
 3. isCNodeCap cap \<Longrightarrow> \<exists>ptr bits grd gsize. cap = CNodeCap ptr bits grd gsize
 4. isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr
 5. isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap
 6. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal (5 subgoals):
 1. isNotificationCap cap \<Longrightarrow> \<exists>ptr bdg cans canr. cap = NotificationCap ptr bdg cans canr
 2. isCNodeCap cap \<Longrightarrow> \<exists>ptr bits grd gsize. cap = CNodeCap ptr bits grd gsize
 3. isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr
 4. isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap
 5. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal (4 subgoals):
 1. isCNodeCap cap \<Longrightarrow> \<exists>ptr bits grd gsize. cap = CNodeCap ptr bits grd gsize
 2. isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr
 3. isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap
 4. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal (3 subgoals):
 1. isThreadCap cap \<Longrightarrow> \<exists>ptr. cap = ThreadCap ptr
 2. isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap
 3. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal (2 subgoals):
 1. isArchObjectCap cap \<Longrightarrow> \<exists>archcap. cap = ArchObjectCap archcap
 2. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal (1 subgoal):
 1. isZombie cap \<Longrightarrow> \<exists>ptr bits num. cap = Zombie ptr bits num proof (prove)
goal:
No subgoals!