theory ArchInvariants_AI

lemma stronger_vspace_objsD:
  "\<lbrakk> (ref \<rhd> p) s;
     valid_vspace_objs s;
     valid_asid_table (arm_asid_table (arch_state s)) s \<rbrakk> \<Longrightarrow>
  \<exists>ao. ko_at (ArchObj ao) p s \<and>
       valid_vspace_obj ao s" apply (clarsimp simp: vs_lookup_def vs_asid_refs_def graph_of_def) apply (clarsimp simp: valid_asid_table_def) apply (drule bspec, fastforce simp: ran_def) apply (drule rtranclD) apply (erule disjE) prefer 2 apply clarsimp apply (drule stronger_vspace_objsD_lemma) apply (erule vs_lookup_atI) apply assumption apply clarsimp apply clarsimp apply (simp add: valid_vspace_objs_def) apply (erule_tac x=p in allE) apply (erule impE) apply (rule exI) apply (erule vs_lookup_atI) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; valid_vspace_objs s; valid_asid_table (asid_table s) s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; valid_asid_table (asid_table s) s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba; \<forall>p\<in>ran (asid_table s). typ_at (AArch AASIDPool) p s; inj_on (asid_table s) (dom (asid_table s))\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>*; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p) \<or> ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> (ref, p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 2. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> (ref, p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) \<noteq> (ref, p) \<and> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 2. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 2. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (4 subgoals):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> ?r31 aa ba \<in> vs_lookup s
 2. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (?r31 aa ba, ?r'31 aa ba) \<in> (vs_lookup1 s)\<^sup>+
 3. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; \<exists>ao. ako_at ao (snd (?r'31 aa ba)) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 4. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (3 subgoals):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+\<rbrakk> \<Longrightarrow> (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ?r'31 aa ba) \<in> (vs_lookup1 s)\<^sup>+
 2. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; \<exists>ao. ako_at ao (snd (?r'31 aa ba)) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 3. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; [VSRef (UCAST(7 \<rightarrow> 32) aa) None] = ref \<longrightarrow> ba \<noteq> p; (([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba), ref, p) \<in> (vs_lookup1 s)\<^sup>+; \<exists>ao. ako_at ao (snd (ref, p)) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s
 2. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some ba; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) ba s; ([VSRef (UCAST(7 \<rightarrow> 32) aa) None], ba) = (ref, p)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>valid_vspace_objs s; asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]; (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> p) s
 2. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]; \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]\<rbrakk> \<Longrightarrow> (?rs43 aa \<rhd> p) s
 2. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]; \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>asid_table s aa = Some p; inj_on (asid_table s) (dom (asid_table s)); typ_at (AArch AASIDPool) p s; ref = [VSRef (UCAST(7 \<rightarrow> 32) aa) None]; \<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s proof (prove)
goal:
No subgoals!