theory Retype_C

lemma cmap_relation_retype:
  assumes cm: "cmap_relation mp mp' Ptr rel"
  and   rel: "rel (makeObject :: 'a :: pspace_storable) ko'"
  shows "cmap_relation
        (\<lambda>x. if x \<in> addrs then Some (makeObject :: 'a :: pspace_storable) else mp x)
        (\<lambda>y. if y \<in> Ptr ` addrs then Some ko' else mp' y)
        Ptr rel" using cm rel apply - apply (rule cmap_relationI) apply (simp add: dom_if cmap_relation_def image_Un) apply (case_tac "x \<in> addrs") apply simp apply simp apply (subst (asm) if_not_P) apply clarsimp apply (erule (2) cmap_relation_relI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (\<lambda>x. if x \<in> addrs then Some makeObject else mp x) (\<lambda>y. if y \<in> PTR('b) ` addrs then Some ko' else mp' y) PTR('b) rel proof (prove)
using this:
cmap_relation mp mp' PTR('b) rel
rel makeObject ko'

goal (1 subgoal):
 1. cmap_relation (\<lambda>x. if x \<in> addrs then Some makeObject else mp x) (\<lambda>y. if y \<in> PTR('b) ` addrs then Some ko' else mp' y) PTR('b) rel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'\<rbrakk> \<Longrightarrow> cmap_relation (\<lambda>x. if x \<in> addrs then Some makeObject else mp x) (\<lambda>y. if y \<in> PTR('b) ` addrs then Some ko' else mp' y) PTR('b) rel proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'\<rbrakk> \<Longrightarrow> PTR('b) ` dom (\<lambda>x. if x \<in> addrs then Some makeObject else mp x) = dom (\<lambda>y. if y \<in> PTR('b) ` addrs then Some ko' else mp' y)
 2. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; (if x \<in> addrs then Some makeObject else mp x) = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; (if x \<in> addrs then Some makeObject else mp x) = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; (if x \<in> addrs then Some makeObject else mp x) = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'; x \<in> addrs\<rbrakk> \<Longrightarrow> rel v v'
 2. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; (if x \<in> addrs then Some makeObject else mp x) = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'; x \<notin> addrs\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; (if x \<in> addrs then Some makeObject else mp x) = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'; x \<notin> addrs\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; mp x = Some v; (if PTR('b) x \<in> PTR('b) ` addrs then Some ko' else mp' (PTR('b) x)) = Some v'; x \<notin> addrs\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (2 subgoals):
 1. \<And>x v v'. \<lbrakk>x \<notin> addrs; cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; mp x = Some v\<rbrakk> \<Longrightarrow> PTR('b) x \<notin> PTR('b) ` addrs
 2. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; mp x = Some v; mp' (PTR('b) x) = Some v'; x \<notin> addrs\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>cmap_relation mp mp' PTR('b) rel; rel makeObject ko'; mp x = Some v; mp' (PTR('b) x) = Some v'; x \<notin> addrs\<rbrakk> \<Longrightarrow> rel v v' proof (prove)
goal:
No subgoals!