theory Retype_C

lemma updateMDB_ctes_of_cap:
  "\<lbrace>\<lambda>s. (\<forall>x\<in>ran(ctes_of s). P (cteCap x)) \<and> no_0 (ctes_of s)\<rbrace>
    updateMDB srcSlot t
  \<lbrace>\<lambda>r s. \<forall>x\<in>ran (ctes_of s). P (cteCap x)\<rbrace>" apply (rule hoare_pre) apply wp apply (clarsimp) apply (erule ranE) apply (clarsimp simp:modify_map_def split:if_splits) apply (drule_tac x = z in bspec) apply fastforce apply simp apply (drule_tac x = x in bspec) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>ran (ctes_of s). P (cteCap x)) \<and> no_0 (ctes_of s)\<rbrace> updateMDB srcSlot t \<lbrace>\<lambda>r s. \<forall>x\<in>ran (ctes_of s). P (cteCap x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> updateMDB srcSlot t \<lbrace>\<lambda>r s. \<forall>x\<in>ran (ctes_of s). P (cteCap x)\<rbrace>
 2. \<And>s. (\<forall>x\<in>ran (ctes_of s). P (cteCap x)) \<and> no_0 (ctes_of s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x\<in>ran (ctes_of s). P (cteCap x)) \<and> no_0 (ctes_of s) \<Longrightarrow> no_0 (ctes_of s) \<and> (\<forall>x\<in>ran (modify_map (ctes_of s) srcSlot (cteMDBNode_update t)). P (cteCap x)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>x \<in> ran (modify_map (ctes_of s) srcSlot (cteMDBNode_update t)); \<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s)\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); modify_map (ctes_of s) srcSlot (cteMDBNode_update t) xa = Some x\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (2 subgoals):
 1. \<And>s z. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); ctes_of s srcSlot = Some z\<rbrakk> \<Longrightarrow> P (cteCap z)
 2. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (3 subgoals):
 1. \<And>s z. \<lbrakk>no_0 (ctes_of s); ctes_of s srcSlot = Some z\<rbrakk> \<Longrightarrow> z \<in> ran (ctes_of s)
 2. \<And>s z. \<lbrakk>no_0 (ctes_of s); ctes_of s srcSlot = Some z; P (cteCap z)\<rbrakk> \<Longrightarrow> P (cteCap z)
 3. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (2 subgoals):
 1. \<And>s z. \<lbrakk>no_0 (ctes_of s); ctes_of s srcSlot = Some z; P (cteCap z)\<rbrakk> \<Longrightarrow> P (cteCap z)
 2. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>\<forall>x\<in>ran (ctes_of s). P (cteCap x); no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x\<rbrakk> \<Longrightarrow> x \<in> ran (ctes_of s)
 2. \<And>s x xa. \<lbrakk>no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x; P (cteCap x)\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>no_0 (ctes_of s); xa \<noteq> srcSlot; ctes_of s xa = Some x; P (cteCap x)\<rbrakk> \<Longrightarrow> P (cteCap x) proof (prove)
goal:
No subgoals!