theory ArchRetype_AI

lemma valid_vspace_objs':
  assumes va: "valid_vspace_objs s"
  shows "valid_vspace_objs s'" proof fix p ao assume p: "(\<exists>\<rhd> p) s'" assume "ko_at (ArchObj ao) p s'" hence "ko_at (ArchObj ao) p s \<or> ArchObj ao = default_object ty dev us" by (simp add: ps_def obj_at_def s'_def split: if_split_asm) moreover { assume "ArchObj ao = default_object ty dev us" with tyunt have "valid_vspace_obj ao s'" by (rule valid_vspace_obj_default) } moreover { assume "ko_at (ArchObj ao) p s" with va p have "valid_vspace_obj ao s" by (auto simp: vs_lookup' elim: valid_vspace_objsD) hence "valid_vspace_obj ao s'" by (rule valid_vspace_obj_pres) } ultimately show "valid_vspace_obj ao s'" by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s' proof (state)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
\<exists>ref. (ref \<rhd> p) s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ako_at ao p s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
using this:
ako_at ao p s'

goal (1 subgoal):
 1. ako_at ao p s \<or> ArchObj ao = default_object ty dev us proof (state)
this:
ako_at ao p s \<or> ArchObj ao = default_object ty dev us

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ako_at ao p s \<or> ArchObj ao = default_object ty dev us

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ako_at ao p s \<or> ArchObj ao = default_object ty dev us

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ArchObj ao = default_object ty dev us

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (chain)
picking this:
ty \<noteq> Untyped
ArchObj ao = default_object ty dev us proof (prove)
using this:
ty \<noteq> Untyped
ArchObj ao = default_object ty dev us

goal (1 subgoal):
 1. valid_vspace_obj ao s' proof (state)
this:
valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ako_at ao p s

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (chain)
picking this:
valid_vspace_objs s
\<exists>ref. (ref \<rhd> p) s'
ako_at ao p s proof (prove)
using this:
valid_vspace_objs s
\<exists>ref. (ref \<rhd> p) s'
ako_at ao p s

goal (1 subgoal):
 1. valid_vspace_obj ao s proof (state)
this:
valid_vspace_obj ao s

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
using this:
valid_vspace_obj ao s

goal (1 subgoal):
 1. valid_vspace_obj ao s' proof (state)
this:
valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (state)
this:
ako_at ao p s \<Longrightarrow> valid_vspace_obj ao s'

goal (1 subgoal):
 1. \<And>p ao. \<lbrakk>\<exists>ref. (ref \<rhd> p) s'; ako_at ao p s'\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s' proof (chain)
picking this:
ako_at ao p s \<or> ArchObj ao = default_object ty dev us
ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'
ako_at ao p s \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
using this:
ako_at ao p s \<or> ArchObj ao = default_object ty dev us
ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'
ako_at ao p s \<Longrightarrow> valid_vspace_obj ao s'

goal (1 subgoal):
 1. valid_vspace_obj ao s' proof (state)
this:
valid_vspace_obj ao s'

goal:
No subgoals!