theory Ipc_IF

lemma sts_to_modify':
  "monadic_rewrite True True (tcb_at tcb and (\<lambda>s :: det_state. tcb \<noteq> cur_thread s))
     (set_thread_state tcb st)
     (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))" apply (clarsimp simp: set_thread_state_def set_object_def) apply (monadic_rewrite_l sts_noop \<open>wpsimp wp: get_object_wp\<close>) apply (simp add: bind_assoc) apply monadic_rewrite_symb_exec_l+ apply (rule_tac P="\<lambda>s'. s' = s \<and> tcba = the (get_tcb tcb s)" in monadic_rewrite_pre_imp_eq) apply (clarsimp simp: put_def modify_def get_def bind_def) apply (wpsimp wp: get_object_wp)+ by (clarsimp simp: get_tcb_def tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (set_thread_state tcb st) (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (do tcba <- gets_the (get_tcb tcb);
y <- do kobj <- get_object tcb;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
set_thread_state_ext tcb
od) (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do tcba <- gets_the (get_tcb tcb);
y <- do kobj <- get_object tcb;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
return ()
od) (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))
 2. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite True True ?Q1 (do tcba <- gets_the (get_tcb tcb);
kobj <- get_object tcb;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_state := st\<rparr>))\<rparr>)
od) (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))
 2. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))) and ?Q1) s proof (prove)
goal (6 subgoals):
 1. \<And>tcba kobj y s. monadic_rewrite True True (?Q117 tcba kobj y s) (put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_state := st\<rparr>))\<rparr>)) (modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))
 2. \<And>tcb kobj y. \<lbrace>?Q91 tcb kobj y\<rbrace> get \<lbrace>?Q117 tcb kobj y\<rbrace>
 3. \<And>tcb kobj. \<lbrace>?Q65 tcb kobj\<rbrace> assert (a_type kobj = ATCB) \<lbrace>?Q91 tcb kobj\<rbrace>
 4. \<And>tcba. \<lbrace>?Q38 tcba\<rbrace> get_object tcb \<lbrace>?Q65 tcba\<rbrace>
 5. \<lbrace>?Q1\<rbrace> gets_the (get_tcb tcb) \<lbrace>?Q38\<rbrace>
 6. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))) and ?Q1) s proof (prove)
goal (6 subgoals):
 1. \<And>tcba kobj y s sa. sa = s \<and> tcba = the (get_tcb tcb s) \<Longrightarrow> put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_state := st\<rparr>))\<rparr>) sa = modify (\<lambda>s. s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>) sa
 2. \<And>tcba kobj y. \<lbrace>?Q91 tcba kobj y\<rbrace> get \<lbrace>\<lambda>s s'. s' = s \<and> tcba = the (get_tcb tcb s)\<rbrace>
 3. \<And>tcb kobj. \<lbrace>?Q65 tcb kobj\<rbrace> assert (a_type kobj = ATCB) \<lbrace>?Q91 tcb kobj\<rbrace>
 4. \<And>tcba. \<lbrace>?Q38 tcba\<rbrace> get_object tcb \<lbrace>?Q65 tcba\<rbrace>
 5. \<lbrace>?Q1\<rbrace> gets_the (get_tcb tcb) \<lbrace>?Q38\<rbrace>
 6. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))) and ?Q1) s proof (prove)
goal (5 subgoals):
 1. \<And>tcba kobj y. \<lbrace>?Q91 tcba kobj y\<rbrace> get \<lbrace>\<lambda>s s'. s' = s \<and> tcba = the (get_tcb tcb s)\<rbrace>
 2. \<And>tcb kobj. \<lbrace>?Q65 tcb kobj\<rbrace> assert (a_type kobj = ATCB) \<lbrace>?Q91 tcb kobj\<rbrace>
 3. \<And>tcba. \<lbrace>?Q38 tcba\<rbrace> get_object tcb \<lbrace>?Q65 tcba\<rbrace>
 4. \<lbrace>?Q1\<rbrace> gets_the (get_tcb tcb) \<lbrace>?Q38\<rbrace>
 5. \<And>s. (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) s \<Longrightarrow> ((\<lambda>s. get_tcb tcb s \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (tcb_at tcb and (\<lambda>s. tcb \<noteq> cur_thread s)) (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>))\<rparr>))) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcba. \<lbrakk>tcb_at tcb s; tcb \<noteq> cur_thread s; get_tcb tcb s = Some y; ko_at (TCB tcba) tcb s\<rbrakk> \<Longrightarrow> tcb_at tcb (s\<lparr>kheap := \<lambda>a. if a = tcb then Some (TCB (the (get_tcb tcb s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)