theory ArchKHeap_AI

lemma in_device_frame_obj_upd:
  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
   in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)
   = in_device_frame x s" apply (rule iffI) apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm) apply (elim disjE) apply clarsimp apply (intro exI) apply (rule conjI,assumption) apply (simp add: a_type_def) apply (fastforce simp: a_type_def) apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm) apply (rule_tac x = sz in exI) apply (intro conjI impI) apply (fastforce simp: a_type_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) = in_device_frame x s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> in_device_frame x s
 2. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); x && ~~ mask (pageBitsForSize sz) = p \<or> (\<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz))\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); x && ~~ mask (pageBitsForSize sz) = p\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 3. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz)); p = x && ~~ mask (pageBitsForSize sz); k = ArchObj (DataPage True sz); ko = ArchObj (DataPage True sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 3. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz)); p = x && ~~ mask (pageBitsForSize sz); k = ArchObj (DataPage True sz); ko = ArchObj (DataPage True sz)\<rbrakk> \<Longrightarrow> kheap s (x && ~~ mask (pageBitsForSize (?sz26 sz))) = Some (?ko27 sz) \<and> a_type (?ko27 sz) = AArch (ADeviceData (?sz26 sz))
 2. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 3. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sz. \<lbrakk>kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz)); p = x && ~~ mask (pageBitsForSize sz); k = ArchObj (DataPage True sz); ko = ArchObj (DataPage True sz)\<rbrakk> \<Longrightarrow> a_type (ArchObj (DataPage True sz)) = AArch (ADeviceData sz)
 2. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 3. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz); \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)\<rbrakk> \<Longrightarrow> \<exists>sz ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz)
 2. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; in_device_frame x s\<rbrakk> \<Longrightarrow> in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> \<exists>sz. (x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz)) \<and> (x && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz))) proof (prove)
goal (1 subgoal):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> (x && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type ko = AArch (ADeviceData sz)) \<and> (x && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz))) proof (prove)
goal (2 subgoals):
 1. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz)); x && ~~ mask (pageBitsForSize sz) = p\<rbrakk> \<Longrightarrow> a_type ko = AArch (ADeviceData sz)
 2. \<And>sz. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko; kheap s (x && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz)); x && ~~ mask (pageBitsForSize sz) \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz) proof (prove)
goal:
No subgoals!