theory ArchRetype_AI

lemma equal_kernel_mappings:
  "equal_kernel_mappings s \<Longrightarrow>
      if ty = ArchObject PageDirectoryObj
      then equal_kernel_mappings
           (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr ty n us))\<rparr>)
      else equal_kernel_mappings s'" apply (simp add: equal_kernel_mappings_def) apply (intro conjI impI) apply (elim allEI) apply (simp add: obj_at_def restrict_map_def) apply (simp add: s'_def ps_def) apply (elim allEI) apply (simp add: obj_at_def restrict_map_def) apply (simp add: s'_def ps_def) apply (simp add: default_object_def default_arch_object_def tyunt
            split: Structures_A.apiobject_type.split
                   aobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equal_kernel_mappings s \<Longrightarrow> if ty = ArchObject PageDirectoryObj then equal_kernel_mappings (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr ty n us))\<rparr>) else equal_kernel_mappings s' proof (prove)
goal (1 subgoal):
 1. \<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) \<Longrightarrow> (ty = ArchObject PageDirectoryObj \<longrightarrow> (\<forall>x y pd pd'. ako_at (PageDirectory pd) x (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<and> ako_at (PageDirectory pd') y (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w))) \<and> (ty \<noteq> ArchObject PageDirectoryObj \<longrightarrow> (\<forall>x y pd pd'. ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>x y pd pd'. ako_at (PageDirectory pd) x (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<and> ako_at (PageDirectory pd') y (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)
 2. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); ty \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>x y pd pd'. ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (2 subgoals):
 1. \<And>x y pd pd'. \<lbrakk>ty = ArchObject PageDirectoryObj; ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> ako_at (PageDirectory pd) x (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<and> ako_at (PageDirectory pd') y (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr (ArchObject PageDirectoryObj) n us))\<rparr>) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)
 2. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); ty \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>x y pd pd'. ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (2 subgoals):
 1. \<And>x y pd pd'. \<lbrakk>ty = ArchObject PageDirectoryObj; kheap s x = Some (ArchObj (PageDirectory pd)) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> x \<notin> set (retype_addrs ptr (ArchObject PageDirectoryObj) n us) \<longrightarrow> y \<notin> set (retype_addrs ptr (ArchObject PageDirectoryObj) n us) \<longrightarrow> kheap s' x = Some (ArchObj (PageDirectory pd)) \<and> kheap s' y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)
 2. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); ty \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>x y pd pd'. ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); ty \<noteq> ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> \<forall>x y pd pd'. ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd'. \<lbrakk>ty \<noteq> ArchObject PageDirectoryObj; ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> ako_at (PageDirectory pd) x s' \<and> ako_at (PageDirectory pd') y s' \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd'. \<lbrakk>ty \<noteq> ArchObject PageDirectoryObj; kheap s x = Some (ArchObj (PageDirectory pd)) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> kheap s' x = Some (ArchObj (PageDirectory pd)) \<and> kheap s' y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w) proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd'. \<lbrakk>ty \<noteq> ArchObject PageDirectoryObj; kheap s x = Some (ArchObj (PageDirectory pd)) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrakk> \<Longrightarrow> (x \<in> set (retype_addrs ptr ty n us) \<longrightarrow> (y \<in> set (retype_addrs ptr ty n us) \<longrightarrow> default_object ty dev us = ArchObj (PageDirectory pd) \<and> default_object ty dev us = ArchObj (PageDirectory pd') \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)) \<and> (y \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> default_object ty dev us = ArchObj (PageDirectory pd) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w))) \<and> (x \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> y \<in> set (retype_addrs ptr ty n us) \<longrightarrow> kheap s x = Some (ArchObj (PageDirectory pd)) \<and> default_object ty dev us = ArchObj (PageDirectory pd') \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)) proof (prove)
goal:
No subgoals!