theory Retype_R

lemma mapM_x_threadSet_valid_pspace:
  "\<lbrace>valid_pspace' and K (curdom \<le> maxDomain)\<rbrace>
    mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs \<lbrace>\<lambda>y. valid_pspace'\<rbrace>" apply (rule hoare_gen_asm) apply (wp mapM_x_wp' threadSet_valid_pspace') apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and K (curdom \<le> maxDomain)\<rbrace> mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs \<lbrace>\<lambda>y. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. curdom \<le> maxDomain \<Longrightarrow> \<lbrace>valid_pspace'\<rbrace> mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs \<lbrace>\<lambda>y. valid_pspace'\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> case (tcbCTable, tcbCTable_update) of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q)) = getF (Thread a b c d e f g h i j k l m n p q)
 2. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> case (tcbVTable, tcbVTable_update) of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q)) = getF (Thread a b c d e f g h i j k l m n p q)
 3. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> case (tcbReply, tcbReply_update) of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q)) = getF (Thread a b c d e f g h i j k l m n p q)
 4. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> case (tcbCaller, tcbCaller_update) of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q)) = getF (Thread a b c d e f g h i j k l m n p q)
 5. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> case (tcbIPCBufferFrame, tcbIPCBufferFrame_update) of (getF, setF) \<Rightarrow> getF (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q)) = getF (Thread a b c d e f g h i j k l m n p q)
 6. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> \<forall>s. valid_tcb_state' (tcbState (Thread a b c d e f g h i j k l m n p q)) s \<longrightarrow> valid_tcb_state' (tcbState (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q))) s
 7. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> \<forall>s. valid_bound_ntfn' (tcbBoundNotification (Thread a b c d e f g h i j k l m n p q)) s \<longrightarrow> valid_bound_ntfn' (tcbBoundNotification (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q))) s
 8. \<And>x a b c d e f g h i j k l m n p q. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> is_aligned (tcbIPCBuffer (Thread a b c d e f g h i j k l m n p q)) msg_align_bits \<longrightarrow> is_aligned (tcbIPCBuffer (tcbDomain_update (\<lambda>_. curdom) (Thread a b c d e f g h i j k l m n p q))) msg_align_bits
 9. \<And>x. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> \<forall>tcb. tcbDomain tcb \<le> maxDomain \<longrightarrow> tcbDomain (tcbDomain_update (\<lambda>_. curdom) tcb) \<le> maxDomain
 10. \<And>x. \<lbrakk>curdom \<le> maxDomain; x \<in> set addrs\<rbrakk> \<Longrightarrow> \<forall>tcb. tcbPriority tcb \<le> maxPriority \<longrightarrow> tcbPriority (tcbDomain_update (\<lambda>_. curdom) tcb) \<le> maxPriority
A total of 12 subgoals... proof (prove)
goal:
No subgoals!