theory Recycle_C

lemma cmap_relation_If_upd:
  "\<lbrakk> cmap_relation f g ptrfun rel; rel v v'; ptrfun ` S = S'; inj ptrfun \<rbrakk>
   \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> S then Some v else f x)
                     (\<lambda>y. if y \<in> S' then Some v' else g y)
        ptrfun rel" apply (simp add: cmap_relation_def dom_If_Some) apply (rule context_conjI) apply blast apply clarsimp apply (case_tac "x \<in> S") apply simp apply clarsimp apply (subst if_not_P) apply (clarsimp simp: inj_eq) apply (drule bspec, erule domI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation f g ptrfun rel; rel v v'; ptrfun ` S = S'; inj ptrfun\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> S then Some v else f x) (\<lambda>y. if y \<in> S' then Some v' else g y) ptrfun rel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrfun ` dom f = dom g \<and> (\<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x)))); rel v v'; ptrfun ` S = S'; inj ptrfun\<rbrakk> \<Longrightarrow> ptrfun ` (S \<union> dom f) = S' \<union> dom g \<and> (\<forall>x\<in>S \<union> dom f. rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> S' then Some v' else g (ptrfun x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptrfun ` dom f = dom g \<and> (\<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x)))); rel v v'; ptrfun ` S = S'; inj ptrfun\<rbrakk> \<Longrightarrow> ptrfun ` (S \<union> dom f) = S' \<union> dom g
 2. \<lbrakk>ptrfun ` dom f = dom g \<and> (\<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x)))); rel v v'; ptrfun ` S = S'; inj ptrfun; ptrfun ` (S \<union> dom f) = S' \<union> dom g\<rbrakk> \<Longrightarrow> \<forall>x\<in>S \<union> dom f. rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> S' then Some v' else g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptrfun ` dom f = dom g \<and> (\<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x)))); rel v v'; ptrfun ` S = S'; inj ptrfun; ptrfun ` (S \<union> dom f) = S' \<union> dom g\<rbrakk> \<Longrightarrow> \<forall>x\<in>S \<union> dom f. rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> S' then Some v' else g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; x \<in> S \<or> x \<in> dom f; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x)))\<rbrakk> \<Longrightarrow> rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> ptrfun ` S then Some v' else g (ptrfun x))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; x \<in> S \<or> x \<in> dom f; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<in> S\<rbrakk> \<Longrightarrow> rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> ptrfun ` S then Some v' else g (ptrfun x)))
 2. \<And>x. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; x \<in> S \<or> x \<in> dom f; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S\<rbrakk> \<Longrightarrow> rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> ptrfun ` S then Some v' else g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; x \<in> S \<or> x \<in> dom f; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S\<rbrakk> \<Longrightarrow> rel (the (if x \<in> S then Some v else f x)) (the (if ptrfun x \<in> ptrfun ` S then Some v' else g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S; f x = Some y\<rbrakk> \<Longrightarrow> rel y (the (if ptrfun x \<in> ptrfun ` S then Some v' else g (ptrfun x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S; f x = Some y\<rbrakk> \<Longrightarrow> ptrfun x \<notin> ptrfun ` S
 2. \<And>x y. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S; f x = Some y\<rbrakk> \<Longrightarrow> rel y (the (g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; ptrfun ` dom f = dom g; \<forall>x\<in>dom f. rel (the (f x)) (the (g (ptrfun x))); x \<notin> S; f x = Some y\<rbrakk> \<Longrightarrow> rel y (the (g (ptrfun x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>rel v v'; inj ptrfun; ptrfun ` (S \<union> dom f) = ptrfun ` S \<union> dom g; S' = ptrfun ` S; ptrfun ` dom f = dom g; x \<notin> S; f x = Some y; rel (the (f x)) (the (g (ptrfun x)))\<rbrakk> \<Longrightarrow> rel y (the (g (ptrfun x))) proof (prove)
goal:
No subgoals!