theory Ipc_IF

lemma sts_no_fail:
  "no_fail (\<lambda>s :: det_state. tcb_at tcb s) (set_thread_state tcb st)" apply (simp add: set_thread_state_def set_object_def) apply (simp add: set_thread_state_ext_def get_thread_state_def
                   thread_get_def set_scheduler_action_def) apply (rule no_fail_pre) apply (wpsimp wp: get_object_wp)+ apply (clarsimp simp: get_tcb_def tcb_at_def obj_at_def a_type_def is_tcb_def
                 split: kernel_object.splits option.splits) by (metis kernel_object.exhaust option.inject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at tcb) (set_thread_state tcb st) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at tcb) (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) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at tcb) (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;
tcba <- gets_the (get_tcb tcb);
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable (tcb_state tcba) \<and> cur = tcb \<and> action = resume_cur_thread) (modify (scheduler_action_update (\<lambda>_. choose_new_thread)))
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (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;
tcba <- gets_the (get_tcb tcb);
cur <- gets cur_thread;
action <- gets scheduler_action;
when (\<not> runnable (tcb_state tcba) \<and> cur = tcb \<and> action = resume_cur_thread) (modify (scheduler_action_update (\<lambda>_. choose_new_thread)))
od)
 2. \<And>s. tcb_at tcb s \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at tcb s \<Longrightarrow> (\<exists>y. get_tcb tcb s = Some y) \<and> ((\<exists>y. get_tcb tcb s = Some y) \<longrightarrow> obj_at (\<lambda>_. True) tcb s \<and> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB) \<and> (\<forall>ko. ko_at ko tcb s \<longrightarrow> a_type ko = ATCB \<longrightarrow> (\<exists>y. get_tcb 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>) = Some y))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>\<forall>x11 x12. ko \<noteq> CNode x11 x12; (\<forall>x2. ko \<noteq> TCB x2) \<or> kheap s tcb = Some ko; \<forall>x3. ko \<noteq> Endpoint x3; \<forall>x4. ko \<noteq> Notification x4; \<forall>x5. ko \<noteq> ArchObj x5\<rbrakk> \<Longrightarrow> (\<exists>y. kheap s tcb = Some y) \<and> (\<forall>x2. (\<forall>x11 x12. x2 = CNode x11 x12 \<longrightarrow> kheap s tcb \<noteq> Some (CNode x11 x12)) \<and> (\<forall>x3. x2 = Endpoint x3 \<longrightarrow> kheap s tcb \<noteq> Some (Endpoint x3)) \<and> (\<forall>x4. x2 = Notification x4 \<longrightarrow> kheap s tcb \<noteq> Some (Notification x4)) \<and> (\<forall>x5. x2 = ArchObj x5 \<longrightarrow> kheap s tcb \<noteq> Some (ArchObj x5)))