kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma sts_iflive[wp]:
  "\<lbrace>\<lambda>s. (\<not> halted st \<longrightarrow> ex_nonz_cap_to t s)
         \<and> if_live_then_nonz_cap s\<rbrace>
     set_thread_state t st
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: set_thread_state_def) apply (wpsimp wp: set_object_iflive) by (fastforce dest: get_tcb_SomeD if_live_then_nonz_capD2
                simp: tcb_cap_cases_def live_def
                split: Structures_A.thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> halted st \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<not> halted st \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; if_live_then_nonz_cap s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> (live (TCB (y\<lparr>tcb_state := st\<rparr>)) \<longrightarrow> ex_nonz_cap_to t s) \<and> obj_at (same_caps (TCB (y\<lparr>tcb_state := st\<rparr>))) t s
theory TcbAcc_AI

lemma sbn_iflive[wp]:
  "\<lbrace>\<lambda>s. (bound ntfn \<longrightarrow> ex_nonz_cap_to t s)
         \<and> if_live_then_nonz_cap s\<rbrace>
     set_bound_notification t ntfn
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: set_bound_notification_def) apply (wpsimp wp: set_object_iflive) apply (fastforce dest: get_tcb_SomeD if_live_then_nonz_capD2
                   simp: tcb_cap_cases_def live_def
                   split: Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ntfn \<noteq> None \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ((\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>(\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; if_live_then_nonz_cap s; get_tcb t s = Some y\<rbrakk> \<Longrightarrow> (live (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) \<longrightarrow> ex_nonz_cap_to t s) \<and> obj_at (same_caps (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: set_thread_state_def) apply (wp|simp)+ apply (fastforce simp: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> obj_at (same_caps (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>))) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp, simp) apply (fastforce simp: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> obj_at (same_caps (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>))) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: set_thread_state_def) apply (wp|simp)+ apply (fastforce simp: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> obj_at (same_caps (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>))) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp, simp) apply (fastforce simp: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. zombies_final s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> obj_at (same_caps (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>))) t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_refs_of_helper: "
          {r. (r \<in> tcb_st_refs_of ts \<or>
               r \<in> tcb_bound_refs ntfnptr) \<and>
              snd r = TCBBound} =
          tcb_bound_refs ntfnptr" by (auto simp add: tcb_st_refs_of_def tcb_bound_refs_def split: thread_state.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {r. (r \<in> tcb_st_refs_of ts \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound} = tcb_bound_refs ntfnptr
theory TcbAcc_AI

lemma sts_refs_of[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of s) (t := tcb_st_refs_of st
                         \<union> {r. r \<in> state_refs_of s t \<and> snd r = TCBBound}))\<rbrace>
    set_thread_state t st
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD
                   simp: state_refs_of_def
                 intro!: ext) apply (simp add: get_tcb_def sts_refs_of_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(t := tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound}))\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(t := tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound}))\<rbrace> do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((state_refs_of s)(t := tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound})) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (state_refs_of (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of (tcb_state tcb) \<or> r \<in> tcb_bound_refs (tcb_bound_notification tcb)) \<and> snd r = TCBBound} = tcb_st_refs_of st \<union> tcb_bound_refs (tcb_bound_notification (the (get_tcb t s))) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma kheap_Some_state_hyp_refs_ofD:
  "kheap s p = Some ko \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko" by (rule ko_at_state_hyp_refs_ofD; simp add: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s p = Some ko \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko
theory TcbAcc_AI

lemma sts_hyp_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
    set_thread_state t st
   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp | simp del: fun_upd_apply)+ apply (clarsimp simp: get_tcb_def split: option.splits kernel_object.splits
                  simp del: fun_upd_apply) apply (subst state_hyp_refs_of_tcb_state_update; assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>P (state_hyp_refs_of s); kheap s t = Some (TCB x2)\<rbrakk> \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (x2\<lparr>tcb_state := st\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_refs_of_helper: "
          {r. (r \<in> tcb_st_refs_of ts \<or>
               r \<in> tcb_bound_refs ntfnptr) \<and>
              snd r \<noteq> TCBBound} =
          tcb_st_refs_of ts" by (auto simp add: tcb_st_refs_of_def tcb_bound_refs_def split: thread_state.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {r. (r \<in> tcb_st_refs_of ts \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r \<noteq> TCBBound} = tcb_st_refs_of ts
theory TcbAcc_AI

lemma sbn_refs_of[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of s) (t := tcb_bound_refs ntfn
                         \<union> {r. r \<in> state_refs_of s t \<and> snd r \<noteq> TCBBound}))\<rbrace>
    set_bound_notification t ntfn
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply (wp, simp) apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD
                   simp: state_refs_of_def
                 intro!: ext) apply (auto simp: get_tcb_def sbn_refs_of_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(t := tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound}))\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(t := tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound}))\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((state_refs_of s)(t := tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound})) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (state_refs_of (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_bound_refs ntfn \<union> {r. (r \<in> tcb_st_refs_of (tcb_state tcb) \<or> r \<in> tcb_bound_refs (tcb_bound_notification tcb)) \<and> snd r \<noteq> TCBBound} = tcb_st_refs_of (tcb_state (the (get_tcb t s))) \<union> tcb_bound_refs ntfn proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_hyp_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace>
    set_bound_notification t ntfn
   \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply (wp, simp del: fun_upd_apply) apply (clarsimp elim!: rsubst[where P=P] dest!: get_tcb_SomeD simp del: fun_upd_apply
                  intro!: ext) apply (subst state_hyp_refs_of_tcb_bound_ntfn_update; auto simp: get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do tcb <- gets_the (get_tcb t);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x tcb. kheap s t = Some (TCB tcb) \<Longrightarrow> state_hyp_refs_of s x = state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) x proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_thread_set:
  "set_thread_state p st = (do thread_set (tcb_state_update (\<lambda>_. st)) p;
                               do_extended_op (set_thread_state_ext p)
                            od)" by (simp add: set_thread_state_def thread_set_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_thread_state p st = do thread_set (tcb_state_update (\<lambda>_. st)) p;
do_extended_op (set_thread_state_ext p)
od
theory TcbAcc_AI

lemma set_bound_notification_thread_set:
  "set_bound_notification p ntfn = thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) p" by (simp add: set_bound_notification_def thread_set_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_bound_notification p ntfn = thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) p
theory TcbAcc_AI

lemma set_thread_state_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: set_thread_state_thread_set) apply (wp, simp, wp thread_set_caps_of_state_trivial) apply (rule ball_tcb_cap_casesI, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do y <- thread_set (tcb_state_update (\<lambda>_. st)) t;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb\<lparr>tcb_state := st\<rparr>) = getF tcb
 2. \<And>s. P (caps_of_state s) \<Longrightarrow> P (caps_of_state s) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_st_tcb_at_neq:
  "\<lbrace>pred_tcb_at proj P t and K (t\<noteq>t')\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply (wp, simp) apply (clarsimp cong: if_cong) apply (drule get_tcb_SomeD) apply (simp add: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t and K (t \<noteq> t')\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t and (\<lambda>y. t \<noteq> t')\<rbrace> do tcb <- gets_the (get_tcb t');
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t' = Some y);
return (the (kh t'))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t' \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
od \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pred_tcb_at proj P t s \<and> t \<noteq> t' \<Longrightarrow> (\<exists>y. get_tcb t' s = Some y) \<longrightarrow> (\<exists>y. kheap s t' = Some y) \<longrightarrow> a_type (the (kheap s t')) = ATCB \<longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := \<lambda>a. if a = t' then Some (TCB (the (get_tcb t' s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>pred_tcb_at proj P t s; t \<noteq> t'; get_tcb t' s = Some y; kheap s t' = Some (TCB tcb)\<rbrakk> \<Longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := \<lambda>a. if a = t' then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>pred_tcb_at proj P t s; t \<noteq> t'; kheap s t' = Some (TCB tcb); kheap s t' = Some (TCB y)\<rbrakk> \<Longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := \<lambda>a. if a = t' then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_st_tcb_at_cases:
  "\<lbrace>\<lambda>s. ((t = t') \<longrightarrow> P ts) \<and> ((t \<noteq> t') \<longrightarrow> st_tcb_at P t' s)\<rbrace>
     set_thread_state t ts
   \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>" apply (cases "t = t'", simp_all) apply (wp sts_st_tcb_at') apply simp apply (wp sts_st_tcb_at_neq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t = t' \<longrightarrow> P ts) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at P t' s)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>s. P ts\<rbrace> set_thread_state t' ts \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at P t'\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = t'; P ts\<rbrakk> \<Longrightarrow> K (P ts) s
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at P t'\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at P t'\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t \<noteq> t'; st_tcb_at P t' s\<rbrakk> \<Longrightarrow> (st_tcb_at P t' and K (t' \<noteq> t)) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_bound_tcb_at_cases:
  "\<lbrace>\<lambda>s. ((t = t') \<longrightarrow> P ntfn) \<and> ((t \<noteq> t') \<longrightarrow> bound_tcb_at P t' s)\<rbrace>
     set_bound_notification t ntfn
   \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace>" apply (cases "t = t'", simp_all) apply (wp sbn_bound_tcb_at') apply simp apply (wp sbn_st_tcb_at_neq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t = t' \<longrightarrow> P ntfn) \<and> (t \<noteq> t' \<longrightarrow> bound_tcb_at P t' s)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>\<lambda>s. P ntfn\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>bound_tcb_at P t'\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>t = t'; P ntfn\<rbrakk> \<Longrightarrow> K (P ntfn) s
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>bound_tcb_at P t'\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>bound_tcb_at P t'\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t \<noteq> t'; bound_tcb_at P t' s\<rbrakk> \<Longrightarrow> (bound_tcb_at P t' and K (t' \<noteq> t)) s proof (prove)
goal:
No subgoals!