theory StateRelation_C

lemma (in kernel) cmap_relation_cs_atD:
  "\<lbrakk> cmap_relation as cs addr_fun rel; cs (addr_fun x) = Some y; inj addr_fun \<rbrakk> \<Longrightarrow>
  \<exists>ko. as x = Some ko \<and> rel ko y" apply (clarsimp simp: cmap_relation_def) apply (subgoal_tac "x \<in> dom as") apply (drule (1) bspec) apply (clarsimp simp: dom_def) apply (subgoal_tac "addr_fun x \<in> addr_fun ` dom as") prefer 2 apply fastforce apply (erule imageE) apply (drule (1) injD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation as cs addr_fun rel; cs (addr_fun x) = Some y; inj addr_fun\<rbrakk> \<Longrightarrow> \<exists>ko. as x = Some ko \<and> rel ko y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> \<exists>ko. as x = Some ko \<and> rel ko y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); x \<in> dom as\<rbrakk> \<Longrightarrow> \<exists>ko. as x = Some ko \<and> rel ko y
 2. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; x \<in> dom as; rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> \<exists>ko. as x = Some ko \<and> rel ko y
 2. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); addr_fun x \<in> addr_fun ` dom as\<rbrakk> \<Longrightarrow> x \<in> dom as
 2. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> addr_fun x \<in> addr_fun ` dom as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x)))\<rbrakk> \<Longrightarrow> addr_fun x \<in> addr_fun ` dom as
 2. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); addr_fun x \<in> addr_fun ` dom as\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); addr_fun x \<in> addr_fun ` dom as\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>cs (addr_fun x) = Some y; inj addr_fun; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); addr_fun x = addr_fun xa; xa \<in> dom as\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>cs (addr_fun x) = Some y; addr_fun ` dom as = dom cs; \<forall>x\<in>dom as. rel (the (as x)) (the (cs (addr_fun x))); addr_fun x = addr_fun xa; xa \<in> dom as; x = xa\<rbrakk> \<Longrightarrow> x \<in> dom as proof (prove)
goal:
No subgoals!