kings-crown/FVELER_Isabelle huggingface dataset:
theory Map_Extra

lemma dom_empty_is_empty:
  "(dom m = {}) = (m = Map.empty)" proof (rule iffI) assume a: "dom m = {}" { assume "m \<noteq> Map.empty" hence "dom m \<noteq> {}" by - (subst (asm) empty_forall_equiv, simp add: dom_def) hence False using a by blast } thus "m = Map.empty" by blast next assume a: "m = Map.empty" thus "dom m = {}" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (dom m = {}) = (m = (\<lambda>x. None)) proof (state)
goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
this:
dom m = {}

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
this:
dom m = {}

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
this:
m \<noteq> (\<lambda>x. None)

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (prove)
using this:
m \<noteq> (\<lambda>x. None)

goal (1 subgoal):
 1. dom m \<noteq> {} proof (state)
this:
dom m \<noteq> {}

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (prove)
using this:
dom m \<noteq> {}

goal (1 subgoal):
 1. False proof (prove)
using this:
dom m \<noteq> {}
dom m = {}

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
this:
m \<noteq> (\<lambda>x. None) \<Longrightarrow> False

goal (2 subgoals):
 1. dom m = {} \<Longrightarrow> m = (\<lambda>x. None)
 2. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (prove)
using this:
m \<noteq> (\<lambda>x. None) \<Longrightarrow> False

goal (1 subgoal):
 1. m = (\<lambda>x. None) proof (state)
this:
m = (\<lambda>x. None)

goal (1 subgoal):
 1. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
goal (1 subgoal):
 1. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (state)
this:
m = (\<lambda>x. None)

goal (1 subgoal):
 1. m = (\<lambda>x. None) \<Longrightarrow> dom m = {} proof (prove)
using this:
m = (\<lambda>x. None)

goal (1 subgoal):
 1. dom m = {} proof (state)
this:
dom m = {}

goal:
No subgoals!
theory Map_Extra

lemma map_add_dom_eq:
  "dom m = dom m' \<Longrightarrow> m ++ m' = m'" by (rule ext) (auto simp: map_add_def split: option.splits)

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

lemma map_add_right_dom_eq:
  "\<lbrakk> m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0' ++ m\<^sub>1'; dom m\<^sub>1 = dom m\<^sub>1' \<rbrakk> \<Longrightarrow> m\<^sub>1 = m\<^sub>1'" unfolding map_add_def by (rule ext, rule ccontr,
      drule_tac x=x in fun_cong, clarsimp split: option.splits,
      drule sym, drule sym, force+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m\<^sub>0 ++ m\<^sub>1 = m\<^sub>0' ++ m\<^sub>1'; dom m\<^sub>1 = dom m\<^sub>1'\<rbrakk> \<Longrightarrow> m\<^sub>1 = m\<^sub>1' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. case m\<^sub>1 x of None \<Rightarrow> m\<^sub>0 x | Some x \<Rightarrow> Some x) = (\<lambda>x. case m\<^sub>1' x of None \<Rightarrow> m\<^sub>0' x | Some x \<Rightarrow> Some x); dom m\<^sub>1 = dom m\<^sub>1'\<rbrakk> \<Longrightarrow> m\<^sub>1 = m\<^sub>1'
theory Map_Extra

lemma map_le_same_dom_eq:
  "\<lbrakk> m\<^sub>0 \<subseteq>\<^sub>m m\<^sub>1 ; dom m\<^sub>0 = dom m\<^sub>1 \<rbrakk> \<Longrightarrow> m\<^sub>0 = m\<^sub>1" by (simp add: map_le_antisym map_le_def)

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

lemma restrict_map_cancel:
  "(m |` S = m |` T) = (dom m \<inter> S = dom m \<inter> T)" by (fastforce dest: fun_cong simp: restrict_map_def None_not_eq split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m |` S = m |` T) = (dom m \<inter> S = dom m \<inter> T)
theory Map_Extra

lemma map_add_restrict_dom_right [simp]:
  "(m ++ m') |` dom m' = m'" by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m ++ m') |` dom m' = m'
theory Map_Extra

lemma restrict_map_UNIV [simp]:
  "m |` UNIV = m" by (simp add: restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` UNIV = m
theory Map_Extra

lemma restrict_map_dom:
  "S = dom m \<Longrightarrow> m |` S = m" by (rule ext, auto simp: restrict_map_def None_not_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S = dom m \<Longrightarrow> m |` S = m
theory Map_Extra

lemma restrict_map_subdom:
  "dom m \<subseteq> S \<Longrightarrow> m |` S = m" by (fastforce simp: restrict_map_def None_com)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom m \<subseteq> S \<Longrightarrow> m |` S = m
theory Map_Extra

lemma map_add_restrict:
  "(m\<^sub>0 ++ m\<^sub>1) |` S = ((m\<^sub>0 |` S) ++ (m\<^sub>1 |` S))" by (force simp: map_add_def restrict_map_def)

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

lemma map_le_restrict:
  "m \<subseteq>\<^sub>m m' \<Longrightarrow> m = m' |` dom m" by (force simp: map_le_def restrict_map_def None_com)

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

lemma restrict_map_le:
  "m |` S \<subseteq>\<^sub>m m" by (auto simp: map_le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` S \<subseteq>\<^sub>m m
theory Map_Extra

lemma restrict_map_remerge:
  "\<lbrakk> S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` S ++ m |` T = m |` (S \<union> T)" by (rule ext, clarsimp simp: restrict_map_def map_add_def
                         split: option.splits)

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

lemma restrict_map_empty:
  "dom m \<inter> S = {} \<Longrightarrow> m |` S = Map.empty" by (fastforce simp: restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom m \<inter> S = {} \<Longrightarrow> m |` S = (\<lambda>x. None)
theory Map_Extra

lemma map_add_restrict_comp_right [simp]:
  "(m |` S ++ m |` (UNIV - S)) = m" by (force simp: map_add_def restrict_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` S ++ m |` (UNIV - S) = m
theory Map_Extra

lemma map_add_restrict_comp_right_dom [simp]:
  "(m |` S ++ m |` (dom m - S)) = m" by (rule ext, auto simp: map_add_def restrict_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` S ++ m |` (dom m - S) = m
theory Map_Extra

lemma map_add_restrict_comp_left [simp]:
  "(m |` (UNIV - S) ++ m |` S) = m" by (subst map_add_comm, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` (UNIV - S) ++ m |` S = m
theory Map_Extra

lemma map_add_restrict_nonmember_right:
  "x \<notin> dom m' \<Longrightarrow> (m ++ m') |` {x} = m |` {x}" by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom m' \<Longrightarrow> (m ++ m') |` {x} = m |` {x}
theory Map_Extra

lemma map_add_restrict_nonmember_left:
  "x \<notin> dom m \<Longrightarrow> (m ++ m') |` {x} = m' |` {x}" by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom m \<Longrightarrow> (m ++ m') |` {x} = m' |` {x}
theory Map_Extra

lemma map_add_restrict_right:
  "x \<subseteq> dom m' \<Longrightarrow> (m ++ m') |` x = m' |` x" by (rule ext, auto simp: restrict_map_def map_add_def split: option.splits)

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

lemma map_le_dom_subset_restrict:
  "\<lbrakk> m' \<subseteq>\<^sub>m m; dom m' \<subseteq> S \<rbrakk> \<Longrightarrow> m' \<subseteq>\<^sub>m (m |` S)" by (force simp: restrict_map_def map_le_def)

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

lemma map_le_dom_restrict_sub_add:
  "m' \<subseteq>\<^sub>m m \<Longrightarrow> m |` (dom m - dom m') ++ m' = m" by (rule ext, auto simp: None_com map_add_def restrict_map_def map_le_def
                     split: option.splits; force simp: Some_com)

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

lemma subset_map_restrict_sub_add:
  "T \<subseteq> S \<Longrightarrow> m |` (S - T) ++ m |` T = m |` S" by (rule ext) (auto simp: restrict_map_def map_add_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. T \<subseteq> S \<Longrightarrow> m |` (S - T) ++ m |` T = m |` S
theory Map_Extra

lemma restrict_map_sub_union:
  "m |` (dom m - (S \<union> T)) = (m |` (dom m - T)) |` (dom m - S)" by (auto simp: restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m |` (dom m - (S \<union> T)) = m |` (dom m - T) |` (dom m - S)
theory Map_Extra

lemma prod_restrict_map_add:
  "\<lbrakk> S \<union> T = U; S \<inter> T = {} \<rbrakk> \<Longrightarrow> m |` (X \<times> S) ++ m |` (X \<times> T) = m |` (X \<times> U)" by (auto simp: map_add_def restrict_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<union> T = U; S \<inter> T = {}\<rbrakk> \<Longrightarrow> m |` (X \<times> S) ++ m |` (X \<times> T) = m |` (X \<times> U)
theory Map_Extra

lemma restrict_map_sub_disj: "h |` S \<bottom> h `- S" by (fastforce simp: sub_restrict_map_def restrict_map_def map_disj_def
               split: option.splits if_split_asm)

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

lemma restrict_map_sub_add: "h |` S ++ h `- S = h" by (fastforce simp: sub_restrict_map_def restrict_map_def map_add_def
               split: option.splits if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h |` S ++ h `- S = h
theory Map_Extra

lemma map_disj_empty_right [simp]:
  "h \<bottom> Map.empty" by (simp add: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h \<bottom> (\<lambda>x. None)
theory Map_Extra

lemma map_disj_empty_left [simp]:
  "Map.empty \<bottom> h" by (simp add: map_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. None) \<bottom> h
theory Map_Extra

lemma map_disj_com:
  "h\<^sub>0 \<bottom> h\<^sub>1 = h\<^sub>1 \<bottom> h\<^sub>0" by (simp add: map_disj_def, fast)

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

lemma map_disjD:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> dom h\<^sub>0 \<inter> dom h\<^sub>1 = {}" by (simp add: map_disj_def)

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

lemma map_disjI:
  "dom h\<^sub>0 \<inter> dom h\<^sub>1 = {} \<Longrightarrow> h\<^sub>0 \<bottom> h\<^sub>1" by (simp add: map_disj_def)

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

lemma map_add_com:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 ++ h\<^sub>1 = h\<^sub>1 ++ h\<^sub>0" by (drule map_disjD, rule map_add_comm, force)

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

lemma map_add_left_commute:
  "h\<^sub>0 \<bottom> h\<^sub>1 \<Longrightarrow> h\<^sub>0 ++ (h\<^sub>1 ++ h\<^sub>2) = h\<^sub>1 ++ (h\<^sub>0 ++ h\<^sub>2)" by (simp add: map_add_com map_disj_com)

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

lemma map_add_disj:
  "h\<^sub>0 \<bottom> (h\<^sub>1 ++ h\<^sub>2) = (h\<^sub>0 \<bottom> h\<^sub>1 \<and> h\<^sub>0 \<bottom> h\<^sub>2)" by (simp add: map_disj_def, fast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>0 \<bottom> h\<^sub>1 ++ h\<^sub>2 = (h\<^sub>0 \<bottom> h\<^sub>1 \<and> h\<^sub>0 \<bottom> h\<^sub>2)
theory Map_Extra

lemma map_add_disj':
  "(h\<^sub>1 ++ h\<^sub>2) \<bottom> h\<^sub>0 = (h\<^sub>1 \<bottom> h\<^sub>0 \<and> h\<^sub>2 \<bottom> h\<^sub>0)" by (simp add: map_disj_def, fast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>1 ++ h\<^sub>2 \<bottom> h\<^sub>0 = (h\<^sub>1 \<bottom> h\<^sub>0 \<and> h\<^sub>2 \<bottom> h\<^sub>0)
theory Map_Extra

lemma map_disj_None_right:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; x \<in> dom h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>1 x = None" by (auto simp: map_disj_def dom_def)

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

lemma map_disj_None_left:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; x \<in> dom h\<^sub>1 \<rbrakk> \<Longrightarrow> h\<^sub>0 x = None" by (auto simp: map_disj_def dom_def)

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

lemma map_disj_None_left':
  "\<lbrakk> h\<^sub>0 x = Some y ; h\<^sub>1 \<bottom> h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>1 x = None " by (auto simp: map_disj_def)

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

lemma map_disj_None_right':
  "\<lbrakk> h\<^sub>1 x = Some y ; h\<^sub>1 \<bottom> h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0 x = None " by (auto simp: map_disj_def)

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

lemma map_disj_common:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; h\<^sub>0 p = Some v ; h\<^sub>1 p = Some v' \<rbrakk> \<Longrightarrow> False" by (frule (1) map_disj_None_left', simp)

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

lemma map_disj_eq_dom_left:
  "\<lbrakk> h\<^sub>0 \<bottom> h\<^sub>1 ; dom h\<^sub>0' = dom h\<^sub>0 \<rbrakk> \<Longrightarrow> h\<^sub>0' \<bottom> h\<^sub>1" by (auto simp: map_disj_def)

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

lemma map_add_eval_left:
  "\<lbrakk> x \<in> dom h ; h \<bottom> h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h x" by (auto dest!: map_disj_None_right simp: map_add_def cong: option.case_cong)

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

lemma map_add_eval_right:
  "\<lbrakk> x \<in> dom h' \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x" by (rule map_add_dom_app_simps)

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

lemma map_add_eval_right':
  "\<lbrakk> x \<notin> dom h \<rbrakk> \<Longrightarrow> (h ++ h') x = h' x" by (rule map_add_dom_app_simps)

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

lemma map_add_left_dom_eq:
  assumes eq: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'"
  assumes etc: "h\<^sub>0 \<bottom> h\<^sub>1" "h\<^sub>0' \<bottom> h\<^sub>1'" "dom h\<^sub>0 = dom h\<^sub>0'"
  shows "h\<^sub>0 = h\<^sub>0'" proof - from eq have "h\<^sub>1 ++ h\<^sub>0 = h\<^sub>1' ++ h\<^sub>0'" using etc by (simp add: map_add_ac) thus ?thesis using etc by (fastforce elim!: map_add_right_dom_eq simp: map_add_ac) 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 (chain)
picking this:
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>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'
dom h\<^sub>0 = dom h\<^sub>0'

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'
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0' \<bottom> h\<^sub>1'
dom h\<^sub>0 = dom h\<^sub>0'

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_eq:
  assumes eq: "h\<^sub>0 ++ h = h\<^sub>1 ++ h"
  assumes disj: "h\<^sub>0 \<bottom> h" "h\<^sub>1 \<bottom> h"
  shows "h\<^sub>0 = h\<^sub>1" proof (rule ext) fix x from eq have eq': "(h\<^sub>0 ++ h) x = (h\<^sub>1 ++ h) x" by auto { assume "x \<in> dom h" hence "h\<^sub>0 x = h\<^sub>1 x" using disj by (simp add: map_disj_None_left) } moreover { assume "x \<notin> dom h" hence "h\<^sub>0 x = h\<^sub>1 x" using disj eq' by (simp add: map_add_eval_left') } ultimately show "h\<^sub>0 x = h\<^sub>1 x" by cases qed

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

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

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

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<in> dom h

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (prove)
using this:
x \<in> dom h

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

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

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<in> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<in> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<in> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<notin> dom h

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (prove)
using this:
x \<notin> dom h

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

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

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (state)
this:
x \<notin> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x

goal (1 subgoal):
 1. \<And>x. h\<^sub>0 x = h\<^sub>1 x proof (chain)
picking this:
x \<in> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x
x \<notin> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x proof (prove)
using this:
x \<in> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x
x \<notin> dom h \<Longrightarrow> h\<^sub>0 x = h\<^sub>1 x

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

goal:
No subgoals!
theory Map_Extra

lemma map_add_right_eq:
  "\<lbrakk>h ++ h\<^sub>0 = h ++ h\<^sub>1; h\<^sub>0 \<bottom> h; h\<^sub>1 \<bottom> h\<rbrakk> \<Longrightarrow> h\<^sub>0 = h\<^sub>1" by (rule_tac h=h in map_add_left_eq, auto simp: map_add_ac)

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

lemma map_disj_add_eq_dom_right_eq:
  assumes merge: "h\<^sub>0 ++ h\<^sub>1 = h\<^sub>0' ++ h\<^sub>1'" and d: "dom h\<^sub>0 = dom h\<^sub>0'" and
      ab_disj: "h\<^sub>0 \<bottom> h\<^sub>1" and cd_disj: "h\<^sub>0' \<bottom> h\<^sub>1'"
  shows "h\<^sub>1 = h\<^sub>1'" proof (rule ext) fix x from merge have merge_x: "(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0' ++ h\<^sub>1') x" by simp with d ab_disj cd_disj show  "h\<^sub>1 x = h\<^sub>1' x" by - (case_tac "h\<^sub>1 x", case_tac "h\<^sub>1' x", simp, fastforce simp: map_disj_def,
          case_tac "h\<^sub>1' x", clarsimp, simp add: Some_com,
          force simp: map_disj_def, simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h\<^sub>1 = h\<^sub>1' proof (state)
goal (1 subgoal):
 1. \<And>x. h\<^sub>1 x = h\<^sub>1' x proof (state)
goal (1 subgoal):
 1. \<And>x. h\<^sub>1 x = h\<^sub>1' x proof (chain)
picking this:
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 (1 subgoal):
 1. \<And>x. h\<^sub>1 x = h\<^sub>1' x proof (chain)
picking this:
dom h\<^sub>0 = dom h\<^sub>0'
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0' \<bottom> h\<^sub>1'
(h\<^sub>0 ++ h\<^sub>1) x = (h\<^sub>0' ++ h\<^sub>1') x proof (prove)
using this:
dom h\<^sub>0 = dom h\<^sub>0'
h\<^sub>0 \<bottom> h\<^sub>1
h\<^sub>0' \<bottom> h\<^sub>1'
(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 (state)
this:
h\<^sub>1 x = h\<^sub>1' x

goal:
No subgoals!