theory Tcb_R

lemma threadSet_valid_objs_tcbPriority_update:
  "\<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace>
     threadSet (tcbPriority_update (\<lambda>_. x)) t
   \<lbrace>\<lambda>_. valid_objs'\<rbrace>" 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'_tcbPriority_update) apply (fastforce  simp: obj_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace> threadSet (tcbPriority_update (\<lambda>_. x)) t \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace> do tcb <- getObject t;
setObject t (tcbPriority_update (\<lambda>_. x) tcb)
od \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?B tcb\<rbrace> setObject t (tcbPriority_update (\<lambda>_. x) tcb) \<lbrace>\<lambda>_. valid_objs'\<rbrace>
 2. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace> getObject t \<lbrace>?B\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority)\<rbrace> getObject t \<lbrace>?B\<rbrace>
 2. \<And>tcb. \<lbrace>?B tcb\<rbrace> setObject t (tcbPriority_update (\<lambda>_. x) tcb) \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrace>valid_objs' and (\<lambda>_. x \<le> maxPriority) and ko_at' tcb t\<rbrace> setObject t (tcbPriority_update (\<lambda>_. x) tcb) \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrace>?Q2 tcb\<rbrace> setObject t (tcbPriority_update (\<lambda>_. x) tcb) \<lbrace>\<lambda>_. valid_objs'\<rbrace>
 2. \<And>tcb s. (valid_objs' and (\<lambda>_. x \<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>_. x \<le> maxPriority) and ko_at' tcb t) s \<Longrightarrow> (valid_objs' and (tcb_at' t and valid_obj' (injectKOS (tcbPriority_update (\<lambda>_. x) tcb)))) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s ko. \<lbrakk>valid_objs' s; x \<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; x \<le> maxPriority; ko_at' tcb t s; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_obj' (injectKOS tcb) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s
 2. \<And>tcb s. \<lbrakk>valid_objs' s; x \<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; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. x) tcb) s
 2. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal (3 subgoals):
 1. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_tcb' tcb s
 2. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s; tcb_at' t s\<rbrakk> \<Longrightarrow> x \<le> maxPriority
 3. \<And>tcb s. \<lbrakk>valid_objs' s; x \<le> maxPriority; ko_at' tcb t s; valid_tcb' tcb s\<rbrakk> \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!