kings-crown/FVELER_Isabelle huggingface dataset:
theory RWHelper_DP

lemma sep_irq_node_dom_simps:
  "sep_irq_node_dom (slot \<mapsto>c -) {}"
  "sep_irq_node_dom (slot \<mapsto>c cap) {}" apply (simp add:sep_map_rewrite_any sep_irq_node_dom_sep_map_predicate) apply (simp add:sep_map_rewrite_spec sep_irq_node_dom_sep_map_predicate split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_irq_node_dom (slot \<mapsto>c -) {} &&& sep_irq_node_dom (slot \<mapsto>c cap) {} proof (prove)
goal (1 subgoal):
 1. sep_irq_node_dom (slot \<mapsto>c cap) {} proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_map_spec_conj:
  "\<lbrakk>sep_map_spec P s; sep_map_spec P' s'\<rbrakk>
    \<Longrightarrow> sep_map_spec (P \<and>* P')
                     (SepState (sep_heap s ++ sep_heap s')
                               (sep_irq_node s ++ sep_irq_node s'))" by (clarsimp simp: sep_map_spec_def sep_conj_def
                     plus_sep_state_def sep_state_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_map_spec P s; sep_map_spec P' s'\<rbrakk> \<Longrightarrow> sep_map_spec (P \<and>* P') (SepState (sep_heap s ++ sep_heap s') (sep_irq_node s ++ sep_irq_node s'))
theory RWHelper_DP

lemma sep_spec_simps:
  "sep_map_spec (slot \<mapsto>c cap)
  (SepState [(fst slot,Slot (snd slot)) \<mapsto> (CDL_Cap (Some (reset_cap_asid cap)))]
            Map.empty)" apply (clarsimp simp:sep_map_spec_def sep_map_c_def sep_map_general_def) apply (case_tac s') apply (clarsimp simp:object_to_sep_state_def) apply (rule ext) apply (clarsimp simp: object_project_def object_slots_object_clean
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_map_spec (slot \<mapsto>c cap) (SepState [(fst slot, Slot (snd slot)) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x y obj. \<lbrakk>slot = (x, y); sep_heap s' = object_to_sep_state x obj {Slot y}; sep_irq_node s' = (\<lambda>x. None); object_slots obj = [y \<mapsto> cap]\<rbrakk> \<Longrightarrow> s' = SepState [(x, Slot y) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>s' x y obj x1 x2. \<lbrakk>slot = (x, y); sep_heap s' = object_to_sep_state x obj {Slot y}; sep_irq_node s' = (\<lambda>x. None); object_slots obj = [y \<mapsto> cap]; s' = SepState x1 x2\<rbrakk> \<Longrightarrow> s' = SepState [(x, Slot y) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>x y obj. \<lbrakk>slot = (x, y); object_slots obj = [y \<mapsto> cap]\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id', comp_id). if obj_id' = x \<and> comp_id = Slot y then Some (object_project comp_id obj) else None) = [(x, Slot y) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] proof (prove)
goal (1 subgoal):
 1. \<And>x y obj xa. \<lbrakk>slot = (x, y); object_slots obj = [y \<mapsto> cap]\<rbrakk> \<Longrightarrow> (case xa of (obj_id', comp_id) \<Rightarrow> if obj_id' = x \<and> comp_id = Slot y then Some (object_project comp_id obj) else None) = [(x, Slot y) \<mapsto> CDL_Cap (Some (reset_cap_asid cap))] xa proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_conj_spec:
  "\<lbrakk> < P \<and>* Q > s\<rbrakk>
   \<Longrightarrow> \<exists>s'. < P \<and>* (=) s' > s" by (auto simp:sep_state_projection_def sep_conj_def
    sep_disj_sep_state_def sep_state_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (P \<and>* Q) s \<Longrightarrow> \<exists>s'. cdl.lift (P \<and>* (=) s') s
theory RWHelper_DP

lemma sep_conj_spec_value:
  "\<lbrakk> < P \<and>* (=) s' > s; sep_heap_dom P m; p \<notin> m\<rbrakk>
  \<Longrightarrow> (sep_heap s') p = (sep_heap (sep_state_projection s) |` (UNIV - m)) p" apply (clarsimp simp:sep_state_projection_def sep_conj_def
    sep_disj_sep_state_def sep_state_disj_def) apply (drule(2) sep_heap_domD) apply (simp add: plus_sep_state_def sep_state_add_def
            split: sep_state.splits) apply (clarsimp simp: map_add_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift (P \<and>* (=) s') s; sep_heap_dom P m; p \<notin> m\<rbrakk> \<Longrightarrow> sep_heap s' p = (cdl.lift sep_heap s |` (UNIV - m)) p proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>sep_heap_dom P m; p \<notin> m; sep_heap x \<bottom> sep_heap s'; sep_irq_node x \<bottom> sep_irq_node s'; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + s'; P x\<rbrakk> \<Longrightarrow> sep_heap s' p = (case p of (obj_id, comp_id) \<Rightarrow> map_option (object_project comp_id) (cdl_objects s obj_id)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<notin> m; sep_heap x \<bottom> sep_heap s'; sep_irq_node x \<bottom> sep_irq_node s'; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + s'; P x; p \<notin> dom (sep_heap x)\<rbrakk> \<Longrightarrow> sep_heap s' p = (case p of (obj_id, comp_id) \<Rightarrow> map_option (object_project comp_id) (cdl_objects s obj_id)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>p \<notin> m; sep_heap x \<bottom> sep_heap s'; sep_irq_node x \<bottom> sep_irq_node s'; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap x ++ sep_heap s' \<and> (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node x ++ sep_irq_node s'; P x; p \<notin> dom (sep_heap x)\<rbrakk> \<Longrightarrow> sep_heap s' p = (sep_heap x ++ sep_heap s') p proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma write_estimate_via_sep:
  assumes sep_valid: "\<And>obj Q. \<lbrace>\<lambda>s. < P \<and>* Q > s \<rbrace>
    f \<lbrace>\<lambda>r s. < P' \<and>* Q > s \<rbrace>"
  and sep_heap_dom: "sep_heap_dom P m"
  and sep_heap_dom': "sep_heap_dom P' m"
  shows "IsSepWritingEstimateOf f (\<lambda>s. < P \<and>* Q> s)
    (\<lambda>s.  sep_heap (sep_state_projection s)) m" apply (clarsimp simp: valid_def IsSepWritingEstimateOf_def) apply (drule sep_conj_spec) apply clarsimp apply (drule use_valid[OF _ sep_valid]) apply simp apply (drule(1) sep_conj_spec_value[OF _ sep_heap_dom]) apply (drule(1) sep_conj_spec_value[OF _ sep_heap_dom']) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. IsSepWritingEstimateOf f (cdl.lift (P \<and>* Q)) (cdl.lift sep_heap) m proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba. \<lbrakk>(aa, ba) \<in> fst (f s); cdl.lift (P \<and>* Q) s; (a, b) \<notin> m\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba. \<lbrakk>(aa, ba) \<in> fst (f s); (a, b) \<notin> m; \<exists>s'. cdl.lift (P \<and>* (=) s') s\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba s'. \<lbrakk>(aa, ba) \<in> fst (f s); (a, b) \<notin> m; cdl.lift (P \<and>* (=) s') s\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b s aa ba s'. \<lbrakk>(a, b) \<notin> m; cdl.lift (P \<and>* (=) s') s\<rbrakk> \<Longrightarrow> cdl.lift (P \<and>* ?Q21 a b s aa ba s') s
 2. \<And>a b s aa ba s'. \<lbrakk>(a, b) \<notin> m; cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* ?Q21 a b s aa ba s') ba\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba s'. \<lbrakk>(a, b) \<notin> m; cdl.lift (P \<and>* (=) s') s; cdl.lift (P' \<and>* (=) s') ba\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba s'. \<lbrakk>(a, b) \<notin> m; cdl.lift (P' \<and>* (=) s') ba; sep_heap s' (a, b) = (cdl.lift sep_heap s |` (UNIV - m)) (a, b)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s aa ba s'. \<lbrakk>(a, b) \<notin> m; sep_heap s' (a, b) = (cdl.lift sep_heap s |` (UNIV - m)) (a, b); sep_heap s' (a, b) = (cdl.lift sep_heap ba |` (UNIV - m)) (a, b)\<rbrakk> \<Longrightarrow> cdl.lift sep_heap ba (a, b) = cdl.lift sep_heap s (a, b) proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma map_eqI:
  "\<lbrakk>a |` m = b |` m;a |` (UNIV - m)  = b |` (UNIV - m)\<rbrakk> \<Longrightarrow> a = b" apply (rule ext) apply (drule_tac x = x in fun_cong)+ apply (auto simp:restrict_map_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a |` m = b |` m; a |` (UNIV - m) = b |` (UNIV - m)\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>a |` m = b |` m; a |` (UNIV - m) = b |` (UNIV - m)\<rbrakk> \<Longrightarrow> a x = b x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(a |` m) x = (b |` m) x; (a |` (UNIV - m)) x = (b |` (UNIV - m)) x\<rbrakk> \<Longrightarrow> a x = b x proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma using_writing_estimate:
  assumes we: "IsSepWritingEstimateOf f P proj m"
  shows "\<lbrace>\<lambda>s. P s \<and> Q ((proj s) |` (UNIV - m)) \<rbrace> f \<lbrace>\<lambda>r s. Q ((proj s) |` (UNIV - m))\<rbrace>" apply (clarsimp simp:valid_def) apply (erule arg_cong[where f = Q,THEN iffD1,rotated]) apply (erule sep_writing_estimateD[OF we]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> Q (proj s |` (UNIV - m))\<rbrace> f \<lbrace>\<lambda>r s. Q (proj s |` (UNIV - m))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; Q (proj s |` (UNIV - m))\<rbrakk> \<Longrightarrow> Q (proj b |` (UNIV - m)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> proj s |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma using_strong_writing_estimate:
  assumes we: "IsStrongSepWritingEstimateOf f P proj m g"
  shows
  "\<lbrace>\<lambda>s. P s \<and> Q ((proj s) |` (UNIV - m) ++ g (proj s))  \<rbrace> f \<lbrace>\<lambda>r s. Q (proj s)\<rbrace>" apply (clarsimp simp:valid_def) apply (erule arg_cong[where f = Q,THEN iffD1,rotated]) apply (rule map_eqI[where m = m]) apply (drule(1) sep_strong_writing_estimateD[OF we,THEN conjunct1,symmetric]) apply (rule ext) apply (clarsimp simp:restrict_map_def
     map_add_def split:option.splits) apply (frule(1) sep_strong_writing_estimateD[OF we,THEN conjunct1,symmetric]) apply (drule(1) sep_strong_writing_estimateD[OF we,THEN conjunct2,symmetric]) apply (rule ext) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<and> Q (proj s |` (UNIV - m) ++ g (proj s))\<rbrace> f \<lbrace>\<lambda>r s. Q (proj s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; Q (proj s |` (UNIV - m) ++ g (proj s))\<rbrakk> \<Longrightarrow> Q (proj b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> proj s |` (UNIV - m) ++ g (proj s) = proj b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` m = proj b |` m
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P s; g (proj s) = proj b |` m\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` m = proj b |` m
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>P s; g (proj s) = proj b |` m\<rbrakk> \<Longrightarrow> ((proj s |` (UNIV - m) ++ g (proj s)) |` m) x = (proj b |` m) x
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; g (proj s) = proj b |` m\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; g (proj s) = proj b |` m; proj s |` (UNIV - m) = proj b |` (UNIV - m)\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m) = proj b |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>P s; g (proj s) = proj b |` m; proj s |` (UNIV - m) = proj b |` (UNIV - m)\<rbrakk> \<Longrightarrow> ((proj s |` (UNIV - m) ++ g (proj s)) |` (UNIV - m)) x = (proj b |` (UNIV - m)) x proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma is_tcb_obj_type:
  "is_tcb = (\<lambda>x. object_type x = TcbType)" by (auto simp:is_tcb_def object_type_def split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb = (\<lambda>x. object_type x = TcbType)
theory RWHelper_DP

lemma update_slots_rev:
  "update_slots slots obj = obj' \<Longrightarrow>
  obj = update_slots (object_slots obj) obj'" by (clarsimp simp:update_slots_def object_slots_def
    split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_slots slots obj = obj' \<Longrightarrow> obj = update_slots (object_slots obj) obj'
theory RWHelper_DP

lemma all_scheduable_tcbsD:
  "ptr \<in> all_scheduable_tcbs (cdl_objects s)
  \<Longrightarrow> tcb_at_heap tcb_scheduable ptr (cdl_objects s)" by (simp add:all_scheduable_tcbs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<in> all_scheduable_tcbs (cdl_objects s) \<Longrightarrow> tcb_at_heap tcb_scheduable ptr (cdl_objects s)
theory RWHelper_DP

lemma all_scheduable_tcbsD':
  "ptr \<notin> all_scheduable_tcbs (cdl_objects s)
  \<Longrightarrow> \<not> tcb_at_heap tcb_scheduable ptr (cdl_objects s)" by (simp add:all_scheduable_tcbs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<notin> all_scheduable_tcbs (cdl_objects s) \<Longrightarrow> \<not> tcb_at_heap tcb_scheduable ptr (cdl_objects s)
theory RWHelper_DP

lemma scheduable_cap_reset_cap_asid[simp]:
  "scheduable_cap (reset_cap_asid cap) = scheduable_cap cap" by (case_tac cap,simp_all add: reset_cap_asid_def scheduable_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduable_cap (reset_cap_asid cap) = scheduable_cap cap
theory RWHelper_DP

lemma sep_inv_to_all_scheduable_tcbs:
  assumes sep: "\<And>P. \<lbrace><P>\<rbrace> f \<lbrace>\<lambda>r. <P>\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> f
   \<lbrace>\<lambda>r s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace>" apply (clarsimp simp:valid_def all_scheduable_tcbs_rewrite) apply (erule use_valid) apply (rule hoare_strengthen_post) apply (rule sep) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> f \<lbrace>\<lambda>r s. P (all_scheduable_tcbs (cdl_objects s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (sep_all_scheduable_tcbs (cdl.lift sep_heap b)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> \<lbrace>?P9 s a b\<rbrace> f \<lbrace>\<lambda>a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap b))\<rbrace>
 2. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> ?P9 s a b s proof (prove)
goal (3 subgoals):
 1. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> \<lbrace>?P9 s a b\<rbrace> f \<lbrace>?Q12 s a b\<rbrace>
 2. \<And>s a b rv sa. \<lbrakk>P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)); ?Q12 s a b rv sa\<rbrakk> \<Longrightarrow> P (sep_all_scheduable_tcbs (cdl.lift sep_heap sa))
 3. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> ?P9 s a b s proof (prove)
goal (2 subgoals):
 1. \<And>s a b rv sa. \<lbrakk>P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)); cdl.lift (?P15 s a b) sa\<rbrakk> \<Longrightarrow> P (sep_all_scheduable_tcbs (cdl.lift sep_heap sa))
 2. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> cdl.lift (?P15 s a b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) \<Longrightarrow> P (sep_all_scheduable_tcbs (cdl.lift sep_heap s)) proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma validE_to_valid:
  assumes validE:"\<And>E. \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. Q\<rbrace>,\<lbrace>\<lambda>r s. E\<rbrace>"
  shows "\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. Q\<rbrace>" using validE[where E = False] apply (clarsimp simp:validE_def valid_def) apply (drule_tac spec) apply (erule(1) impE) apply (drule_tac bspec) apply assumption apply (auto split:sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q s'); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); P (?s9 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s9 s a b)). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q s')\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q s'\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> ?x13 s a b \<in> fst (f s)
 2. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); case ?x13 s a b of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q s'\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); case (a, b) of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q s'\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma all_scheduable_tcbs_corrupt[simp]:
  "all_scheduable_tcbs (cdl_objects (corrupt_intents xa x s)) = all_scheduable_tcbs (cdl_objects s)" apply (simp add:all_scheduable_tcbs_def object_at_heap_def) apply (intro set_eqI iffI) apply (clarsimp simp:corrupt_intents_def tcb_scheduable_def
     split:option.splits cdl_object.splits if_splits) apply (clarsimp simp:corrupt_intents_def
    map_add_def tcb_scheduable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_scheduable_tcbs (cdl_objects (corrupt_intents xa x s)) = all_scheduable_tcbs (cdl_objects s) proof (prove)
goal (1 subgoal):
 1. {ptr. \<exists>object. cdl_objects (corrupt_intents xa x s) ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} = {ptr. \<exists>object. cdl_objects s ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} proof (prove)
goal (2 subgoals):
 1. \<And>xb. xb \<in> {ptr. \<exists>object. cdl_objects (corrupt_intents xa x s) ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} \<Longrightarrow> xb \<in> {ptr. \<exists>object. cdl_objects s ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)}
 2. \<And>xb. xb \<in> {ptr. \<exists>object. cdl_objects s ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} \<Longrightarrow> xb \<in> {ptr. \<exists>object. cdl_objects (corrupt_intents xa x s) ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} proof (prove)
goal (1 subgoal):
 1. \<And>xb. xb \<in> {ptr. \<exists>object. cdl_objects s ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} \<Longrightarrow> xb \<in> {ptr. \<exists>object. cdl_objects (corrupt_intents xa x s) ptr = Some object \<and> (\<exists>tcb. object = Tcb tcb \<and> tcb_scheduable tcb)} proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma single_scheduable_tcb:
  "all_scheduable_tcbs (cdl_objects s) = {cur_thread}
  \<Longrightarrow> \<exists>tcb. cdl_objects s cur_thread = Some tcb \<and> (
    (object_slots tcb) tcb_pending_op_slot = Some RunningCap
    \<or> (object_slots tcb) tcb_pending_op_slot = Some RestartCap)" by (fastforce simp: all_scheduable_tcbs_def slots_of_def
                      tcb_scheduable_def object_slots_def opt_cap_def
                      object_at_heap_def
               dest!: singleton_eqD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_scheduable_tcbs (cdl_objects s) = {cur_thread} \<Longrightarrow> \<exists>tcb. cdl_objects s cur_thread = Some tcb \<and> (object_slots tcb tcb_pending_op_slot = Some RunningCap \<or> object_slots tcb tcb_pending_op_slot = Some RestartCap)
theory Invocation_DP

lemma intent_reset_projection[simp]:
  "intent_reset (intent_reset a) = intent_reset a" by (simp add:intent_reset_def split:cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset (intent_reset a) = intent_reset a
theory Invocation_DP

lemma asid_reset_intent_reset_switch:
  "asid_reset (intent_reset x) = intent_reset (asid_reset x)" apply (cut_tac object_clean_def2[unfolded Fun.comp_def,simplified,symmetric]) apply (drule_tac x = x in fun_cong) apply (simp add:object_clean_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_reset (intent_reset x) = intent_reset (asid_reset x) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. asid_reset (intent_reset x)) = object_clean \<Longrightarrow> asid_reset (intent_reset x) = intent_reset (asid_reset x) proof (prove)
goal (1 subgoal):
 1. asid_reset (intent_reset x) = object_clean x \<Longrightarrow> asid_reset (intent_reset x) = intent_reset (asid_reset x) proof (prove)
goal:
No subgoals!