kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma transform_cdt_none:
  "\<lbrakk> cte_at slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s);
       (cdt s) slot = None \<rbrakk>
    \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = None" apply (case_tac slot) apply (clarsimp simp: transform_cdt_def map_lift_over_eq_None) apply (rule ccontr, clarsimp) apply (subst(asm) transform_cslot_ptr_inj, simp_all) apply (drule(1) mdb_cte_atD) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = None\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = None; slot = (a, b)\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (a, b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s (a, b) = None; slot = (a, b); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba)\<rbrakk> \<Longrightarrow> cdt s (aa, ba) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>cte_wp_at (\<lambda>_. True) (a, b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s (a, b) = None; slot = (a, b); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); transform_cslot_ptr (a, b) = transform_cslot_ptr (aa, ba); cdt s (aa, ba) = Some (ab, bb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>cdt s (aa, ba) = Some (ab, bb); cte_wp_at (\<lambda>_. True) (a, b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s (a, b) = None; slot = (a, b); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>cte_wp_at (\<lambda>_. True) (a, b) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s (a, b) = None; slot = (a, b); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); swp (cte_wp_at ((\<noteq>) cap.NullCap)) s (ab, bb) \<and> swp (cte_wp_at ((\<noteq>) cap.NullCap)) s (aa, ba)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cdt_some:
  "\<lbrakk> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s);
      (cdt s) slot = Some slot' \<rbrakk>
  \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot)
          = Some (transform_cslot_ptr slot')" apply (case_tac slot) apply (case_tac slot') apply (clarsimp simp: transform_cdt_def map_lift_over_eq_Some
                        transform_cdt_slot_inj_on_mdb_cte_at) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = Some (transform_cslot_ptr slot') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'; slot = (a, b)\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = Some (transform_cslot_ptr slot') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s slot = Some slot'; slot = (a, b); slot' = (aa, ba)\<rbrakk> \<Longrightarrow> transform_cdt s (transform_cslot_ptr slot) = Some (transform_cslot_ptr slot') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); cdt s (a, b) = Some (aa, ba); slot = (a, b); slot' = (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>ab bb. transform_cslot_ptr (a, b) = transform_cslot_ptr (ab, bb) \<and> (\<exists>a b. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (a, b)) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cdt_some_rev:
  "\<lbrakk> transform_cdt s (transform_cslot_ptr slot_a)
           = Some (transform_cslot_ptr slot);
    cte_at slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s)(cdt s) \<rbrakk>
  \<Longrightarrow>\<exists>slot_b. transform_cslot_ptr slot_b
        = transform_cslot_ptr slot_a \<and> (cdt s) slot_b = Some slot" apply (clarsimp simp: transform_cdt_def map_lift_over_eq_Some) apply (subst(asm) transform_cslot_ptr_inj, assumption, simp_all) apply (drule(1) mdb_cte_atD, clarsimp simp: cte_wp_at_caps_of_state) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_cdt s (transform_cslot_ptr slot_a) = Some (transform_cslot_ptr slot); cte_wp_at (\<lambda>_. True) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrakk> \<Longrightarrow> \<exists>slot_b. transform_cslot_ptr slot_b = transform_cslot_ptr slot_a \<and> cdt s slot_b = Some slot proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr slot_a = transform_cslot_ptr (a, b); transform_cslot_ptr slot = transform_cslot_ptr (aa, ba); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>aa ba. transform_cslot_ptr (aa, ba) = transform_cslot_ptr (a, b) \<and> cdt s (aa, ba) = Some slot proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); cdt s (a, b) = Some (aa, ba); cte_wp_at (\<lambda>_. True) slot s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr slot_a = transform_cslot_ptr (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (aa, ba) s
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, ba) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr slot_a = transform_cslot_ptr (a, b); slot = (aa, ba); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>ab bb. transform_cslot_ptr (ab, bb) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (aa, ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, ba) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); transform_cslot_ptr slot_a = transform_cslot_ptr (a, b); slot = (aa, ba); inj_on transform_cslot_ptr (dom (cdt s) \<union> ran (cdt s)); cdt s (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>ab bb. transform_cslot_ptr (ab, bb) = transform_cslot_ptr (a, b) \<and> cdt s (ab, bb) = Some (aa, ba) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma page_table_not_in_cdt:"\<lbrakk>page_table_at a s;cte_wp_at P (a, ba) s\<rbrakk> \<Longrightarrow> False" apply (clarsimp simp:obj_at_def a_type_def) apply (clarsimp split:Structures_A.kernel_object.split_asm if_splits arch_kernel_obj.split_asm) apply (clarsimp simp:cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) a s; cte_wp_at P (a, ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>cte_wp_at P (a, ba) s; kheap s a = Some ko; (case ko of kernel_object.CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | kernel_object.Endpoint endpoint \<Rightarrow> AEndpoint | kernel_object.Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | arch_kernel_obj.PageTable pt \<Rightarrow> APageTable | arch_kernel_obj.PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cte_wp_at P (a, ba) s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cte_at_single_update : "cte_at x s \<Longrightarrow> cte_at x (abs_cdt_single_update s c p)" by (clarsimp simp:abs_cdt_single_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) x s \<Longrightarrow> cte_wp_at (\<lambda>_. True) x (abs_cdt_single_update s c p)
theory KHeap_DR

lemma cdt_single_remove_eq:
assumes mdb:"mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
shows
"\<lbrakk>cte_at c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) = transform_cdt (abs_cdt_single_remove s c)" apply (simp add: transform_cdt_def abs_cdt_single_remove_def) apply (subst map_lift_over_upd[unfolded fun_upd_def]) defer apply (rule ext) apply (clarsimp simp:cdl_cdt_single_remove_def transform_def transform_cdt_def) apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top>]) apply (auto simp: cte_wp_at_caps_of_state ran_def dest!: mdb_cte_atD [OF _ mdb]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) = transform_cdt (abs_cdt_single_remove s c) proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) = map_lift_over transform_cslot_ptr (\<lambda>x. if x = c then None else cdt s x) proof (prove)
goal (2 subgoals):
 1. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option None \<union> dom (cdt s) \<union> ran (cdt s))
 2. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) = (\<lambda>x. if x = transform_cslot_ptr c then map_option transform_cslot_ptr None else map_lift_over transform_cslot_ptr (cdt s) x) proof (prove)
goal (2 subgoals):
 1. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) = (\<lambda>x. if x = transform_cslot_ptr c then map_option transform_cslot_ptr None else map_lift_over transform_cslot_ptr (cdt s) x)
 2. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option None \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<And>x. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove (transform s) (transform_cslot_ptr c)) x = (if x = transform_cslot_ptr c then map_option transform_cslot_ptr None else map_lift_over transform_cslot_ptr (cdt s) x)
 2. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option None \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option None \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cte_wp_at (\<lambda>_. True) c s; x \<in> {c} \<union> set_option None \<union> dom (cdt s) \<union> ran (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x ?s6 proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma dom_onto_ex:
  "\<lbrakk>f =  h` g ; x\<in> f\<rbrakk> \<Longrightarrow> \<exists>t. h t = x \<and> t\<in> g" apply (clarsimp simp:dom_def image_def | rule conjI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = h ` g; x \<in> f\<rbrakk> \<Longrightarrow> \<exists>t. h t = x \<and> t \<in> g proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>f = {y. \<exists>x\<in>g. y = h x}; xa \<in> g; x = h xa\<rbrakk> \<Longrightarrow> \<exists>t. h t = h xa \<and> t \<in> g proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma dom_onto_is:
  "\<lbrakk>f =  h` g ; x\<in> g\<rbrakk> \<Longrightarrow> h x \<in> f" apply (clarsimp simp: image_def) apply (rule bexI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = h ` g; x \<in> g\<rbrakk> \<Longrightarrow> h x \<in> f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = {y. \<exists>x\<in>g. y = h x}; x \<in> g\<rbrakk> \<Longrightarrow> \<exists>xa\<in>g. h x = h xa proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f = {y. \<exists>x\<in>g. y = h x}; x \<in> g\<rbrakk> \<Longrightarrow> h x = h ?x4
 2. \<lbrakk>f = {y. \<exists>x\<in>g. y = h x}; x \<in> g\<rbrakk> \<Longrightarrow> ?x4 \<in> g proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cdl_remove_parent_def':
 "remove_parent slot =
  modify (\<lambda>s. cdl_cdt_single_remove (cdl_cdt_set_update s
                                       {x. if cdl_cdt s x = Some slot then True else False}
                                       (\<lambda>x. cdl_cdt s slot)) slot)" apply (clarsimp simp:remove_parent_def simpler_modify_def bind_def) apply (rule ext) apply (clarsimp simp:cdl_cdt_single_remove_def cdl_cdt_set_update_def cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. remove_parent slot = modify (\<lambda>s. cdl_cdt_single_remove (cdl_cdt_set_update s {x. if cdl_cdt s x = Some slot then True else False} (\<lambda>x. cdl_cdt s slot)) slot) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({((), s\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt s x = Some slot then cdl_cdt s slot else cdl_cdt s x\<rparr>)}, False)) = (\<lambda>s. ({((), cdl_cdt_single_remove (cdl_cdt_set_update s {x. cdl_cdt s x = Some slot} (\<lambda>x. cdl_cdt s slot)) slot)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. ({((), s\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt s x = Some slot then cdl_cdt s slot else cdl_cdt s x\<rparr>)}, False) = ({((), cdl_cdt_single_remove (cdl_cdt_set_update s {x. cdl_cdt s x = Some slot} (\<lambda>x. cdl_cdt s slot)) slot)}, False) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cdt_single_update_helper:
  "s' = transform s \<Longrightarrow> cdl_cdt (cdl_cdt_single_update s' a b) = transform_cdt (abs_cdt_single_update s a' b') \<Longrightarrow> (cdl_cdt_single_update s' a b ) = transform (abs_cdt_single_update s a' b')" by (clarsimp simp:cdl_cdt_single_update_def abs_cdt_single_update_def transform_def transform_current_thread_def transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' = transform s; cdl_cdt (cdl_cdt_single_update s' a b) = transform_cdt (abs_cdt_single_update s a' b')\<rbrakk> \<Longrightarrow> cdl_cdt_single_update s' a b = transform (abs_cdt_single_update s a' b')
theory KHeap_DR

lemma transform_cdt_set_update_helper:
  "s' = transform s \<Longrightarrow> cdl_cdt (cdl_cdt_set_update s' df f) = transform_cdt (abs_cdt_set_update s dg g) \<Longrightarrow> (cdl_cdt_set_update s' df f ) = transform (abs_cdt_set_update s dg g)" by (clarsimp simp:cdl_cdt_set_update_def abs_cdt_set_update_def transform_def transform_current_thread_def transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' = transform s; cdl_cdt (cdl_cdt_set_update s' df f) = transform_cdt (abs_cdt_set_update s dg g)\<rbrakk> \<Longrightarrow> cdl_cdt_set_update s' df f = transform (abs_cdt_set_update s dg g)
theory KHeap_DR

lemma transform_cdt_single_remove_helper:
  "s'= transform s \<Longrightarrow> cdl_cdt (cdl_cdt_single_remove s' a) = transform_cdt (abs_cdt_single_remove s a') \<Longrightarrow> (cdl_cdt_single_remove (transform s) a) = transform (abs_cdt_single_remove s a')" by (clarsimp simp:cdl_cdt_single_remove_def abs_cdt_single_remove_def transform_def transform_current_thread_def transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' = transform s; cdl_cdt (cdl_cdt_single_remove s' a) = transform_cdt (abs_cdt_single_remove s a')\<rbrakk> \<Longrightarrow> cdl_cdt_single_remove (transform s) a = transform (abs_cdt_single_remove s a')
theory KHeap_DR

lemma dcorres_gets_all_param:
  "(\<And>x. dcorres R P P' h (g x)) \<Longrightarrow> dcorres R P P' h (do x \<leftarrow> gets f; g x od)" by (clarsimp simp: corres_underlying_def bind_def gets_def get_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. dcorres R P P' h (g x)) \<Longrightarrow> dcorres R P P' h (gets f >>= g)
theory KHeap_DR

lemma empty_slot_ext_dcorres: "dcorres dc P P' (return ()) (empty_slot_ext slot v)" apply (clarsimp simp: empty_slot_ext_def) apply (auto simp: corres_underlying_def update_cdt_list_def set_cdt_list_def
                        modify_def bind_def put_def gets_def get_def return_def  split: option.splits if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (empty_slot_ext slot v) proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) (update_cdt_list (\<lambda>list. case v of None \<Rightarrow> list(slot := []) | Some p \<Rightarrow> if p = slot then list(p := list_remove (list p) slot) else list(p := list_replace_list (list p) slot (list slot), slot := []))) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cap_case_irq_handler_not[simp]: "\<forall>irq. v \<noteq> cap.IRQHandlerCap irq \<Longrightarrow> (case v of cap.IRQHandlerCap irq \<Rightarrow> f irq | _ \<Rightarrow> g) = g" by (case_tac v; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>irq. v \<noteq> IRQHandlerCap irq \<Longrightarrow> (case v of IRQHandlerCap irq \<Rightarrow> f irq | _ \<Rightarrow> g) = g
theory KHeap_DR

lemma ntfn_not_waiting_ep_recv:
  "\<lbrakk> valid_objs s;kheap s epptr = Some (kernel_object.Notification ntfn) \<rbrakk>
        \<Longrightarrow> ep_waiting_set_recv epptr s = {}" apply (rule set_eqI) apply (clarsimp simp: ep_waiting_set_recv_def) apply (simp add: valid_objs_def) apply (rename_tac ptr t payload) apply (drule_tac x=ptr in bspec) apply (clarsimp simp: dom_def) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def obj_at_def is_ep_def
                 split: Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s epptr = Some (kernel_object.Notification ntfn)\<rbrakk> \<Longrightarrow> ep_waiting_set_recv epptr s = {} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_objs s; kheap s epptr = Some (kernel_object.Notification ntfn)\<rbrakk> \<Longrightarrow> (x \<in> ep_waiting_set_recv epptr s) = (x \<in> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>valid_objs s; kheap s epptr = Some (kernel_object.Notification ntfn); kheap s x = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s epptr = Some (kernel_object.Notification ntfn); kheap s x = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr t payload. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s epptr = Some (kernel_object.Notification ntfn); kheap s ptr = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptr t payload. \<lbrakk>kheap s epptr = Some (kernel_object.Notification ntfn); kheap s ptr = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload\<rbrakk> \<Longrightarrow> ptr \<in> dom (kheap s)
 2. \<And>ptr t payload. \<lbrakk>kheap s epptr = Some (kernel_object.Notification ntfn); kheap s ptr = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload; \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptr t payload. \<lbrakk>kheap s epptr = Some (kernel_object.Notification ntfn); kheap s ptr = Some (TCB t); tcb_state t = BlockedOnReceive epptr payload; \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma ep_q_refs_of_no_TCBBound[simp]:
  "(x, TCBBound) \<notin> ep_q_refs_of ep" by (clarsimp simp: ep_q_refs_of_def split: Structures_A.endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, TCBBound) \<notin> ep_q_refs_of ep
theory KHeap_DR

lemma ntfn_bound_refs_no_TCBBound[simp]:
  "(x, TCBBound) \<notin> ntfn_bound_refs ep" by (clarsimp simp: ntfn_bound_refs_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, TCBBound) \<notin> ntfn_bound_refs ep
theory KHeap_DR

lemma kheap_to_ko_at:
  "kheap s x = Some aa \<Longrightarrow> ko_at aa x s" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s x = Some aa \<Longrightarrow> ko_at aa x s
theory KHeap_DR

lemma filter_modify_empty_corres:
  "filter_set = {}  \<Longrightarrow> dcorres dc \<top> \<top> (tcb_filter_modify filter_set f)
             (return a)" by (clarsimp simp:corres_underlying_def tcb_filter_modify_def return_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filter_set = {} \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (tcb_filter_modify filter_set f) (return a)
theory KHeap_DR

lemma valid_objs_valid_ep_simp:
  "\<lbrakk>valid_objs s;kheap s epptr = Some (kernel_object.Endpoint ep)\<rbrakk> \<Longrightarrow> valid_ep ep s" apply (simp add:valid_objs_def) apply (drule_tac x = epptr in bspec) apply (simp add: dom_def) apply (clarsimp simp: valid_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s epptr = Some (kernel_object.Endpoint ep)\<rbrakk> \<Longrightarrow> valid_ep ep s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s epptr = Some (kernel_object.Endpoint ep)\<rbrakk> \<Longrightarrow> valid_ep ep s proof (prove)
goal (2 subgoals):
 1. kheap s epptr = Some (kernel_object.Endpoint ep) \<Longrightarrow> epptr \<in> dom (kheap s)
 2. \<lbrakk>kheap s epptr = Some (kernel_object.Endpoint ep); \<exists>obj. kheap s epptr = Some obj \<and> valid_obj epptr obj s\<rbrakk> \<Longrightarrow> valid_ep ep s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s epptr = Some (kernel_object.Endpoint ep); \<exists>obj. kheap s epptr = Some obj \<and> valid_obj epptr obj s\<rbrakk> \<Longrightarrow> valid_ep ep s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma tcb_type_set_obj_ep:
  "\<lbrace>(=) s'a\<rbrace> KHeap_A.set_object word1 (kernel_object.Endpoint Structures_A.endpoint.IdleEP)
   \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace>" including unfold_objects by (wpsimp wp: set_object_wp_strong simp: a_type_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s'a\<rbrace> KHeap_A.set_object word1 (kernel_object.Endpoint IdleEP) \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s'a\<rbrace> KHeap_A.set_object word1 (kernel_object.Endpoint IdleEP) \<lbrace>\<lambda>r s. \<forall>x. tcb_at x s \<longrightarrow> tcb_at x s'a\<rbrace>