theory KHeap_AI

lemma typ_at_pspace_aligned:
  assumes type_invs: "\<And>T p. f \<lbrace>typ_at T p\<rbrace>"
  assumes dom_shrink: "\<And>x. f \<lbrace>\<lambda>s. x \<notin> dom (kheap s)\<rbrace>"
  shows "f \<lbrace>pspace_aligned\<rbrace>" apply (clarsimp simp: valid_def pspace_aligned_def) apply (drule_tac x = x in bspec) subgoal indom apply (rule ccontr) apply (drule(1) use_valid[OF _ dom_shrink]) apply force done apply (frule(1) indom) apply (clarsimp simp: dom_def obj_bits_T) apply (drule use_valid[OF _ type_invs]) apply (simp add: obj_at_def) apply (intro exI conjI, simp+) apply (simp add: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> f \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); (a, b) \<in> fst (f s); kheap b x = Some y\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (f s); kheap b x = Some y\<rbrakk> \<Longrightarrow> x \<in> dom (kheap s)
 2. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (f s); kheap b x = Some y; is_aligned x (obj_bits (the (kheap s x)))\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a_, b_) \<in> fst (f s_); kheap b_ x_ = Some y_\<rbrakk> \<Longrightarrow> x_ \<in> dom (kheap s_) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a_, b_) \<in> fst (f s_); kheap b_ x_ = Some y_; x_ \<notin> dom (kheap s_)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap b_ x_ = Some y_; x_ \<notin> dom (kheap s_); x_ \<notin> dom (kheap b_)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (f s); kheap b x = Some y; is_aligned x (obj_bits (the (kheap s x)))\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (f s); kheap b x = Some y; is_aligned x (obj_bits (the (kheap s x))); x \<in> dom (kheap s)\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits y) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y ya. \<lbrakk>(a, b) \<in> fst (f s); kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits_type (a_type y)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x y ya. \<lbrakk>kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya\<rbrakk> \<Longrightarrow> typ_at (?T21 s a b x y ya) (?p21 s a b x y ya) s
 2. \<And>s a b x y ya. \<lbrakk>kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya; typ_at (?T21 s a b x y ya) (?p21 s a b x y ya) b\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits_type (a_type y)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x y ya. \<lbrakk>kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (?p21 s a b x y ya) = Some ko \<and> a_type ko = ?T21 s a b x y ya
 2. \<And>s a b x y ya. \<lbrakk>kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya; typ_at (?T21 s a b x y ya) (?p21 s a b x y ya) b\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits_type (a_type y)) proof (prove)
goal (1 subgoal):
 1. \<And>s b x y ya. \<lbrakk>kheap b x = Some y; is_aligned x (obj_bits_type (a_type ya)); kheap s x = Some ya; typ_at (a_type ya) x b\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits_type (a_type y)) proof (prove)
goal:
No subgoals!