theory ArchInvariants_AI

lemma stronger_vspace_objsD_lemma:
  "\<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r,r') \<in> (vs_lookup1 s)\<^sup>+ \<rbrakk>
  \<Longrightarrow> \<exists>ao. ko_at (ArchObj ao) (snd r') s \<and>
          valid_vspace_obj ao s" apply (erule trancl_induct) apply (frule vs_lookup1_is_arch) apply (cases r) apply clarsimp apply (frule (2) valid_vspace_objsD) apply (drule (1) vs_lookup_step) apply (drule (2) vs_lookup1_ko_at_dest) apply clarsimp apply (drule (2) valid_vspace_objsD) apply (fastforce simp: valid_vspace_obj_def) apply clarsimp apply (frule (2) vs_lookup1_ko_at_dest) apply (drule (1) vs_lookup_trancl_step) apply (drule (1) vs_lookup_step) apply clarsimp apply (drule (2) valid_vspace_objsD) apply (fastforce simp: valid_vspace_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, r') \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd r') s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> vs_lookup1 s; \<exists>ao'. ako_at ao' (snd r) s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>y a b. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> vs_lookup1 s; \<exists>ao'. ako_at ao' (snd r) s; r = (a, b)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao'. \<lbrakk>valid_vspace_objs s; (aa \<rhd> ba) s; ((aa, ba), a, b) \<in> vs_lookup1 s; r = (aa, ba); ako_at ao' ba s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao'. \<lbrakk>valid_vspace_objs s; (aa \<rhd> ba) s; ((aa, ba), a, b) \<in> vs_lookup1 s; r = (aa, ba); ako_at ao' ba s; valid_vspace_obj ao' s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao'. \<lbrakk>valid_vspace_objs s; ((aa, ba), a, b) \<in> vs_lookup1 s; r = (aa, ba); ako_at ao' ba s; valid_vspace_obj ao' s; (a \<rhd> b) s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao'. \<lbrakk>valid_vspace_objs s; r = (aa, ba); ako_at ao' ba s; valid_vspace_obj ao' s; (a \<rhd> b) s; \<exists>ao'a. ako_at ao'a b s \<and> (\<exists>tp. vs_ref_aatype (hd a) = Some tp \<and> aa_type ao' = tp)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao' ao'a. \<lbrakk>valid_vspace_objs s; r = (aa, ba); ako_at ao' ba s; valid_vspace_obj ao' s; (a \<rhd> b) s; vs_ref_aatype (hd a) = Some (aa_type ao'); ako_at ao'a b s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ao' ao'a. \<lbrakk>valid_vspace_objs s; r = (aa, ba); ako_at ao' ba s; valid_vspace_obj ao' s; vs_ref_aatype (hd a) = Some (aa_type ao'); ako_at ao'a b s; valid_vspace_obj ao'a s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao b s \<and> valid_vspace_obj ao s
 2. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, y) \<in> (vs_lookup1 s)\<^sup>+; (y, z) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (snd y) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao (snd z) s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao. \<lbrakk>valid_vspace_objs s; r \<in> vs_lookup s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s; \<exists>ao'. ako_at ao' ba s \<and> (\<exists>tp. vs_ref_aatype (hd aa) = Some tp \<and> aa_type ao = tp)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao. \<lbrakk>valid_vspace_objs s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s; \<exists>ao'. ako_at ao' ba s \<and> (\<exists>tp. vs_ref_aatype (hd aa) = Some tp \<and> aa_type ao = tp); (a \<rhd> b) s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao. \<lbrakk>valid_vspace_objs s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s; \<exists>ao'. ako_at ao' ba s \<and> (\<exists>tp. vs_ref_aatype (hd aa) = Some tp \<and> aa_type ao = tp); (aa \<rhd> ba) s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao ao'. \<lbrakk>valid_vspace_objs s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s; (aa \<rhd> ba) s; vs_ref_aatype (hd aa) = Some (aa_type ao); ako_at ao' ba s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ao ao'. \<lbrakk>valid_vspace_objs s; (r, a, b) \<in> (vs_lookup1 s)\<^sup>+; ((a, b), aa, ba) \<in> vs_lookup1 s; ako_at ao b s; valid_vspace_obj ao s; vs_ref_aatype (hd aa) = Some (aa_type ao); ako_at ao' ba s; valid_vspace_obj ao' s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao ba s \<and> valid_vspace_obj ao s proof (prove)
goal:
No subgoals!