kings-crown/FVELER_Isabelle huggingface dataset:
theory Separation_SD

lemma sep_map_S_decomp':
  "\<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk>
  \<Longrightarrow> obj_id \<mapsto>S obj = ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj)" apply (rule ext, rename_tac s) apply (clarsimp simp: sep_map_S_def sep_map_S'_def) apply (subgoal_tac "(Slot ` slots) \<inter> (Slot ` (UNIV - slots)) = {}") apply (drule_tac p=obj_id and obj=obj and s=s in sep_map_decomp) apply clarsimp apply (clarsimp simp: image_Un [THEN sym]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> (obj_id \<mapsto>S obj) s = ((obj_id, slots) \<mapsto>S' obj \<and>* (obj_id, UNIV - slots) \<mapsto>S' obj) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (UNIV - {Fields}) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj (Slot ` (UNIV - slots))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV; Slot ` slots \<inter> Slot ` (UNIV - slots) = {}\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (UNIV - {Fields}) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj (Slot ` (UNIV - slots))) s
 2. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> Slot ` (UNIV - slots) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV; (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj (Slot ` (UNIV - slots))) s = sep_map_general obj_id obj (Slot ` slots \<union> Slot ` (UNIV - slots)) s\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (UNIV - {Fields}) s = (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj (Slot ` (UNIV - slots))) s
 2. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> Slot ` (UNIV - slots) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV; (sep_map_general obj_id obj (Slot ` slots) \<and>* sep_map_general obj_id obj (Slot ` (UNIV - slots))) s = sep_map_general obj_id obj (Slot ` slots \<union> Slot ` (UNIV - slots)) s\<rbrakk> \<Longrightarrow> sep_map_general obj_id obj (UNIV - {Fields}) s = sep_map_general obj_id obj (Slot ` slots \<union> Slot ` (UNIV - slots)) s
 2. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> Slot ` (UNIV - slots) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slots \<noteq> {}; slots \<noteq> UNIV\<rbrakk> \<Longrightarrow> Slot ` slots \<inter> Slot ` (UNIV - slots) = {} proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_S_decomp_list:
  "\<lbrakk>dom (object_slots obj) = set slots; distinct slots\<rbrakk> \<Longrightarrow>
   (obj_id \<mapsto>S obj) = (\<And>* map (\<lambda>slot. (obj_id,slot) \<mapsto>s obj) slots  \<and>* obj_id \<mapsto>E obj)" by (metis sep_list_conj_sep_map_set_conj sep_map_S_decomp List.finite_set)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom (object_slots obj) = set slots; distinct slots\<rbrakk> \<Longrightarrow> obj_id \<mapsto>S obj = (\<And>* map (\<lambda>slot. (obj_id, slot) \<mapsto>s obj) slots \<and>* obj_id \<mapsto>E obj)
theory Separation_SD

lemma sep_map_general_strictly_exact:
  "strictly_exact (sep_map_general obj_id obj comp_ids)" apply (clarsimp simp: strictly_exact_def sep_map_general_def) apply (case_tac h, case_tac h', clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strictly_exact (sep_map_general obj_id obj comp_ids) proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>sep_heap h = object_to_sep_state obj_id obj comp_ids; sep_irq_node h = (\<lambda>x. None); sep_heap h' = object_to_sep_state obj_id obj comp_ids; sep_irq_node h' = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_general_precise:
  "precise (sep_map_general obj_id obj comp_ids)" by (rule strictly_precise, rule sep_map_general_strictly_exact)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. precise (sep_map_general obj_id obj comp_ids)
theory Separation_SD

lemma sep_map_c_strictly_exact:
  "strictly_exact (ptr \<mapsto>c cap)" apply (case_tac ptr) apply (clarsimp simp: strictly_exact_def sep_map_c_def_alt) apply (case_tac h, case_tac h', clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strictly_exact (ptr \<mapsto>c cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b. ptr = (a, b) \<Longrightarrow> strictly_exact (ptr \<mapsto>c cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b h h'. \<lbrakk>ptr = (a, b); sep_heap h = cap_to_sep_state a cap b; sep_irq_node h = (\<lambda>x. None); sep_heap h' = cap_to_sep_state a cap b; sep_irq_node h' = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_c_precise:
  "precise (ptr \<mapsto>c cap)" by (rule strictly_precise, rule sep_map_c_strictly_exact)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. precise (ptr \<mapsto>c cap)
theory Separation_SD

lemma sep_map_irq_strictly_exact:
  "strictly_exact (irq \<mapsto>irq obj_id)" apply (clarsimp simp: strictly_exact_def sep_map_irq_def) apply (case_tac h, case_tac h', clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strictly_exact (irq \<mapsto>irq obj_id) proof (prove)
goal (1 subgoal):
 1. \<And>h h'. \<lbrakk>sep_heap h = (\<lambda>x. None); sep_irq_node h = [irq \<mapsto> obj_id]; sep_heap h' = (\<lambda>x. None); sep_irq_node h' = [irq \<mapsto> obj_id]\<rbrakk> \<Longrightarrow> h = h' proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_irq_precise:
  "precise (irq \<mapsto>irq obb_id)" by (rule strictly_precise, rule sep_map_irq_strictly_exact)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. precise (irq \<mapsto>irq obb_id)
theory Frame_SD

lemma dom_object_to_sep_state:
  "dom (object_to_sep_state ptr obj cmp) = {ptr} \<times> cmp" apply (clarsimp simp: object_to_sep_state_def split:if_splits) apply (auto simp:object_project_def split:if_splits cdl_component_id.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (object_to_sep_state ptr obj cmp) = {ptr} \<times> cmp proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id \<in> cmp then Some (object_project comp_id obj) else None) = {ptr} \<times> cmp proof (prove)
goal:
No subgoals!
theory Frame_SD

lemma object_to_sep_state_restrict:
  "object_to_sep_state obj_id obj M |` ({obj_id} \<times> m) = object_to_sep_state obj_id obj (M \<inter> m)" by (rule ext,
    clarsimp simp:object_to_sep_state_def restrict_map_def
    split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_to_sep_state obj_id obj M |` ({obj_id} \<times> m) = object_to_sep_state obj_id obj (M \<inter> m)
theory Frame_SD

lemma object_to_sep_state_add:
  "\<lbrakk>{obj_id} \<times> m \<inter> dom M = {};b\<in> m\<rbrakk> \<Longrightarrow>
   (object_to_sep_state obj_id obj m ++ M) (obj_id, b)
   = Some (object_project b obj)" apply (subgoal_tac "(obj_id, b)\<in> {obj_id} \<times> m") apply (drule(1) inter_empty_not_both) apply (clarsimp simp:object_to_sep_state_def map_add_def dom_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m\<rbrakk> \<Longrightarrow> (object_to_sep_state obj_id obj m ++ M) (obj_id, b) = Some (object_project b obj) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m; (obj_id, b) \<in> {obj_id} \<times> m\<rbrakk> \<Longrightarrow> (object_to_sep_state obj_id obj m ++ M) (obj_id, b) = Some (object_project b obj)
 2. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m\<rbrakk> \<Longrightarrow> (obj_id, b) \<in> {obj_id} \<times> m proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m; (obj_id, b) \<notin> dom M\<rbrakk> \<Longrightarrow> (object_to_sep_state obj_id obj m ++ M) (obj_id, b) = Some (object_project b obj)
 2. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m\<rbrakk> \<Longrightarrow> (obj_id, b) \<in> {obj_id} \<times> m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{obj_id} \<times> m \<inter> dom M = {}; b \<in> m\<rbrakk> \<Longrightarrow> (obj_id, b) \<in> {obj_id} \<times> m proof (prove)
goal:
No subgoals!
theory Frame_SD

lemma singleton_intersect:
  "({x} \<times> UNIV \<inter> A = {}) = (\<forall>y. (x,y) \<notin> A)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({x} \<times> UNIV \<inter> A = {}) = (\<forall>y. (x, y) \<notin> A)
theory Frame_SD

lemma disjoint_union_diff:
  "a \<inter> b = {} \<Longrightarrow> a \<union> b - a = b" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<inter> b = {} \<Longrightarrow> a \<union> b - a = b
theory Frame_SD

lemma intent_reset_update_slots_single:
  "intent_reset (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj)
  = update_slots ((object_slots (intent_reset obj))(slot \<mapsto> cap)) (intent_reset obj)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset (update_slots ((object_slots obj)(slot \<mapsto> cap)) obj) = update_slots ((object_slots (intent_reset obj))(slot \<mapsto> cap)) (intent_reset obj)
theory Frame_SD

lemma sep_any_exist:
  "( sep_any m p \<and>* R ) s = (\<exists>x. ( m p x \<and>* R ) s)" by (auto simp:sep_state_projection_def
    sep_any_def sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_any m p \<and>* R) s = (\<exists>x. (m p x \<and>* R) s)
theory Frame_SD

lemma object_project_slot:
  "object_project (Slot slot) obj =
   CDL_Cap (object_slots (object_clean obj) slot)" by (clarsimp simp:object_project_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_project (Slot slot) obj = CDL_Cap (object_slots (object_clean obj) slot)
theory Frame_SD

lemma intent_reset_has_slots:
  "intent_reset obj = intent_reset obj' \<Longrightarrow> has_slots obj = has_slots obj'" by (clarsimp simp:intent_reset_def  has_slots_def
    split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset obj = intent_reset obj' \<Longrightarrow> has_slots obj = has_slots obj'
theory Frame_SD

lemma object_clean_has_slots:
  "object_clean obj = object_clean obj' \<Longrightarrow> has_slots obj = has_slots obj'" by (clarsimp simp:object_clean_def2
    dest!: asid_reset_has_slots intent_reset_has_slots)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean obj = object_clean obj' \<Longrightarrow> has_slots obj = has_slots obj'
theory Frame_SD

lemma set_object_slot_wp:
 "\<lbrace>\<lambda>s. <(obj_id, slot) \<mapsto>c - \<and>* R> s \<and>
       cdl_objects s obj_id = Some obj \<and>
       (\<exists>obj'. object_clean obj = object_clean obj' \<and>
       nobj = (update_slots ((object_slots obj') (slot \<mapsto> cap)) obj'))\<rbrace>
  set_object obj_id nobj
  \<lbrace>\<lambda>rv. <(obj_id, slot) \<mapsto>c cap \<and>* R>\<rbrace>" apply (rule hoare_name_pre_state) apply clarsimp apply (rule hoare_weaken_pre) apply (rule set_object_slot_wp_helper) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some obj \<and> (\<exists>obj'. object_clean obj = object_clean obj' \<and> nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj')\<rbrace> set_object obj_id nobj \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s \<and> cdl_objects s obj_id = Some obj \<and> (\<exists>obj'. object_clean obj = object_clean obj' \<and> nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj') \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_object obj_id nobj \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s obj'. \<lbrakk>cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some obj; object_clean obj = object_clean obj'; nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_object obj_id (update_slots ((object_slots obj')(slot \<mapsto> cap)) obj') \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s obj'. \<lbrakk>cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some obj; object_clean obj = object_clean obj'; nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s obj'\<rbrace> set_object obj_id (update_slots ((object_slots obj')(slot \<mapsto> cap)) obj') \<lbrace>\<lambda>rv. cdl.lift ((obj_id, slot) \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>s obj' sa. \<lbrakk>cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some obj; object_clean obj = object_clean obj'; nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'; s = sa\<rbrakk> \<Longrightarrow> ?Q8 s obj' sa proof (prove)
goal (1 subgoal):
 1. \<And>s obj' sa. \<lbrakk>cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) s; cdl_objects s obj_id = Some obj; object_clean obj = object_clean obj'; nobj = update_slots ((object_slots obj')(slot \<mapsto> cap)) obj'; s = sa\<rbrakk> \<Longrightarrow> cdl.lift ((obj_id, slot) \<mapsto>c - \<and>* R) sa \<and> cdl_objects sa obj_id = Some (?obj11 s obj') \<and> object_clean (?obj11 s obj') = object_clean obj' proof (prove)
goal:
No subgoals!
theory Frame_SD

lemma object_wipe_slots_object_clean:
  "object_wipe_slots (object_clean obj) = object_clean (object_wipe_slots obj)" apply (case_tac obj, simp_all add: object_wipe_slots_def object_clean_def
                       intent_reset_def asid_reset_def update_slots_def object_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_wipe_slots (object_clean obj) = object_clean (object_wipe_slots obj) proof (prove)
goal:
No subgoals!
theory Frame_SD

lemma object_wipe_slots_intent_reset:
  "object_wipe_slots (intent_reset obj) = intent_reset (object_wipe_slots obj)" by (case_tac obj,simp_all add:object_wipe_slots_def update_slots_def intent_reset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_wipe_slots (intent_reset obj) = intent_reset (object_wipe_slots obj)
theory Frame_SD

lemma set_cdl_tcb_intent_wp:
  "\<lbrace>\<lambda>s. <obj_id \<mapsto>f Tcb tcb \<and>* R> s\<rbrace>
    update_thread obj_id (\<lambda>tcb. tcb\<lparr>cdl_tcb_intent := x\<rparr>)
   \<lbrace>\<lambda>rv s. <obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>) \<and>* R> s\<rbrace>" apply (rule hoare_weaken_pre) apply (wp set_cdl_tcb_field_wp) apply (clarsimp simp: object_wipe_slots_def object_clean_def update_slots_def
                          asid_reset_def object_slots_def intent_reset_def) apply (clarsimp simp: object_slots_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R)\<rbrace> update_thread obj_id (cdl_tcb_intent_update (\<lambda>_. x)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>) \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> update_thread obj_id (cdl_tcb_intent_update (\<lambda>_. x)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>) \<and>* R)\<rbrace>
 2. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcb'. object_clean (object_wipe_slots (Tcb tcb)) = object_clean (object_wipe_slots (Tcb tcb')) \<Longrightarrow> object_clean (object_wipe_slots (Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>))) = object_clean (object_wipe_slots (Tcb (tcb'\<lparr>cdl_tcb_intent := x\<rparr>)))
 2. \<And>tcb. object_slots (Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>)) = object_slots (Tcb tcb)
 3. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. object_slots (Tcb (tcb\<lparr>cdl_tcb_intent := x\<rparr>)) = object_slots (Tcb tcb)
 2. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal:
No subgoals!
theory Frame_SD

lemma set_cdl_tcb_fault_endpoint_wp:
  "\<lbrace>\<lambda>s. <obj_id \<mapsto>f Tcb tcb \<and>* R> s\<rbrace>
    update_thread obj_id (\<lambda>tcb. tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)
   \<lbrace>\<lambda>rv s. <obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>) \<and>* R> s\<rbrace>" apply (rule hoare_weaken_pre) apply (wp set_cdl_tcb_field_wp) apply (clarsimp simp: object_wipe_slots_def asid_reset_def update_slots_def
                          object_clean_def object_slots_def intent_reset_def) apply (case_tac tcb,case_tac tcb',simp) apply (clarsimp simp:object_slots_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R)\<rbrace> update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>) \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> update_thread obj_id (cdl_tcb_fault_endpoint_update (\<lambda>_. x)) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>) \<and>* R)\<rbrace>
 2. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcb'. object_clean (object_wipe_slots (Tcb tcb)) = object_clean (object_wipe_slots (Tcb tcb')) \<Longrightarrow> object_clean (object_wipe_slots (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>))) = object_clean (object_wipe_slots (Tcb (tcb'\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)))
 2. \<And>tcb. object_slots (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) = object_slots (Tcb tcb)
 3. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal (3 subgoals):
 1. \<And>tcb tcb'. tcb\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = tcb'\<lparr>cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> \<Longrightarrow> tcb\<lparr>cdl_tcb_fault_endpoint := x, cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr> = tcb'\<lparr>cdl_tcb_fault_endpoint := x, cdl_tcb_caps := \<lambda>x. None, cdl_tcb_intent := undefined\<rparr>
 2. \<And>tcb. object_slots (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) = object_slots (Tcb tcb)
 3. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal (2 subgoals):
 1. \<And>tcb. object_slots (Tcb (tcb\<lparr>cdl_tcb_fault_endpoint := x\<rparr>)) = object_slots (Tcb tcb)
 2. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f Tcb tcb \<and>* R) s proof (prove)
goal:
No subgoals!
theory ProofHelpers_DP

lemma do_kernel_op_wp:
  assumes "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>_ s. Q s \<rbrace>"
  shows "\<lbrace> P \<circ> kernel_state \<rbrace> do_kernel_op f \<lbrace> \<lambda>_ s. Q (kernel_state s) \<rbrace>" using assms apply (simp only: do_kernel_op_def split_def) apply wp apply (simp add: valid_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P \<circ> kernel_state\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P \<circ> kernel_state\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P \<circ> kernel_state\<rbrace> do ms <- gets kernel_state;
p <- select_f (f ms);
modify (kernel_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; (P \<circ> kernel_state) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (kernel_state s)). Q (kernel_state (s\<lparr>kernel_state := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory ProofHelpers_DP

lemma option_select_none_wp [wp]:
  "\<lbrace>\<lambda>s. P s \<and> xs = {}\<rbrace>
    option_select xs
   \<lbrace>\<lambda>rv s. P s \<and> K (rv = None) s\<rbrace>" apply (clarsimp simp: option_select_def) by (wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> xs = {}\<rbrace> option_select xs \<lbrace>\<lambda>rv s. P s \<and> K (rv = None) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. xs = {} \<Longrightarrow> \<lbrace>P\<rbrace> return None \<lbrace>\<lambda>rv s. P s \<and> rv = None\<rbrace>
theory ProofHelpers_DP

lemma sep_conj_zip_take_drop:
  "\<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow>
   (\<And>* map (\<lambda>(x, y). f x y) (take n (zip xs ys)) \<and>*
    f (xs ! n) a \<and>*
    \<And>* map (\<lambda>(x, y). f x y) (drop (Suc n) (zip xs ys)))
  =
   (\<And>* map (\<lambda>(x, y). f x y) (zip xs (take n ys @ a # drop (Suc n) ys)))" apply (subst zip_take_drop, assumption, assumption) apply (subst take_zip) apply (subst drop_zip) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> (\<And>* map (\<lambda>(x, y). f x y) (take n (zip xs ys)) \<and>* f (xs ! n) a \<and>* \<And>* map (\<lambda>(x, y). f x y) (drop (Suc n) (zip xs ys))) = \<And>* map2 f xs (take n ys @ a # drop (Suc n) ys) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> (\<And>* map (\<lambda>(x, y). f x y) (take n (zip xs ys)) \<and>* f (xs ! n) a \<and>* \<And>* map (\<lambda>(x, y). f x y) (drop (Suc n) (zip xs ys))) = \<And>* map (\<lambda>(x, y). f x y) (zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> (\<And>* map2 f (take n xs) (take n ys) \<and>* f (xs ! n) a \<and>* \<And>* map (\<lambda>(x, y). f x y) (drop (Suc n) (zip xs ys))) = \<And>* map (\<lambda>(x, y). f x y) (zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> (\<And>* map2 f (take n xs) (take n ys) \<and>* f (xs ! n) a \<and>* \<And>* map2 f (drop (Suc n) xs) (drop (Suc n) ys)) = \<And>* map (\<lambda>(x, y). f x y) (zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)) proof (prove)
goal:
No subgoals!