theory ArchKHeap_AI

lemma vs_lookup_vspace_obj_at_lift:
  assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow>
                             \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>"
  assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace>" apply (simp add: vs_lookup_def vs_lookup1_def) apply (simp add: ex_ko_at_def2) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state]) apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P']) apply (rule hoare_vcg_prop) apply (clarsimp simp add: valid_def) apply (erule_tac P=P in rsubst) apply (rule ext)+ apply (erule use_valid, rule obj_at, simp) by (auto simp: vs_refs.vspace_only
           intro!: vspace_obj_pred_fI[where f=Ex])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ({((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs (asid_table s))\<rbrace> f \<lbrace>\<lambda>rv s. P ({((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs (asid_table s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ({((rs, p), rs', p'). obj_at (\<lambda>ko. \<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko) p s}\<^sup>* `` vs_asid_refs (asid_table s))\<rbrace> f \<lbrace>\<lambda>rv s. P ({((rs, p), rs', p'). obj_at (\<lambda>ko. \<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko) p s}\<^sup>* `` vs_asid_refs (asid_table s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. P ({a. case a of (a, b) \<Rightarrow> (case a of (rs, p) \<Rightarrow> \<lambda>a. case a of (rs', p') \<Rightarrow> obj_at (\<lambda>ko. \<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko) p s) b}\<^sup>* `` vs_asid_refs (arm_asid_table x))\<rbrace> f \<lbrace>\<lambda>_ a. P ({aa. case aa of (aa, b) \<Rightarrow> (case aa of (rs, p) \<Rightarrow> \<lambda>aa. case aa of (rs', p') \<Rightarrow> obj_at (\<lambda>ko. \<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko) p a) b}\<^sup>* `` vs_asid_refs (arm_asid_table x))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. P ({a. case a of (a, b) \<Rightarrow> (case a of (rs, p) \<Rightarrow> \<lambda>a. case a of (rs', p') \<Rightarrow> xa rs' p rs p') b}\<^sup>* `` vs_asid_refs (arm_asid_table x))\<rbrace> f \<lbrace>\<lambda>_ a. P ({a. case a of (a, b) \<Rightarrow> (case a of (rs, p) \<Rightarrow> \<lambda>a. case a of (rs', p') \<Rightarrow> xa rs' p rs p') b}\<^sup>* `` vs_asid_refs (arm_asid_table x))\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x P. \<lbrace>\<lambda>s. P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s a b. \<lbrakk>P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s); (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> P (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p b) proof (prove)
goal (1 subgoal):
 1. \<And>P s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s) = (\<lambda>rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p b) proof (prove)
goal (1 subgoal):
 1. \<And>P s a b rs p rs' p'. (a, b) \<in> fst (f s) \<Longrightarrow> obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s = obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p b proof (prove)
goal (2 subgoals):
 1. \<And>rs rs' p'. vspace_obj_pred (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a)
 2. \<And>P s a b rs p rs' p'. obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s = obj_at (\<lambda>a. \<exists>r. rs = r # rs' \<and> (r, p') \<in> vs_refs a) p s