theory IsolatedThreadAction

lemma threadGet_isolatable:
  assumes v: "\<And>tsr. \<forall>tcb. f (put_tcb_state_regs_tcb tsr tcb) = f tcb"
  shows "thread_actions_isolatable idx (threadGet f t)" apply (clarsimp simp: threadGet_def thread_actions_isolatable_def
                        isolate_thread_actions_def split_def
                        getObject_get_assert liftM_def
                        bind_select_f_bind[symmetric]
                        select_f_returns select_f_asserts bind_assoc) apply (clarsimp simp: monadic_rewrite_def exec_gets
                        getSchedulerAction_def) apply (simp add: obj_at_partial_overwrite_If) apply (rule bind_apply_cong[OF refl]) apply (clarsimp simp: exec_gets exec_modify o_def
                        ksPSpace_update_partial_id in_monad) apply (erule obj_atE') apply (clarsimp simp: projectKOs
                        partial_overwrite_def put_tcb_state_regs_def
                  cong: if_cong) apply (simp add: projectKO_opt_tcb v split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (threadGet f t) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (do v <- gets (tcb_at' t);
y <- assert v;
x <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) t \<circ> ksPSpace);
return (f x)
od) (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;
y <- assert (tcb_at' t s);
y <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return (f (the (projectKO_opt (the (ksPSpace s t)))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- assert (tcb_at' t s);
x <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) t \<circ> ksPSpace);
return (f x)
od) s = (do y <- assert (tcb_at' t (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s));
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 (f (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) t)))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> (do y <- assert (tcb_at' t s);
x <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) t \<circ> ksPSpace);
return (f x)
od) s = (do y <- assert (tcb_at' t s);
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 (f (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) t)))))
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s rv st. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; (rv, st) \<in> fst (assert (tcb_at' t s) s)\<rbrakk> \<Longrightarrow> (do x <- gets (the \<circ> projectKO_opt \<circ> the \<circ> swp ($) t \<circ> ksPSpace);
return (f x)
od) st = (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 (f (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) t)))))
od) st proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; tcb_at' t s\<rbrakk> \<Longrightarrow> return (f (the (projectKO_opt (the (ksPSpace s t))))) s = return (f (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) t))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; True; ps_clear t (objBitsKO ko) s\<rbrakk> \<Longrightarrow> return (f (the (projectKO_opt (the (ksPSpace s t))))) s = return (f (the (projectKO_opt (the (partial_overwrite idx (\<lambda>y. undefined) (ksPSpace s) t))))) s proof (prove)
goal (1 subgoal):
 1. \<And>s obj x. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s; ksPSpace s (idx x) = Some (KOTCB obj); is_aligned (idx x) (objBitsKO (KOTCB obj)); ps_clear (idx x) (objBitsKO (KOTCB obj)) s; t = idx x\<rbrakk> \<Longrightarrow> return (f (the (projectKO_opt (KOTCB obj)))) s = return (f (the (projectKO_opt (KOTCB (put_tcb_state_regs_tcb undefined obj))))) s proof (prove)
goal:
No subgoals!