theory Finalise_DR

lemma finalise_cap_remainder:
  "\<lbrace>\<top>\<rbrace>CSpace_A.finalise_cap cap final \<lbrace>\<lambda>r s. fst (r) = (remainder_cap final cap) \<rbrace>" apply (case_tac cap; simp add: remainder_cap_def) apply (wp|clarsimp)+ apply (fastforce simp:valid_def) apply (simp add: liftM_def |clarify)+ apply (wp|clarsimp|rule conjI)+ apply (simp add:arch_finalise_cap_def) apply (cases final) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (simp_all) apply (wp|clarsimp)+ apply (simp_all split:option.splits) apply (wp | clarsimp | rule conjI)+ apply (rename_tac arch_cap) apply (case_tac arch_cap; simp) apply (wp|clarsimp split:option.splits | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> CSpace_A.finalise_cap cap final \<lbrace>\<lambda>r s. fst r = remainder_cap final cap\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = cap.UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>x31 x32 x33. cap = cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> liftM (\<lambda>y. (cap.NullCap, cap.NullCap)) (when final (IpcCancel_A.cancel_all_ipc x31)) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>x41 x42 x43. cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> liftM (\<lambda>y. (cap.NullCap, cap.NullCap)) (when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 5. \<And>x51 x52 x53. cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 6. \<And>x61 x62 x63. cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), cap.NullCap) \<lbrace>\<lambda>r s. fst r = Zombie x61 (Some x62) (2 ^ x62)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- IpcCancel_A.unbind_notification x7;
y <- IpcCancel_A.suspend x7;
y <- local.prepare_thread_delete x7;
return (Zombie x7 None 5, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x7 None 5\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 8. cap = cap.DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- CSpace_A.deleting_irq_handler x10;
return (cap.NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>cap = cap.EndpointCap x31 x32 x33; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q50 x31 x32 x33\<rbrace> IpcCancel_A.cancel_all_ipc x31 \<lbrace>(\<lambda>r s. fst r = cap.NullCap) \<circ> (\<lambda>y. (cap.NullCap, cap.NullCap))\<rbrace>
 2. \<And>x31 x32 x33 s. \<lbrakk>cap = cap.EndpointCap x31 x32 x33; True\<rbrakk> \<Longrightarrow> (if final then ?Q50 x31 x32 x33 else ((\<lambda>r s. fst r = cap.NullCap) \<circ> (\<lambda>y. (cap.NullCap, cap.NullCap))) ()) s
 3. \<And>x41 x42 x43. cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> liftM (\<lambda>y. (cap.NullCap, cap.NullCap)) (when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>x51 x52 x53. cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 5. \<And>x61 x62 x63. cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), cap.NullCap) \<lbrace>\<lambda>r s. fst r = Zombie x61 (Some x62) (2 ^ x62)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 6. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- IpcCancel_A.unbind_notification x7;
y <- IpcCancel_A.suspend x7;
y <- local.prepare_thread_delete x7;
return (Zombie x7 None 5, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x7 None 5\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 7. cap = cap.DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 8. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 9. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- CSpace_A.deleting_irq_handler x10;
return (cap.NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 10. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- assert final;
return (Zombie x111 x112 x113, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x111 x112 x113\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x31 x32 x33 s. \<lbrakk>cap = cap.EndpointCap x31 x32 x33; True\<rbrakk> \<Longrightarrow> (if final then ?Q50 x31 x32 x33 else ((\<lambda>r s. fst r = cap.NullCap) \<circ> (\<lambda>y. (cap.NullCap, cap.NullCap))) ()) s
 2. \<And>x41 x42 x43. cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> liftM (\<lambda>y. (cap.NullCap, cap.NullCap)) (when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>x51 x52 x53. cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>x61 x62 x63. cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), cap.NullCap) \<lbrace>\<lambda>r s. fst r = Zombie x61 (Some x62) (2 ^ x62)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 5. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- IpcCancel_A.unbind_notification x7;
y <- IpcCancel_A.suspend x7;
y <- local.prepare_thread_delete x7;
return (Zombie x7 None 5, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x7 None 5\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 6. cap = cap.DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 7. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 8. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- CSpace_A.deleting_irq_handler x10;
return (cap.NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 9. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- assert final;
return (Zombie x111 x112 x113, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x111 x112 x113\<rbrace>
 10. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x41 x42 x43. cap = cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do x <- when final (do y <- IpcCancel_A.unbind_maybe_notification x41;
cancel_all_signals x41
od);
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>x51 x52 x53. cap = cap.ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>x61 x62 x63. cap = cap.CNodeCap x61 x62 x63 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), cap.NullCap) \<lbrace>\<lambda>r s. fst r = Zombie x61 (Some x62) (2 ^ x62)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 4. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- IpcCancel_A.unbind_notification x7;
y <- IpcCancel_A.suspend x7;
y <- local.prepare_thread_delete x7;
return (Zombie x7 None 5, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x7 None 5\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 5. cap = cap.DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 6. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 7. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- CSpace_A.deleting_irq_handler x10;
return (cap.NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 8. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- assert final;
return (Zombie x111 x112 x113, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = Zombie x111 x112 x113\<rbrace>
 9. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> arch_finalise_cap x12 final \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap arch_cap; final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap = ArchObjectCap arch_cap; final; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap arch_cap; final; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap arch_cap; final; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap arch_cap; final; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 5. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap arch_cap; final; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 6. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap = ArchObjectCap (ASIDPoolCap x11 x12); final; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- local.delete_asid_pool x12 x11;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap ASIDControlCap; final; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); final; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x35 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> do y <- local.unmap_page x34 a v x32;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); final; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x42 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> do y <- local.unmap_page_table a v x41;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 5. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); final; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x52 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some a \<Rightarrow> do y <- local.delete_asid a x51;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 6. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x35 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> do y <- local.unmap_page x34 a v x32;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); final; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x42 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> do y <- local.unmap_page_table a v x41;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); final; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x52 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some a \<Rightarrow> do y <- local.delete_asid a x51;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); final\<rbrakk> \<Longrightarrow> (x35 = None \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- local.unmap_page x34 a b x32;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 2. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); final; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> (x42 = None \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- local.unmap_page_table a b x41;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 3. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); final; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> (x52 = None \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- local.delete_asid x2 x51;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>)
 4. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>cap = ArchObjectCap x12; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap arch_cap; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case arch_cap of ASIDPoolCap ptr b \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid_pool b ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | ASIDControlCap \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s None \<Rightarrow> return (cap.NullCap, cap.NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do local.unmap_page s a v ptr;
return (cap.NullCap, cap.NullCap)
od | arch_cap.PageTableCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageTableCap ptr (Some (a, v)) \<Rightarrow> case final of True \<Rightarrow> do local.unmap_page_table a v ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr None \<Rightarrow> return (cap.NullCap, cap.NullCap) | arch_cap.PageDirectoryCap ptr (Some a) \<Rightarrow> case final of True \<Rightarrow> do local.delete_asid a ptr;
return (cap.NullCap, cap.NullCap)
od | False \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap = ArchObjectCap (ASIDPoolCap x11 x12); \<not> final; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 2. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap ASIDControlCap; \<not> final; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); \<not> final; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x35 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> do y <- local.unmap_page x34 a v x32;
return (cap.NullCap, cap.NullCap)
od \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 4. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); \<not> final; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x42 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | Some (a, v) \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace>
 5. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); \<not> final; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> case x52 of None \<Rightarrow> return (cap.NullCap, cap.NullCap) | _ \<Rightarrow> return (cap.NullCap, cap.NullCap) \<lbrace>\<lambda>r s. fst r = cap.NullCap\<rbrace> proof (prove)
goal:
No subgoals!