theory CSpace_R

lemma arch_update_setCTE_ifunsafe:
  "\<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and if_unsafe_then_cap'\<rbrace>
  setCTE p (cteCap_update (\<lambda>_. cap) oldcte)
  \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (clarsimp simp: ifunsafe'_def2 cte_wp_at_ctes_of pred_conj_def) apply (rule hoare_lift_Pf2 [where f=irq_node']) prefer 2 apply wp apply wp apply (clarsimp simp: cte_wp_at_ctes_of is_arch_update'_def) apply (frule capMaster_same_refs) apply clarsimp apply (rule conjI, clarsimp) apply (erule_tac x=p in allE) apply clarsimp apply (erule impE) apply clarsimp apply clarsimp apply (rule_tac x=cref' in exI) apply clarsimp apply clarsimp apply (erule_tac x=cref in allE) apply clarsimp apply (rule_tac x=cref' in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (is_arch_update' cap) p and cte_wp_at' ((=) oldcte) p and if_unsafe_then_cap'\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<exists>cte. ctes_of x p = Some cte \<and> is_arch_update' cap cte) \<and> ctes_of x p = Some oldcte \<and> (\<forall>cref. (\<exists>cte. ctes_of x cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of x cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') (irq_node' x)))\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') (irq_node' s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<exists>cte. ctes_of xa p = Some cte \<and> is_arch_update' cap cte) \<and> ctes_of xa p = Some oldcte \<and> (\<forall>cref. (\<exists>cte. ctes_of xa cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of xa cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>_ a. \<forall>cref. (\<exists>cte. ctes_of a cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of a cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>_ x. P (irq_node' x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>x. P (irq_node' x)\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>_ x. P (irq_node' x)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>xa. (\<exists>cte. ctes_of xa p = Some cte \<and> is_arch_update' cap cte) \<and> ctes_of xa p = Some oldcte \<and> (\<forall>cref. (\<exists>cte. ctes_of xa cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of xa cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>_ a. \<forall>cref. (\<exists>cte. ctes_of a cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of a cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<exists>cte. ctes_of xa p = Some cte \<and> is_arch_update' cap cte) \<and> ctes_of xa p = Some oldcte \<and> (\<forall>cref. (\<exists>cte. ctes_of xa cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of xa cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))\<rbrace> setCTE p (cteCap_update (\<lambda>_. cap) oldcte) \<lbrace>\<lambda>_ a. \<forall>cref. (\<exists>cte. ctes_of a cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of a cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. (\<exists>cte. ctes_of s p = Some cte \<and> is_arch_update' cap cte) \<and> ctes_of s p = Some oldcte \<and> (\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)) \<Longrightarrow> \<forall>cref. (\<exists>cte. ((ctes_of s)(p \<mapsto> cteCap_update (\<lambda>_. cap) oldcte)) cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ((ctes_of s)(p \<mapsto> cteCap_update (\<lambda>_. cap) oldcte)) cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte)\<rbrakk> \<Longrightarrow> (cref = p \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' cap x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x)))) \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' cap x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)))) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte) \<and> zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> (cref = p \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' cap x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x)))) \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' cap x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)))) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> (cref = p \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x)))) \<and> (cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)))) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; (\<exists>cte. ctes_of s p = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x)\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; cteCap oldcte \<noteq> capability.NullCap \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x)\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cteCap oldcte \<noteq> capability.NullCap
 2. \<And>x s. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; \<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 3. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; \<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (2 subgoals):
 1. \<And>x s cref' cte'. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; ctes_of s cref' = Some cte'; p \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (2 subgoals):
 1. \<And>x s cref' cte'. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cap \<noteq> capability.NullCap; ctes_of s cref' = Some cte'; p \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> (cref' = p \<longrightarrow> p \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> p \<in> cte_refs' (cteCap cte') x))
 2. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte)\<rbrakk> \<Longrightarrow> cref \<noteq> p \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x))) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref cte. \<lbrakk>\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x); ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cref \<noteq> p; ctes_of s cref = Some cte; cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref cte. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cref \<noteq> p; ctes_of s cref = Some cte; cteCap cte \<noteq> capability.NullCap; (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref cte cref' cte'. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cref \<noteq> p; ctes_of s cref = Some cte; cteCap cte \<noteq> capability.NullCap; ctes_of s cref' = Some cte'; cref \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> \<exists>cref'. (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)) proof (prove)
goal (1 subgoal):
 1. \<And>x s cref cte cref' cte'. \<lbrakk>ctes_of s p = Some oldcte; isArchObjectCap cap; capMasterCap cap = capMasterCap (cteCap oldcte); cte_refs' cap = cte_refs' (cteCap oldcte); zobj_refs' cap = zobj_refs' (cteCap oldcte); cref \<noteq> p; ctes_of s cref = Some cte; cteCap cte \<noteq> capability.NullCap; ctes_of s cref' = Some cte'; cref \<in> cte_refs' (cteCap cte') x\<rbrakk> \<Longrightarrow> (cref' = p \<longrightarrow> cref \<in> cte_refs' (cteCap oldcte) x) \<and> (cref' \<noteq> p \<longrightarrow> (\<exists>cte'. ctes_of s cref' = Some cte' \<and> cref \<in> cte_refs' (cteCap cte') x)) proof (prove)
goal:
No subgoals!