theory ArchDetype_AI

lemma pspace_respects_device_region_detype[detype_invs_proofs]:
  "pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))" proof - have "pspace_respects_device_region s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (intro pspace_respects_device_regionI) using pspace_aligned_detype valid_objs_detype invs apply (simp_all add: clear_um.pspace detype_def dom_def clear_um_def
                  split: if_split_asm ) apply (drule pspace_respects_device_regionD[rotated -1],auto)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (state)
goal (1 subgoal):
 1. pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. pspace_respects_device_region s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. pspace_respects_device_region s proof (state)
this:
pspace_respects_device_region s

goal (1 subgoal):
 1. pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
pspace_respects_device_region s

goal (1 subgoal):
 1. pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (4 subgoals):
 1. \<And>ptr sz. \<lbrakk>pspace_respects_device_region s; kheap (clear_um (untyped_range cap) (detype (untyped_range cap) s)) ptr = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - dom (device_state (machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))))
 2. \<And>ptr sz. \<lbrakk>pspace_respects_device_region s; kheap (clear_um (untyped_range cap) (detype (untyped_range cap) s)) ptr = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> dom (device_state (machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))))
 3. pspace_respects_device_region s \<Longrightarrow> pspace_aligned (clear_um (untyped_range cap) (detype (untyped_range cap) s))
 4. pspace_respects_device_region s \<Longrightarrow> valid_objs (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
pspace_aligned (detype (untyped_range cap) s)
valid_objs (detype (untyped_range cap) s)
invs s

goal (4 subgoals):
 1. \<And>ptr sz. \<lbrakk>pspace_respects_device_region s; kheap (clear_um (untyped_range cap) (detype (untyped_range cap) s)) ptr = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - dom (device_state (machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))))
 2. \<And>ptr sz. \<lbrakk>pspace_respects_device_region s; kheap (clear_um (untyped_range cap) (detype (untyped_range cap) s)) ptr = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> dom (device_state (machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))))
 3. pspace_respects_device_region s \<Longrightarrow> pspace_aligned (clear_um (untyped_range cap) (detype (untyped_range cap) s))
 4. pspace_respects_device_region s \<Longrightarrow> valid_objs (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (2 subgoals):
 1. \<And>ptr sz. \<lbrakk>pspace_aligned (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>); valid_objs (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>); invs s; pspace_respects_device_region s; ptr \<notin> untyped_range cap; kheap s ptr = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage False sz)) \<subseteq> - {a. \<exists>y. device_state (machine_state s) a = Some y}
 2. \<And>ptr sz. \<lbrakk>pspace_aligned (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>); valid_objs (trans_state (\<lambda>_. detype_ext (untyped_range cap) (exst s)) s\<lparr>kheap := \<lambda>x. if x \<in> untyped_range cap then None else kheap s x\<rparr>); invs s; pspace_respects_device_region s; ptr \<notin> untyped_range cap; kheap s ptr = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> obj_range ptr (ArchObj (DataPage True sz)) \<subseteq> {a. \<exists>y. device_state (machine_state s) a = Some y} proof (prove)
goal:
No subgoals! proof (state)
this:
pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))

goal:
No subgoals!