theory SR_lemmas_C

lemma cmap_relation_upd_relI:
  fixes am :: "word32 \<rightharpoonup> 'a" and cm :: "'b typ_heap"
  assumes cr: "cmap_relation am cm f rel"
  and   cof: "am dest = Some v"
  and   cl:  "cm (f dest) = Some v'"
  and   cc:  "rel' nv nv'"
  and   rel: "\<And>x ov ov'. \<lbrakk> x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov' \<rbrakk> \<Longrightarrow> rel' ov ov'"
  and   inj: "inj f"
  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel'" using assms apply - apply (rule cmap_relationE1, assumption+) apply clarsimp apply (rule cmap_relationI) apply (simp add: cmap_relation_def) apply (case_tac "x = dest") apply simp apply (simp add: inj_eq split: if_split_asm) apply (erule (2) rel) apply (erule (2) cmap_relation_relI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel' proof (prove)
using this:
cmap_relation am cm f rel
am dest = Some v
cm (f dest) = Some v'
rel' nv nv'
\<lbrakk>?x \<noteq> dest; am ?x = Some ?ov; cm (f ?x) = Some ?ov'; rel ?ov ?ov'\<rbrakk> \<Longrightarrow> rel' ?ov ?ov'
inj f

goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm f rel; am dest = Some v; cm (f dest) = Some v'; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f\<rbrakk> \<Longrightarrow> cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel' proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>cmap_relation am cm f rel; am dest = Some v; cm (f dest) = Some v'; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v y'; cm (f dest) = Some y'\<rbrakk> \<Longrightarrow> cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'\<rbrakk> \<Longrightarrow> cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'\<rbrakk> \<Longrightarrow> f ` dom (am(dest \<mapsto> nv)) = dom (cm(f dest \<mapsto> nv'))
 2. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; (am(dest \<mapsto> nv)) x = Some va; (cm(f dest \<mapsto> nv')) (f x) = Some v'a\<rbrakk> \<Longrightarrow> rel' va v'a proof (prove)
goal (1 subgoal):
 1. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; (am(dest \<mapsto> nv)) x = Some va; (cm(f dest \<mapsto> nv')) (f x) = Some v'a\<rbrakk> \<Longrightarrow> rel' va v'a proof (prove)
goal (2 subgoals):
 1. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; (am(dest \<mapsto> nv)) x = Some va; (cm(f dest \<mapsto> nv')) (f x) = Some v'a; x = dest\<rbrakk> \<Longrightarrow> rel' va v'a
 2. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; (am(dest \<mapsto> nv)) x = Some va; (cm(f dest \<mapsto> nv')) (f x) = Some v'a; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel' va v'a proof (prove)
goal (1 subgoal):
 1. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; (am(dest \<mapsto> nv)) x = Some va; (cm(f dest \<mapsto> nv')) (f x) = Some v'a; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel' va v'a proof (prove)
goal (1 subgoal):
 1. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; am x = Some va; cm (f x) = Some v'a; x \<noteq> dest\<rbrakk> \<Longrightarrow> rel' va v'a proof (prove)
goal (1 subgoal):
 1. \<And>x va v'a. \<lbrakk>cmap_relation am cm f rel; rel' nv nv'; \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel' ov ov'; inj f; am dest = Some v; rel v v'; cm (f dest) = Some v'; am x = Some va; cm (f x) = Some v'a\<rbrakk> \<Longrightarrow> rel va v'a proof (prove)
goal:
No subgoals!