kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma if_live_then_nonz_capD:
  assumes x: "if_live_then_nonz_cap s" "obj_at P p s"
  assumes y: "\<And>obj. \<lbrakk> P obj; kheap s p = Some obj \<rbrakk> \<Longrightarrow> live obj"
  shows "ex_nonz_cap_to p s" using x apply (clarsimp simp: if_live_then_nonz_cap_def) apply (erule allE[where x=p]) apply (fastforce simp: obj_at_def dest!: y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to p s proof (prove)
using this:
if_live_then_nonz_cap s
obj_at P p s

goal (1 subgoal):
 1. ex_nonz_cap_to p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr. obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s; obj_at P p s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; obj_at live p s \<longrightarrow> ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma if_live_then_nonz_capD2:
  "\<lbrakk> if_live_then_nonz_cap s; kheap s p = Some obj;
     live obj \<rbrakk> \<Longrightarrow> ex_nonz_cap_to p s" apply (subgoal_tac "ko_at obj p s") apply (erule(1) if_live_then_nonz_capD) apply simp apply (simp add: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap s; kheap s p = Some obj; live obj\<rbrakk> \<Longrightarrow> ex_nonz_cap_to p s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>if_live_then_nonz_cap s; kheap s p = Some obj; live obj; ko_at obj p s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to p s
 2. \<lbrakk>if_live_then_nonz_cap s; kheap s p = Some obj; live obj\<rbrakk> \<Longrightarrow> ko_at obj p s proof (prove)
goal (2 subgoals):
 1. \<And>obja. \<lbrakk>kheap s p = Some obj; live obj; ko_at obj p s; obj = obja; kheap s p = Some obja\<rbrakk> \<Longrightarrow> live obja
 2. \<lbrakk>if_live_then_nonz_cap s; kheap s p = Some obj; live obj\<rbrakk> \<Longrightarrow> ko_at obj p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap s; kheap s p = Some obj; live obj\<rbrakk> \<Longrightarrow> ko_at obj p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cte_wp_at_caps_of_state:
 "cte_wp_at P p s = (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)" by (clarsimp simp add: cte_wp_at_def caps_of_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s = (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)
theory Invariants_AI

lemma ex_cte_cap_wp_to_weakenE:
  "\<lbrakk> ex_cte_cap_wp_to P p s;
      \<And>cte_cap. \<lbrakk> P cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s) \<rbrakk> \<Longrightarrow> Q cte_cap \<rbrakk>
       \<Longrightarrow> ex_cte_cap_wp_to Q p s" apply (simp add: ex_cte_cap_wp_to_def) apply (elim exEI) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_cte_cap_wp_to P p s; \<And>cte_cap. \<lbrakk>P cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> Q cte_cap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to Q p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>a b. cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; \<And>cte_cap. \<lbrakk>P cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> Q cte_cap\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. Q c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>cte_cap. \<lbrakk>P cte_cap; p \<in> cte_refs cte_cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> Q cte_cap; cte_wp_at (\<lambda>c. P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (x, xa) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. Q c \<and> p \<in> cte_refs c (interrupt_irq_node s)) (x, xa) s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma if_unsafe_then_capD:
  "\<lbrakk> cte_wp_at P p s; if_unsafe_then_cap s; \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap \<rbrakk>
     \<Longrightarrow> ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. P cap' \<and> appropriate_cte_cap cap' cap) p s" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (unfold if_unsafe_then_cap_def) apply (elim allE, drule(1) mp) apply (auto elim!: ex_cte_cap_wp_to_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; if_unsafe_then_cap s; \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. P cap' \<and> appropriate_cte_cap cap' cap) p s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>if_unsafe_then_cap s; \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap; caps_of_state s p = Some cap; P cap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. P cap' \<and> appropriate_cte_cap cap' cap) p s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>\<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) cref s; \<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap; caps_of_state s p = Some cap; P cap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. P cap' \<and> appropriate_cte_cap cap' cap) p s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>\<And>cap. P cap \<Longrightarrow> cap \<noteq> NullCap; caps_of_state s p = Some cap; P cap; cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. P cap' \<and> appropriate_cte_cap cap' cap) p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma zombies_finalD:
  "\<lbrakk> cte_wp_at P p s; zombies_final s; \<And>cap. P cap \<Longrightarrow> is_zombie cap \<rbrakk>
     \<Longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s" unfolding zombies_final_def apply (drule spec, erule mp) apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; zombies_final s; \<And>cap. P cap \<Longrightarrow> is_zombie cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; \<forall>p. cte_wp_at is_zombie p s \<longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s; \<And>cap. P cap \<Longrightarrow> is_zombie cap\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_final_cap' cap s) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; \<And>cap. P cap \<Longrightarrow> is_zombie cap\<rbrakk> \<Longrightarrow> cte_wp_at is_zombie p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma physical_valid_cap_not_empty_range:
  "\<lbrakk>valid_cap cap s; cap_class cap = PhysicalClass\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}" apply (case_tac cap) apply (simp_all add:cap_range_def valid_cap_simps cap_aligned_def is_aligned_no_overflow) apply (rename_tac arch_cap) apply (clarsimp simp: physical_arch_cap_has_ref) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {} proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = NullCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 8. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 9. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap_class cap = PhysicalClass; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_range cap \<noteq> {}
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>is_aligned (the (aobj_ref x12)) (arch_obj_size x12) \<and> arch_obj_size x12 < word_bits \<and> valid_arch_cap x12 s; acap_class x12 = PhysicalClass; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> \<exists>y. aobj_ref x12 = Some y proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>is_aligned (the (aobj_ref arch_cap)) (arch_obj_size arch_cap) \<and> arch_obj_size arch_cap < word_bits \<and> valid_arch_cap arch_cap s; acap_class arch_cap = PhysicalClass; cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> \<exists>y. aobj_ref arch_cap = Some y proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_ioc_def2:
  "valid_ioc s \<equiv>
   \<forall>p. is_original_cap s p \<longrightarrow> null_filter (caps_of_state s) p \<noteq> None" apply (rule eq_reflection) apply (clarsimp simp add: valid_ioc_def) apply (intro iff_allI weak_imp_cong refl) apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc s \<equiv> \<forall>p. is_original_cap s p \<longrightarrow> null_filter (caps_of_state s) p \<noteq> None proof (prove)
goal (1 subgoal):
 1. valid_ioc s = (\<forall>p. is_original_cap s p \<longrightarrow> null_filter (caps_of_state s) p \<noteq> None) proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s) = (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>y. null_filter (caps_of_state s) (a, b) = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s = (\<exists>y. null_filter (caps_of_state s) (a, b) = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>a b. caps_of_state s (a, b) \<noteq> Some NullCap \<Longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap) = (\<exists>y. caps_of_state s (a, b) = Some y) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma reply_master_caps_of_stateD:
  "\<And>slot. \<lbrakk> valid_reply_masters s; caps_of_state s slot = Some (ReplyCap t True rights)\<rbrakk>
   \<Longrightarrow> slot = (t, tcb_cnode_index 2)" by (simp add: valid_reply_masters_def cte_wp_at_caps_of_state is_master_reply_cap_to_def
           del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>valid_reply_masters s; caps_of_state s slot = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> slot = (t, tcb_cnode_index 2)
theory Invariants_AI

lemma has_reply_cap_cte_wpD:
  "\<And>t slot. cte_wp_at (is_reply_cap_to t) slot s \<Longrightarrow> has_reply_cap t s" by (fastforce simp: has_reply_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t slot. cte_wp_at (is_reply_cap_to t) slot s \<Longrightarrow> has_reply_cap t s
theory Invariants_AI

lemma reply_cap_doesnt_exist_strg:
  "(valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
      \<longrightarrow> \<not> has_reply_cap t s" by (clarsimp dest!: valid_reply_capsD
                simp: st_tcb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<longrightarrow> \<not> has_reply_cap t s
theory Invariants_AI

lemma mdb_cte_atD:
  "\<lbrakk> m c = Some p; mdb_cte_at ct_at m \<rbrakk>
     \<Longrightarrow> ct_at p \<and> ct_at c" by (simp add: mdb_cte_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some p; mdb_cte_at ct_at m\<rbrakk> \<Longrightarrow> ct_at p \<and> ct_at c
theory Invariants_AI

lemma zobj_refs_to_obj_refs:
  "(x \<in> zobj_refs cap) = (x \<in> obj_refs cap \<and> \<not> is_zombie cap)" by (cases cap, simp_all add: is_zombie_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> zobj_refs cap) = (x \<in> obj_refs cap \<and> \<not> is_zombie cap)
theory Invariants_AI

lemma idle_no_refs:
  "valid_idle s \<Longrightarrow> state_refs_of s (idle_thread s) = {}" apply (clarsimp simp: valid_idle_def) apply (clarsimp simp: pred_tcb_at_def obj_at_def tcb_ntfn_is_bound_def state_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle s \<Longrightarrow> state_refs_of s (idle_thread s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr\<rbrakk> \<Longrightarrow> state_refs_of s idle_thread_ptr = {} proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma idle_not_queued: (* ARMHYP? *)
  "\<lbrakk>valid_idle s; sym_refs (state_refs_of s);
   state_refs_of s ptr = queue \<times> {rt}\<rbrakk> \<Longrightarrow>
   idle_thread s \<notin> queue" by (frule idle_no_refs, fastforce simp: valid_idle_def sym_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; sym_refs (state_refs_of s); state_refs_of s ptr = queue \<times> {rt}\<rbrakk> \<Longrightarrow> idle_thread s \<notin> queue
theory Invariants_AI

lemma idle_not_queued': (* ARMHYP? *)
  "\<lbrakk>valid_idle s; sym_refs (state_refs_of s);
   state_refs_of s ptr = insert t queue \<times> {rt}\<rbrakk> \<Longrightarrow>
   idle_thread s \<notin> queue" by (frule idle_no_refs, fastforce simp: valid_idle_def sym_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; sym_refs (state_refs_of s); state_refs_of s ptr = insert t queue \<times> {rt}\<rbrakk> \<Longrightarrow> idle_thread s \<notin> queue
theory Invariants_AI

lemma mdb_cte_atI:
  "\<lbrakk> \<And>c p. m c = Some p \<Longrightarrow> ct_at p \<and> ct_at c \<rbrakk>
     \<Longrightarrow> mdb_cte_at ct_at m" by (simp add: mdb_cte_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>c p. m c = Some p \<Longrightarrow> ct_at p \<and> ct_at c) \<Longrightarrow> mdb_cte_at ct_at m
theory Invariants_AI

lemma only_idleD:
  "\<lbrakk> st_tcb_at idle t s; only_idle s \<rbrakk> \<Longrightarrow> t = idle_thread s" by (simp add: only_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at idle t s; only_idle s\<rbrakk> \<Longrightarrow> t = idle_thread s
theory Invariants_AI

lemma only_idleI:
  "(\<And>t. st_tcb_at idle t s \<Longrightarrow> t = idle_thread s) \<Longrightarrow> only_idle s" by (simp add: only_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>t. st_tcb_at idle t s \<Longrightarrow> t = idle_thread s) \<Longrightarrow> only_idle s
theory Invariants_AI

lemma valid_refs_def2:
  "valid_refs R = (\<lambda>s. \<forall>c \<in> ran (caps_of_state s). R \<inter> cap_range c = {})" apply (simp add: valid_refs_def cte_wp_at_caps_of_state ran_def) apply (rule ext, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_refs R = (\<lambda>s. \<forall>c\<in>ran (caps_of_state s). R \<inter> cap_range c = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> R \<inter> cap_range cap = {}) = (\<lambda>s. \<forall>c. (\<exists>a b. caps_of_state s (a, b) = Some c) \<longrightarrow> R \<inter> cap_range c = {}) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma idle_no_ex_cap:
  "\<lbrakk>valid_global_refs s; valid_objs s\<rbrakk> \<Longrightarrow>
   \<not> ex_nonz_cap_to (idle_thread s) s" apply (simp add: ex_nonz_cap_to_def valid_global_refs_def valid_refs_def2 cte_wp_at_caps_of_state
              del: split_paired_Ex split_paired_All) apply (intro allI notI impI) apply (drule bspec, blast) apply (clarsimp simp: cap_range_def zobj_refs_to_obj_refs) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; valid_objs s\<rbrakk> \<Longrightarrow> \<not> ex_nonz_cap_to (idle_thread s) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}; valid_objs s\<rbrakk> \<Longrightarrow> \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> idle_thread s \<notin> zobj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>cref cap. \<lbrakk>\<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}; valid_objs s; caps_of_state s cref = Some cap; idle_thread s \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cap. \<lbrakk>valid_objs s; caps_of_state s cref = Some cap; idle_thread s \<in> zobj_refs cap; global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>valid_objs s; caps_of_state s (a, b) = Some cap; global_refs s \<inter> (untyped_range cap \<union> obj_refs cap) = {}; idle_thread s \<in> obj_refs cap; \<not> is_zombie cap\<rbrakk> \<Longrightarrow> False
theory Invariants_AI

lemma caps_of_state_cteD:
  "caps_of_state s p = Some cap \<Longrightarrow> cte_wp_at ((=) cap) p s" by (simp add: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s p = Some cap \<Longrightarrow> cte_wp_at ((=) cap) p s
theory Invariants_AI

lemma untyped_mdb_alt:
  "untyped_mdb (cdt s) (caps_of_state s) = untyped_children_in_mdb s" apply (simp add: untyped_children_in_mdb_def untyped_mdb_def cte_wp_at_caps_of_state) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb (cdt s) (caps_of_state s) = untyped_children_in_mdb s proof (prove)
goal (1 subgoal):
 1. (\<forall>a b aa ba cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s))) = (\<forall>a b aa ba. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> is_untyped_cap cap \<and> (\<exists>capa. caps_of_state s (aa, ba) = Some capa \<and> obj_refs capa \<inter> untyped_range cap \<noteq> {})) \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s)) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma untyped_children_in_mdbE:
  assumes x: "untyped_children_in_mdb s" "cte_wp_at ((=) cap) ptr s"
             "is_untyped_cap cap" "cte_wp_at P ptr' s"
  assumes y: "\<And>cap'. \<lbrakk> cte_wp_at ((=) cap') ptr' s; P cap' \<rbrakk> \<Longrightarrow>
                 obj_refs cap' \<inter> untyped_range cap \<noteq> {}"
  assumes z: "ptr' \<in> descendants_of ptr (cdt s) \<Longrightarrow> Q"
  shows Q using x apply (clarsimp simp: untyped_children_in_mdb_def
                  simp del: split_paired_All split_paired_Ex) apply (erule allE[where x=ptr], erule allE[where x=ptr'], erule impE) apply (rule exI, (erule conjI)+) apply (clarsimp simp: cte_wp_at_def y) apply (erule z) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (prove)
using this:
untyped_children_in_mdb s
cte_wp_at ((=) cap) ptr s
is_untyped_cap cap
cte_wp_at P ptr' s

goal (1 subgoal):
 1. Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr ptr'. (\<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s) \<longrightarrow> ptr' \<in> descendants_of ptr (cdt s); cte_wp_at ((=) cap) ptr s; is_untyped_cap cap; cte_wp_at P ptr' s\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) cap) ptr s; is_untyped_cap cap; cte_wp_at P ptr' s\<rbrakk> \<Longrightarrow> \<exists>cap. cte_wp_at ((=) cap) ptr s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s
 2. \<lbrakk>cte_wp_at ((=) cap) ptr s; is_untyped_cap cap; cte_wp_at P ptr' s; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (2 subgoals):
 1. cte_wp_at P ptr' s \<Longrightarrow> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) ptr' s
 2. \<lbrakk>cte_wp_at ((=) cap) ptr s; is_untyped_cap cap; cte_wp_at P ptr' s; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) ptr s; is_untyped_cap cap; cte_wp_at P ptr' s; ptr' \<in> descendants_of ptr (cdt s)\<rbrakk> \<Longrightarrow> Q proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cte_wp_at_cases2:
  "cte_wp_at P t s =
   ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and>
                  well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or>
    (\<exists>tcb cap. kheap s (fst t) = Some (TCB tcb) \<and>
               (tcb_cnode_map tcb (snd t) = Some cap \<and> P cap)))" by (auto simp add: cte_wp_at_cases tcb_cap_cases_def tcb_cnode_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P t s = ((\<exists>sz fun cap. kheap s (fst t) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd t) = Some cap \<and> P cap) \<or> (\<exists>tcb cap. kheap s (fst t) = Some (TCB tcb) \<and> tcb_cnode_map tcb (snd t) = Some cap \<and> P cap))