theory Tcb_R

lemma setMCPriority_valid_objs'[wp]:
  "\<lbrace>valid_objs' and K (prio \<le> maxPriority)\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" unfolding setMCPriority_def including no_pre apply (simp add: threadSet_def) apply wp prefer 2 apply (rule getObject_tcb_sp) apply (rule hoare_weaken_pre) apply (rule setObject_tcb_valid_objs) apply (clarsimp simp: valid_obj'_def) apply (frule (1) ko_at_valid_objs') apply (simp add: projectKOs) apply (simp add: valid_obj'_def) apply (subgoal_tac "tcb_at' t s") apply simp apply (rule valid_tcb'_tcbMCP_update) apply (fastforce  simp: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (prio \<le> maxPriority)\<rbrace> setMCPriority t prio \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (prio \<le> maxPriority)\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (prio \<le> maxPriority)\<rbrace> threadSet (tcbMCP_update (\<lambda>_. prio)) t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>y. prio \<le> maxPriority)\<rbrace> do tcb <- getObject t;
setObject t (tcbMCP_update (\<lambda>_. prio) tcb)
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?B tcb\<rbrace> setObject t (tcbMCP_update (\<lambda>_. prio) tcb) \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<lbrace>valid_objs' and (\<lambda>y. prio \<le> maxPriority)\<rbrace> getObject t \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs' and (\<lambda>y. prio \<le> maxPriority)\<rbrace> getObject t \<lbrace>?B\<rbrace>
 2. \<And>tcb. \<lbrace>?B tcb\<rbrace> setObject t (tcbMCP_update (\<lambda>_. prio) tcb) \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrace>valid_objs' and (\<lambda>y. prio \<le> maxPriority) and ko_at' tcb t\<rbrace> setObject t (tcbMCP_update (\<lambda>_. prio) tcb) \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?Q2 tcb\<rbrace> setObject t (tcbMCP_update (\<lambda>_. prio) tcb) \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>tcb s. (valid_objs' and (\<lambda>y. prio \<le> maxPriority) and ko_at' tcb t) s \<Longrightarrow> ?Q2 tcb s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. (valid_objs' and (\<lambda>y. prio \<le> maxPriority) and ko_at' tcb t) s \<Longrightarrow> (valid_objs' and (tcb_at' t and valid_obj' (injectKOS (tcbMCP_update (\<lambda>_. prio) tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s ko. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; projectKO_opt ko = Some tcb\<rbrakk> \<Longrightarrow> injectKOS tcb = ko
 2. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s
 2. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_tcb' (tcbMCP_update (\<lambda>_. prio) tcb) s
 2. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_tcb' tcb s \<and> prio \<le> maxPriority
 2. \<And>tcb s. \<lbrakk>valid_objs' s; prio \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!