theory Untyped_AI

lemma create_cap_valid_global_refs[wp]:
  "\<lbrace>valid_global_refs
      and cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace>
     create_cap tp sz p dev (cref, oref)
   \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>" apply (simp add: valid_global_refs_def valid_refs_def
                   cte_wp_at_caps_of_state create_cap_def pred_conj_def) apply (simp only: imp_conv_disj) apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_disj_lift) apply (subgoal_tac "global_refs s \<inter> cap_range (default_cap tp oref sz dev) = {}") apply auto[1] apply (erule disjoint_subset2) apply (cases p, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>a b cap. caps_of_state x (a, b) = Some cap \<longrightarrow> global_refs x \<inter> cap_range cap = {}) \<and> (\<exists>cap. caps_of_state x p = Some cap \<and> cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>a b cap. caps_of_state x (a, b) \<noteq> Some cap \<or> global_refs x \<inter> cap_range cap = {}) \<and> (\<exists>cap. caps_of_state x p = Some cap \<and> cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap)\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv s. \<forall>a b cap. caps_of_state s (a, b) \<noteq> Some cap \<or> global_refs s \<inter> cap_range cap = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s p = Some cap; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap; global_refs s \<inter> cap_range xb \<noteq> {}\<rbrakk> \<Longrightarrow> ((x, xa) = cref \<longrightarrow> default_cap tp oref sz dev \<noteq> xb) \<and> ((x, xa) \<noteq> cref \<longrightarrow> caps_of_state s (x, xa) \<noteq> Some xb) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s p = Some cap; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap; global_refs s \<inter> cap_range xb \<noteq> {}; global_refs s \<inter> cap_range (default_cap tp oref sz dev) = {}\<rbrakk> \<Longrightarrow> ((x, xa) = cref \<longrightarrow> default_cap tp oref sz dev \<noteq> xb) \<and> ((x, xa) \<noteq> cref \<longrightarrow> caps_of_state s (x, xa) \<noteq> Some xb)
 2. \<And>s x xa xb cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s p = Some cap; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap; global_refs s \<inter> cap_range xb \<noteq> {}\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (default_cap tp oref sz dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s p = Some cap; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap; global_refs s \<inter> cap_range xb \<noteq> {}\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range (default_cap tp oref sz dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb cap. \<lbrakk>\<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> global_refs s \<inter> cap_range cap = {}; caps_of_state s p = Some cap; global_refs s \<inter> cap_range xb \<noteq> {}\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range cap = {} proof (prove)
goal:
No subgoals!