kings-crown/FVELER_Isabelle huggingface dataset:
theory Map_Extra

lemma map_disj_add_eq_dom_left_eq:
  assumes add: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'" and
          dom: "dom h\<^sub>1 = dom h\<^sub>1'" and
          disj: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0' \<bottom> h\<^sub>1'"
  shows "h\<^sub>0 = h\<^sub>0'" proof - have "h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'" using add disj by (simp add: map_add_ac) thus ?thesis using dom disj by - (rule map_disj_add_eq_dom_right_eq, auto simp: map_disj_com) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 = h\<^sub>0' proof (state)
goal (1 subgoal):
 1. h\<^sub>0 = h\<^sub>0' proof (prove)
goal (1 subgoal):
 1. h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0' proof (prove)
using this:
h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0' \<bottom> h\<^sub>1'

goal (1 subgoal):
 1. h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0' proof (state)
this:
h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'

goal (1 subgoal):
 1. h\<^sub>0 = h\<^sub>0' proof (prove)
using this:
h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'

goal (1 subgoal):
 1. h\<^sub>0 = h\<^sub>0' proof (prove)
using this:
h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'
dom h\<^sub>1 = dom h\<^sub>1'
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0' \<bottom> h\<^sub>1'

goal (1 subgoal):
 1. h\<^sub>0 = h\<^sub>0' proof (state)
this:
h\<^sub>0 = h\<^sub>0'

goal:
No subgoals!
theory Map_Extra

lemma map_add_left_cancel:
  assumes disj: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0 \<bottom> h\<^sub>1'"
  shows "(h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1') = (h\<^sub>1 = h\<^sub>1')" proof (rule iffI, rule ext) fix x assume "(h\<^sub>0 ++ h\<^sub>1) = (h\<^sub>0 ++ h\<^sub>1')" hence "(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x" by auto hence "h\<^sub>1 x = h\<^sub>1' x" using disj by (cases "x \<in> dom h\<^sub>0"; simp add: map_disj_None_right map_add_eval_right') thus "h\<^sub>1 x = h\<^sub>1' x" by auto qed auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1') = (h\<^sub>1 = h\<^sub>1') proof (state)
goal (2 subgoals):
 1. \<And>x. h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' \<Longrightarrow> h\<^sub>1 x = h\<^sub>1' x
 2. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' proof (state)
goal (2 subgoals):
 1. \<And>x. h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' \<Longrightarrow> h\<^sub>1 x = h\<^sub>1' x
 2. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' proof (state)
this:
h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1'

goal (2 subgoals):
 1. \<And>x. h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' \<Longrightarrow> h\<^sub>1 x = h\<^sub>1' x
 2. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' proof (prove)
using this:
h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1'

goal (1 subgoal):
 1. (h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x proof (state)
this:
(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x

goal (2 subgoals):
 1. \<And>x. h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' \<Longrightarrow> h\<^sub>1 x = h\<^sub>1' x
 2. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' proof (prove)
using this:
(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x

goal (1 subgoal):
 1. h\<^sub>1 x = h\<^sub>1' x proof (prove)
using this:
(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0 ++ h\<^sub>1') x
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0 \<bottom> h\<^sub>1'

goal (1 subgoal):
 1. h\<^sub>1 x = h\<^sub>1' x proof (state)
this:
h\<^sub>1 x = h\<^sub>1' x

goal (2 subgoals):
 1. \<And>x. h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' \<Longrightarrow> h\<^sub>1 x = h\<^sub>1' x
 2. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1' proof (prove)
using this:
h\<^sub>1 x = h\<^sub>1' x

goal (1 subgoal):
 1. h\<^sub>1 x = h\<^sub>1' x proof (state)
this:
h\<^sub>1 x = h\<^sub>1' x

goal (1 subgoal):
 1. h\<^sub>1 = h\<^sub>1' \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0 ++ h\<^sub>1'
theory Map_Extra

lemma map_add_lr_disj:
  "\<lbrakk> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'; h\<^sub>1 \<bottom> h\<^sub>1'  \<rbrakk> \<Longrightarrow> dom h\<^sub>1 \<subseteq> dom h\<^sub>0'" by (clarsimp simp: map_disj_def map_add_def, drule_tac x=x in fun_cong)
     (auto split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'; h\<^sub>1 \<bottom> h\<^sub>1'\<rbrakk> \<Longrightarrow> dom h\<^sub>1 \<subseteq> dom h\<^sub>0'
theory Map_Extra

lemma map_disj_update_left [simp]:
  "p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1(p \<mapsto> v) = h\<^sub>0 \<bottom> h\<^sub>1" by (clarsimp simp: map_disj_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1(p \<mapsto> v) = h\<^sub>0 \<bottom> h\<^sub>1
theory Map_Extra

lemma map_disj_update_right [simp]:
  "p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>1(p \<mapsto> v) \<bottom> h\<^sub>0 = h\<^sub>1 \<bottom> h\<^sub>0" by (simp add: map_disj_com)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<in> dom h\<^sub>1 \<Longrightarrow> h\<^sub>1(p \<mapsto> v) \<bottom> h\<^sub>0 = h\<^sub>1 \<bottom> h\<^sub>0
theory Map_Extra

lemma map_add_update_right:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; p \<in> dom h\<^sub>1  \<rbrakk> \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1)(p \<mapsto> v) = (h\<^sub>0 ++ h\<^sub>1 (p \<mapsto> v))" by (drule (1) map_disj_None_left)
     (auto simp: map_add_def cong: option.case_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 \<bottom> h\<^sub>1; p \<in> dom h\<^sub>1\<rbrakk> \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1)(p \<mapsto> v) = h\<^sub>0 ++ h\<^sub>1(p \<mapsto> v)
theory Map_Extra

lemma map_add3_update:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>1  \<bottom> h\<^sub>2 ; h\<^sub>0 \<bottom> h\<^sub>2 ; p \<in> dom h\<^sub>0 \<rbrakk>
  \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1 ++ h\<^sub>2)(p \<mapsto> v) = h\<^sub>0(p \<mapsto> v) ++ h\<^sub>1 ++ h\<^sub>2" by (auto simp: map_add_update_left[symmetric] map_add_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 \<bottom> h\<^sub>1; h\<^sub>1 \<bottom> h\<^sub>2; h\<^sub>0 \<bottom> h\<^sub>2; p \<in> dom h\<^sub>0\<rbrakk> \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>1 ++ h\<^sub>2)(p \<mapsto> v) = h\<^sub>0(p \<mapsto> v) ++ h\<^sub>1 ++ h\<^sub>2
theory Map_Extra

lemma map_le_override [simp]:
  "\<lbrakk> h \<bottom> h' \<rbrakk> \<Longrightarrow> h \<subseteq>\<^sub>m h ++ h'" by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<bottom> h' \<Longrightarrow> h \<subseteq>\<^sub>m h ++ h'
theory Map_Extra

lemma map_leI_left:
  "\<lbrakk> h = h\<^sub>0 ++ h\<^sub>1 ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h = h\<^sub>0 ++ h\<^sub>1; h\<^sub>0 \<bottom> h\<^sub>1\<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h
theory Map_Extra

lemma map_leI_right:
  "\<lbrakk> h = h\<^sub>0 ++ h\<^sub>1 ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>1 \<subseteq>\<^sub>m h" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h = h\<^sub>0 ++ h\<^sub>1; h\<^sub>0 \<bottom> h\<^sub>1\<rbrakk> \<Longrightarrow> h\<^sub>1 \<subseteq>\<^sub>m h
theory Map_Extra

lemma map_disj_map_le:
  "\<lbrakk> h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0' \<bottom> h\<^sub>1" by (force simp: map_disj_def map_le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0; h\<^sub>0 \<bottom> h\<^sub>1\<rbrakk> \<Longrightarrow> h\<^sub>0' \<bottom> h\<^sub>1
theory Map_Extra

lemma map_le_on_disj_left:
  "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 ; h' = h\<^sub>0 ++ h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" unfolding map_le_def by (rule ballI, erule_tac x=a in ballE, auto simp: map_add_eval_left)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h' \<subseteq>\<^sub>m h; h\<^sub>0 \<bottom> h\<^sub>1; h' = h\<^sub>0 ++ h\<^sub>1\<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a\<in>dom h'. h' a = h a; h\<^sub>0 \<bottom> h\<^sub>1; h' = h\<^sub>0 ++ h\<^sub>1\<rbrakk> \<Longrightarrow> \<forall>a\<in>dom h\<^sub>0. h\<^sub>0 a = h a
theory Map_Extra

lemma map_le_on_disj_right:
  "\<lbrakk> h' \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 ; h' = h\<^sub>1 ++ h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h" by (auto simp: map_le_on_disj_left map_add_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h' \<subseteq>\<^sub>m h; h\<^sub>0 \<bottom> h\<^sub>1; h' = h\<^sub>1 ++ h\<^sub>0\<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h
theory Map_Extra

lemma map_le_add_cancel:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0' ++ h\<^sub>1 \<subseteq>\<^sub>m h\<^sub>0 ++ h\<^sub>1" by (auto simp: map_le_def map_add_def map_disj_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 \<bottom> h\<^sub>1; h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0\<rbrakk> \<Longrightarrow> h\<^sub>0' ++ h\<^sub>1 \<subseteq>\<^sub>m h\<^sub>0 ++ h\<^sub>1
theory Map_Extra

lemma map_le_conv:
  "(h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 \<and> h\<^sub>0' \<noteq> h\<^sub>0) = (\<exists>h\<^sub>1. h\<^sub>0 = h\<^sub>0' ++ h\<^sub>1 \<and> h\<^sub>0' \<bottom> h\<^sub>1 \<and> h\<^sub>0' \<noteq> h\<^sub>0)" unfolding map_le_def map_disj_def map_add_def by (rule iffI,
      clarsimp intro!: exI[where x="\<lambda>x. if x \<notin> dom h\<^sub>0' then h\<^sub>0 x else None"])
     (fastforce intro: split: option.splits if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (h\<^sub>0' \<subseteq>\<^sub>m h\<^sub>0 \<and> h\<^sub>0' \<noteq> h\<^sub>0) = (\<exists>h\<^sub>1. h\<^sub>0 = h\<^sub>0' ++ h\<^sub>1 \<and> h\<^sub>0' \<bottom> h\<^sub>1 \<and> h\<^sub>0' \<noteq> h\<^sub>0) proof (prove)
goal (1 subgoal):
 1. ((\<forall>a\<in>dom h\<^sub>0'. h\<^sub>0' a = h\<^sub>0 a) \<and> h\<^sub>0' \<noteq> h\<^sub>0) = (\<exists>h\<^sub>1. h\<^sub>0 = (\<lambda>x. case h\<^sub>1 x of None \<Rightarrow> h\<^sub>0' x | Some x \<Rightarrow> Some x) \<and> dom h\<^sub>0' \<inter> dom h\<^sub>1 = {} \<and> h\<^sub>0' \<noteq> h\<^sub>0)
theory Map_Extra

lemma map_disj_comp [simp]:
  "h\<^sub>0 \<bottom> h\<^sub>1 |` (UNIV - dom h\<^sub>0)" by (force simp: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 |` (UNIV - dom h\<^sub>0)
theory Map_Extra

lemma restrict_map_disj:
  "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h |` T" by (auto simp: map_disj_def restrict_map_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h |` T
theory Map_Extra

lemma map_disj_restrict_dom [simp]:
  "h\<^sub>0 \<bottom> h\<^sub>1 |` (dom h\<^sub>1 - dom h\<^sub>0)" by (force simp: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 |` (dom h\<^sub>1 - dom h\<^sub>0)
theory Map_Extra

lemma restrict_map_disj_dom_empty:
  "h \<bottom> h' \<Longrightarrow> h |` dom h' = Map.empty" by (fastforce simp: map_disj_def restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<bottom> h' \<Longrightarrow> h |` dom h' = (\<lambda>x. None)
theory Map_Extra

lemma restrict_map_univ_disj_eq:
  "h \<bottom> h' \<Longrightarrow> h |` (UNIV - dom h') = h" by (rule ext, auto simp: map_disj_def restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<bottom> h' \<Longrightarrow> h |` (UNIV - dom h') = h
theory Map_Extra

lemma restrict_map_disj_dom:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h |` dom h\<^sub>0 \<bottom> h |` dom h\<^sub>1" by (auto simp: map_disj_def restrict_map_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h |` dom h\<^sub>0 \<bottom> h |` dom h\<^sub>1
theory Map_Extra

lemma map_add_restrict_dom_left:
  "h \<bottom> h' \<Longrightarrow> (h ++ h') |` dom h = h" by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
                     split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<bottom> h' \<Longrightarrow> (h ++ h') |` dom h = h
theory Map_Extra

lemma map_add_restrict_dom_left':
  "h \<bottom> h' \<Longrightarrow> S = dom h \<Longrightarrow> (h ++ h') |` S = h" by (rule ext, auto simp: restrict_map_def map_add_def dom_def map_disj_def
                     split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<bottom> h'; S = dom h\<rbrakk> \<Longrightarrow> (h ++ h') |` S = h
theory Map_Extra

lemma restrict_map_disj_left:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` S \<bottom> h\<^sub>1" by (auto simp: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` S \<bottom> h\<^sub>1
theory Map_Extra

lemma restrict_map_disj_right:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S" by (auto simp: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S
theory Map_Extra

lemma map_dom_disj_restrict_right:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>0') |` dom h\<^sub>1 = h\<^sub>0' |` dom h\<^sub>1" by (simp add: map_add_restrict restrict_map_empty map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> (h\<^sub>0 ++ h\<^sub>0') |` dom h\<^sub>1 = h\<^sub>0' |` dom h\<^sub>1
theory Map_Extra

lemma restrict_map_on_disj:
  "h\<^sub>0' \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` dom h\<^sub>0' \<bottom> h\<^sub>1" unfolding map_disj_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0' \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 |` dom h\<^sub>0' \<bottom> h\<^sub>1 proof (prove)
goal (1 subgoal):
 1. dom h\<^sub>0' \<inter> dom h\<^sub>1 = {} \<Longrightarrow> dom (h\<^sub>0 |` dom h\<^sub>0') \<inter> dom h\<^sub>1 = {}
theory Map_Extra

lemma restrict_map_on_disj':
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S" by (rule restrict_map_disj_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1 |` S
theory Map_Extra

lemma map_le_sub_dom:
  "\<lbrakk> h\<^sub>0 ++ h\<^sub>1 \<subseteq>\<^sub>m h ; h\<^sub>0 \<bottom> h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h |` (dom h - dom h\<^sub>1)" by (rule map_le_override_bothD, subst map_le_dom_restrict_sub_add)
     (auto elim: map_add_le_mapE simp: map_add_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 ++ h\<^sub>1 \<subseteq>\<^sub>m h; h\<^sub>0 \<bottom> h\<^sub>1\<rbrakk> \<Longrightarrow> h\<^sub>0 \<subseteq>\<^sub>m h |` (dom h - dom h\<^sub>1)
theory Map_Extra

lemma map_submap_break:
  "\<lbrakk> h \<subseteq>\<^sub>m h' \<rbrakk> \<Longrightarrow> h' = (h' |` (UNIV - dom h)) ++ h" by (fastforce split: option.splits
                simp: map_le_restrict restrict_map_def map_le_def map_add_def
                      dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<subseteq>\<^sub>m h' \<Longrightarrow> h' = h' |` (UNIV - dom h) ++ h
theory Map_Extra

lemma map_add_disj_restrict_both:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1; S \<inter> S' = {}; T \<inter> T' = {} \<rbrakk>
   \<Longrightarrow> (h\<^sub>0 |` S) ++ (h\<^sub>1 |` T) \<bottom> (h\<^sub>0 |` S') ++ (h\<^sub>1 |` T')" by (auto simp: map_add_ac intro!: restrict_map_disj_both restrict_map_disj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h\<^sub>0 \<bottom> h\<^sub>1; S \<inter> S' = {}; T \<inter> T' = {}\<rbrakk> \<Longrightarrow> h\<^sub>0 |` S ++ h\<^sub>1 |` T \<bottom> h\<^sub>0 |` S' ++ h\<^sub>1 |` T'
theory AbstractSeparation_SD

lemma sep_state_add_comm:
  "sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x" by (fastforce simp: sep_state_add_def sep_state_disj_def intro!:map_add_com)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x
theory Hoare_Sep_Tactics

lemma hoare_eq_pre:  " \<lbrakk> \<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>" by (erule hoare_pre_subst [rotated], auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>
theory Hoare_Sep_Tactics

lemma hoare_eq_preE:  " \<lbrakk> \<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" apply (rule hoare_weaken_preE) apply (assumption) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; G s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; G s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma hoare_eq_preE_R:  " \<lbrakk> \<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>,-" apply (clarsimp simp: validE_R_def) apply (erule hoare_eq_preE) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = G s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>G\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Hoare_Sep_Tactics

lemma hoare_eq_post: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>" by (rule hoare_strengthen_post, assumption, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>
theory Hoare_Sep_Tactics

lemma hoare_eq_postE: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>E\<rbrace>" by (metis (full_types) hoare_post_impErr')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>E\<rbrace>
theory Hoare_Sep_Tactics

lemma hoare_eq_postE_R: " \<lbrakk> \<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, -" by (metis hoare_post_imp_R)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv s. Q rv s = G rv s; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>G\<rbrace>, -
theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp:
    "\<And>sep_lift.
     (\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s) )\<rbrace> f \<lbrace>\<lambda>_. (\<lambda>s. (Q \<and>* R) (sep_lift s))\<rbrace>) \<Longrightarrow>
     \<lbrace>(\<lambda>s. ( P \<and>* (Q \<longrightarrow>* R) ) (sep_lift s))\<rbrace> f \<lbrace>\<lambda>_. (\<lambda>s.(R) (sep_lift s))\<rbrace>" apply (atomize) apply (erule_tac x="(Q \<longrightarrow>* R)" in allE) apply (rule hoare_strengthen_post) apply (assumption) apply (sep_mp) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<forall>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift. \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>?Q1 sep_lift\<rbrace>
 2. \<And>sep_lift rv s. \<lbrakk>\<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; ?Q1 sep_lift rv s\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; R (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal:
No subgoals!