theory VSpace_R

lemma find_pd_for_asid_pd_at_asid_again:
  "\<lbrace>\<lambda>s. (\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s)
       \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s)
       \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0\<rbrace>
      find_pd_for_asid asid
   \<lbrace>P\<rbrace>,\<lbrace>Q\<rbrace>" apply (unfold validE_def, rule hoare_name_pre_state, fold validE_def) apply (case_tac "\<exists>pd. vspace_at_asid asid pd s") apply clarsimp apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> rv = pd" and E="\<bottom>\<bottom>" in hoare_post_impErr) apply (rule hoare_pre, wp find_pd_for_asid_valids) apply fastforce apply simp+ apply (rule_tac Q="\<lambda>rv s'. s' = s \<and> vspace_at_asid asid rv s'"
              and E="\<lambda>rv s'. s' = s" in hoare_post_impErr) apply (rule hoare_pre, wp) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0 \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<exists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<nexists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<nexists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s pd. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s'. s' = s \<and> rv = pd\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
 2. \<And>s pd rv sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; sa = s \<and> rv = pd\<rbrakk> \<Longrightarrow> P rv sa
 3. \<And>s pd e sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; False\<rbrakk> \<Longrightarrow> Q e sa
 4. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<nexists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s pd sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; s = sa\<rbrakk> \<Longrightarrow> (vspace_at_asid asid (?pd17 s pd) and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) sa \<and> sa = s \<and> (vspace_at_asid asid (?pd20 s pd) and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned (?pd20 s pd) pdBits \<longrightarrow> ?pd20 s pd = pd)) sa
 2. \<And>s pd rv sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; sa = s \<and> rv = pd\<rbrakk> \<Longrightarrow> P rv sa
 3. \<And>s pd e sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; False\<rbrakk> \<Longrightarrow> Q e sa
 4. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<nexists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s pd rv sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; sa = s \<and> rv = pd\<rbrakk> \<Longrightarrow> P rv sa
 2. \<And>s pd e sa. \<lbrakk>vspace_at_asid asid pd s; \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s; (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> (\<forall>ex. Q ex s); valid_vspace_objs s; pspace_aligned s; asid \<noteq> 0; False\<rbrakk> \<Longrightarrow> Q e sa
 3. \<And>s. \<lbrakk>(\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> P pd s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid asid pd s) \<longrightarrow> Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<nexists>pd. vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>P\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s'. s' = s \<and> vspace_at_asid asid rv s'\<rbrace>, \<lbrace>\<lambda>rv s'. s' = s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s; sa = s \<and> vspace_at_asid asid rv sa\<rbrakk> \<Longrightarrow> P rv sa
 3. \<And>s e sa. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s; sa = s\<rbrakk> \<Longrightarrow> Q e sa proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s; s = sa\<rbrakk> \<Longrightarrow> sa = s \<and> sa = s \<and> True
 2. \<And>s rv sa. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s; sa = s \<and> vspace_at_asid asid rv sa\<rbrakk> \<Longrightarrow> P rv sa
 3. \<And>s e sa. \<lbrakk>(\<forall>ex. Q ex s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0; \<forall>pd. \<not> vspace_at_asid asid pd s; sa = s\<rbrakk> \<Longrightarrow> Q e sa proof (prove)
goal:
No subgoals!