theory SR_lemmas_C

lemma cmap_relation_ko_atD:
  fixes ko :: "'a :: pspace_storable" and  mp :: "word32 \<rightharpoonup> 'a"
  assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel"
  and     ko: "ko_at' ko ptr s"
  shows   "\<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko'" using ps ko unfolding cmap_relation_def apply clarsimp apply (drule bspec [where x = "ptr"]) apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: obj_at'_def projectKOs) apply (drule equalityD1) apply (drule subsetD [where c = "f ptr"]) apply (rule imageI) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
using this:
cmap_relation (projectKO_opt \<circ>\<^sub>m ksPSpace s) (cslift s') f rel
ko_at' ko ptr s

goal (1 subgoal):
 1. \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
using this:
f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s') \<and> (\<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m ksPSpace s). rel (the ((projectKO_opt \<circ>\<^sub>m ksPSpace s) x)) (the (cslift s' (f x))))
ko_at' ko ptr s

goal (1 subgoal):
 1. \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko ptr s; f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s'); \<forall>x\<in>dom (projectKO_opt \<circ>\<^sub>m ksPSpace s). rel (the ((projectKO_opt \<circ>\<^sub>m ksPSpace s) x)) (the (cslift s' (f x)))\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' ko ptr s; f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s')\<rbrakk> \<Longrightarrow> ptr \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)
 2. \<lbrakk>ko_at' ko ptr s; f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s'); rel (the ((projectKO_opt \<circ>\<^sub>m ksPSpace s) ptr)) (the (cslift s' (f ptr)))\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko ptr s; f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s'); rel (the ((projectKO_opt \<circ>\<^sub>m ksPSpace s) ptr)) (the (cslift s' (f ptr)))\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) = dom (cslift s'); rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s; f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) \<subseteq> dom (cslift s')\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (2 subgoals):
 1. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s\<rbrakk> \<Longrightarrow> f ptr \<in> f ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)
 2. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s; f ptr \<in> dom (cslift s')\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (2 subgoals):
 1. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s\<rbrakk> \<Longrightarrow> ptr \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)
 2. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s; f ptr \<in> dom (cslift s')\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>rel ko (the (cslift s' (f ptr))); ksPSpace s ptr = Some koa; is_aligned ptr (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear ptr (objBitsKO koa) s; f ptr \<in> dom (cslift s')\<rbrakk> \<Longrightarrow> \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko' proof (prove)
goal:
No subgoals!