kings-crown/FVELER_Isabelle huggingface dataset:
theory Sep_Tactic_Examples

lemma sep_drule_side_condition_lemma:
 "\<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap ) s;
    object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow>
   (D \<and>* G \<and>* E \<and>* F  \<and>*(obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>*  obj_id \<mapsto>f obj) s" apply (sep_drule sep_rule_double_conjunct_example, assumption) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* obj_id \<mapsto>f obj \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>c cap) s; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_slots obj slot = Some cap; ((obj_id, slot) \<mapsto>s obj \<and>* obj_id \<mapsto>f obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* D \<and>* G \<and>* E \<and>* F) s\<rbrakk> \<Longrightarrow> (D \<and>* G \<and>* E \<and>* F \<and>* (obj_id, slot) \<mapsto>s obj \<and>* H \<and>* Z \<and>* J \<and>* L \<and>* Y \<and>* A \<and>* B \<and>* obj_id \<mapsto>f obj) s proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma eq_on_subset:
  "\<lbrakk>B \<subseteq> A ; eq_on A s s' \<rbrakk> \<Longrightarrow> eq_on B s s'" by (auto simp:eq_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<subseteq> A; eq_on A s s'\<rbrakk> \<Longrightarrow> eq_on B s s'
theory RWHelper_DP

lemma eq_on_trans:
  "\<lbrakk>eq_on a s sa ; eq_on a sa sb\<rbrakk> \<Longrightarrow> eq_on a s sb" by (simp add:eq_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_on a s sa; eq_on a sa sb\<rbrakk> \<Longrightarrow> eq_on a s sb
theory RWHelper_DP

lemma ReadingEstimateOf_read_subset:
  "\<lbrakk>IsReadingEstimateOf a f w;  a \<subseteq> b\<rbrakk> \<Longrightarrow> IsReadingEstimateOf b f w" by (auto simp add:IsReadingEstimateOf_def eq_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsReadingEstimateOf a f w; a \<subseteq> b\<rbrakk> \<Longrightarrow> IsReadingEstimateOf b f w
theory RWHelper_DP

lemma ReadingEstimateOf_write_subset:
  "\<lbrakk>IsReadingEstimateOf a f w;  w' \<subseteq> w\<rbrakk> \<Longrightarrow> IsReadingEstimateOf a f w'" by (auto simp add:IsReadingEstimateOf_def eq_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsReadingEstimateOf a f w; w' \<subseteq> w\<rbrakk> \<Longrightarrow> IsReadingEstimateOf a f w'
theory RWHelper_DP

lemma reading_estimateD:
  "\<lbrakk>IsReadingEstimateOf a f w; eq_on a s s'\<rbrakk> \<Longrightarrow> eq_on w (f s) (f s')" by (auto simp:IsReadingEstimateOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsReadingEstimateOf a f w; eq_on a s s'\<rbrakk> \<Longrightarrow> eq_on w (f s) (f s')
theory RWHelper_DP

lemma not_writingD:
  "ptr \<notin> WritingOf f \<Longrightarrow> (f s) ptr = s ptr" by (auto simp:WritingOf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr \<notin> WritingOf f \<Longrightarrow> f s ptr = s ptr
theory RWHelper_DP

lemma well_ordered_estimate:
  "WritingOf f \<subseteq> writing_estimate \<Longrightarrow>
    ReadingOf f \<subseteq> ReadingEstimateOf f writing_estimate" by (auto simp add:IsReadingEstimateOf_def ReadingEstimateOf_def eq_on_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. WritingOf f \<subseteq> writing_estimate \<Longrightarrow> ReadingOf f \<subseteq> ReadingEstimateOf f writing_estimate
theory RWHelper_DP

lemma writing_estimate_pipe:
  "\<lbrakk>WritingOf f \<subseteq> Q; WritingOf g \<subseteq> Q\<rbrakk> \<Longrightarrow> WritingOf (f\<circ>g) \<subseteq> Q" apply (subst WritingOf_def) apply clarsimp apply (rule ccontr) apply (drule(1) contra_subsetD)+ apply (drule_tac s = "g xa" in not_writingD) apply (drule_tac s = xa in not_writingD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>WritingOf f \<subseteq> Q; WritingOf g \<subseteq> Q\<rbrakk> \<Longrightarrow> WritingOf (f \<circ> g) \<subseteq> Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>WritingOf f \<subseteq> Q; WritingOf g \<subseteq> Q\<rbrakk> \<Longrightarrow> (\<Union>s. {ptr. (f \<circ> g) s ptr \<noteq> s ptr}) \<subseteq> Q proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>WritingOf f \<subseteq> Q; WritingOf g \<subseteq> Q; f (g xa) x \<noteq> xa x\<rbrakk> \<Longrightarrow> x \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>WritingOf f \<subseteq> Q; WritingOf g \<subseteq> Q; f (g xa) x \<noteq> xa x; x \<notin> Q\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f (g xa) x \<noteq> xa x; x \<notin> Q; x \<notin> WritingOf f; x \<notin> WritingOf g\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f (g xa) x \<noteq> xa x; x \<notin> Q; x \<notin> WritingOf g; f (g xa) x = g xa x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f (g xa) x \<noteq> xa x; x \<notin> Q; f (g xa) x = g xa x; g xa x = xa x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma reading_writing_estimate:
  "\<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g)\<rbrakk> \<Longrightarrow> eq_on R (g s) (g s')" apply (subst eq_on_def) apply clarsimp apply (case_tac "ptr \<in> WritingOf g") apply (clarsimp simp:IsReadingEstimateOf_def) apply (elim impE allE) apply simp apply (clarsimp simp:eq_on_def) apply (clarsimp simp:WritingOf_def eq_on_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g)\<rbrakk> \<Longrightarrow> eq_on R (g s) (g s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g)\<rbrakk> \<Longrightarrow> \<forall>ptr\<in>R. g s ptr = g s' ptr proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal (2 subgoals):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<in> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr
 2. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<notin> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal (2 subgoals):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; \<forall>s s'. eq_on R s s' \<longrightarrow> eq_on (WritingOf g) (g s) (g s'); ptr \<in> R; ptr \<in> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr
 2. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<notin> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal (3 subgoals):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; ptr \<in> R; ptr \<in> WritingOf g\<rbrakk> \<Longrightarrow> eq_on R (?s4 ptr) (?s'5 ptr)
 2. \<And>ptr. \<lbrakk>eq_on R s s'; ptr \<in> R; ptr \<in> WritingOf g; eq_on (WritingOf g) (g (?s4 ptr)) (g (?s'5 ptr))\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr
 3. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<notin> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal (2 subgoals):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; ptr \<in> R; ptr \<in> WritingOf g; eq_on (WritingOf g) (g s) (g s')\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr
 2. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<notin> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g); ptr \<in> R; ptr \<notin> WritingOf g\<rbrakk> \<Longrightarrow> g s ptr = g s' ptr proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma reading_estimate_pipe:
  assumes reg: "IsReadingEstimateOf R g M"
  and ref: " IsReadingEstimateOf R f M"
  and wg: "WritingOf g \<subseteq> M"
  and wf: "WritingOf f \<subseteq> M"
  shows "IsReadingEstimateOf R (f \<circ> g) M" apply (clarsimp simp: IsReadingEstimateOf_def) apply (cut_tac ReadingEstimateOf_write_subset[OF reg wg]) apply (drule(1) reading_writing_estimate[rotated]) apply (erule reading_estimateD[OF ref]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. IsReadingEstimateOf R (f \<circ> g) M proof (prove)
goal (1 subgoal):
 1. \<And>s s'. eq_on R s s' \<Longrightarrow> eq_on M (f (g s)) (f (g s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on R s s'; IsReadingEstimateOf R g (WritingOf g)\<rbrakk> \<Longrightarrow> eq_on M (f (g s)) (f (g s')) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>eq_on R s s'; eq_on R (g s) (g s')\<rbrakk> \<Longrightarrow> eq_on M (f (g s)) (f (g s')) proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_writing_estimateD:
  "\<lbrakk>IsSepWritingEstimateOf f P proj m; (r, s') \<in> fst (f s);P s \<rbrakk>
  \<Longrightarrow> proj s |` (UNIV - m) = proj s' |` (UNIV - m)" apply (rule ext) apply (clarsimp simp: restrict_map_def
    IsSepWritingEstimateOf_def) apply (drule_tac x = x in spec) apply (drule_tac x = "proj s x" in spec) apply (drule(1) use_valid) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsSepWritingEstimateOf f P proj m; (r, s') \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> proj s |` (UNIV - m) = proj s' |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>IsSepWritingEstimateOf f P proj m; (r, s') \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> (proj s |` (UNIV - m)) x = (proj s' |` (UNIV - m)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>ptr v. \<lbrace>\<lambda>s. proj s ptr = v \<and> P s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace>; (r, s') \<in> fst (f s); P s; x \<notin> m\<rbrakk> \<Longrightarrow> proj s x = proj s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(r, s') \<in> fst (f s); P s; x \<notin> m; \<forall>v. \<lbrace>\<lambda>s. proj s x = v \<and> P s \<and> x \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s x = v\<rbrace>\<rbrakk> \<Longrightarrow> proj s x = proj s' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(r, s') \<in> fst (f s); P s; x \<notin> m; \<lbrace>\<lambda>sa. proj sa x = proj s x \<and> P sa \<and> x \<notin> m\<rbrace> f \<lbrace>\<lambda>r sa. proj sa x = proj s x\<rbrace>\<rbrakk> \<Longrightarrow> proj s x = proj s' x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>P s; x \<notin> m; \<lbrace>\<lambda>sa. proj sa x = proj s x \<and> P sa \<and> x \<notin> m\<rbrace> f \<lbrace>\<lambda>r sa. proj sa x = proj s x\<rbrace>\<rbrakk> \<Longrightarrow> proj s x = proj s x \<and> P s \<and> x \<notin> m
 2. \<And>x. \<lbrakk>P s; x \<notin> m; \<lbrace>\<lambda>sa. proj sa x = proj s x \<and> P sa \<and> x \<notin> m\<rbrace> f \<lbrace>\<lambda>r sa. proj sa x = proj s x\<rbrace>; proj s' x = proj s x\<rbrakk> \<Longrightarrow> proj s x = proj s' x proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_writing_estimate_imp:
  "\<lbrakk>IsSepWritingEstimateOf f P' proj m; \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
  \<Longrightarrow> IsSepWritingEstimateOf f P proj m" apply (clarsimp simp:IsSepWritingEstimateOf_def) apply (drule_tac x = ptr in spec) apply (drule_tac x = v in spec) apply (erule hoare_pre) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsSepWritingEstimateOf f P' proj m; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> IsSepWritingEstimateOf f P proj m proof (prove)
goal (1 subgoal):
 1. \<And>ptr v. \<lbrakk>\<forall>ptr v. \<lbrace>\<lambda>s. proj s ptr = v \<and> P' s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. proj s ptr = v \<and> P s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr v. \<lbrakk>\<And>s. P s \<Longrightarrow> P' s; \<forall>v. \<lbrace>\<lambda>s. proj s ptr = v \<and> P' s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. proj s ptr = v \<and> P s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr v. \<lbrakk>\<And>s. P s \<Longrightarrow> P' s; \<lbrace>\<lambda>s. proj s ptr = v \<and> P' s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. proj s ptr = v \<and> P s \<and> ptr \<notin> m\<rbrace> f \<lbrace>\<lambda>r s. proj s ptr = v\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr v s. \<lbrakk>\<And>s. P s \<Longrightarrow> P' s; proj s ptr = v \<and> P s \<and> ptr \<notin> m\<rbrakk> \<Longrightarrow> proj s ptr = v \<and> P' s \<and> ptr \<notin> m proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_strong_writing_estimateD:
  "\<lbrakk>IsStrongSepWritingEstimateOf f P proj m g; (r, s') \<in> fst (f s);P s \<rbrakk>
  \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m)" apply (simp add:
    IsStrongSepWritingEstimateOf_def) apply (drule_tac x = "proj s " in spec) apply (drule use_valid) apply assumption apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IsStrongSepWritingEstimateOf f P proj m g; (r, s') \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>state. \<lbrace>\<lambda>s. proj s = state \<and> P s\<rbrace> f \<lbrace>\<lambda>r s. proj s |` m = g state \<and> proj s |` (UNIV - m) = state |` (UNIV - m)\<rbrace>; (r, s') \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r, s') \<in> fst (f s); P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>\<rbrakk> \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P2\<rbrace> f \<lbrace>?Q2\<rbrace>
 2. \<lbrakk>P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>\<rbrakk> \<Longrightarrow> ?P2 s
 3. \<lbrakk>P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>; ?Q2 r s'\<rbrakk> \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>\<rbrakk> \<Longrightarrow> proj s = proj s \<and> P s
 2. \<lbrakk>P s; \<lbrace>\<lambda>sa. proj sa = proj s \<and> P sa\<rbrace> f \<lbrace>\<lambda>r sa. proj sa |` m = g (proj s) \<and> proj sa |` (UNIV - m) = proj s |` (UNIV - m)\<rbrace>; proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m)\<rbrakk> \<Longrightarrow> proj s' |` m = g (proj s) \<and> proj s' |` (UNIV - m) = proj s |` (UNIV - m) proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma intent_reset_twice[simp]:
 "intent_reset (intent_reset z) = intent_reset z" apply (case_tac z) apply (simp_all add:intent_reset_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intent_reset (intent_reset z) = intent_reset z proof (prove)
goal (10 subgoals):
 1. z = Endpoint \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 2. z = Notification \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 3. \<And>x3. z = Tcb x3 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 4. \<And>x4. z = CNode x4 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 5. \<And>x5. z = AsidPool x5 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 6. \<And>x6. z = PageTable x6 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 7. \<And>x7. z = PageDirectory x7 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 8. \<And>x8. z = Frame x8 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 9. z = Untyped \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z
 10. \<And>x10. z = IRQNode x10 \<Longrightarrow> intent_reset (intent_reset z) = intent_reset z proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma largest_set:
  "UNIV \<subseteq> cmps \<Longrightarrow> cmps = UNIV" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UNIV \<subseteq> cmps \<Longrightarrow> cmps = UNIV
theory RWHelper_DP

lemma sep_heap_domD:
  "\<lbrakk>sep_heap_dom P m; P s ; p \<notin> m\<rbrakk>
   \<Longrightarrow> p \<notin> dom (sep_heap s)" by (fastforce simp:sep_heap_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap_dom P m; P s; p \<notin> m\<rbrakk> \<Longrightarrow> p \<notin> dom (sep_heap s)
theory RWHelper_DP

lemma sep_heap_domD':
  "\<lbrakk>sep_heap_dom P m;P s\<rbrakk>
   \<Longrightarrow> m = dom (sep_heap s)" by (fastforce simp:sep_heap_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap_dom P m; P s\<rbrakk> \<Longrightarrow> m = dom (sep_heap s)
theory RWHelper_DP

lemma sep_irq_node_domD':
  "\<lbrakk>sep_irq_node_dom P m; P s\<rbrakk>
   \<Longrightarrow> m = dom (sep_irq_node s)" by (fastforce simp: sep_irq_node_dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_irq_node_dom P m; P s\<rbrakk> \<Longrightarrow> m = dom (sep_irq_node s)
theory RWHelper_DP

lemma sep_specD:
  "\<lbrakk>sep_map_spec P s; P s'\<rbrakk> \<Longrightarrow> s = s'" by (clarsimp simp: sep_map_spec_def)

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

lemma sep_heap_dom_sep_map_predicate:
  "m = {ptr}\<times> cmps \<Longrightarrow>
  sep_heap_dom (sep_map_predicate ptr P cmps) m" apply (clarsimp simp: sep_map_general_def
    object_to_sep_state_def
    sep_heap_dom_def sep_map_predicate_def
    split:sep_state.splits if_splits) apply (rule set_eqI) apply (clarsimp simp:dom_def object_project_def split:cdl_component_id.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m = {ptr} \<times> cmps \<Longrightarrow> sep_heap_dom (sep_map_predicate ptr P cmps) m proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>m = {ptr} \<times> cmps; sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None); sep_irq_node s = (\<lambda>x. None); P obj\<rbrakk> \<Longrightarrow> dom (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None) = {ptr} \<times> cmps proof (prove)
goal (1 subgoal):
 1. \<And>s obj x. \<lbrakk>m = {ptr} \<times> cmps; sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None); sep_irq_node s = (\<lambda>x. None); P obj\<rbrakk> \<Longrightarrow> (x \<in> dom (\<lambda>(obj_id', comp_id). if obj_id' = ptr \<and> comp_id \<in> cmps then Some (object_project comp_id obj) else None)) = (x \<in> {ptr} \<times> cmps) proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_irq_node_dom_sep_map_predicate:
  "sep_irq_node_dom (sep_map_predicate ptr P cmps) {}" apply (clarsimp simp: sep_map_general_def object_to_sep_state_def
    sep_irq_node_dom_def sep_map_predicate_def
    split:sep_state.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_irq_node_dom (sep_map_predicate ptr P cmps) {} proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_map_rewrite_spec:
  "sep_map_general = (\<lambda>p obj cmps.  sep_map_predicate p ((=) obj) cmps)"
  "sep_map_o = (\<lambda>p obj. sep_map_predicate p ((=) obj) UNIV)"
  "sep_map_f = (\<lambda>p obj. sep_map_predicate p ((=) obj) {Fields})"
  "sep_map_c = (\<lambda>p cap. let (ptr,slot) = p in
   sep_map_predicate ptr (\<lambda>obj. object_slots obj = [ slot \<mapsto> cap]) {Slot slot})" by (fastforce simp: sep_map_predicate_def sep_any_def sep_map_general_def
                      sep_map_o_def sep_map_f_def sep_map_c_def split_def
               split: sep_state.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sep_map_general = (\<lambda>p obj. sep_map_predicate p ((=) obj)) &&& sep_map_o = (\<lambda>p obj. sep_map_predicate p ((=) obj) UNIV)) &&& sep_map_f = (\<lambda>p obj. sep_map_predicate p ((=) obj) {Fields}) &&& sep_map_c = (\<lambda>p cap. let (ptr, slot) = p in sep_map_predicate ptr (\<lambda>obj. object_slots obj = [slot \<mapsto> cap]) {Slot slot})
theory RWHelper_DP

lemma sep_map_rewrite_any:
  "sep_any_map_c = (\<lambda>ptr state.
   sep_map_predicate (fst ptr) (\<lambda>obj. \<exists>cap. object_slots obj = [(snd ptr) \<mapsto> cap]) {Slot (snd ptr)} state)" by (fastforce simp: sep_map_predicate_def sep_map_general_def sep_any_def
                      sep_map_o_def sep_map_f_def sep_map_c_def split_def
               split: sep_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_any_map_c = (\<lambda>ptr. sep_map_predicate (fst ptr) (\<lambda>obj. \<exists>cap. object_slots obj = [snd ptr \<mapsto> cap]) {Slot (snd ptr)})
theory RWHelper_DP

lemma sep_heap_dom_conj:
  "\<lbrakk>sep_heap_dom P m;sep_heap_dom P' m'\<rbrakk> \<Longrightarrow> sep_heap_dom (P \<and>* P') (m \<union> m')" apply (clarsimp simp: sep_heap_dom_def sep_conj_def
                        sep_disj_sep_state_def sep_state_disj_def) apply (auto simp: map_disj_def plus_sep_state_def sep_state_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sep_heap_dom P m; sep_heap_dom P' m'\<rbrakk> \<Longrightarrow> sep_heap_dom (P \<and>* P') (m \<union> m') proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>s. P s \<longrightarrow> dom (sep_heap s) = m; \<forall>s. P' s \<longrightarrow> dom (sep_heap s) = m'; sep_heap x \<bottom> sep_heap y; sep_irq_node x \<bottom> sep_irq_node y; P x; P' y\<rbrakk> \<Longrightarrow> dom (sep_heap (x + y)) = m \<union> m' proof (prove)
goal:
No subgoals!
theory RWHelper_DP

lemma sep_heap_dom_simps:
  "sep_heap_dom (slot \<mapsto>c -) ({(fst slot,Slot (snd slot))})"
  "sep_heap_dom (slot \<mapsto>c cap) ({(fst slot,Slot (snd slot))})" apply (simp add:sep_map_rewrite_any sep_heap_dom_sep_map_predicate) apply (simp add:sep_map_rewrite_spec sep_heap_dom_sep_map_predicate split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_heap_dom (slot \<mapsto>c -) {(fst slot, Slot (snd slot))} &&& sep_heap_dom (slot \<mapsto>c cap) {(fst slot, Slot (snd slot))} proof (prove)
goal (1 subgoal):
 1. sep_heap_dom (slot \<mapsto>c cap) {(fst slot, Slot (snd slot))} proof (prove)
goal:
No subgoals!