theory Retype_C

lemma cmap_relation_updI:
  "\<lbrakk>cmap_relation am cm f rel; am dest = Some ov; rel nv nv'; inj f\<rbrakk> \<Longrightarrow> cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel" apply (clarsimp simp: cmap_relation_def) apply (rule conjI) apply (drule_tac t="dom cm" in sym) apply fastforce apply clarsimp apply (case_tac "x = dest") apply simp apply clarsimp apply (subgoal_tac "f x \<noteq> f dest") apply simp apply force apply clarsimp apply (drule (1) injD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm f rel; am dest = Some ov; rel nv nv'; inj f\<rbrakk> \<Longrightarrow> cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> dom cm = insert (f dest) (dom cm) \<and> (\<forall>x\<in>dom am. rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> dom cm = insert (f dest) (dom cm)
 2. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am. rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); dom cm = f ` dom am\<rbrakk> \<Longrightarrow> dom cm = insert (f dest) (dom cm)
 2. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am. rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom am. rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y\<rbrakk> \<Longrightarrow> rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x = dest\<rbrakk> \<Longrightarrow> rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x)))
 2. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel (the (if x = dest then Some nv else am x)) (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel y (the (if f x = f dest then Some nv' else cm (f x))) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest; f x \<noteq> f dest\<rbrakk> \<Longrightarrow> rel y (the (if f x = f dest then Some nv' else cm (f x)))
 2. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> f x \<noteq> f dest proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest; f x \<noteq> f dest\<rbrakk> \<Longrightarrow> rel y (the (cm (f x)))
 2. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> f x \<noteq> f dest proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest\<rbrakk> \<Longrightarrow> f x \<noteq> f dest proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; inj f; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest; f x = f dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>am dest = Some ov; rel nv nv'; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); am x = Some y; x \<noteq> dest; f x = f dest; x = dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!