theory Retype_AI

lemma psp_al:
  shows "pspace_aligned s'" unfolding pspace_aligned_def s'_def ps_def proof (clarsimp split: if_split_asm) fix x assume "x \<in> set (retype_addrs ptr ty n us)" thus "is_aligned x (obj_bits (default_object ty dev us))" apply - apply (drule retype_addrs_aligned) apply (insert cover tyunt) apply (fastforce simp:range_cover_def word_bits_def)+ apply (simp add: obj_bits_dev_irr
              split: Structures_A.apiobject_type.splits) done next fix x y assume "x \<notin> set (retype_addrs ptr ty n us)" and px: "kheap s x = Some y" have "pspace_aligned s" by (rule valid_pspaceE[OF vp],simp) thus "is_aligned x (obj_bits y)" proof show "x \<in> dom (kheap s)" by (rule domI) fact+ next assume "is_aligned x (obj_bits (the (kheap s x)))" thus "is_aligned x (obj_bits y)" using px by simp qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned s' proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom (kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)). is_aligned x (obj_bits (the (kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) x))) proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set (retype_addrs ptr ty n us) \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us))
 2. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set (retype_addrs ptr ty n us) \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us))
 2. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
this:
x \<in> set (retype_addrs ptr ty n us)

goal (2 subgoals):
 1. \<And>x. x \<in> set (retype_addrs ptr ty n us) \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us))
 2. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
using this:
x \<in> set (retype_addrs ptr ty n us)

goal (1 subgoal):
 1. is_aligned x (obj_bits (default_object ty dev us)) proof (prove)
goal (1 subgoal):
 1. x \<in> set (retype_addrs ptr ty n us) \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us)) proof (prove)
goal (4 subgoals):
 1. is_aligned ptr (obj_bits_api ty us)
 2. ?sz1 < word_bits
 3. obj_bits_api ty us \<le> ?sz1
 4. is_aligned x (obj_bits_api ty us) \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> is_aligned ptr (obj_bits_api ty us)
 2. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> ?sz1 < word_bits
 3. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> ?sz1
 4. \<lbrakk>is_aligned x (obj_bits_api ty us); range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (obj_bits_api ty us); range_cover ptr sz (obj_bits_api ty us) n; ty \<noteq> Untyped\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits (default_object ty dev us)) proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned x (obj_bits (default_object ty dev us))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
this:
x \<notin> set (retype_addrs ptr ty n us)
kheap s x = Some y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. pspace_aligned s proof (state)
this:
pspace_aligned s

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<notin> set (retype_addrs ptr ty n us); kheap s x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
using this:
pspace_aligned s

goal (1 subgoal):
 1. is_aligned x (obj_bits y) proof (state)
goal (2 subgoals):
 1. ?x \<in> dom (kheap s)
 2. is_aligned ?x (obj_bits (the (kheap s ?x))) \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. x \<in> dom (kheap s) proof (state)
this:
x \<in> dom (kheap s)

goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> is_aligned x (obj_bits y) proof (state)
this:
is_aligned x (obj_bits (the (kheap s x)))

goal (1 subgoal):
 1. is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
using this:
is_aligned x (obj_bits (the (kheap s x)))

goal (1 subgoal):
 1. is_aligned x (obj_bits y) proof (prove)
using this:
is_aligned x (obj_bits (the (kheap s x)))
kheap s x = Some y

goal (1 subgoal):
 1. is_aligned x (obj_bits y) proof (state)
this:
is_aligned x (obj_bits y)

goal:
No subgoals! proof (state)
this:
is_aligned x (obj_bits y)

goal:
No subgoals!