theory CSpace1_R

lemma getSlotCap_valid:
  "\<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace>
  getSlotCap p \<lbrace>Q\<rbrace>" apply (rule use_spec) apply (simp add: spec_valid_def) apply (rule hoare_add_post[OF getSlotCap_valid_cap1]) apply clarsimp apply (rule hoare_add_post[OF getSlotCap_valid_cap2]) apply clarsimp apply (rule hoare_add_post) apply (rule_tac P="\<lambda>x. x = s" in getSlotCap_inv) apply (clarsimp) apply (clarsimp simp add: valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace> getSlotCap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> \<lbrace>\<lambda>s. valid_objs' s \<and> (cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<forall>cap. valid_cap' cap s \<longrightarrow> Q cap s))\<rbrace> getSlotCap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa)) \<Longrightarrow> valid_objs' sa
 2. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv s. valid_cap' rv s \<longrightarrow> Q rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv s. valid_cap' rv s \<longrightarrow> Q rv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa)) \<Longrightarrow> valid_objs' sa
 2. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> valid_cap' rv s \<longrightarrow> Q rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> valid_cap' rv s \<longrightarrow> Q rv s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrace>?P'10 s\<rbrace> getSlotCap p \<lbrace>?Q'10 s\<rbrace>
 2. \<And>s sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa)) \<Longrightarrow> ?P'10 s sa
 3. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv sa. ?Q'10 s rv sa \<longrightarrow> cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> valid_cap' rv sa \<longrightarrow> Q rv sa\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa)) \<Longrightarrow> sa = s
 2. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv sa. sa = s \<longrightarrow> cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> valid_cap' rv sa \<longrightarrow> Q rv sa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>sa. sa = s \<and> valid_objs' sa \<and> (cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> (\<forall>cap. valid_cap' cap sa \<longrightarrow> Q cap sa))\<rbrace> getSlotCap p \<lbrace>\<lambda>rv sa. sa = s \<longrightarrow> cte_wp_at' (\<lambda>_. True) p sa \<longrightarrow> valid_cap' rv sa \<longrightarrow> Q rv sa\<rbrace> proof (prove)
goal:
No subgoals!