kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AI

lemma pspace_no_overlap_retype_addrs_empty:
  assumes nptr: "pspace_no_overlap_range_cover ptr sz s"
  and xv: "x \<in> set (retype_addrs ptr ty n us)"
  and yv: "y \<notin> set (retype_addrs ptr ty n us)"
  and kov: "kheap s y = Some ko"
  and tyv: "ty \<noteq> Structures_A.apiobject_type.Untyped"
  and cover: "range_cover ptr sz (obj_bits_api ty us) n"
  and oab: "obj_bits_api ty us \<le> sz"
  shows "{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {}" proof - have "{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}" by (subst obj_bits_api_default_object [OF tyv, symmetric],
      rule retype_addrs_mem_subset_ptr_bits) fact+ moreover have "{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {}" by (subst Int_commute, rule pspace_no_overlapE) fact+ ultimately show ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (state)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (prove)
goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> up_aligned_area ptr sz proof (state)
this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> up_aligned_area ptr sz

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (state)
this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> up_aligned_area ptr sz

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (prove)
goal (1 subgoal):
 1. up_aligned_area ptr sz \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (state)
this:
up_aligned_area ptr sz \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {}

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (chain)
picking this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> up_aligned_area ptr sz
up_aligned_area ptr sz \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (prove)
using this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<subseteq> up_aligned_area ptr sz
up_aligned_area ptr sz \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {}

goal (1 subgoal):
 1. {x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {} proof (state)
this:
{x..x + (2 ^ obj_bits (default_object ty dev us) - 1)} \<inter> {y..y + (2 ^ obj_bits ko - 1)} = {}

goal:
No subgoals!
theory Retype_AI

lemma usable_range_subseteq:
  "\<lbrakk>cap_aligned cap;is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<subseteq> untyped_range cap" apply (clarsimp simp:is_cap_simps cap_aligned_def split:if_splits) apply (erule order_trans[OF is_aligned_no_wrap']) apply (erule of_nat_power) apply (simp add:word_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned cap; is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>x dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; f < 2 ^ bits; r + word_of_nat f \<le> x; x \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r \<le> x proof (prove)
goal (2 subgoals):
 1. \<And>x dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; f < 2 ^ bits; r + word_of_nat f \<le> x; x \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> ?off21 x dev r bits f < 2 ^ bits
 2. \<And>x dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; f < 2 ^ bits; r + word_of_nat f \<le> x; x \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r + ?off21 x dev r bits f \<le> x proof (prove)
goal (2 subgoals):
 1. \<And>x dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; r + word_of_nat f \<le> x; x \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> bits < LENGTH(32)
 2. \<And>x dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; f < 2 ^ bits; r + word_of_nat f \<le> x; x \<le> r + 2 ^ bits - 1\<rbrakk> \<Longrightarrow> r + word_of_nat f \<le> x proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma usable_range_emptyD:
  "\<lbrakk>cap_aligned cap;is_untyped_cap cap ;usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> 2 ^ cap_bits cap \<le> free_index_of cap" apply (clarsimp simp:is_cap_simps not_le free_index_of_def cap_aligned_def split:if_splits) apply (drule(1) of_nat_power [where 'a=machine_word_len, folded word_bits_def]) apply (drule word_plus_mono_right[OF _ is_aligned_no_overflow[unfolded p_assoc_help],rotated]) apply simp apply (simp add:p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned cap; is_untyped_cap cap; usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> 2 ^ cap_bits cap \<le> free_index_of cap proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; f < 2 ^ bits; r + 2 ^ bits - 1 < r + word_of_nat f\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits; r + 2 ^ bits - 1 < r + word_of_nat f; word_of_nat f < 2 ^ bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; r + 2 ^ bits - 1 < r + word_of_nat f; word_of_nat f < 2 ^ bits\<rbrakk> \<Longrightarrow> ?y21 dev r bits f \<le> 2 ^ bits - 1
 2. \<And>dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; r + 2 ^ bits - 1 < r + word_of_nat f; word_of_nat f < 2 ^ bits; r + ?y21 dev r bits f \<le> r + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f. \<lbrakk>cap = UntypedCap dev r bits f; bits < word_bits; r + 2 ^ bits - 1 < r + word_of_nat f; word_of_nat f < 2 ^ bits; r + word_of_nat f \<le> r + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma cap_refs_respects_device_region_cap_range:
  "\<lbrakk>cte_wp_at (\<lambda>c.  {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s;
    cap_refs_respects_device_region s\<rbrakk>
    \<Longrightarrow> up_aligned_area ptr sz \<subseteq> (if dev then device_region s else - device_region s)" unfolding cap_refs_respects_device_region_def apply (drule spec[where x = slot]) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s; cap_refs_respects_device_region s\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> (if dev then dom (device_state (machine_state s)) else - dom (device_state (machine_state s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s; \<forall>cref. \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) cref s\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> (if dev then dom (device_state (machine_state s)) else - dom (device_state (machine_state s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s; \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) slot s\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<subseteq> (if dev then dom (device_state (machine_state s)) else - dom (device_state (machine_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>if cap_is_device cap then cap_range cap \<subseteq> dom (device_state (machine_state s)) else cap_range cap \<subseteq> - dom (device_state (machine_state s)); caps_of_state s slot = Some cap; up_aligned_area ptr sz \<subseteq> cap_range cap; dev = cap_is_device cap\<rbrakk> \<Longrightarrow> (cap_is_device cap \<longrightarrow> up_aligned_area ptr sz \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device cap \<longrightarrow> up_aligned_area ptr sz \<subseteq> - dom (device_state (machine_state s))) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma obj_at_pres: "\<And>P x. obj_at P x s \<Longrightarrow> obj_at P x s'" by (clarsimp simp: obj_at_def s'_def ps_def dest: domI)
     (rule pspace_no_overlapC [OF orth _ _ cover vp])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P x. obj_at P x s \<Longrightarrow> obj_at P x s'
theory Retype_AI

lemma orthr:
  "\<And>x obj. kheap s x = Some obj \<Longrightarrow> x \<notin> set (retype_addrs ptr ty n us)" apply (rule ccontr) apply (frule pspace_no_overlapC[OF orth _ _ _ vp,rotated]) apply (rule cover) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x obj. kheap s x = Some obj \<Longrightarrow> x \<notin> set (retype_addrs ptr ty n us) proof (prove)
goal (1 subgoal):
 1. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> range_cover ptr sz (obj_bits_api (?ty2 x obj) (?us2 x obj)) (?n2 x obj)
 2. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> x \<in> set (retype_addrs ptr (?ty2 x obj) (?n2 x obj) (?us2 x obj))
 3. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us); ?P2 x obj\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> x \<in> set (retype_addrs ptr ty n us)
 2. \<And>x obj. \<lbrakk>kheap s x = Some obj; \<not> x \<notin> set (retype_addrs ptr ty n us); ?P2 x obj\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma cte_at_pres: "\<And>p. cte_at p s \<Longrightarrow> cte_at p s'" unfolding cte_at_cases s'_def ps_def apply (erule disjE) apply (clarsimp simp: well_formed_cnode_n_def orthr)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s' proof (prove)
goal (1 subgoal):
 1. \<And>p. (\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> snd p \<in> dom tcb_cap_cases) \<Longrightarrow> (\<exists>sz fun. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun \<Longrightarrow> (\<exists>sz fun. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> snd p \<in> dom tcb_cap_cases)
 2. \<And>p. \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> snd p \<in> dom tcb_cap_cases \<Longrightarrow> (\<exists>sz fun. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> snd p \<in> dom fun) \<or> (\<exists>tcb. kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst p) = Some (TCB tcb) \<and> snd p \<in> dom tcb_cap_cases) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pred_tcb_at_pres: "\<And>P t. pred_tcb_at proj P t s \<Longrightarrow> pred_tcb_at proj P t s'" unfolding pred_tcb_at_def by (erule obj_at_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P t. pred_tcb_at proj P t s \<Longrightarrow> pred_tcb_at proj P t s' proof (prove)
goal (1 subgoal):
 1. \<And>P t. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s'
theory Retype_AI

lemma le_subset: "\<lbrakk>(a::('g::len) word) \<le> c\<rbrakk> \<Longrightarrow> {c..b} \<subseteq> {a..b}" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> c \<Longrightarrow> {c..b} \<subseteq> {a..b}
theory Retype_AI

lemma refs_eq:
  "state_refs_of s' = state_refs_of s" unfolding s'_def ps_def apply (clarsimp intro!: ext simp: state_refs_of_def
                    simp: orthr
                   split: option.splits) apply (cases ty, simp_all add: tyunt default_object_def
                                 default_tcb_def default_ep_def
                                 default_notification_def default_ntfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of s' = state_refs_of s proof (prove)
goal (1 subgoal):
 1. state_refs_of (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) = state_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s x = None; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> refs_of (default_object ty dev us) = {} proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma cte_retype:
    "\<And>P p. \<not> P cap.NullCap \<Longrightarrow>
     cte_wp_at P p s' = cte_wp_at P p s" unfolding s'_def ps_def apply (safe elim!: cte_wp_atE) apply (clarsimp split: if_split_asm
                              Structures_A.apiobject_type.split_asm
                        simp: default_object_def tyunt default_tcb_def
                              empty_cnode_def cte_wp_at_cases
                       dest!: orthr
                  | simp add: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. \<not> P NullCap \<Longrightarrow> cte_wp_at P p s' = cte_wp_at P p s proof (prove)
goal (1 subgoal):
 1. \<And>P p. \<not> P NullCap \<Longrightarrow> cte_wp_at P p (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) = cte_wp_at P p s proof (prove)
goal (4 subgoals):
 1. \<And>P a b sz fun cte. \<lbrakk>\<not> P NullCap; kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst (a, b)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (a, b)) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 2. \<And>P a b tcb getF setF restr. \<lbrakk>\<not> P NullCap; kheap (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) s
 3. \<And>P a b sz fun cte. \<lbrakk>\<not> P NullCap; kheap s (fst (a, b)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (a, b)) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)
 4. \<And>P a b tcb getF setF restr. \<lbrakk>\<not> P NullCap; kheap s (fst (a, b)) = Some (TCB tcb); tcb_cap_cases (snd (a, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (a, b) (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma iflive_s: "if_live_then_nonz_cap s" by (rule valid_pspaceE [OF vp])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap s
theory Retype_AI

lemma default_object_not_live: "\<not> live (default_object ty dev us)" apply (cases ty, simp_all add: tyunt default_object_def default_tcb_not_live default_arch_object_not_live) apply (simp add: live_def default_ep_def default_notification_def default_ntfn_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> live (default_object ty dev us) proof (prove)
goal (3 subgoals):
 1. ty = EndpointObject \<Longrightarrow> \<not> live (Endpoint default_ep)
 2. ty = NotificationObject \<Longrightarrow> \<not> live (Notification default_notification)
 3. ty = CapTableObject \<Longrightarrow> \<not> live (CNode us (empty_cnode us)) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma final_retype: "is_final_cap' cap s' = is_final_cap' cap s" by (simp add: is_final_cap'_def2 cte_retype)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_final_cap' cap s' = is_final_cap' cap s
theory Retype_AI

lemma not_final_NullCap: "\<And>s. \<not> is_final_cap' cap.NullCap s" by (simp add: is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> is_final_cap' NullCap s
theory Retype_AI

lemma F: "\<And>x c s. (caps_of_state s x = Some c) = (cte_wp_at ((=) c) x s)" apply (simp add: caps_of_state_cte_wp_at) apply (fastforce simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x c s. (caps_of_state s x = Some c) = cte_wp_at ((=) c) x s proof (prove)
goal (1 subgoal):
 1. \<And>x c s. (\<exists>cap. cte_wp_at ((=) cap) x s) \<longrightarrow> ((THE cap. cte_wp_at ((=) cap) x s) = c) = cte_wp_at ((=) c) x s proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma F2: "\<And>x c s. (null_filter (caps_of_state s) x = Some c)
             = (cte_wp_at (\<lambda>cap. cap \<noteq> cap.NullCap \<and> cap = c) x s)" apply (simp add: null_filter_def F) apply (fastforce simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x c s. (null_filter (caps_of_state s) x = Some c) = cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) x s proof (prove)
goal (1 subgoal):
 1. \<And>x c s. (cte_wp_at ((=) NullCap) x s \<longrightarrow> \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) x s) \<and> (\<not> cte_wp_at ((=) NullCap) x s \<longrightarrow> cte_wp_at ((=) c) x s = cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) x s) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma F3: "\<And>x s. (None = null_filter (caps_of_state s) x)
              = (\<forall>c. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> cap.NullCap \<and> cap = c) x s)" apply safe apply (simp add: F2[symmetric]) apply (rule sym, rule ccontr, clarsimp simp: F2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x s. (None = null_filter (caps_of_state s) x) = (\<forall>c. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) x s) proof (prove)
goal (2 subgoals):
 1. \<And>a b s c. \<lbrakk>None = null_filter (caps_of_state s) (a, b); cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) (a, b) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b s. \<forall>c. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) (a, b) s \<Longrightarrow> None = null_filter (caps_of_state s) (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<forall>c. \<not> cte_wp_at (\<lambda>cap. cap \<noteq> NullCap \<and> cap = c) (a, b) s \<Longrightarrow> None = null_filter (caps_of_state s) (a, b) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma (in retype_region_proofs) null_filter:
  "null_filter (caps_of_state s') = null_filter (caps_of_state s)" apply (rule ext) apply (case_tac "null_filter (caps_of_state s) x") apply (simp add: eq_commute) apply (simp add: F3 cte_retype) apply simp apply (simp add: F2 cte_retype) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state s') = null_filter (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>x. null_filter (caps_of_state s') x = null_filter (caps_of_state s) x proof (prove)
goal (2 subgoals):
 1. \<And>x. null_filter (caps_of_state s) x = None \<Longrightarrow> null_filter (caps_of_state s') x = null_filter (caps_of_state s) x
 2. \<And>x a. null_filter (caps_of_state s) x = Some a \<Longrightarrow> null_filter (caps_of_state s') x = null_filter (caps_of_state s) x proof (prove)
goal (2 subgoals):
 1. \<And>x. None = null_filter (caps_of_state s) x \<Longrightarrow> None = null_filter (caps_of_state s') x
 2. \<And>x a. null_filter (caps_of_state s) x = Some a \<Longrightarrow> null_filter (caps_of_state s') x = null_filter (caps_of_state s) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. null_filter (caps_of_state s) x = Some a \<Longrightarrow> null_filter (caps_of_state s') x = null_filter (caps_of_state s) x proof (prove)
goal (1 subgoal):
 1. \<And>x a. null_filter (caps_of_state s) x = Some a \<Longrightarrow> null_filter (caps_of_state s') x = Some a proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma idle_s':
  "idle_thread s' = idle_thread s" by (simp add: s'_def ps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_thread s' = idle_thread s
theory Retype_AI

lemma valid_idle:
  "valid_idle s \<Longrightarrow> valid_idle s'" by (clarsimp simp add: valid_idle_def idle_s' refs_eq
                         pred_tcb_at_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle s \<Longrightarrow> valid_idle s'
theory Retype_AI

lemma arch_state [simp]:
  "arch_state s' = arch_state s" by (simp add: s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_state s' = arch_state s
theory Retype_AI

lemma irq_node [simp]:
  "interrupt_irq_node s' = interrupt_irq_node s" by (simp add: s'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interrupt_irq_node s' = interrupt_irq_node s
theory Retype_AI

lemma caps_retype:
  assumes nonnull: "cap \<noteq> cap.NullCap"
  and      newcap: "caps_of_state s' p = Some cap"
  shows            "caps_of_state s p = Some cap" proof - from newcap have "cte_wp_at ((=) cap) p s'" by (simp add: cte_wp_at_caps_of_state) hence "cte_wp_at ((=) cap) p s" by (rule_tac subst [OF cte_retype], rule_tac nonnull, assumption) thus ?thesis by (simp add: cte_wp_at_caps_of_state) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s p = Some cap proof (state)
goal (1 subgoal):
 1. caps_of_state s p = Some cap proof (chain)
picking this:
caps_of_state s' p = Some cap proof (prove)
using this:
caps_of_state s' p = Some cap

goal (1 subgoal):
 1. cte_wp_at ((=) cap) p s' proof (state)
this:
cte_wp_at ((=) cap) p s'

goal (1 subgoal):
 1. caps_of_state s p = Some cap proof (prove)
using this:
cte_wp_at ((=) cap) p s'

goal (1 subgoal):
 1. cte_wp_at ((=) cap) p s proof (state)
this:
cte_wp_at ((=) cap) p s

goal (1 subgoal):
 1. caps_of_state s p = Some cap proof (prove)
using this:
cte_wp_at ((=) cap) p s

goal (1 subgoal):
 1. caps_of_state s p = Some cap proof (state)
this:
caps_of_state s p = Some cap

goal:
No subgoals!