theory Untyped_R

lemma dom_n' [simp]: "dom n' = dom n" apply (simp add: n'_def) apply (simp add: modify_map_if dom_def) apply (rule set_eqI) apply simp apply (rule iffI) apply auto[1] apply clarsimp apply (case_tac y) apply (case_tac "mdbNext parent_node = x") apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom n' = dom n proof (prove)
goal (1 subgoal):
 1. dom (modify_map n (mdbNext parent_node) (cteMDBNode_update (mdbPrev_update (\<lambda>a. site)))) = dom n proof (prove)
goal (1 subgoal):
 1. {a. \<exists>y. (mdbNext parent_node = a \<longrightarrow> (\<exists>cap node. n a = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> a \<longrightarrow> (\<exists>cap node. n a = Some (CTE cap node) \<and> y = CTE cap node))} = {a. \<exists>y. n a = Some y} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> {a. \<exists>y. (mdbNext parent_node = a \<longrightarrow> (\<exists>cap node. n a = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> a \<longrightarrow> (\<exists>cap node. n a = Some (CTE cap node) \<and> y = CTE cap node))}) = (x \<in> {a. \<exists>y. n a = Some y}) proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<exists>y. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> y = CTE cap node))) = (\<exists>y. n x = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<exists>y. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> y = CTE cap node)) \<Longrightarrow> \<exists>y. n x = Some y
 2. \<And>x. \<exists>y. n x = Some y \<Longrightarrow> \<exists>y. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> y = CTE cap node)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<exists>y. n x = Some y \<Longrightarrow> \<exists>y. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = y)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. n x = Some (CTE cap node) \<and> y = CTE cap node)) proof (prove)
goal (1 subgoal):
 1. \<And>x y. n x = Some y \<Longrightarrow> \<exists>ya. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = ya)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> ya = CTE cap node)) proof (prove)
goal (1 subgoal):
 1. \<And>x y x1 x2. \<lbrakk>n x = Some y; y = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>ya. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = ya)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> ya = CTE cap node)) proof (prove)
goal (2 subgoals):
 1. \<And>x y x1 x2. \<lbrakk>n x = Some y; y = CTE x1 x2; mdbNext parent_node = x\<rbrakk> \<Longrightarrow> \<exists>ya. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = ya)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> ya = CTE cap node))
 2. \<And>x y x1 x2. \<lbrakk>n x = Some y; y = CTE x1 x2; mdbNext parent_node \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>ya. (mdbNext parent_node = x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> CTE cap (mdbPrev_update (\<lambda>a. site) node) = ya)) \<and> (mdbNext parent_node \<noteq> x \<longrightarrow> (\<exists>cap node. y = CTE cap node \<and> ya = CTE cap node)) proof (prove)
goal:
No subgoals!