kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_DR

lemma seq_alt_when:"(do a \<leftarrow> when c (f \<sqinter> g); h a od) = ((do a\<leftarrow>when c f ; h a od)\<sqinter> (do a\<leftarrow>when c g; h a od))" apply (clarsimp simp:when_def) apply (subst alternative_bind_distrib)+ apply (clarsimp simp:alternative_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when c (f \<sqinter> g) >>= h = (when c f >>= h \<sqinter> when c g >>= h) proof (prove)
goal (1 subgoal):
 1. (c \<longrightarrow> (f \<sqinter> g) >>= h = (f >>= h \<sqinter> g >>= h)) \<and> (\<not> c \<longrightarrow> h () = (h () \<sqinter> h ())) proof (prove)
goal (1 subgoal):
 1. (c \<longrightarrow> (f >>= h \<sqinter> g >>= h) = (f >>= h \<sqinter> g >>= h)) \<and> (\<not> c \<longrightarrow> h () = (h () \<sqinter> h ())) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_store_word_offs_spec:
  "\<lbrakk>within_page buf (base + of_nat (x * word_size)) sz\<rbrakk> \<Longrightarrow>
  dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs)
   (corrupt_frame buf) (store_word_offs base x y)" using zip_store_word_corres[where xs = "[x]" and base = base and buf = buf and sz = sz and s_id = s_id and ys = "[y]"] apply (clarsimp simp:zipWithM_x_One) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (store_word_offs base x y) proof (prove)
using this:
\<forall>x\<in>set [x]. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (zipWithM_x (store_word_offs base) [x] [y])

goal (1 subgoal):
 1. within_page buf (base + word_of_nat (x * word_size)) sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz s_id and ipc_frame_ptr_at buf s_id and valid_etcbs) (corrupt_frame buf) (store_word_offs base x y) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma update_cap_rights_cong:
  "\<lbrakk> is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap \<Longrightarrow> R = R' \<rbrakk> \<Longrightarrow>
  transform_cap (cap_rights_update R' cap) = update_cap_rights R (transform_cap cap)" by (clarsimp simp: is_reply_cap_def
                     cap_rights_update_def acap_rights_update_def update_cap_rights_def
               split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Structures_A.is_ep_cap cap \<or> Structures_A.is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap \<Longrightarrow> R = R') \<Longrightarrow> transform_cap (cap_rights_update R' cap) = update_cap_rights R (transform_cap cap)
theory Ipc_DR

lemma transform_cap_rights:
  "is_ep_cap cap \<or> is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap
  \<Longrightarrow> (Structures_A.cap_rights cap) = Types_D.cap_rights (transform_cap cap)" by (auto simp: is_cap_simps is_arch_page_cap_def Types_D.cap_rights_def transform_cap_def
           split: arch_cap.splits cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Structures_A.is_ep_cap cap \<or> Structures_A.is_ntfn_cap cap \<or> is_reply_cap cap \<or> is_arch_page_cap cap \<Longrightarrow> Structures_A.cap_rights cap = Types_D.cap_rights (transform_cap cap)
theory Ipc_DR

lemma evalMonad_thread_get_eq:
  "evalMonad (thread_get f x) b = (case (get_tcb x b) of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t))" apply (simp add:thread_get_def) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_simps weak_det_spec_simps)+ apply wp apply clarsimp apply (clarsimp simp:gets_the_def gets_def get_def bind_def return_def assert_opt_def) apply (case_tac "get_tcb x b") apply (clarsimp simp:return_def fail_def evalMonad_def split:option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (thread_get f x) b = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (1 subgoal):
 1. evalMonad (do tcb <- gets_the (get_tcb x);
return (f tcb)
od) b = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (4 subgoals):
 1. empty_when_fail (gets_the (get_tcb x))
 2. weak_det_spec ((=) b) (gets_the (get_tcb x))
 3. \<And>s. \<lbrace>(=) s\<rbrace> gets_the (get_tcb x) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (gets_the (get_tcb x)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> gets_the (get_tcb x) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (gets_the (get_tcb x)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. s = sa \<Longrightarrow> get_tcb x sa \<noteq> None \<longrightarrow> s = sa
 2. (case evalMonad (gets_the (get_tcb x)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (1 subgoal):
 1. (case evalMonad (gets_the (get_tcb x)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (1 subgoal):
 1. (case evalMonad (\<lambda>s. (case get_tcb x s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal (2 subgoals):
 1. get_tcb x b = None \<Longrightarrow> (case evalMonad (\<lambda>s. (case get_tcb x s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t))
 2. \<And>a. get_tcb x b = Some a \<Longrightarrow> (case evalMonad (\<lambda>s. (case get_tcb x s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (return (f r)) b) = (case get_tcb x b of None \<Rightarrow> None | Some t \<Rightarrow> Some (f t)) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma ipc_buffer_wp_at_exst_update[simp]:
  "ipc_buffer_wp_at buf t (exst_update f s) =
   ipc_buffer_wp_at buf t s" by (simp add: ipc_buffer_wp_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ipc_buffer_wp_at buf t (exst_update f s) = ipc_buffer_wp_at buf t s
theory Ipc_DR

lemma ipc_buffer_wp_set_cap[wp]:
  "\<lbrace>ipc_buffer_wp_at buf t\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>\<lambda>ya. ipc_buffer_wp_at buf t\<rbrace>" apply (clarsimp simp: set_cap_def split_def) apply (wpsimp wp: set_object_wp get_object_wp) apply (rule conjI|clarsimp simp:ipc_buffer_wp_at_def obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> CSpaceAcc_A.set_cap cap' a \<lbrace>\<lambda>ya. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> do obj <- KHeap_A.get_object (fst a);
(case obj of kernel_object.CNode sz cn \<Rightarrow> if snd a \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ kernel_object.CNode sz $ cn(snd a \<mapsto> cap') else fail | TCB tcb \<Rightarrow> if snd a = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap'\<rparr> else if snd a = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap'\<rparr> else if snd a = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap'\<rparr> else if snd a = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap'\<rparr> else if snd a = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap'\<rparr> else fail | _ \<Rightarrow> fail) >>= KHeap_A.set_object (fst a)
od \<lbrace>\<lambda>ya. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ipc_buffer_wp_at buf t s; ko_at ko (fst a) s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko = kernel_object.CNode x xa \<longrightarrow> snd a \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> kernel_object.CNode x (\<lambda>b. if b = snd a then Some cap' else xa b))) s)) \<and> (\<forall>x. ko = TCB x \<longrightarrow> (snd a = tcb_cnode_index 0 \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> TCB (x\<lparr>tcb_ctable := cap'\<rparr>))) s)) \<and> (snd a \<noteq> tcb_cnode_index 0 \<longrightarrow> (snd a = tcb_cnode_index (Suc 0) \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> TCB (x\<lparr>tcb_vtable := cap'\<rparr>))) s)) \<and> (snd a \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (snd a = tcb_cnode_index 2 \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> TCB (x\<lparr>tcb_reply := cap'\<rparr>))) s)) \<and> (snd a \<noteq> tcb_cnode_index 2 \<longrightarrow> (snd a = tcb_cnode_index 3 \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> TCB (x\<lparr>tcb_caller := cap'\<rparr>))) s)) \<and> (snd a \<noteq> tcb_cnode_index 3 \<longrightarrow> snd a = tcb_cnode_index 4 \<longrightarrow> ipc_buffer_wp_at buf t (update_kheap ((kheap s)(fst a \<mapsto> TCB (x\<lparr>tcb_ipcframe := cap'\<rparr>))) s)))))) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma ipc_buffer_wp_at_cap_insert_ext[wp]:
  "\<lbrace>ipc_buffer_wp_at buf t \<rbrace> cap_insert_ext src_parent src_slot dest_slot src_p dest_p \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>" apply (simp only:ipc_buffer_wp_at_def) by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> cap_insert_ext src_parent src_slot dest_slot src_p dest_p \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t\<rbrace> cap_insert_ext src_parent src_slot dest_slot src_p dest_p \<lbrace>\<lambda>r. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = buf) t\<rbrace>
theory Ipc_DR

lemma is_ep_cap_transform_simp[simp]:
  "Types_D.is_ep_cap (transform_cap cap) = is_ep_cap cap" by (simp add:transform_cap_def cap_type_simps
    split:cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.is_ep_cap (transform_cap cap) = Structures_A.is_ep_cap cap
theory Ipc_DR

lemma dcorres_return:
  "r a b \<Longrightarrow> dcorres (r) (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)" by (clarsimp simp:return_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r a b \<Longrightarrow> dcorres r (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)
theory Ipc_DR

lemma opt_cap_valid_etcbs:
  "\<lbrakk>tcb_at ptr s; valid_etcbs s; ptr \<noteq> idle_thread s;
    sl \<in> tcb_abstract_slots \<or> sl = tcb_pending_op_slot\<rbrakk> \<Longrightarrow>
  \<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap" apply (clarsimp simp: tcb_at_def) apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp: opt_cap_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at ptr s; valid_etcbs s; ptr \<noteq> idle_thread s; sl \<in> tcb_abstract_slots \<or> sl = tcb_pending_op_slot\<rbrakk> \<Longrightarrow> \<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_etcbs s; ptr \<noteq> idle_thread s; sl = tcb_caller_slot \<or> sl = tcb_cspace_slot \<or> sl = tcb_ipcbuffer_slot \<or> sl = tcb_replycap_slot \<or> sl = tcb_vspace_slot \<or> sl = tcb_pending_op_slot; get_tcb ptr s = Some tcb\<rbrakk> \<Longrightarrow> \<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>valid_etcbs s; ptr \<noteq> idle_thread s; sl = tcb_caller_slot \<or> sl = tcb_cspace_slot \<or> sl = tcb_ipcbuffer_slot \<or> sl = tcb_replycap_slot \<or> sl = tcb_vspace_slot \<or> sl = tcb_pending_op_slot; get_tcb ptr s = Some tcb; \<exists>etcb. get_etcb ptr s = Some etcb\<rbrakk> \<Longrightarrow> \<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma lookup_ipc_buffer_tcb_at:
  "evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a \<Longrightarrow> tcb_at thread sa" apply (case_tac a) apply clarsimp apply (frule lookup_ipc_buffer_None_evalMonad) apply (clarsimp simp:tcb_at_def get_tcb_SomeD obj_at_def)+ apply (frule lookup_ipc_buffer_SomeB_evalMonad) apply (clarsimp simp:is_tcb_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a \<Longrightarrow> tcb_at thread sa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a; a = None\<rbrakk> \<Longrightarrow> tcb_at thread sa
 2. \<And>aa. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a; a = Some aa\<rbrakk> \<Longrightarrow> tcb_at thread sa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some None; a = None\<rbrakk> \<Longrightarrow> tcb_at thread sa
 2. \<And>aa. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a; a = Some aa\<rbrakk> \<Longrightarrow> tcb_at thread sa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some None; a = None; \<exists>obj. ko_at (TCB obj) thread sa \<and> (\<forall>b rs sz. ipc_frame_cte_at thread b rs sz sa \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<notin> rs \<or> AllowRead \<notin> rs))\<rbrakk> \<Longrightarrow> tcb_at thread sa
 2. \<And>aa. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some a; a = Some aa\<rbrakk> \<Longrightarrow> tcb_at thread sa proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some aa); a = Some aa\<rbrakk> \<Longrightarrow> \<exists>ko. kheap sa thread = Some ko \<and> is_tcb ko proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some aa); a = Some aa; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread b rs sz sa \<and> ko_at (TCB obj) thread sa \<and> aa = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<exists>ko. kheap sa thread = Some ko \<and> is_tcb ko proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma copy_mrs_valid_irq_node:
  "\<lbrace>valid_irq_node\<rbrace> copy_mrs a b c d e
            \<lbrace>\<lambda>rva s. valid_irq_node s\<rbrace>" apply (simp add:valid_irq_node_def) apply (wpsimp wp: hoare_vcg_all_lift|wps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node\<rbrace> copy_mrs a b c d e \<lbrace>\<lambda>rva. valid_irq_node\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrace> copy_mrs a b c d e \<lbrace>\<lambda>rva s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_handle_arch_fault_reply:
  "dcorres dc \<top> (tcb_at y and valid_idle and not_idle_thread y and  valid_etcbs)
   (corrupt_tcb_intent y)
   (handle_arch_fault_reply a y mi mrs)" apply (cases a) apply (clarsimp simp: handle_arch_fault_reply_def) apply (rule corres_guard_imp) apply (rule corres_corrupt_tcb_intent_return) apply assumption apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply a y mi mrs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. a = VMFault x1 x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (handle_arch_fault_reply a y mi mrs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. a = VMFault x1 x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (return True) proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. a = VMFault x1 x2 \<Longrightarrow> dcorres dc (?Q1 x1 x2) (?Q'1 x1 x2) (corrupt_tcb_intent y) (return True)
 2. \<And>x1 x2 s. \<lbrakk>a = VMFault x1 x2; True\<rbrakk> \<Longrightarrow> ?Q1 x1 x2 s
 3. \<And>x1 x2 s. \<lbrakk>a = VMFault x1 x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'1 x1 x2 s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 s. \<lbrakk>a = VMFault x1 x2; True\<rbrakk> \<Longrightarrow> True
 2. \<And>x1 x2 s. \<lbrakk>a = VMFault x1 x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at y and not_idle_thread y and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 s. \<lbrakk>a = VMFault x1 x2; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s\<rbrakk> \<Longrightarrow> (tcb_at y and not_idle_thread y and valid_etcbs) s proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma alternative_distrib2:
  "(do x \<leftarrow> a;  (b x \<sqinter> c x) od) = ((do x\<leftarrow>a; b x od) \<sqinter> (do x\<leftarrow>a; c x od)) " apply (simp add:bind_def alternative_def UNION_eq) apply (rule ext)+ apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- a;
b x \<sqinter> c x
od = (a >>= b \<sqinter> a >>= c) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, s) \<Rightarrow> (fst (b x s) \<union> fst (c x s), snd (b x s) \<or> snd (c x s)))}, (\<exists>x\<in>fst (a s). snd (case x of (x, s) \<Rightarrow> (fst (b x s) \<union> fst (c x s), snd (b x s) \<or> snd (c x s)))) \<or> snd (a s))) = (\<lambda>s. ({y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, xa) \<Rightarrow> b x xa)} \<union> {y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, xa) \<Rightarrow> c x xa)}, (\<exists>x\<in>fst (a s). snd (case x of (x, xa) \<Rightarrow> b x xa)) \<or> snd (a s) \<or> (\<exists>x\<in>fst (a s). snd (case x of (x, xa) \<Rightarrow> c x xa)) \<or> snd (a s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. ({y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, s) \<Rightarrow> (fst (b x s) \<union> fst (c x s), snd (b x s) \<or> snd (c x s)))}, (\<exists>x\<in>fst (a s). snd (case x of (x, s) \<Rightarrow> (fst (b x s) \<union> fst (c x s), snd (b x s) \<or> snd (c x s)))) \<or> snd (a s)) = ({y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, xa) \<Rightarrow> b x xa)} \<union> {y. \<exists>x\<in>fst (a s). y \<in> fst (case x of (x, xa) \<Rightarrow> c x xa)}, (\<exists>x\<in>fst (a s). snd (case x of (x, xa) \<Rightarrow> b x xa)) \<or> snd (a s) \<or> (\<exists>x\<in>fst (a s). snd (case x of (x, xa) \<Rightarrow> c x xa)) \<or> snd (a s)) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma set_cap_overlap:
  "cdl_objects s recv = Some (Tcb tcb)
    \<Longrightarrow> (KHeap_D.set_cap (recv,tcb_pending_op_slot) a >>= K (KHeap_D.set_cap (recv,tcb_pending_op_slot) b)) s
        = (KHeap_D.set_cap (recv,tcb_pending_op_slot) b) s" apply (rule monad_state_eqI) by (auto simp: KHeap_D.set_cap_def KHeap_D.set_object_def in_monad has_slots_def
                 update_slots_def simpler_modify_def snd_bind valid_def
                 snd_return gets_the_def snd_gets assert_opt_def object_slots_def
           cong: cdl_object.case_cong split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects s recv = Some (Tcb tcb) \<Longrightarrow> (KHeap_D.set_cap (recv, tcb_pending_op_slot) a >>= K (KHeap_D.set_cap (recv, tcb_pending_op_slot) b)) s = KHeap_D.set_cap (recv, tcb_pending_op_slot) b s proof (prove)
goal (3 subgoals):
 1. \<And>r t. \<lbrakk>cdl_objects s recv = Some (Tcb tcb); (r, t) \<in> fst ((KHeap_D.set_cap (recv, tcb_pending_op_slot) a >>= K (KHeap_D.set_cap (recv, tcb_pending_op_slot) b)) s)\<rbrakk> \<Longrightarrow> (r, t) \<in> fst (KHeap_D.set_cap (recv, tcb_pending_op_slot) b s)
 2. \<And>r t. \<lbrakk>cdl_objects s recv = Some (Tcb tcb); (r, t) \<in> fst (KHeap_D.set_cap (recv, tcb_pending_op_slot) b s)\<rbrakk> \<Longrightarrow> (r, t) \<in> fst ((KHeap_D.set_cap (recv, tcb_pending_op_slot) a >>= K (KHeap_D.set_cap (recv, tcb_pending_op_slot) b)) s)
 3. cdl_objects s recv = Some (Tcb tcb) \<Longrightarrow> snd ((KHeap_D.set_cap (recv, tcb_pending_op_slot) a >>= K (KHeap_D.set_cap (recv, tcb_pending_op_slot) b)) s) = snd (KHeap_D.set_cap (recv, tcb_pending_op_slot) b s)
theory Ipc_DR

lemma when_return:
  "when f (return ()) = return ()" by (simp add:when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. when f (return ()) = return ()
theory Ipc_DR

lemma dcorres_if_rhs:
  assumes G: "G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b"
  and nG: "\<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q' a c"
  shows "corres_underlying sr nf nf' rvr P
    (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s)) a (if G then b else c)" apply (clarsimp) apply (safe) apply (erule G) apply (erule nG) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' rvr P (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s)) a (if G then b else c) proof (prove)
goal (1 subgoal):
 1. (G \<longrightarrow> corres_underlying sr nf nf' rvr P Q a b) \<and> (\<not> G \<longrightarrow> corres_underlying sr nf nf' rvr P Q' a c) proof (prove)
goal (2 subgoals):
 1. G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b
 2. \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q' a c proof (prove)
goal (1 subgoal):
 1. \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q' a c proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma option_select_not_empty:
  "A\<noteq>{} \<Longrightarrow> option_select A = (do a\<leftarrow>select A;return (Some a) od)" by (clarsimp simp:option_select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {} \<Longrightarrow> option_select A = do a <- select A;
return (Some a)
od