theory TcbAcc_R

lemma threadSet_corres_noop_splitT:
  assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow>
                         tcb_relation tcb (fn tcb')"
  assumes y: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases.
                 getF (fn tcb) = getF tcb"
  assumes z: "corres r P Q' m m'"
  assumes w: "\<lbrace>P'\<rbrace> threadSet fn t \<lbrace>\<lambda>x. Q'\<rbrace>"
  assumes e: "\<And>tcb'. exst_same tcb' (fn tcb')"
  shows      "corres r P (tcb_at' t and P')
                           m (threadSet fn t >>= (\<lambda>rv. m'))" apply (rule corres_guard_imp) apply (subst return_bind[symmetric]) apply (rule corres_split_nor[OF threadSet_corres_noopT]) apply (simp add: x) apply (rule y) apply (rule e) apply (rule z) apply (wp w)+ apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P (tcb_at' t and P') m (do rv <- threadSet fn t;
m'
od) proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' m (do rv <- threadSet fn t;
m'
od)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at' t and P') s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres r ?Q ?Q' (do a <- return ?x5;
m
od) (do rv <- threadSet fn t;
m'
od)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at' t and P') s \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcb (fn tcb')
 2. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn tcb) = getF tcb
 3. \<And>tcb'. exst_same tcb' (fn tcb')
 4. corres r ?R7 ?R'7 m m'
 5. \<lbrace>?Q7\<rbrace> return ?x5 \<lbrace>\<lambda>x. ?R7\<rbrace>
 6. \<lbrace>?Q'7\<rbrace> threadSet fn t \<lbrace>\<lambda>x. ?R'7\<rbrace>
 7. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (fn tcb) = getF tcb
 2. \<And>tcb'. exst_same tcb' (fn tcb')
 3. corres r ?R7 ?R'7 m m'
 4. \<lbrace>?Q7\<rbrace> return ?x5 \<lbrace>\<lambda>x. ?R7\<rbrace>
 5. \<lbrace>?Q'7\<rbrace> threadSet fn t \<lbrace>\<lambda>x. ?R'7\<rbrace>
 6. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 7. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. \<And>tcb'. exst_same tcb' (fn tcb')
 2. corres r ?R7 ?R'7 m m'
 3. \<lbrace>?Q7\<rbrace> return ?x5 \<lbrace>\<lambda>x. ?R7\<rbrace>
 4. \<lbrace>?Q'7\<rbrace> threadSet fn t \<lbrace>\<lambda>x. ?R'7\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 6. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. corres r ?R7 ?R'7 m m'
 2. \<lbrace>?Q7\<rbrace> return ?x5 \<lbrace>\<lambda>x. ?R7\<rbrace>
 3. \<lbrace>?Q'7\<rbrace> threadSet fn t \<lbrace>\<lambda>x. ?R'7\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 5. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and ?Q'7) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q7\<rbrace> return ?x5 \<lbrace>\<lambda>x. P\<rbrace>
 2. \<lbrace>?Q'7\<rbrace> threadSet fn t \<lbrace>\<lambda>x. Q'\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 4. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and ?Q'7) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and P) s
 2. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and P') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at' t and P') s \<Longrightarrow> (tcb_at' t and P') s proof (prove)
goal:
No subgoals!