kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma mdb_Null_descendants:
  "\<lbrakk> cte_wp_at ((=) cap.NullCap) p s; valid_mdb s \<rbrakk> \<Longrightarrow>
      descendants_of p (cdt s) = {}" apply (clarsimp simp add: valid_mdb_def cte_wp_at_caps_of_state swp_def) apply (erule(1) mdb_cte_at_Null_descendants) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) NullCap) p s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some NullCap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma mdb_Null_None:
  "\<lbrakk> cte_wp_at ((=) cap.NullCap) p s; valid_mdb s \<rbrakk> \<Longrightarrow>
      cdt s p = None" apply (clarsimp simp add: valid_mdb_def cte_wp_at_caps_of_state swp_def) apply (erule(1) mdb_cte_at_Null_None) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) NullCap) p s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s p = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some NullCap; mdb_cte_at (\<lambda>y. \<exists>cap. caps_of_state s y = Some cap \<and> NullCap \<noteq> cap) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cdt s p = None proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma list_all2_zip_split:
  "\<lbrakk> list_all2 P as cs; list_all2 Q bs ds \<rbrakk> \<Longrightarrow>
   list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y))
              (zip as bs) (zip cs ds)" apply (induct as arbitrary: bs cs ds) apply simp apply (case_tac cs; simp) apply (case_tac bs; simp) apply (case_tac ds; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 P as cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip as bs) (zip cs ds) proof (prove)
goal (2 subgoals):
 1. \<And>bs cs ds. \<lbrakk>list_all2 P [] cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip [] bs) (zip cs ds)
 2. \<And>a as bs cs ds. \<lbrakk>\<And>bs cs ds. \<lbrakk>list_all2 P as cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip as bs) (zip cs ds); list_all2 P (a # as) cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip (a # as) bs) (zip cs ds) proof (prove)
goal (1 subgoal):
 1. \<And>a as bs cs ds. \<lbrakk>\<And>bs cs ds. \<lbrakk>list_all2 P as cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip as bs) (zip cs ds); list_all2 P (a # as) cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip (a # as) bs) (zip cs ds) proof (prove)
goal (1 subgoal):
 1. \<And>a as bs cs ds aa list. \<lbrakk>\<And>bs cs ds. \<lbrakk>list_all2 P as cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip as bs) (zip cs ds); P a aa \<and> list_all2 P as list; list_all2 Q bs ds; cs = aa # list\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip (a # as) bs) (zip (aa # list) ds) proof (prove)
goal (1 subgoal):
 1. \<And>a as bs cs ds aa list ab lista. \<lbrakk>\<And>bs cs ds. \<lbrakk>list_all2 P as cs; list_all2 Q bs ds\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) (zip as bs) (zip cs ds); P a aa \<and> list_all2 P as list; list_all2 Q (ab # lista) ds; cs = aa # list; bs = ab # lista\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. P (fst x) (fst y) \<and> Q (snd x) (snd y)) ((a, ab) # zip as lista) (zip (aa # list) ds) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma set_cdt_tcb_valid[wp]:
  "\<lbrace>tcb_cap_valid cap ptr\<rbrace> set_cdt m \<lbrace>\<lambda>rv. tcb_cap_valid cap ptr\<rbrace>" by (simp add: set_cdt_def, wp, simp add: tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap ptr\<rbrace> set_cdt m \<lbrace>\<lambda>rv. tcb_cap_valid cap ptr\<rbrace>
theory Untyped_AI

lemma tcb_cap_valid_rvk[simp]:
  "tcb_cap_valid cap ptr (is_original_cap_update f s)
     = tcb_cap_valid cap ptr s" by (simp add: tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap ptr (is_original_cap_update f s) = tcb_cap_valid cap ptr s
theory Untyped_AI

lemma tcb_cap_valid_more_update[simp]:
  "tcb_cap_valid cap ptr (trans_state f s)
     = tcb_cap_valid cap ptr s" by (simp add: tcb_cap_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap ptr (trans_state f s) = tcb_cap_valid cap ptr s
theory Untyped_AI

lemma default_non_Null[simp]:
  "cap.NullCap \<noteq> default_cap tp oref sz dev" by (cases tp, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. NullCap \<noteq> default_cap tp oref sz dev
theory Untyped_AI

lemma cs_valid_cap:
  "cs p = Some c \<Longrightarrow> s \<turnstile> c" using valid_objs apply (simp add: cs_def) apply (drule cte_wp_at_valid_objs_valid_cap [rotated, where P="(=) c"]) apply (simp add: cte_wp_at_caps_of_state) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cs p = Some c \<Longrightarrow> s \<turnstile> c proof (prove)
using this:
valid_objs s

goal (1 subgoal):
 1. cs p = Some c \<Longrightarrow> s \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some c; valid_objs s\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (2 subgoals):
 1. caps_of_state s p = Some c \<Longrightarrow> cte_wp_at ((=) c) ?p1 s
 2. \<lbrakk>caps_of_state s p = Some c; \<exists>cap. c = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some c; \<exists>cap. c = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> s \<turnstile> c proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cs_cap_aligned:
  "cs p = Some c \<Longrightarrow> cap_aligned c" apply (drule cs_valid_cap) apply (simp add: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cs p = Some c \<Longrightarrow> cap_aligned c proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c \<Longrightarrow> cap_aligned c proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma d_rangeD:
  "\<lbrakk>descendants_range ac p s; m \<Turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> \<exists>c. cs p' = Some c \<and> untyped_range c \<inter> untyped_range ac = {}" apply (drule(1) descendants_rangeD[where s= s,folded m_def cs_def]) apply clarsimp apply (drule disjoint_subset2[OF untyped_range_in_cap_range]) apply (drule disjoint_subset[OF untyped_range_in_cap_range]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range ac p s; m \<Turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> \<exists>c. cs p' = Some c \<and> untyped_range c \<inter> untyped_range ac = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> p'; \<exists>c. cs p' = Some c \<and> cap_range c \<inter> cap_range ac = {}\<rbrakk> \<Longrightarrow> \<exists>c. cs p' = Some c \<and> untyped_range c \<inter> untyped_range ac = {} proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>m \<Turnstile> p \<rightarrow> p'; cs p' = Some c; cap_range c \<inter> cap_range ac = {}\<rbrakk> \<Longrightarrow> untyped_range c \<inter> untyped_range ac = {} proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>m \<Turnstile> p \<rightarrow> p'; cs p' = Some c; cap_range c \<inter> untyped_range ac = {}\<rbrakk> \<Longrightarrow> untyped_range c \<inter> untyped_range ac = {} proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>m \<Turnstile> p \<rightarrow> p'; cs p' = Some c; untyped_range c \<inter> untyped_range ac = {}\<rbrakk> \<Longrightarrow> untyped_range c \<inter> untyped_range ac = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma subseteq_imp_not_subset: "A \<subseteq> B \<Longrightarrow> \<not> B \<subset> A" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> \<not> B \<subset> A
theory Untyped_AI

lemma default_cap_replies[simp]:
  "\<not> is_reply_cap (default_cap otype oref sz dev)"
  "\<not> is_master_reply_cap (default_cap otype oref sz dev)" by (cases otype, simp_all add: is_cap_simps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_reply_cap (default_cap otype oref sz dev) &&& \<not> is_master_reply_cap (default_cap otype oref sz dev)
theory Untyped_AI

lemma inter_non_emptyD:
 "\<lbrakk>A \<subseteq> B; A \<inter> C \<noteq> {}\<rbrakk> \<Longrightarrow> B \<inter> C \<noteq> {}" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; A \<inter> C \<noteq> {}\<rbrakk> \<Longrightarrow> B \<inter> C \<noteq> {}
theory Untyped_AI

lemma cap_class_default_cap:
  "cap_class (default_cap tp oref sz dev) = PhysicalClass" apply (case_tac tp) apply (simp_all add: default_cap_def physical_arch_cap_has_ref aobj_ref_default) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_class (default_cap tp oref sz dev) = PhysicalClass proof (prove)
goal (6 subgoals):
 1. tp = Untyped \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass
 2. tp = TCBObject \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass
 3. tp = EndpointObject \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass
 4. tp = NotificationObject \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass
 5. tp = CapTableObject \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass
 6. \<And>x6. tp = ArchObject x6 \<Longrightarrow> cap_class (default_cap tp oref sz dev) = PhysicalClass proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma caps_overlap_reservedD:
  "\<lbrakk>caps_overlap_reserved S s; caps_of_state s slot = Some cap;
    is_untyped_cap cap\<rbrakk>
   \<Longrightarrow> usable_untyped_range cap \<inter> S = {}" apply (simp add: caps_overlap_reserved_def) apply (erule ballE) apply (erule(1) impE) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_overlap_reserved S s; caps_of_state s slot = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; caps_of_state s slot = Some cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s slot = Some cap; is_untyped_cap cap; is_untyped_cap ?cap \<longrightarrow> usable_untyped_range ?cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<lbrakk>caps_of_state s slot = Some cap; is_untyped_cap cap; ?cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s slot = Some cap; is_untyped_cap cap; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<lbrakk>caps_of_state s slot = Some cap; is_untyped_cap cap; cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s slot = Some cap; is_untyped_cap cap; cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma cap_range_inter_emptyD:
  "cap_range a \<inter> cap_range b = {} \<Longrightarrow> untyped_range a \<inter> untyped_range b = {}" apply (drule disjoint_subset2[OF untyped_range_in_cap_range]) apply (drule disjoint_subset[OF untyped_range_in_cap_range]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range a \<inter> cap_range b = {} \<Longrightarrow> untyped_range a \<inter> untyped_range b = {} proof (prove)
goal (1 subgoal):
 1. cap_range a \<inter> untyped_range b = {} \<Longrightarrow> untyped_range a \<inter> untyped_range b = {} proof (prove)
goal (1 subgoal):
 1. untyped_range a \<inter> untyped_range b = {} \<Longrightarrow> untyped_range a \<inter> untyped_range b = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma set_tuple_pick:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>tup \<in> set (zip (xs rv s) (ys rv s)). Q (fst tup) rv s\<rbrace>"
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>y \<in> set (ys rv s). R y rv s\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>tup \<in> set (zip (xs rv s) (ys rv s)). R (snd tup) rv s\<rbrace>" apply (safe elim!: hoare_strengthen_post) apply (clarsimp simp: set_zip)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>set (xs rv s). Q x rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>tup\<in>set (zip (xs rv s) (ys rv s)). Q (fst tup) rv s\<rbrace>) &&& (\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>y\<in>set (ys rv s). R y rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>tup\<in>set (zip (xs rv s) (ys rv s)). R (snd tup) rv s\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>rv s a b. \<lbrakk>\<forall>x\<in>set (xs rv s). Q x rv s; (a, b) \<in> set (zip (xs rv s) (ys rv s))\<rbrakk> \<Longrightarrow> Q (fst (a, b)) rv s
 2. \<And>rv s a b. \<lbrakk>\<forall>y\<in>set (ys rv s). R y rv s; (a, b) \<in> set (zip (xs rv s) (ys rv s))\<rbrakk> \<Longrightarrow> R (snd (a, b)) rv s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma obj_at_foldr_intro:
  "P obj \<and> p \<in> set xs \<Longrightarrow> obj_at P p (s \<lparr> kheap := foldr (\<lambda>p ps. ps (p \<mapsto> obj)) xs (kheap s) \<rparr>)" by (clarsimp simp: obj_at_def foldr_upd_app_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P obj \<and> p \<in> set xs \<Longrightarrow> obj_at P p (s\<lparr>kheap := foldr (\<lambda>p ps. ps(p \<mapsto> obj)) xs (kheap s)\<rparr>)
theory Untyped_AI

lemma set_zip_helper:
  "t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys" by (clarsimp simp add: set_zip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<in> set (zip xs ys) \<Longrightarrow> fst t \<in> set xs \<and> snd t \<in> set ys
theory Untyped_AI

lemma untyped_range_default_empty:
  "tp \<noteq> Untyped \<Longrightarrow> untyped_range (default_cap tp sz us dev) = {}" by (cases tp, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<noteq> Untyped \<Longrightarrow> untyped_range (default_cap tp sz us dev) = {}
theory Untyped_AI

lemma obj_refs_default_cap:
  "obj_refs (default_cap tp oref sz dev) \<subseteq> {oref}" apply (cases tp, simp_all add: aobj_ref_default) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs (default_cap tp oref sz dev) \<subseteq> {oref} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma obj_refs_default_nut:
  "tp \<noteq> Untyped \<Longrightarrow> obj_refs (default_cap tp oref sz dev) = {oref}" apply (cases tp, simp_all add: aobj_ref_default) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<noteq> Untyped \<Longrightarrow> obj_refs (default_cap tp oref sz dev) = {oref} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma map_snd_zip_prefix_help:
  "map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le>
   map (\<lambda>x. cap_range (default_cap tp x us dev)) ys" apply (induct xs arbitrary: ys) apply simp apply (case_tac ys) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys proof (prove)
goal (2 subgoals):
 1. \<And>ys. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip [] ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys
 2. \<And>a xs ys. (\<And>ys. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys) \<Longrightarrow> map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip (a # xs) ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. (\<And>ys. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys) \<Longrightarrow> map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip (a # xs) ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys proof (prove)
goal (2 subgoals):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys; ys = []\<rbrakk> \<Longrightarrow> map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip (a # xs) ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys
 2. \<And>a xs ys aa list. \<lbrakk>\<And>ys. map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys; ys = aa # list\<rbrakk> \<Longrightarrow> map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip (a # xs) ys) \<le> map (\<lambda>x. cap_range (default_cap tp x us dev)) ys proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma delete_objects_pspace_no_overlap[wp]:
  "\<lbrace>\<lambda>s. (\<exists>dev idx. s \<turnstile> (UntypedCap dev ptr bits idx))
      \<and> pspace_aligned s \<and> valid_objs s \<and> (S = {ptr .. ptr + 2 ^ bits - 1})\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_. pspace_no_overlap S\<rbrace>" apply (unfold delete_objects_def) apply wp apply (simp add: do_machine_op_def split_def) apply wp apply (clarsimp simp: pspace_no_overlap_detype') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>dev idx. s \<turnstile> UntypedCap dev ptr bits idx) \<and> pspace_aligned s \<and> valid_objs s \<and> S = {ptr..ptr + 2 ^ bits - 1}\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_. pspace_no_overlap S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>dev idx. s \<turnstile> UntypedCap dev ptr bits idx) \<and> pspace_aligned s \<and> valid_objs s \<and> S = {ptr..ptr + 2 ^ bits - 1}\<rbrace> do do_machine_op (freeMemory ptr bits);
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_. pspace_no_overlap S\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>x s. pspace_no_overlap S (detype {ptr..ptr + 2 ^ bits - 1} s)\<rbrace>
 2. \<And>s. (\<exists>dev idx. s \<turnstile> UntypedCap dev ptr bits idx) \<and> pspace_aligned s \<and> valid_objs s \<and> S = {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ms <- gets machine_state;
p <- select_f (freeMemory ptr bits ms);
modify (machine_state_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>x s. pspace_no_overlap S (detype {ptr..ptr + 2 ^ bits - 1} s)\<rbrace>
 2. \<And>s. (\<exists>dev idx. s \<turnstile> UntypedCap dev ptr bits idx) \<and> pspace_aligned s \<and> valid_objs s \<and> S = {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>dev idx. s \<turnstile> UntypedCap dev ptr bits idx) \<and> pspace_aligned s \<and> valid_objs s \<and> S = {ptr..ptr + 2 ^ bits - 1} \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). pspace_no_overlap S (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma retype_region_descendants_range:
  "\<lbrace>\<lambda>s. descendants_range x cref s
    \<and> pspace_no_overlap_range_cover ptr sz s \<and> valid_pspace s
    \<and> range_cover ptr sz (obj_bits_api ty us) n\<rbrace> retype_region ptr n us ty dev
          \<lbrace>\<lambda>rv s. descendants_range x cref s\<rbrace>" apply (simp add:descendants_range_def) apply (rule hoare_pre) apply (wps retype_region_mdb) apply (wp hoare_vcg_ball_lift retype_cte_wp_at) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. descendants_range x cref s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. descendants_range x cref\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s) \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s\<rbrace>
 2. \<And>s. (\<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s) \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s'. \<forall>p'\<in>descendants_of cref (cdt prev_s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s'\<rbrace>
 2. \<And>s. (\<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s) \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) p' s) \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n \<Longrightarrow> \<forall>xa\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range x = {}) xa s \<and> pspace_no_overlap (up_aligned_area ptr (?sz11 s xa)) s \<and> valid_pspace s \<and> range_cover ptr (?sz11 s xa) (obj_bits_api ty us) n proof (prove)
goal:
No subgoals!