theory CNode_DR

lemma dcorres_update_cap_data_bind:
  "\<lbrakk>cap = transform_cap cap' ; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c') \<rbrakk> \<Longrightarrow>
   dcorres r P (valid_idle and valid_cap cap' and P')
           ((CSpace_D.update_cap_data b data cap) >>= f)
           (f' (CSpace_A.update_cap_data b data cap'))" apply (subst return_bind [symmetric, where f=f']) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule dcorres_update_cap_data, simp) apply simp apply assumption apply (clarsimp simp: CSpace_D.update_cap_data_def) apply (wp | wpc)+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> dcorres r P (valid_idle and valid_cap cap' and P') (CSpace_D.update_cap_data b data cap >>= f) (f' (CSpace_A.update_cap_data b data cap')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> dcorres r P (valid_idle and valid_cap cap' and P') (CSpace_D.update_cap_data b data cap >>= f) (return (CSpace_A.update_cap_data b data cap') >>= f') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> dcorres r ?Q ?Q' (CSpace_D.update_cap_data b data cap >>= f) (return (CSpace_A.update_cap_data b data cap') >>= f')
 2. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> dcorres ?r'4 ?P4 ?P'4 (CSpace_D.update_cap_data b data cap) (return (CSpace_A.update_cap_data b data cap'))
 2. \<And>rv rv'. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); ?r'4 rv rv'\<rbrakk> \<Longrightarrow> dcorres r (?R4 rv) (?R'4 rv') (f rv) (f' rv')
 3. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpace_D.update_cap_data b data cap \<lbrace>?R4\<rbrace>
 4. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> return (CSpace_A.update_cap_data b data cap') \<lbrace>?R'4\<rbrace>
 5. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres r (?R4 rv) (?R'4 rv') (f rv) (f' rv')
 2. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpace_D.update_cap_data b data cap \<lbrace>?R4\<rbrace>
 3. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> return (CSpace_A.update_cap_data b data cap') \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); rv = transform_cap rv'\<rbrakk> \<Longrightarrow> dcorres r (?R4 (transform_cap rv')) (?R'4 rv') (f (transform_cap rv')) (f' rv')
 2. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpace_D.update_cap_data b data cap \<lbrace>?R4\<rbrace>
 3. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> return (CSpace_A.update_cap_data b data cap') \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> CSpace_D.update_cap_data b data cap \<lbrace>\<lambda>a. P\<rbrace>
 2. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> return (CSpace_A.update_cap_data b data cap') \<lbrace>\<lambda>a. P'\<rbrace>
 3. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> return (case transform_cap cap' of cdl_cap.EndpointCap x ba xa \<Rightarrow> if ba = 0 \<and> \<not> b then CSpace_D.badge_update data (transform_cap cap') else cdl_cap.NullCap | cdl_cap.NotificationCap x ba xa \<Rightarrow> if ba = 0 \<and> \<not> b then CSpace_D.badge_update data (transform_cap cap') else cdl_cap.NullCap | cdl_cap.CNodeCap object guard guard_size sz \<Rightarrow> let reserved_bits = 3; guard_bits = 18; guard_size_bits = 5; new_guard_size = unat ((data >> reserved_bits) && mask guard_size_bits); new_guard = (data >> reserved_bits + guard_size_bits) && mask (min (unat ((data >> reserved_bits) && mask guard_size_bits)) guard_bits) in if word_bits < new_guard_size + sz then cdl_cap.NullCap else cdl_cap.CNodeCap object new_guard new_guard_size sz | _ \<Rightarrow> transform_cap cap') \<lbrace>\<lambda>a. P\<rbrace>
 2. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> return (CSpace_A.update_cap_data b data cap') \<lbrace>\<lambda>a. P'\<rbrace>
 3. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); P s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and P) s
 2. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and P') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap = transform_cap cap'; \<And>c'. dcorres r P P' (f (transform_cap c')) (f' c'); (valid_idle and valid_cap cap' and P') s\<rbrakk> \<Longrightarrow> (valid_idle and valid_cap cap' and P') s proof (prove)
goal:
No subgoals!