theory IsolatedThreadAction

lemma getCTE_isolatable:
  "thread_actions_isolatable idx (getCTE p)" apply (clarsimp simp: thread_actions_isolatable_def) apply (simp add: isolate_thread_actions_def bind_assoc split_def) apply (simp add: getCTE_assert_opt bind_select_f_bind[symmetric]
                   bind_assoc select_f_returns) apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def
                        map_to_ctes_partial_overwrite) apply (simp add: assert_opt_def select_f_returns select_f_asserts
            split: option.split) apply (clarsimp simp: exec_modify o_def return_def) apply (simp add: ksPSpace_update_partial_id) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (getCTE p) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (getCTE p) (isolate_thread_actions idx (getCTE p) id id) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (getCTE p) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
p <- select_f (getCTE p s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx tcbs) (snd p\<lparr>ksSchedulerAction := sa\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (gets (\<lambda>s. ctes_of s p) >>= assert_opt) (do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
p <- select_f (assert_opt (ctes_of s p) s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx tcbs) (snd p\<lparr>ksSchedulerAction := sa\<rparr>));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> assert_opt (ctes_of s p) s = (do p <- select_f (assert_opt (ctes_of s p) (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx)) (snd p\<lparr>ksSchedulerAction := ksSchedulerAction s\<rparr>));
return (fst p)
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> \<forall>x2. ctes_of s p = Some x2 \<longrightarrow> return x2 s = (do y <- modify (\<lambda>sa. ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s);
return x2
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; ctes_of s p = Some x2\<rbrakk> \<Longrightarrow> s = ksPSpace_update (partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x)))) s proof (prove)
goal:
No subgoals!