kings-crown/FVELER_Isabelle huggingface dataset:
theory Move_C

lemma asUser_getRegister_threadGet_comm:
  "do
     ra \<leftarrow> asUser a (getRegister r);
     rb \<leftarrow> threadGet fb b;
     c ra rb
   od = do
     rb \<leftarrow> threadGet fb b;
     ra \<leftarrow> asUser a (getRegister r);
     c ra rb
   od" by (rule bind_inv_inv_comm, auto; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ra <- asUser a (getRegister r);
threadGet fb b >>= c ra
od = do rb <- threadGet fb b;
ra <- asUser a (getRegister r);
c ra rb
od
theory Move_C

lemma threadGet_tcbFault_doMachineOp_comm:
  "\<lbrakk> empty_fail m' \<rbrakk> \<Longrightarrow>
   do x \<leftarrow> threadGet tcbFault t; y \<leftarrow> doMachineOp m'; n x y od =
   do y \<leftarrow> doMachineOp m'; x \<leftarrow> threadGet tcbFault t; n x y od" apply (rule submonad_comm2 [OF tcbFault_submonad_args
                                 threadGet_tcbFault_submonad_fn
                                 submonad_doMachineOp]) apply (simp add: thread_replace_def Let_def) apply simp apply (rule refl) apply (simp add: get_def empty_fail_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m' \<Longrightarrow> do x <- threadGet tcbFault t;
doMachineOp m' >>= n x
od = do y <- doMachineOp m';
x <- threadGet tcbFault t;
n x y
od proof (prove)
goal (5 subgoals):
 1. \<And>s x x'. empty_fail m' \<Longrightarrow> thread_replace tcbFault_update t x ((ksMachineState_update \<circ> K) x' s) = (ksMachineState_update \<circ> K) x' (thread_replace tcbFault_update t x s)
 2. \<And>s x. empty_fail m' \<Longrightarrow> tcb_at' t ((ksMachineState_update \<circ> K) x s) = tcb_at' t s
 3. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 4. empty_fail m' \<Longrightarrow> empty_fail get
 5. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (4 subgoals):
 1. \<And>s x. empty_fail m' \<Longrightarrow> tcb_at' t ((ksMachineState_update \<circ> K) x s) = tcb_at' t s
 2. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 3. empty_fail m' \<Longrightarrow> empty_fail get
 4. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (3 subgoals):
 1. \<And>s x. empty_fail m' \<Longrightarrow> True = True
 2. empty_fail m' \<Longrightarrow> empty_fail get
 3. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (2 subgoals):
 1. empty_fail m' \<Longrightarrow> empty_fail get
 2. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal (1 subgoal):
 1. empty_fail m' \<Longrightarrow> empty_fail m' proof (prove)
goal:
No subgoals!
theory Move_C

lemma threadGet_again:
  "\<And>rv s s' n. (rv, s') \<in> fst (threadGet ext t s) \<Longrightarrow>
   (threadGet ext t >>= n) s' = n rv s'" apply (clarsimp simp add: threadGet_def liftM_def in_monad) apply (frule use_valid [OF _ getObject_obj_at']) apply (simp add: objBits_simps')+ apply (frule getObject_tcb_det) apply (clarsimp simp: bind_def split_def) apply (insert no_fail_getObject_tcb) apply (clarsimp simp: no_fail_def obj_at'_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>rv s s' n. (rv, s') \<in> fst (threadGet ext t s) \<Longrightarrow> (threadGet ext t >>= n) s' = n rv s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n x. (x, s') \<in> fst (getObject t s) \<Longrightarrow> (do x <- getObject t;
n (ext x)
od) s' = n (ext x) s' proof (prove)
goal (4 subgoals):
 1. \<And>s s' n x q na ko. (x, s') \<in> fst (getObject t s) \<Longrightarrow> loadObject t q na ko = loadObject_default t q na ko
 2. \<And>s s' n x v. (x, s') \<in> fst (getObject t s) \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>s s' n x. (x, s') \<in> fst (getObject t s) \<Longrightarrow> True
 4. \<And>s s' n x. \<lbrakk>(x, s') \<in> fst (getObject t s); obj_at' ((=) x) t s'\<rbrakk> \<Longrightarrow> (do x <- getObject t;
n (ext x)
od) s' = n (ext x) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n x. \<lbrakk>(x, s') \<in> fst (getObject t s); obj_at' ((=) x) t s'\<rbrakk> \<Longrightarrow> (do x <- getObject t;
n (ext x)
od) s' = n (ext x) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n x. \<lbrakk>(x, s') \<in> fst (getObject t s); obj_at' ((=) x) t s'; fst (getObject t s) = {(x, s)} \<and> s' = s\<rbrakk> \<Longrightarrow> (do x <- getObject t;
n (ext x)
od) s' = n (ext x) s' proof (prove)
goal (1 subgoal):
 1. \<And>s n x. \<lbrakk>obj_at' ((=) x) t s; fst (getObject t s) = {(x, s)}\<rbrakk> \<Longrightarrow> (fst (n (ext x) s), snd (n (ext x) s) \<or> snd (getObject t s)) = n (ext x) s proof (prove)
goal (1 subgoal):
 1. \<And>s n x. \<lbrakk>obj_at' ((=) x) t s; fst (getObject t s) = {(x, s)}; \<And>t. no_fail (tcb_at' t) (getObject t)\<rbrakk> \<Longrightarrow> (fst (n (ext x) s), snd (n (ext x) s) \<or> snd (getObject t s)) = n (ext x) s proof (prove)
goal:
No subgoals!
theory Move_C

lemma setMRs_Nil:
  "setMRs thread buffer [] = stateAssert (tcb_at' thread) [] >>= (\<lambda>_. return 0)" unfolding setMRs_def by (simp add: zipWithM_x_def sequence_x_def zipWith_def
                asUser_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setMRs thread buffer [] = do _ <- stateAssert (tcb_at' thread) [];
return 0
od proof (prove)
goal (1 subgoal):
 1. do intSize <- return (fromIntegral wordSize);
hardwareMRs <- return msgRegisters;
bufferMRs <- return (case buffer of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + PPtr (x * intSize)) [fromIntegral $ length hardwareMRs + 1 .e. msgMaxLength]);
msgLength <- return (min (length []) (length hardwareMRs + length bufferMRs));
mrs <- return (take msgLength []);
asUser thread $ zipWithM_x setRegister hardwareMRs mrs;
zipWithM_x storeWordUser bufferMRs $ drop (length hardwareMRs) mrs;
return $ fromIntegral msgLength
od = do _ <- stateAssert (tcb_at' thread) [];
return 0
od
theory Move_C

lemma device_data_at_ko:
  "typ_at' UserDataDeviceT p s \<Longrightarrow> ko_at' UserDataDevice p s" apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def
    projectKO_user_data_device projectKO_eq projectKO_eq2) apply (case_tac ko, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at' UserDataDeviceT p s \<Longrightarrow> ko_at' UserDataDevice p s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); koTypeOf ko = UserDataDeviceT; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> ko = KOUserDataDevice \<and> is_aligned p (objBitsKO KOUserDataDevice) \<and> ps_clear p (objBitsKO KOUserDataDevice) s proof (prove)
goal:
No subgoals!
theory Move_C

lemma empty_fail_rethrowFailure:
  "empty_fail f \<Longrightarrow> empty_fail (rethrowFailure fn f)" apply (simp add: rethrowFailure_def handleE'_def) apply (erule empty_fail_bind) apply (simp split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (rethrowFailure fn f) proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (do v <- f;
case v of Inl e \<Rightarrow> (throwError \<circ> fn) e | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail (case x of Inl e \<Rightarrow> (throwError \<circ> fn) e | Inr v' \<Rightarrow> return (Inr v')) proof (prove)
goal:
No subgoals!
theory Move_C

lemma mapM_only_length:
  "do ys \<leftarrow> mapM f xs;
      g (length ys)
   od =
   do _ \<leftarrow> mapM_x f xs;
      g (length xs)
   od" by (subst bind_return_subst [OF mapM_length])
     (rule mapM_discarded)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ys <- mapM f xs;
g (length ys)
od = do _ <- mapM_x f xs;
g (length xs)
od
theory Move_C

lemma tcb_aligned':
  "tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits" apply (drule obj_at_aligned') apply (simp add: objBits_simps) apply (simp add: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits proof (prove)
goal (2 subgoals):
 1. \<And>v v'. objBits v = objBits v'
 2. is_aligned t (objBits ?obj) \<Longrightarrow> is_aligned t tcbBlockSizeBits proof (prove)
goal (1 subgoal):
 1. is_aligned t (objBits ?obj) \<Longrightarrow> is_aligned t tcbBlockSizeBits proof (prove)
goal:
No subgoals!
theory Move_C

lemma cte_at_0' [dest!]:
  "\<lbrakk> cte_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> False" apply (clarsimp simp: cte_wp_at_obj_cases') by (auto simp: tcb_cte_cases_def is_aligned_def objBits_simps' dest!:tcb_aligned' split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>_. True) 0 s; no_0_obj' s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>no_0_obj' s; tcb_at' (- n) s; tcb_cte_cases n = Some (a, b)\<rbrakk> \<Longrightarrow> False
theory Move_C

lemma getMessageInfo_le3:
  "\<lbrace>\<top>\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace>" including no_pre apply (simp add: getMessageInfo_def) apply wp apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post) apply wp apply (rename_tac rv s) apply (simp add: messageInfoFromWord_def Let_def msgExtraCapBits_def) apply (cut_tac y="rv >> Types_H.msgLengthBits" in word_and_le1 [where a=3]) apply (simp add: word_le_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do x <- asUser sender (getRegister msgInfoRegister);
return (messageInfoFromWord x)
od \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> asUser sender (getRegister msgInfoRegister) \<lbrace>\<lambda>x a. unat (msgExtraCaps (messageInfoFromWord x)) \<le> 3\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> asUser sender (getRegister msgInfoRegister) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. True \<Longrightarrow> unat (msgExtraCaps (messageInfoFromWord rv)) \<le> 3 proof (prove)
goal (1 subgoal):
 1. \<And>rv s. True \<Longrightarrow> unat (msgExtraCaps (messageInfoFromWord rv)) \<le> 3 proof (prove)
goal (1 subgoal):
 1. \<And>rv s. True \<Longrightarrow> unat (msgExtraCaps (messageInfoFromWord rv)) \<le> 3 proof (prove)
goal (1 subgoal):
 1. \<And>rv. unat ((rv >> msgLengthBits) && 3) \<le> 3 proof (prove)
goal (1 subgoal):
 1. \<And>rv. (rv >> msgLengthBits) && 3 \<le> 3 \<Longrightarrow> unat ((rv >> msgLengthBits) && 3) \<le> 3 proof (prove)
goal:
No subgoals!
theory Move_C

lemma getMessageInfo_msgLength:
  "\<lbrace>\<top>\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv. K (unat (msgLength rv) \<le> msgMaxLength)\<rbrace>" including no_pre apply (simp add: getMessageInfo_def) apply wp apply (rule_tac Q="\<lambda>_. \<top>" in hoare_strengthen_post) apply wp apply (simp add: messageInfoFromWord_def Let_def not_less msgMaxLength_def msgLengthBits_def
            split: if_split) apply (cut_tac y="r" in word_and_le1 [where a="0x7F"]) apply (simp add: word_le_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv. K (unat (msgLength rv) \<le> msgMaxLength)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv. K (unat (msgLength rv) \<le> msgMaxLength)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do x <- asUser sender (getRegister msgInfoRegister);
return (messageInfoFromWord x)
od \<lbrace>\<lambda>rv y. unat (msgLength rv) \<le> msgMaxLength\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> asUser sender (getRegister msgInfoRegister) \<lbrace>\<lambda>x a. unat (msgLength (messageInfoFromWord x)) \<le> msgMaxLength\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>_. True\<rbrace> asUser sender (getRegister msgInfoRegister) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>rv s. True \<Longrightarrow> unat (msgLength (messageInfoFromWord rv)) \<le> msgMaxLength proof (prove)
goal (1 subgoal):
 1. \<And>rv s. True \<Longrightarrow> unat (msgLength (messageInfoFromWord rv)) \<le> msgMaxLength proof (prove)
goal (1 subgoal):
 1. \<And>rv. rv && 0x7F \<le> 0x78 \<longrightarrow> unat (rv && 0x7F) \<le> 120 proof (prove)
goal (1 subgoal):
 1. \<And>rv. r && 0x7F \<le> 0x7F \<Longrightarrow> rv && 0x7F \<le> 0x78 \<longrightarrow> unat (rv && 0x7F) \<le> 120 proof (prove)
goal:
No subgoals!
theory Move_C

lemma cancelAllIPC_sch_act_wf:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  cancelAllIPC ep
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: cancelAllIPC_def) apply (rule hoare_TrueI|wp getEndpoint_wp|wpc|simp)+ apply fastforce? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> cancelAllIPC ep \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> do epa <- getEndpoint ep;
case epa of Structures_H.endpoint.IdleEP \<Rightarrow> return () | _ \<Rightarrow> do setEndpoint ep Structures_H.endpoint.IdleEP;
forM_x (epQueue epa) (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Move_C

lemma cancelAllSignals_sch_act_wf:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  cancelAllSignals ep
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: cancelAllSignals_def) apply (rule hoare_TrueI|wp getNotification_wp|wpc|simp)+ apply fastforce? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> cancelAllSignals ep \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> do ntfn <- getNotification ep;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification ep (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory Move_C

lemma vp_invs_strg': "invs' s \<longrightarrow> valid_pspace' s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<longrightarrow> valid_pspace' s
theory Move_C

lemma setCTE_tcbFault:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>
  setCTE slot cte
  \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> setCTE slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> setObject slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbFault tcb)) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma setNotification_tcb:
  "\<lbrace>obj_at' (\<lambda>tcb::tcb. P tcb) t\<rbrace>
  setNotification ntfn e
  \<lbrace>\<lambda>_. obj_at' P t\<rbrace>" apply (simp add: setNotification_def) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setNotification ntfn e \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject ntfn e \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory Move_C

lemma state_refs_of'_upd:
  "\<lbrakk> valid_pspace' s; ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO ko') ptr s \<rbrakk> \<Longrightarrow>
   state_refs_of' (s\<lparr>ksPSpace := (ksPSpace s)(ptr \<mapsto> ko')\<rparr>) =
   (state_refs_of' s)(ptr := refs_of' ko')" apply (rule ext) apply (clarsimp simp: ps_clear_upd valid_pspace'_def pspace_aligned'_def
                        obj_at'_def ko_wp_at'_def state_refs_of'_def
                 split: option.split if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO ko') ptr s\<rbrakk> \<Longrightarrow> state_refs_of' (s\<lparr>ksPSpace := (ksPSpace s)(ptr \<mapsto> ko')\<rparr>) = (state_refs_of' s)(ptr := refs_of' ko') proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_pspace' s; ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO ko') ptr s\<rbrakk> \<Longrightarrow> state_refs_of' (s\<lparr>ksPSpace := (ksPSpace s)(ptr \<mapsto> ko')\<rparr>) x = ((state_refs_of' s)(ptr := refs_of' ko')) x proof (prove)
goal:
No subgoals!
theory Move_C

lemma ex_st_tcb_at'_simp[simp]:
  "(\<exists>ts. st_tcb_at' ((=) ts) dest s) = tcb_at' dest s" by (auto simp add: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>ts. st_tcb_at' ((=) ts) dest s) = tcb_at' dest s
theory Move_C

lemma threadGet_wp:
  "\<lbrace>\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrace> threadGet f thread \<lbrace>P\<rbrace>" apply (rule hoare_post_imp [OF _ tg_sp']) apply clarsimp apply (frule obj_at_ko_at') apply (clarsimp elim: obj_atE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrace> threadGet f thread \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (obj_at' (\<lambda>t'. f t' = rv) thread and (\<lambda>s. \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s)) s \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>obj_at' (\<lambda>t'. f t' = rv) thread s; \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s\<rbrakk> \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>obj_at' (\<lambda>t'. f t' = rv) thread s; \<forall>tcb. ko_at' tcb thread s \<longrightarrow> P (f tcb) s; \<exists>ko. ko_at' ko thread s \<and> f ko = rv\<rbrakk> \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory Move_C

lemma filter_noteq_op:
  "[x \<leftarrow> xs . x \<noteq> y] = filter ((\<noteq>) y) xs" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<noteq> y) xs = filter ((\<noteq>) y) xs
theory Move_C

lemma all_filter_propI:
  "\<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x" by (induct lst, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set lst. P x \<Longrightarrow> \<forall>x\<in>set (filter Q lst). P x
theory Move_C

lemma returnOK_catch[simp]:
  "(returnOk rv <catch> m) = return rv" unfolding catch_def returnOk_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (returnOk rv <catch> m) = return rv proof (prove)
goal (1 subgoal):
 1. do x <- (return \<circ> Inr) rv;
case x of Inl e \<Rightarrow> m e | Inr b \<Rightarrow> return b
od = return rv
theory Move_C

lemma ignoreFailure_liftM:
  "ignoreFailure = liftM (\<lambda>v. ())" apply (rule ext)+ apply (simp add: ignoreFailure_def liftM_def
                   catch_def) apply (rule bind_apply_cong[OF refl]) apply (simp split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ignoreFailure = liftM (\<lambda>v. ()) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. ignoreFailure x xa = liftM (\<lambda>v. ()) x xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (do x <- x;
case x of Inl e \<Rightarrow> const (return ()) e | Inr b \<Rightarrow> return b
od) xa = (do x <- x;
return ()
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa rv st. (rv, st) \<in> fst (x xa) \<Longrightarrow> (case rv of Inl e \<Rightarrow> const (return ()) e | Inr b \<Rightarrow> return b) st = return () st proof (prove)
goal:
No subgoals!
theory Move_C

lemma dom_eq:
  "dom um = dom um' \<longleftrightarrow> (\<forall>a. um a = None \<longleftrightarrow> um' a = None)" apply (simp add: dom_def del: not_None_eq) apply (rule iffI) apply (rule allI) apply (simp add: set_eq_iff) apply (drule_tac x=a in spec) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (dom um = dom um') = (\<forall>a. (um a = None) = (um' a = None)) proof (prove)
goal (1 subgoal):
 1. ({a. um a \<noteq> None} = {a. um' a \<noteq> None}) = (\<forall>a. (um a = None) = (um' a = None)) proof (prove)
goal (2 subgoals):
 1. {a. um a \<noteq> None} = {a. um' a \<noteq> None} \<Longrightarrow> \<forall>a. (um a = None) = (um' a = None)
 2. \<forall>a. (um a = None) = (um' a = None) \<Longrightarrow> {a. um a \<noteq> None} = {a. um' a \<noteq> None} proof (prove)
goal (2 subgoals):
 1. \<And>a. {a. um a \<noteq> None} = {a. um' a \<noteq> None} \<Longrightarrow> (um a = None) = (um' a = None)
 2. \<forall>a. (um a = None) = (um' a = None) \<Longrightarrow> {a. um a \<noteq> None} = {a. um' a \<noteq> None} proof (prove)
goal (2 subgoals):
 1. \<And>a. \<forall>x. (\<exists>y. um x = Some y) = (\<exists>y. um' x = Some y) \<Longrightarrow> (um a = None) = (um' a = None)
 2. \<forall>a. (um a = None) = (um' a = None) \<Longrightarrow> {a. um a \<noteq> None} = {a. um' a \<noteq> None} proof (prove)
goal (2 subgoals):
 1. \<And>a. (\<exists>y. um a = Some y) = (\<exists>y. um' a = Some y) \<Longrightarrow> (um a = None) = (um' a = None)
 2. \<forall>a. (um a = None) = (um' a = None) \<Longrightarrow> {a. um a \<noteq> None} = {a. um' a \<noteq> None} proof (prove)
goal:
No subgoals!
theory Move_C

lemma dom_user_mem':
  "dom (user_mem' s) = {p. typ_at' UserDataT (p && ~~ mask pageBits) s}" by (clarsimp simp:user_mem'_def dom_def pointerInUserData_def split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (user_mem' s) = {p. typ_at' UserDataT (p && ~~ mask pageBits) s}
theory Move_C

lemma dom_device_mem':
  "dom (device_mem' s) = {p. typ_at' UserDataDeviceT (p && ~~ mask pageBits) s}" by (clarsimp simp: device_mem'_def dom_def pointerInDeviceData_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (device_mem' s) = {p. typ_at' UserDataDeviceT (p && ~~ mask pageBits) s}
theory Move_C

lemma valid_idle'_tcb_at'_ksIdleThread:
  "valid_idle' s \<Longrightarrow> tcb_at' (ksIdleThread s) s" by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle' s \<Longrightarrow> tcb_at' (ksIdleThread s) s
theory Move_C

lemma invs_no_cicd'_valid_idle':
  "invs_no_cicd' s \<Longrightarrow> valid_idle' s" by (simp add: invs_no_cicd'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_idle' s
theory Move_C

lemma empty_fail_getIdleThread [simp,intro!]:
  "empty_fail getIdleThread" by (simp add: getIdleThread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail getIdleThread