theory PageTableDuplicates

lemma archFinaliseCap_valid_duplicates'[wp]:
  "\<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
    and (valid_cap' (capability.ArchObjectCap arch_cap))\<rbrace>
  Arch.finaliseCap arch_cap is_final
  \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>" apply (case_tac arch_cap; clarsimp simp: ARM_H.finaliseCap_def isPageCap_def isPageTableCap_def
                                           isPageDirectoryCap_def isASIDPoolCap_def) apply (intro conjI | clarsimp | wpsimp simp: valid_cap'_def)+ 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' (capability.ArchObjectCap arch_cap)\<rbrace> Arch.finaliseCap arch_cap is_final \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. arch_cap = arch_capability.ASIDPoolCap x11 x12 \<Longrightarrow> (is_final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12))\<rbrace> do y <- deleteASIDPool x12 x11;
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>) \<and> (\<not> is_final \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.ASIDPoolCap x11 x12))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>)
 2. arch_cap = arch_capability.ASIDControlCap \<Longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap arch_capability.ASIDControlCap)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>
 3. \<And>x31 x32 x33 x34 x35. arch_cap = arch_capability.PageCap x31 x32 x33 x34 x35 \<Longrightarrow> ((\<exists>a b. x35 = Some (a, b)) \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35))\<rbrace> case the x35 of (a, v) \<Rightarrow> do y <- unmapPage x34 a v x32;
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>) \<and> (x35 = None \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 None))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>)
 4. \<And>x41 x42. arch_cap = arch_capability.PageTableCap x41 x42 \<Longrightarrow> (is_final \<and> (\<exists>a b. x42 = Some (a, b)) \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42))\<rbrace> case the x42 of (a, v) \<Rightarrow> do y <- unmapPageTable a v x41;
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>) \<and> ((is_final \<longrightarrow> x42 = None) \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>)
 5. \<And>x51 x52. arch_cap = arch_capability.PageDirectoryCap x51 x52 \<Longrightarrow> (is_final \<and> (\<exists>y. x52 = Some y) \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52))\<rbrace> do y <- deleteASID (the x52) x51;
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>) \<and> ((is_final \<longrightarrow> x52 = None) \<longrightarrow> \<lbrace>valid_objs' and pspace_aligned' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and valid_cap' (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>ya a. vs_valid_duplicates' (ksPSpace a)\<rbrace>) proof (prove)
goal:
No subgoals!