theory IsolatedThreadAction

lemma setEndpoint_isolatable:
  "thread_actions_isolatable idx (setEndpoint p e)" supply if_split[split del] apply (simp add: setEndpoint_def setObject_modify_assert
                   assert_def) apply (case_tac "p \<in> range idx") apply (clarsimp simp: thread_actions_isolatable_def
                         monadic_rewrite_def fun_eq_iff
                         liftM_def isolate_thread_actions_def
                         bind_assoc exec_gets getSchedulerAction_def
                         bind_select_f_bind[symmetric]) apply (simp add: obj_at_partial_overwrite_id2) apply (drule_tac x=x in spec) apply (clarsimp simp: obj_at'_def projectKOs select_f_asserts) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               thread_actions_isolatable_if
               thread_actions_isolatable_return
               thread_actions_isolatable_fail) apply (rule gets_isolatable) apply (simp add: obj_at_partial_overwrite_id2) apply (rule modify_isolatable) apply (clarsimp simp: o_def partial_overwrite_def) apply (rule kernel_state.fold_congs[OF refl refl]) apply (clarsimp simp: fun_eq_iff
                     split: if_split) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setEndpoint p e) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (setEndpoint p e) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (2 subgoals):
 1. p \<in> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od)
 2. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>p = idx x; inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- if ep_at' (idx x) s then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e)))
od) s = (do xa <- select_f ((if ep_at' (idx x) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s) then return () else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
(rv, s') <- select_f (modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e))) (snd xa));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>p = idx x; inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- if ep_at' (idx x) s then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e)))
od) s = (do xa <- select_f ((if ep_at' (idx x) s then return () else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
(rv, s') <- select_f (modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e))) (snd xa));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>p = idx x; inj idx; tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- if ep_at' (idx x) s then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e)))
od) s = (do xa <- select_f ((if ep_at' (idx x) s then return () else fail) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
(rv, s') <- select_f (modify (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOEndpoint e))) (snd xa));
modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (s'\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>))
od) s
 2. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (1 subgoal):
 1. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (do f <- gets (ep_at' p);
y <- if f then return () else fail;
modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)))
od) proof (prove)
goal (6 subgoals):
 1. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (gets (ep_at' p))
 2. \<And>x xa. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e))))
 3. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 5. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (6 subgoals):
 1. \<And>g s. \<lbrakk>p \<notin> range idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ep_at' p (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = ep_at' p s
 2. \<And>x xa. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e))))
 3. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 5. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 6. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. p \<notin> range idx \<Longrightarrow> thread_actions_isolatable idx (modify (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e))))
 2. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 4. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 5. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (5 subgoals):
 1. \<And>x xa tsrs act s. \<lbrakk>p \<notin> range idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ksPSpace_update (partial_overwrite idx tsrs) (ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)) s\<lparr>ksSchedulerAction := act\<rparr>) = ksPSpace_update (\<lambda>ps. ps(p \<mapsto> KOEndpoint e)) (ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>))
 2. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 4. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 5. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (5 subgoals):
 1. \<And>tsrs act s. \<lbrakk>p \<notin> range idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ksPSpace_update (\<lambda>x xa. if xa \<in> range idx then put_tcb_state_regs (tsrs (inv idx xa)) (if xa = p then Some (KOEndpoint e) else x xa) else if xa = p then Some (KOEndpoint e) else x xa) (s\<lparr>ksSchedulerAction := act\<rparr>) = ksPSpace_update (\<lambda>x. (\<lambda>xa. if xa \<in> range idx then put_tcb_state_regs (tsrs (inv idx xa)) (x xa) else x xa)(p \<mapsto> KOEndpoint e)) (s\<lparr>ksSchedulerAction := act\<rparr>)
 2. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 4. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 5. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (5 subgoals):
 1. \<And>tsrs act s v. \<lbrakk>p \<notin> range idx; \<forall>x. tcb_at' (idx x) s; ksPSpace (s\<lparr>ksSchedulerAction := act\<rparr>) = v\<rbrakk> \<Longrightarrow> (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (if x = p then Some (KOEndpoint e) else v x) else if x = p then Some (KOEndpoint e) else v x) = (\<lambda>x. if x \<in> range idx then put_tcb_state_regs (tsrs (inv idx x)) (v x) else v x)(p \<mapsto> KOEndpoint e)
 2. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 3. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 4. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 5. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal (4 subgoals):
 1. \<And>x t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q36 x t\<rbrace> if x then return () else fail \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 2. \<And>x t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q36 x t s
 3. \<And>t. p \<notin> range idx \<Longrightarrow> \<lbrace>?Q32 t\<rbrace> gets (ep_at' p) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>t s. \<lbrakk>p \<notin> range idx; tcb_at' t s\<rbrakk> \<Longrightarrow> ?Q32 t s proof (prove)
goal:
No subgoals!