theory ArchCSpacePre_AI

lemma unique_table_caps_upd_eqD:
  "\<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b';
    is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'\<rbrakk>
   \<Longrightarrow> unique_table_caps (ms (a \<mapsto> b')) = unique_table_caps (ms)" unfolding unique_table_caps_def apply (rule iffI) apply (intro allI impI,elim allE) apply (erule impE) apply (rule_tac p = p in fun_upd_Some) apply assumption apply (erule impE) apply (rule_tac p = p' in fun_upd_Some) apply simp apply (simp add: if_distrib split:if_splits) apply (intro allI impI,elim allE) apply (erule impE) apply (rule_tac p = p in fun_upd_Some_rev) apply simp+ apply (erule impE) apply (rule_tac p = p' in fun_upd_Some_rev) apply simp+ apply (simp add: if_distrib split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'\<rbrakk> \<Longrightarrow> unique_table_caps (ms(a \<mapsto> b')) = unique_table_caps ms proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'\<rbrakk> \<Longrightarrow> (\<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)) = (\<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; (ms(a \<mapsto> b')) (?p11 p p' cap cap') = Some (?cap13 p p' cap cap') \<longrightarrow> (ms(a \<mapsto> b')) (?p'12 p p' cap cap') = Some (?cap'14 p p' cap cap') \<longrightarrow> cap_asid (?cap13 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'14 p p' cap cap') = obj_refs (?cap13 p p' cap cap') \<longrightarrow> (is_pd_cap (?cap13 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = ?p11 p p' cap cap') \<and> (is_pt_cap (?cap13 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = ?p11 p p' cap cap')\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> (ms(a \<mapsto> b')) (?p11 p p' cap cap') = Some (?cap13 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; (ms(a \<mapsto> b')) (?p'12 p p' cap cap') = Some (?cap'14 p p' cap cap') \<longrightarrow> cap_asid (?cap13 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'14 p p' cap cap') = obj_refs (?cap13 p p' cap cap') \<longrightarrow> (is_pd_cap (?cap13 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = ?p11 p p' cap cap') \<and> (is_pt_cap (?cap13 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = ?p11 p p' cap cap')\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 3. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms p = Some (?k18 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; (ms(a \<mapsto> b')) (?p'12 p p' cap cap') = Some (?cap'14 p p' cap cap') \<longrightarrow> cap_asid (if a = p then b' else ?k18 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'14 p p' cap cap') = obj_refs (if a = p then b' else ?k18 p p' cap cap') \<longrightarrow> (is_pd_cap (if a = p then b' else ?k18 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p) \<and> (is_pt_cap (if a = p then b' else ?k18 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 3. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; (ms(a \<mapsto> b')) (?p'12 p p' cap cap') = Some (?cap'14 p p' cap cap') \<longrightarrow> cap_asid (if a = p then b' else cap) = None \<longrightarrow> obj_refs (?cap'14 p p' cap cap') = obj_refs (if a = p then b' else cap) \<longrightarrow> (is_pd_cap (if a = p then b' else cap) \<longrightarrow> is_pd_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p) \<and> (is_pt_cap (if a = p then b' else cap) \<longrightarrow> is_pt_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> (ms(a \<mapsto> b')) (?p'12 p p' cap cap') = Some (?cap'14 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b' else cap) = None \<longrightarrow> obj_refs (?cap'14 p p' cap cap') = obj_refs (if a = p then b' else cap) \<longrightarrow> (is_pd_cap (if a = p then b' else cap) \<longrightarrow> is_pd_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p) \<and> (is_pt_cap (if a = p then b' else cap) \<longrightarrow> is_pt_cap (?cap'14 p p' cap cap') \<longrightarrow> ?p'12 p p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 3. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms p' = Some (?k22 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b' else cap) = None \<longrightarrow> obj_refs (if a = p' then b' else ?k22 p p' cap cap') = obj_refs (if a = p then b' else cap) \<longrightarrow> (is_pd_cap (if a = p then b' else cap) \<longrightarrow> is_pd_cap (if a = p' then b' else ?k22 p p' cap cap') \<longrightarrow> p' = p) \<and> (is_pt_cap (if a = p then b' else cap) \<longrightarrow> is_pt_cap (if a = p' then b' else ?k22 p p' cap cap') \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 3. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; ms p = Some cap; ms p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b' else cap) = None \<longrightarrow> obj_refs (if a = p' then b' else cap') = obj_refs (if a = p then b' else cap) \<longrightarrow> (is_pd_cap (if a = p then b' else cap) \<longrightarrow> is_pd_cap (if a = p' then b' else cap') \<longrightarrow> p' = p) \<and> (is_pt_cap (if a = p then b' else cap) \<longrightarrow> is_pt_cap (if a = p' then b' else cap') \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)
 2. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; \<forall>p p' cap cap'. ms p = Some cap \<longrightarrow> ms p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> \<forall>p p' cap cap'. (ms(a \<mapsto> b')) p = Some cap \<longrightarrow> (ms(a \<mapsto> b')) p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; ms (?p65 p p' cap cap') = Some (?cap67 p p' cap cap') \<longrightarrow> ms (?p'66 p p' cap cap') = Some (?cap'68 p p' cap cap') \<longrightarrow> cap_asid (?cap67 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'68 p p' cap cap') = obj_refs (?cap67 p p' cap cap') \<longrightarrow> (is_pd_cap (?cap67 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p65 p p' cap cap') \<and> (is_pt_cap (?cap67 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p65 p p' cap cap')\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms (?p65 p p' cap cap') = Some (?cap67 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; ms (?p'66 p p' cap cap') = Some (?cap'68 p p' cap cap') \<longrightarrow> cap_asid (?cap67 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'68 p p' cap cap') = obj_refs (?cap67 p p' cap cap') \<longrightarrow> (is_pd_cap (?cap67 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p65 p p' cap cap') \<and> (is_pt_cap (?cap67 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p65 p p' cap cap')\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms (?p74 p (?a72 p p' cap cap') p' cap cap') = Some (?k72 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ((\<lambda>a. ms (?p74 p a p' cap cap'))(?a72 p p' cap cap' \<mapsto> ?b72 p p' cap cap')) p = Some (?cap72 p p' cap cap')
 3. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (ms(a \<mapsto> b')) p = Some cap; (ms(a \<mapsto> b')) p' = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; ms (?p'66 p p' cap cap') = Some (?cap'68 p p' cap cap') \<longrightarrow> cap_asid (if ?a72 p p' cap cap' = p then ?k72 p p' cap cap' else ?cap72 p p' cap cap') = None \<longrightarrow> obj_refs (?cap'68 p p' cap cap') = obj_refs (if ?a72 p p' cap cap' = p then ?k72 p p' cap cap' else ?cap72 p p' cap cap') \<longrightarrow> (is_pd_cap (if ?a72 p p' cap cap' = p then ?k72 p p' cap cap' else ?cap72 p p' cap cap') \<longrightarrow> is_pd_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p74 p p p' cap cap') \<and> (is_pt_cap (if ?a72 p p' cap cap' = p then ?k72 p p' cap cap' else ?cap72 p p' cap cap') \<longrightarrow> is_pt_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = ?p74 p p p' cap cap')\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; ms (?p'66 p p' cap cap') = Some (?cap'68 p p' cap cap') \<longrightarrow> cap_asid (if a = p then b else cap) = None \<longrightarrow> obj_refs (?cap'68 p p' cap cap') = obj_refs (if a = p then b else cap) \<longrightarrow> (is_pd_cap (if a = p then b else cap) \<longrightarrow> is_pd_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = p) \<and> (is_pt_cap (if a = p then b else cap) \<longrightarrow> is_pt_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms (?p'66 p p' cap cap') = Some (?cap'68 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b else cap) = None \<longrightarrow> obj_refs (?cap'68 p p' cap cap') = obj_refs (if a = p then b else cap) \<longrightarrow> (is_pd_cap (if a = p then b else cap) \<longrightarrow> is_pd_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = p) \<and> (is_pt_cap (if a = p then b else cap) \<longrightarrow> is_pt_cap (?cap'68 p p' cap cap') \<longrightarrow> ?p'66 p p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (3 subgoals):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ms (?p'80 p p' (?a78 p p' cap cap') cap cap') = Some (?k78 p p' cap cap')
 2. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> ((\<lambda>a. ms (?p'80 p p' a cap cap'))(?a78 p p' cap cap' \<mapsto> ?b78 p p' cap cap')) p' = Some (?cap78 p p' cap cap')
 3. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b else cap) = None \<longrightarrow> obj_refs (if ?a78 p p' cap cap' = p' then ?k78 p p' cap cap' else ?cap78 p p' cap cap') = obj_refs (if a = p then b else cap) \<longrightarrow> (is_pd_cap (if a = p then b else cap) \<longrightarrow> is_pd_cap (if ?a78 p p' cap cap' = p' then ?k78 p p' cap cap' else ?cap78 p p' cap cap') \<longrightarrow> ?p'80 p p' p' cap cap' = p) \<and> (is_pt_cap (if a = p then b else cap) \<longrightarrow> is_pt_cap (if ?a78 p p' cap cap' = p' then ?k78 p p' cap cap' else ?cap78 p p' cap cap') \<longrightarrow> ?p'80 p p' p' cap cap' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap'. \<lbrakk>ms a = Some b; cap_asid b = cap_asid b'; obj_refs b = obj_refs b'; is_pd_cap b = is_pd_cap b'; is_pt_cap b = is_pt_cap b'; (if p = a then Some b' else ms p) = Some cap; (if p' = a then Some b' else ms p') = Some cap'; cap_asid cap = None; obj_refs cap' = obj_refs cap; cap_asid (if a = p then b else cap) = None \<longrightarrow> obj_refs (if a = p' then b else cap') = obj_refs (if a = p then b else cap) \<longrightarrow> (is_pd_cap (if a = p then b else cap) \<longrightarrow> is_pd_cap (if a = p' then b else cap') \<longrightarrow> p' = p) \<and> (is_pt_cap (if a = p then b else cap) \<longrightarrow> is_pt_cap (if a = p' then b else cap') \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p) proof (prove)
goal:
No subgoals!