kings-crown/FVELER_Isabelle huggingface dataset:
theory IsolatedThreadAction

lemma put_tcb_state_regs_twice[simp]:
  "put_tcb_state_regs tsr (put_tcb_state_regs tsr' tcb)
    = put_tcb_state_regs tsr tcb" apply (simp add: put_tcb_state_regs_def put_tcb_state_regs_tcb_def
                   makeObject_tcb
            split: tcb_state_regs.split option.split
                   Structures_H.kernel_object.split) apply (intro all_tcbI impI allI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. put_tcb_state_regs tsr (put_tcb_state_regs tsr' tcb) = put_tcb_state_regs tsr tcb proof (prove)
goal (1 subgoal):
 1. \<forall>x6. tcb = Some (KOTCB x6) \<longrightarrow> (\<forall>x1 x2. tsr' = TCBStateRegs x1 x2 \<longrightarrow> (\<forall>x1a x2a. tsr = TCBStateRegs x1a x2a \<longrightarrow> tcbArch_update (\<lambda>_. atcbContextSet x2a (tcbArch x6)) (tcbState_update (\<lambda>_. x1a) (tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch x6)) (tcbState_update (\<lambda>_. x1) x6))) = tcbArch_update (\<lambda>_. atcbContextSet x2a (tcbArch x6)) (tcbState_update (\<lambda>_. x1a) x6))) proof (prove)
goal (1 subgoal):
 1. \<And>a b c d e f g h i j k l m n p q x1 x2 x1a x2a. \<lbrakk>tcb = Some (KOTCB (Thread a b c d e f g h i j k l m n p q)); tsr' = TCBStateRegs x1 x2; tsr = TCBStateRegs x1a x2a\<rbrakk> \<Longrightarrow> tcbArch_update (\<lambda>_. atcbContextSet x2a (tcbArch (Thread a b c d e f g h i j k l m n p q))) (tcbState_update (\<lambda>_. x1a) (tcbArch_update (\<lambda>_. atcbContextSet x2 (tcbArch (Thread a b c d e f g h i j k l m n p q))) (tcbState_update (\<lambda>_. x1) (Thread a b c d e f g h i j k l m n p q)))) = tcbArch_update (\<lambda>_. atcbContextSet x2a (tcbArch (Thread a b c d e f g h i j k l m n p q))) (tcbState_update (\<lambda>_. x1a) (Thread a b c d e f g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma partial_overwrite_twice[simp]:
  "partial_overwrite idx f (partial_overwrite idx g ps)
       = partial_overwrite idx f ps" by (rule ext, simp add: partial_overwrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partial_overwrite idx f (partial_overwrite idx g ps) = partial_overwrite idx f ps
theory IsolatedThreadAction

lemma get_tcb_state_regs_partial_overwrite[simp]:
  "inj idx \<Longrightarrow>
   get_tcb_state_regs (partial_overwrite idx tcbs f (idx x))
      = tcbs x" apply (simp add: partial_overwrite_def) apply (simp add: put_tcb_state_regs_def
                   get_tcb_state_regs_def
                   put_tcb_state_regs_tcb_def
            split: tcb_state_regs.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> get_tcb_state_regs (partial_overwrite idx tcbs f (idx x)) = tcbs x proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> get_tcb_state_regs (put_tcb_state_regs (tcbs x) (f (idx x))) = tcbs x proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma partial_overwrite_fun_upd:
  "inj idx \<Longrightarrow>
   partial_overwrite idx (tsrs (x := y))
    = (\<lambda>ps. (partial_overwrite idx tsrs ps) (idx x := put_tcb_state_regs y (ps (idx x))))" apply (intro ext, simp add: partial_overwrite_def) apply (clarsimp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> partial_overwrite idx (tsrs(x := y)) = (\<lambda>ps. (partial_overwrite idx tsrs ps)(idx x := put_tcb_state_regs y (ps (idx x)))) proof (prove)
goal (1 subgoal):
 1. \<And>ps xa. inj idx \<Longrightarrow> inv idx xa = x \<longrightarrow> xa \<in> range idx \<longrightarrow> xa \<noteq> idx x \<longrightarrow> put_tcb_state_regs y (ps xa) = put_tcb_state_regs (tsrs x) (ps xa) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma get_tcb_state_regs_ko_at':
  "ko_at' ko p s \<Longrightarrow> get_tcb_state_regs (ksPSpace s p)
       = TCBStateRegs (tcbState ko) ((atcbContextGet o tcbArch) ko)" by (clarsimp simp: obj_at'_def projectKOs get_tcb_state_regs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<Longrightarrow> get_tcb_state_regs (ksPSpace s p) = TCBStateRegs (tcbState ko) ((atcbContextGet \<circ> tcbArch) ko)
theory IsolatedThreadAction

lemma put_tcb_state_regs_ko_at':
  "ko_at' ko p s \<Longrightarrow> put_tcb_state_regs tsr (ksPSpace s p)
       = Some (KOTCB (ko \<lparr> tcbState := tsrState tsr
                         , tcbArch := atcbContextSet (tsrContext tsr) (tcbArch ko)\<rparr>))" by (clarsimp simp: obj_at'_def projectKOs put_tcb_state_regs_def
                     put_tcb_state_regs_tcb_def
              split: tcb_state_regs.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<Longrightarrow> put_tcb_state_regs tsr (ksPSpace s p) = Some (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet (tsrContext tsr) (tcbArch ko)) (tcbState_update (\<lambda>_. tsrState tsr) ko)))
theory IsolatedThreadAction

lemma partial_overwrite_get_tcb_state_regs:
  "\<lbrakk> \<forall>x. tcb_at' (idx x) s; inj idx \<rbrakk> \<Longrightarrow>
   partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x)))
                (ksPSpace s) = ksPSpace s" apply (rule ext, simp add: partial_overwrite_def
                      split: if_split) apply clarsimp apply (drule_tac x=xa in spec) apply (clarsimp simp: obj_at'_def projectKOs put_tcb_state_regs_def
                        get_tcb_state_regs_def put_tcb_state_regs_tcb_def) apply (case_tac obj, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> partial_overwrite idx (\<lambda>x. get_tcb_state_regs (ksPSpace s (idx x))) (ksPSpace s) = ksPSpace s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> x \<in> range idx \<longrightarrow> put_tcb_state_regs (get_tcb_state_regs (ksPSpace s (idx (inv idx x)))) (ksPSpace s x) = ksPSpace s x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> put_tcb_state_regs (get_tcb_state_regs (ksPSpace s (idx xa))) (ksPSpace s (idx xa)) = ksPSpace s (idx xa) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>inj idx; tcb_at' (idx xa) s\<rbrakk> \<Longrightarrow> put_tcb_state_regs (get_tcb_state_regs (ksPSpace s (idx xa))) (ksPSpace s (idx xa)) = ksPSpace s (idx xa) proof (prove)
goal (1 subgoal):
 1. \<And>xa obj. \<lbrakk>inj idx; ksPSpace s (idx xa) = Some (KOTCB obj); is_aligned (idx xa) (objBitsKO (KOTCB obj)); ps_clear (idx xa) (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> tcbArch_update (\<lambda>_. tcbArch obj) (tcbState_update (\<lambda>_. tcbState obj) obj) = obj proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma ksPSpace_update_partial_id:
  "\<lbrakk> \<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x);
       \<forall>x. tcb_at' (idx x) s; inj idx \<rbrakk> \<Longrightarrow>
   ksPSpace_update (\<lambda>ps. partial_overwrite idx (\<lambda>x. get_tcb_state_regs (f ps x)) ps) s
      = s" apply (rule trans, rule kernel_state.fold_congs[OF refl refl]) apply (erule_tac x="ksPSpace s" in meta_allE) apply (clarsimp simp: partial_overwrite_get_tcb_state_regs) apply (rule refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> ksPSpace_update (\<lambda>ps. partial_overwrite idx (\<lambda>x. get_tcb_state_regs (f ps x)) ps) s = s proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx; ksPSpace s = v\<rbrakk> \<Longrightarrow> partial_overwrite idx (\<lambda>x. get_tcb_state_regs (f v x)) v = ?f'3 v
 2. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> ksPSpace_update ?f'3 s = s proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>\<forall>x. tcb_at' (idx x) s; inj idx; ksPSpace s = v; \<And>x. f (ksPSpace s) x = ksPSpace s (idx x) \<or> f (ksPSpace s) x = ksPSpace s (idx x)\<rbrakk> \<Longrightarrow> partial_overwrite idx (\<lambda>x. get_tcb_state_regs (f v x)) v = ?f'3 v
 2. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> ksPSpace_update ?f'3 s = s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x. tcb_at' (idx x) s; inj idx; \<And>x. f (ksPSpace s) x = ksPSpace s (idx x)\<rbrakk> \<Longrightarrow> ksPSpace s = ?f'3 (ksPSpace s)
 2. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> ksPSpace_update ?f'3 s = s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ps x. f ps x = ps (idx x) \<or> f ps x = ksPSpace s (idx x); \<forall>x. tcb_at' (idx x) s; inj idx\<rbrakk> \<Longrightarrow> ksPSpace_update (\<lambda>a. a) s = s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma setRegister_simple:
  "setRegister r v = (\<lambda>con. ({((), con (r := v))}, False))" by (simp add: setRegister_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setRegister r v = (\<lambda>con. ({((), con(r := v))}, False))
theory IsolatedThreadAction

lemma zipWithM_setRegister_simple:
  "zipWithM_x setRegister rs vs
      = (\<lambda>con. ({((), foldl (\<lambda>con (r, v). con (r := v)) con (zip rs vs))}, False))" supply if_split[split del] apply (simp add: zipWithM_x_mapM_x) apply (induct ("zip rs vs")) apply (simp add: mapM_x_Nil return_def) apply (clarsimp simp add: mapM_x_Cons bind_def setRegister_def
                            simpler_modify_def fun_upd_def[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWithM_x setRegister rs vs = (\<lambda>con. ({((), foldl (\<lambda>con (r, v). con(r := v)) con (zip rs vs))}, False)) proof (prove)
goal (1 subgoal):
 1. zipWithM_x setRegister rs vs = (\<lambda>con. ({((), foldl (\<lambda>con (r, v). con(r := v)) con (zip rs vs))}, False)) proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>(x, y). setRegister x y) (zip rs vs) = (\<lambda>con. ({((), foldl (\<lambda>con (r, v). con(r := v)) con (zip rs vs))}, False)) proof (prove)
goal (2 subgoals):
 1. mapM_x (\<lambda>a. case a of (x, y) \<Rightarrow> setRegister x y) [] = (\<lambda>con. ({((), foldl (\<lambda>con a. case a of (r, v) \<Rightarrow> con(r := v)) con [])}, False))
 2. \<And>a list. mapM_x (\<lambda>a. case a of (x, y) \<Rightarrow> setRegister x y) list = (\<lambda>con. ({((), foldl (\<lambda>con a. case a of (r, v) \<Rightarrow> con(r := v)) con list)}, False)) \<Longrightarrow> mapM_x (\<lambda>a. case a of (x, y) \<Rightarrow> setRegister x y) (a # list) = (\<lambda>con. ({((), foldl (\<lambda>con a. case a of (r, v) \<Rightarrow> con(r := v)) con (a # list))}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>a list. mapM_x (\<lambda>a. case a of (x, y) \<Rightarrow> setRegister x y) list = (\<lambda>con. ({((), foldl (\<lambda>con a. case a of (r, v) \<Rightarrow> con(r := v)) con list)}, False)) \<Longrightarrow> mapM_x (\<lambda>a. case a of (x, y) \<Rightarrow> setRegister x y) (a # list) = (\<lambda>con. ({((), foldl (\<lambda>con a. case a of (r, v) \<Rightarrow> con(r := v)) con (a # list))}, False)) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma dom_partial_overwrite:
  "\<forall>x. tcb_at' (idx x) s \<Longrightarrow> dom (partial_overwrite idx tsrs (ksPSpace s))
       = dom (ksPSpace s)" apply (rule set_eqI) apply (clarsimp simp: dom_def partial_overwrite_def put_tcb_state_regs_def
                 split: if_split) apply (fastforce elim!: obj_atE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> dom (partial_overwrite idx tsrs (ksPSpace s)) = dom (ksPSpace s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> (x \<in> dom (partial_overwrite idx tsrs (ksPSpace s))) = (x \<in> dom (ksPSpace s)) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> \<exists>y. ksPSpace s (idx xa) = Some y proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma objBits_2n:
  "(1 :: word32) < 2 ^ objBits obj" by (simp add: objBits_simps' archObjSize_def pageBits_def
                pteBits_def pdeBits_def
         split: kernel_object.split arch_kernel_object.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < 2 ^ objBits obj
theory IsolatedThreadAction

lemma obj_at_partial_overwrite_id1:
  "\<lbrakk> p \<notin> range idx; \<forall>x. tcb_at' (idx x) s \<rbrakk>
    \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s)
             = obj_at' P p s" apply (drule dom_partial_overwrite[where tsrs=f]) apply (simp add: obj_at'_def ps_clear_def partial_overwrite_def
                   projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> range idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = obj_at' P p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<notin> range idx; dom (partial_overwrite idx f (ksPSpace s)) = dom (ksPSpace s)\<rbrakk> \<Longrightarrow> obj_at' P p (ksPSpace_update (partial_overwrite idx f) s) = obj_at' P p s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma gets_isolatable:
  "\<lbrakk>\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow>
        f (ksSchedulerAction_update g
             (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s \<rbrakk> \<Longrightarrow>
   thread_actions_isolatable idx (gets f)" apply (clarsimp simp: thread_actions_isolatable_def) apply (simp add: isolate_thread_actions_def select_f_returns
                   liftM_def bind_assoc) apply (clarsimp simp: monadic_rewrite_def exec_gets
                   getSchedulerAction_def exec_modify) apply (simp add: simpler_gets_def return_def
                   ksPSpace_update_partial_id o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> f (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s) \<Longrightarrow> thread_actions_isolatable idx (gets f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> f (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s; inj idx\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (gets f) (isolate_thread_actions idx (gets f) id id) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> f (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s; inj idx\<rbrakk> \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (gets f) (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 <- modify (\<lambda>sb. ksPSpace_update (partial_overwrite idx tcbs) (s\<lparr>ksSchedulerAction := sa\<rparr>));
return (f s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>g s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> f (ksSchedulerAction_update g (ksPSpace_update (partial_overwrite idx (\<lambda>_. undefined)) s)) = f s; inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> gets f s = return (f s) (ksPSpace_update (partial_overwrite idx (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx) \<circ> partial_overwrite idx (\<lambda>y. undefined)) s) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma kernelExitAssertions_isolatable:
  "thread_actions_isolatable idx (stateAssert kernelExitAssertions [])" unfolding stateAssert_def kernelExitAssertions_def apply (clarsimp simp: thread_actions_isolatable_def get_def assert_def bind_def) apply (simp add: isolate_thread_actions_def select_f_returns liftM_def bind_assoc) apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def exec_modify
                  split: if_split) apply (simp add: simpler_gets_def return_def fail_def modify_def get_def put_def
                   ksPSpace_update_partial_id o_def bind_def select_f_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (stateAssert kernelExitAssertions []) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do s <- get;
assert (0 < ksDomainTime s \<and> valid_domain_list' s)
od) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (\<lambda>s. (if 0 < ksDomainTime s \<and> valid_domain_list' s then return () else fail) s) (isolate_thread_actions idx (\<lambda>s. (if 0 < ksDomainTime s \<and> valid_domain_list' s then return () else fail) s) id id) proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (\<lambda>s. (if 0 < ksDomainTime s \<and> valid_domain_list' s then return () else fail) s) (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;
(rv, s') <- select_f ((if 0 < ksDomainTime s \<and> valid_domain_list' s then return () else fail) s);
modify (\<lambda>s. ksPSpace_update (partial_overwrite idx tcbs) (s'\<lparr>ksSchedulerAction := sa\<rparr>))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. inj idx \<Longrightarrow> (0 < ksDomainTime s \<and> valid_domain_list' s \<longrightarrow> (\<forall>x. tcb_at' (idx x) s) \<longrightarrow> return () s = (do (rv, s') <- select_f (return () (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>));
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) \<and> ((0 < ksDomainTime s \<longrightarrow> \<not> valid_domain_list' s) \<longrightarrow> (\<forall>x. tcb_at' (idx x) s) \<longrightarrow> fail s = (do (rv, s') <- select_f (fail s);
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) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma thread_actions_isolatable_return:
  "thread_actions_isolatable idx (return v)" apply (clarsimp simp: thread_actions_isolatable_def
                        monadic_rewrite_def liftM_def
                        isolate_thread_actions_def
                        split_def bind_assoc select_f_returns
                        exec_gets getSchedulerAction_def) apply (simp add: exec_modify return_def o_def
                   ksPSpace_update_partial_id) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (return v) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> return v 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 v
od) s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma thread_actions_isolatable_fail:
  "thread_actions_isolatable idx fail" by (simp add: thread_actions_isolatable_def
                isolate_thread_actions_def select_f_asserts
                liftM_def bind_assoc getSchedulerAction_def
                monadic_rewrite_def exec_gets)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx fail
theory IsolatedThreadAction

lemma thread_actions_isolatable_returns:
  "thread_actions_isolatable idx (return v)"
  "thread_actions_isolatable idx (returnOk v)"
  "thread_actions_isolatable idx (throwError v)" by (simp add: returnOk_def throwError_def
                thread_actions_isolatable_return)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (return v) &&& thread_actions_isolatable idx (returnOk v) &&& thread_actions_isolatable idx (throwError v)
theory IsolatedThreadAction

lemma thread_actions_isolatable_catch:
  "\<lbrakk> thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x);
       \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> \<rbrakk>
     \<Longrightarrow> thread_actions_isolatable idx (f <catch> g)" apply (simp add: catch_def) apply (erule thread_actions_isolatable_bind) apply (simp add: thread_actions_isolatable_returns
             split: sum.split) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x); \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (f <catch> g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>thread_actions_isolatable idx f; \<And>x. thread_actions_isolatable idx (g x); \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (do x <- f;
case x of Inl e \<Rightarrow> g e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. thread_actions_isolatable idx (g x); \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (case x of Inl e \<Rightarrow> g e | Inr b \<Rightarrow> return b)
 2. \<And>t. \<lbrakk>\<And>x. thread_actions_isolatable idx (g x); \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<And>x. thread_actions_isolatable idx (g x); \<And>t. \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' t\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal:
No subgoals!