theory Retype_C

lemma pspace_aligned_to_C:
  fixes v :: "'a :: pre_storable"
  assumes pal: "pspace_aligned' s"
  and    cmap: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s) :: word32 \<rightharpoonup> 'a)
                              (cslift x :: 'b :: mem_type typ_heap) Ptr rel"
  and     pko: "projectKO_opt ko = Some v"
  and   pkorl: "\<And>ko' (v' :: 'a).  projectKO_opt ko' = Some v' \<Longrightarrow> objBitsKO ko = objBitsKO ko'"
  shows  "\<forall>x\<in>dom (cslift x :: 'b :: mem_type typ_heap). is_aligned (ptr_val x) (objBitsKO ko)"
  (is "\<forall>x\<in>dom ?CS. is_aligned (ptr_val x) (objBitsKO ko)") proof fix z assume "z \<in> dom ?CS" hence "z \<in> Ptr ` dom (projectKO_opt \<circ>\<^sub>m (ksPSpace s) :: word32 \<rightharpoonup> 'a)" using cmap by (simp add: cmap_relation_def) hence pvz: "ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m (ksPSpace s) :: word32 \<rightharpoonup> 'a)" by clarsimp then obtain v' :: 'a where "projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'"
    and pvz: "ptr_val z \<in> dom (ksPSpace s)" apply - apply (frule map_comp_subset_domD) apply (clarsimp simp: dom_def) done thus "is_aligned (ptr_val z) (objBitsKO ko)" using pal unfolding pspace_aligned'_def apply - apply (drule (1) bspec) apply (simp add: pkorl) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (cslift x). is_aligned (ptr_val x) (objBitsKO ko) proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (state)
this:
z \<in> dom (cslift x)

goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (prove)
using this:
z \<in> dom (cslift x)

goal (1 subgoal):
 1. z \<in> PTR('b) ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) proof (prove)
using this:
z \<in> dom (cslift x)
cmap_relation (projectKO_opt \<circ>\<^sub>m ksPSpace s) (cslift x) PTR('b) rel

goal (1 subgoal):
 1. z \<in> PTR('b) ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) proof (state)
this:
z \<in> PTR('b) ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)

goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (prove)
using this:
z \<in> PTR('b) ` dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)

goal (1 subgoal):
 1. ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) proof (state)
this:
ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)

goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (chain)
picking this:
ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s) proof (prove)
using this:
ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'; ptr_val z \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v'. \<lbrakk>projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'; ptr_val z \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> thesis; ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v'. \<lbrakk>projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'; ptr_val z \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> thesis; ptr_val z \<in> dom (projectKO_opt \<circ>\<^sub>m ksPSpace s); ptr_val z \<in> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'
ptr_val z \<in> dom (ksPSpace s)

goal (1 subgoal):
 1. \<And>xa. xa \<in> dom (cslift x) \<Longrightarrow> is_aligned (ptr_val xa) (objBitsKO ko) proof (prove)
using this:
projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'
ptr_val z \<in> dom (ksPSpace s)

goal (1 subgoal):
 1. is_aligned (ptr_val z) (objBitsKO ko) proof (prove)
using this:
projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'
ptr_val z \<in> dom (ksPSpace s)
pspace_aligned' s

goal (1 subgoal):
 1. is_aligned (ptr_val z) (objBitsKO ko) proof (prove)
using this:
projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'
ptr_val z \<in> dom (ksPSpace s)
\<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))

goal (1 subgoal):
 1. is_aligned (ptr_val z) (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'; ptr_val z \<in> dom (ksPSpace s); \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))\<rbrakk> \<Longrightarrow> is_aligned (ptr_val z) (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>projectKO_opt (the (ksPSpace s (ptr_val z))) = Some v'; ptr_val z \<in> dom (ksPSpace s); is_aligned (ptr_val z) (objBitsKO (the (ksPSpace s (ptr_val z))))\<rbrakk> \<Longrightarrow> is_aligned (ptr_val z) (objBitsKO ko) proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (ptr_val z) (objBitsKO ko)

goal:
No subgoals!