theory PageTableDuplicates

lemma finaliseCap_valid_duplicates'[wp]:
  "\<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
  and (valid_cap' cap)\<rbrace>
  finaliseCap cap call final \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (case_tac cap,simp_all add:isCap_simps finaliseCap_def) apply (wp|intro conjI|clarsimp split: option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' cap\<rbrace> global.finaliseCap cap call final \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>x1. cap = capability.ThreadCap x1 \<Longrightarrow> (call \<longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ThreadCap x1)\<rbrace> do cte_ptr <- getThreadCSpaceRoot x1;
y <- unbindNotification x1;
y <- ThreadDecls_H.suspend x1;
y <- prepareThreadDelete x1;
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>) \<and> (\<not> call \<longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ThreadCap x1)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>)
 2. cap = capability.NullCap \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' capability.NullCap\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>x31 x32 x33 x34. cap = capability.NotificationCap x31 x32 x33 x34 \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.NotificationCap x31 x32 x33 x34)\<rbrace> do y <- when call (do y <- unbindMaybeNotification x31;
cancelAllSignals x31
od);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>x4. cap = capability.IRQHandlerCap x4 \<Longrightarrow> (call \<longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.IRQHandlerCap x4)\<rbrace> do y <- deletingIRQHandler x4;
return (capability.NullCap, capability.IRQHandlerCap x4)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>) \<and> (\<not> call \<longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.IRQHandlerCap x4)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>)
 5. \<And>x51 x52 x53 x54 x55 x56. cap = capability.EndpointCap x51 x52 x53 x54 x55 x56 \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56)\<rbrace> do y <- when call (cancelAllIPC x51);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. cap = capability.DomainCap \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' capability.DomainCap\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>x71 x72 x73. cap = capability.Zombie x71 x72 x73 \<Longrightarrow> call \<longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.Zombie x71 x72 x73)\<rbrace> return (capability.Zombie x71 x72 x73, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>x8. cap = capability.ArchObjectCap x8 \<Longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap x8)\<rbrace> Arch.finaliseCap x8 call \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 9. \<And>x91 x92 x93. cap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ReplyCap x91 x92 x93)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 10. \<And>x101 x102 x103 x104. cap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<not> final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.UntypedCap x101 x102 x103 x104)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
A total of 12 subgoals... proof (prove)
goal:
No subgoals!