kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma not_final_not_zombieD:
  "\<lbrakk> \<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)};
     zombies_final s \<rbrakk> \<Longrightarrow> \<not> is_zombie cap" apply (rule notI) apply (erule(2) zombies_finalE) apply (simp add: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; zombies_final s\<rbrakk> \<Longrightarrow> \<not> is_zombie cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_final_cap' cap s; fst (get_cap p s) = {(cap, s)}; zombies_final s; is_zombie cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap, s)}; zombies_final s; is_zombie cap\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) ?p2 s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma appropriate_cte_cap_irqs:
  "(\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap')
       = ((cap_irqs cap = {}) = (cap_irqs cap' = {}))" apply (rule iffI) apply (drule_tac x="cap.IRQControlCap" in spec) apply (clarsimp simp add: appropriate_cte_cap_def) apply (simp add: appropriate_cte_cap_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap') = ((cap_irqs cap = {}) = (cap_irqs cap' = {})) proof (prove)
goal (2 subgoals):
 1. \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap' \<Longrightarrow> (cap_irqs cap = {}) = (cap_irqs cap' = {})
 2. (cap_irqs cap = {}) = (cap_irqs cap' = {}) \<Longrightarrow> \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap' proof (prove)
goal (2 subgoals):
 1. appropriate_cte_cap IRQControlCap cap = appropriate_cte_cap IRQControlCap cap' \<Longrightarrow> (cap_irqs cap = {}) = (cap_irqs cap' = {})
 2. (cap_irqs cap = {}) = (cap_irqs cap' = {}) \<Longrightarrow> \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap' proof (prove)
goal (1 subgoal):
 1. (cap_irqs cap = {}) = (cap_irqs cap' = {}) \<Longrightarrow> \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp cap' proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma cte_wp_at_conj:
  "cte_wp_at (\<lambda>c. P c \<and> Q c) p s = (cte_wp_at P p s \<and> cte_wp_at Q p s)" by (fastforce simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. P c \<and> Q c) p s = (cte_wp_at P p s \<and> cte_wp_at Q p s)
theory CSpaceInv_AI

lemma cte_wp_at_disj:
  "cte_wp_at (\<lambda>c. P c \<or> Q c) p s = (cte_wp_at P p s \<or> cte_wp_at Q p s)" by (fastforce simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. P c \<or> Q c) p s = (cte_wp_at P p s \<or> cte_wp_at Q p s)
theory CSpaceInv_AI

lemma gen_obj_refs_Null[simp]:
  "gen_obj_refs cap.NullCap = {}" by (simp add: gen_obj_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gen_obj_refs NullCap = {}
theory CSpaceInv_AI

lemma delete_duplicate_valid_pspace:
  "\<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and>
        tcb_cap_valid cap.NullCap p s\<rbrace>
  set_cap cap.NullCap p
  \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply (simp add: valid_pspace_def) apply (wp set_cap_valid_objs delete_duplicate_iflive delete_duplicate_ifunsafe
            set_cap_zombies, auto elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace s \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> tcb_cap_valid NullCap p s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s \<and> tcb_cap_valid NullCap p s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s))\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_object_idle [wp]:
  "\<lbrace>\<lambda>s. valid_idle s \<and>
     (\<forall>t t'. ko_at (TCB t) p s
             \<and> ko = (TCB t')
             \<and> idle (tcb_state t)
             \<and> tcb_bound_notification t = None
             \<and> valid_arch_idle (tcb_iarch t)
             \<longrightarrow> idle (tcb_state t')
                 \<and> tcb_bound_notification t' = None
                 \<and> valid_arch_idle (tcb_iarch t'))\<rbrace>
     set_object p ko
   \<lbrace>\<lambda>rv. valid_idle\<rbrace>" by (wpsimp wp: set_object_wp_strong simp: obj_at_def valid_idle_def pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle s \<and> (\<forall>t t'. ko_at (TCB t) p s \<and> ko = TCB t' \<and> idle (tcb_state t) \<and> tcb_bound_notification t = None \<and> valid_arch_idle (tcb_iarch t) \<longrightarrow> idle (tcb_state t') \<and> tcb_bound_notification t' = None \<and> valid_arch_idle (tcb_iarch t'))\<rbrace> set_object p ko \<lbrace>\<lambda>rv. valid_idle\<rbrace>
theory CSpaceInv_AI

lemma set_cap_cte_at_neg[wp]:
  "\<lbrace>\<lambda>s. \<not> cte_at sl s\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<not> cte_at sl s\<rbrace>" apply (simp add: cte_at_typ) apply (wp set_cap_typ_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at (\<lambda>_. True) sl s\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<not> cte_wp_at (\<lambda>_. True) sl s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> typ_at (ACapTable (length (snd sl))) (fst sl) s \<and> (typ_at ATCB (fst sl) s \<longrightarrow> snd sl \<notin> dom tcb_cap_cases)\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<not> typ_at (ACapTable (length (snd sl))) (fst sl) s \<and> (typ_at ATCB (fst sl) s \<longrightarrow> snd sl \<notin> dom tcb_cap_cases)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_cte_wp_at_neg:
  "\<lbrace>\<lambda>s. cte_at sl' s \<and> (if sl = sl' then \<not> P cap else \<not> cte_wp_at P sl s)\<rbrace>
     set_cap cap sl'
   \<lbrace>\<lambda>rv s. \<not> cte_wp_at P sl s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>_. True) sl' s \<and> (if sl = sl' then \<not> P cap else \<not> cte_wp_at P sl s)\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<not> cte_wp_at P sl s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (sl = sl' \<longrightarrow> (\<exists>cap. caps_of_state s sl' = Some cap) \<and> \<not> P cap) \<and> (sl \<noteq> sl' \<longrightarrow> (\<exists>cap. caps_of_state s sl' = Some cap) \<and> (\<forall>cap. caps_of_state s sl = Some cap \<longrightarrow> \<not> P cap))\<rbrace> set_cap cap sl' \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s sl = Some cap \<longrightarrow> \<not> P cap\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_reply_masters [wp]:
  "\<lbrace>valid_reply_masters and cte_at ptr and
       (\<lambda>s. \<forall>x. (\<exists> rights. cap = cap.ReplyCap x True rights) \<longrightarrow>
                fst ptr = x \<and> snd ptr = tcb_cnode_index 2) \<rbrace>
   set_cap cap ptr \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" apply (simp add: valid_reply_masters_def cte_wp_at_caps_of_state is_master_reply_cap_to_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and cte_wp_at (\<lambda>_. True) ptr and (\<lambda>s. \<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst ptr = x \<and> snd ptr = tcb_cnode_index 2)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and cte_wp_at (\<lambda>_. True) ptr and (\<lambda>s. \<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst ptr = x \<and> snd ptr = tcb_cnode_index 2)\<rbrace> set_cap cap ptr \<lbrace>\<lambda>_ s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>a b t. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2) and cte_wp_at (\<lambda>_. True) ptr and (\<lambda>s. \<forall>x. (\<exists>rights. cap = ReplyCap x True rights) \<longrightarrow> fst ptr = x \<and> snd ptr = tcb_cnode_index 2)) s \<Longrightarrow> \<forall>a b t. (\<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) (a, b) = Some capa \<and> (\<exists>rights. capa = ReplyCap t True rights)) \<longrightarrow> a = t \<and> b = tcb_cnode_index 2 proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_irq_handlers:
 "\<lbrace>\<lambda>s. valid_irq_handlers s
      \<and> cte_wp_at (\<lambda>cap'. \<forall>irq \<in> cap_irqs cap - cap_irqs cap'. irq_issued irq s) ptr s\<rbrace>
    set_cap cap ptr
  \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: valid_irq_handlers_def irq_issued_def Ball_def) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply (clarsimp simp: cte_wp_at_caps_of_state elim!: ranE split: if_split_asm) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers s \<and> cte_wp_at (\<lambda>cap'. \<forall>irq\<in>cap_irqs cap - cap_irqs cap'. irq_issued irq s) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal)) \<and> cte_wp_at (\<lambda>cap'. \<forall>x. x \<in> cap_irqs cap \<and> x \<notin> cap_irqs cap' \<longrightarrow> interrupt_states s x = IRQSignal) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal)) \<and> cte_wp_at (\<lambda>cap'. \<forall>x. x \<in> cap_irqs cap \<and> x \<notin> cap_irqs cap' \<longrightarrow> interrupt_states s x = IRQSignal) ptr s \<Longrightarrow> \<forall>x. x \<notin> ran ((caps_of_state s)(ptr \<mapsto> cap)) \<or> (\<forall>xa. xa \<notin> cap_irqs x \<or> interrupt_states s xa = IRQSignal) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b xa. \<lbrakk>xa \<in> cap_irqs cap; \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal); caps_of_state s (a, b) = Some capa; \<forall>x. x \<in> cap_irqs cap \<and> x \<notin> cap_irqs capa \<longrightarrow> interrupt_states s x = IRQSignal; ptr = (a, b)\<rbrakk> \<Longrightarrow> interrupt_states s xa = IRQSignal
 2. \<And>s x capa a b xa. \<lbrakk>xa \<in> cap_irqs x; \<forall>x. x \<in> ran (caps_of_state s) \<longrightarrow> (\<forall>xa. xa \<in> cap_irqs x \<longrightarrow> interrupt_states s xa = IRQSignal); caps_of_state s ptr = Some capa; \<forall>x. x \<in> cap_irqs cap \<and> x \<notin> cap_irqs capa \<longrightarrow> interrupt_states s x = IRQSignal; (a, b) \<noteq> ptr; caps_of_state s (a, b) = Some x\<rbrakk> \<Longrightarrow> interrupt_states s xa = IRQSignal proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma arch_obj_caps_of:
  "caps_of (ArchObj ko) = {}" by (simp add: caps_of_def cap_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of (ArchObj ko) = {}
theory CSpaceInv_AI

lemma get_cap_wp:
  "\<lbrace>\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> Q cap s\<rbrace> get_cap p \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def cte_wp_at_def) apply (frule in_inv_by_hoareD [OF get_cap_inv]) apply (drule get_cap_det) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap. cte_wp_at ((=) cap) p s \<longrightarrow> Q cap s\<rbrace> get_cap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cap. fst (get_cap p s) = {(cap, s)} \<longrightarrow> Q cap s; (a, b) \<in> fst (get_cap p s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cap. fst (get_cap p s) = {(cap, s)} \<longrightarrow> Q cap s; (a, b) \<in> fst (get_cap p s); b = s\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>cap. fst (get_cap p s) = {(cap, s)} \<longrightarrow> Q cap s; b = s; get_cap p s = ({(a, s)}, False)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma cap_irqs_must_be_irqhandler: "irq \<in> cap_irqs cap \<Longrightarrow> cap = IRQHandlerCap irq" by (simp add: cap_irqs_def cap_irq_opt_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq \<in> cap_irqs cap \<Longrightarrow> cap = IRQHandlerCap irq
theory CSpaceInv_AI

lemma final_cap_duplicate:
  "\<lbrakk> fst (get_cap p s) = {(cap', s)};
     fst (get_cap p' s) = {(cap'', s)};
     p \<noteq> p'; is_final_cap' cap s; r \<in> gen_obj_refs cap;
     r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap'' \<rbrakk>
     \<Longrightarrow> P" apply (clarsimp simp add: is_final_cap'_def
                            gen_obj_refs_Int_not) apply (erule(1) obvious) apply simp apply blast apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; is_final_cap' cap s; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''; {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} = {(a, b)}\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> p \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}}
 2. \<And>a b. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}
 2. \<And>a b. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> p' \<in> {cref. \<exists>cap'. fst (get_cap cref s) = {(cap', s)} \<and> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {}} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (get_cap p s) = {(cap', s)}; fst (get_cap p' s) = {(cap'', s)}; p \<noteq> p'; r \<in> gen_obj_refs cap; r \<in> gen_obj_refs cap'; r \<in> gen_obj_refs cap''\<rbrakk> \<Longrightarrow> gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {} proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gen_obj_refs_subset:
  "(gen_obj_refs cap \<subseteq> gen_obj_refs cap')
       = (obj_refs cap \<subseteq> obj_refs cap'
             \<and> cap_irqs cap \<subseteq> cap_irqs cap'
             \<and> arch_gen_refs cap \<subseteq> arch_gen_refs cap')" apply (simp add: gen_obj_refs_def) apply (subgoal_tac "\<forall>x y. Inl x \<noteq> Inr y") apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (gen_obj_refs cap \<subseteq> gen_obj_refs cap') = (obj_refs cap \<subseteq> obj_refs cap' \<and> cap_irqs cap \<subseteq> cap_irqs cap' \<and> arch_gen_refs cap \<subseteq> arch_gen_refs cap') proof (prove)
goal (1 subgoal):
 1. (ObjRef ` obj_refs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap' \<and> IRQRef ` cap_irqs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap' \<and> ArchRef ` arch_gen_refs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') = (obj_refs cap \<subseteq> obj_refs cap' \<and> cap_irqs cap \<subseteq> cap_irqs cap' \<and> arch_gen_refs cap \<subseteq> arch_gen_refs cap') proof (prove)
goal (2 subgoals):
 1. \<forall>x y. Inl x \<noteq> Inr y \<Longrightarrow> (ObjRef ` obj_refs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap' \<and> IRQRef ` cap_irqs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap' \<and> ArchRef ` arch_gen_refs cap \<subseteq> ObjRef ` obj_refs cap' \<union> IRQRef ` cap_irqs cap' \<union> ArchRef ` arch_gen_refs cap') = (obj_refs cap \<subseteq> obj_refs cap' \<and> cap_irqs cap \<subseteq> cap_irqs cap' \<and> arch_gen_refs cap \<subseteq> arch_gen_refs cap')
 2. \<forall>x y. Inl x \<noteq> Inr y proof (prove)
goal (1 subgoal):
 1. \<forall>x y. Inl x \<noteq> Inr y proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_cap_caps_of_state2:
  "\<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s)\<rbrace>
  set_cap cap p
  \<lbrace>\<lambda>rv s. P (caps_of_state s) (cdt s) (is_original_cap s)\<rbrace>" apply (rule_tac Q="\<lambda>rv s. \<exists>m mr. P (caps_of_state s) m mr
                                  \<and> (cdt s = m) \<and> (is_original_cap s = mr)"
           in hoare_post_imp) apply simp apply (wp hoare_vcg_ex_lift) apply (rule_tac x="cdt s" in exI) apply (rule_tac x="is_original_cap s" in exI) apply (simp add: fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. P (caps_of_state s) (cdt s) (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<exists>m mr. P (caps_of_state s) m mr \<and> cdt s = m \<and> is_original_cap s = mr \<Longrightarrow> P (caps_of_state s) (cdt s) (is_original_cap s)
 2. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>m mr. P (caps_of_state s) m mr \<and> cdt s = m \<and> is_original_cap s = mr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<exists>m mr. P (caps_of_state s) m mr \<and> cdt s = m \<and> is_original_cap s = mr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s) \<Longrightarrow> \<exists>x xa. P ((caps_of_state s)(p \<mapsto> cap)) x xa \<and> cdt s = x \<and> is_original_cap s = xa proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s) \<Longrightarrow> \<exists>x. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) x \<and> cdt s = cdt s \<and> is_original_cap s = x proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s) \<Longrightarrow> P ((caps_of_state s)(p \<mapsto> cap)) (cdt s) (is_original_cap s) \<and> cdt s = cdt s \<and> is_original_cap s = is_original_cap s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gen_obj_refs_empty:
  "(gen_obj_refs cap = {}) =
         (cap_irqs cap = {} \<and> obj_refs cap = {}
            \<and> arch_gen_refs cap = {})" by (simp add: gen_obj_refs_def conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (gen_obj_refs cap = {}) = (cap_irqs cap = {} \<and> obj_refs cap = {} \<and> arch_gen_refs cap = {})
theory CSpaceInv_AI

lemma final_NullCap:
  "is_final_cap' NullCap = \<bottom>" by (rule ext, simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' NullCap = (\<lambda>_. False)
theory CSpaceInv_AI

lemma set_cap_only_idle [wp]:
  "set_cap cap p \<lbrace>only_idle\<rbrace>" by (wp only_idle_lift set_cap_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_cap cap p \<lbrace>\<lambda>_. only_idle\<rbrace>