kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_R

lemma ex_nonz_cap_notRange:
  "ex_nonz_cap_to' p s \<Longrightarrow> p \<notin> base_bits" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (case_tac "isUntypedCap (cteCap cte)") apply (clarsimp simp: isCap_simps) apply (drule subsetD[OF zobj_refs_capRange, rotated]) apply (rule valid_capAligned, erule ctes_of_valid) apply (drule(1) objRefs_notrange) apply (drule_tac a=p in equals0D) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to' p s \<Longrightarrow> p \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; p \<in> zobj_refs' (cteCap cte); base \<le> p; p \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; p \<in> zobj_refs' (cteCap cte); base \<le> p; p \<le> base + (2 ^ bits - 1); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; p \<in> zobj_refs' (cteCap cte); base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; p \<in> zobj_refs' (cteCap cte); base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> capAligned (cteCap cte)
 2. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte); p \<in> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>ctes_of s cref = Some cte; base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte); p \<in> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte); p \<in> capRange (cteCap cte); capRange (cteCap cte) \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>base \<le> p; p \<le> base + (2 ^ bits - 1); \<not> isUntypedCap (cteCap cte); p \<in> capRange (cteCap cte); p \<notin> capRange (cteCap cte) \<inter> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma live_notRange:
  "\<lbrakk> ko_wp_at' P p s; \<And>ko. P ko \<Longrightarrow> live' ko \<rbrakk> \<Longrightarrow> p \<notin> base_bits" apply (drule if_live_then_nonz_capE' [OF iflive ko_wp_at'_weakenE]) apply simp apply (erule ex_nonz_cap_notRange) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_wp_at' P p s; \<And>ko. P ko \<Longrightarrow> live' ko\<rbrakk> \<Longrightarrow> p \<notin> base_bits proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>\<And>ko. P ko \<Longrightarrow> live' ko; P ko\<rbrakk> \<Longrightarrow> live' ko
 2. \<lbrakk>\<And>ko. P ko \<Longrightarrow> live' ko; ex_nonz_cap_to' p s\<rbrakk> \<Longrightarrow> p \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ko. P ko \<Longrightarrow> live' ko; ex_nonz_cap_to' p s\<rbrakk> \<Longrightarrow> p \<notin> base_bits proof (prove)
goal:
No subgoals!
theory Detype_R

lemma refs_notRange:
  "(x, tp) \<in> state_refs_of' s y \<Longrightarrow> y \<notin> base_bits" apply (drule state_refs_of'_elemD) apply (erule live_notRange) apply (rule refs_of_live') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, tp) \<in> state_refs_of' s y \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>obj. (x, tp) \<in> refs_of' obj) y s \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<And>ko. (x, tp) \<in> refs_of' ko \<Longrightarrow> live' ko proof (prove)
goal (1 subgoal):
 1. \<And>ko. (x, tp) \<in> refs_of' ko \<Longrightarrow> refs_of' ko \<noteq> {} proof (prove)
goal:
No subgoals!
theory Detype_R

lemma st_tcb:
    "\<And>P p. \<lbrakk> st_tcb_at' P p s; \<not> P Inactive; \<not> P IdleThreadState \<rbrakk> \<Longrightarrow> st_tcb_at' P p state'" by (fastforce simp: pred_tcb_at'_def obj_at'_real_def
                       projectKOs
                 dest: live_notRange)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. \<lbrakk>st_tcb_at' P p s; \<not> P Structures_H.thread_state.Inactive; \<not> P Structures_H.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> st_tcb_at' P p state'
theory Detype_R

lemma irq_nodes_global:
    "\<forall>irq :: 10 word. irq_node' s + (ucast irq) * 16 \<in> global_refs' s" by (simp add: global_refs'_def mult.commute mult.left_commute cteSizeBits_def shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>irq. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> global_refs' s
theory Detype_R

lemma global_refs:
  "global_refs' s \<inter> base_bits = {}" using cap apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule valid_global_refsD' [OF _ refs]) apply (fastforce simp add: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs' s \<inter> base_bits = {} proof (prove)
using this:
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s

goal (1 subgoal):
 1. global_refs' s \<inter> base_bits = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>ctes_of s ptr = Some cte; cteCap cte = capability.UntypedCap d base bits idx\<rbrakk> \<Longrightarrow> global_refs' s \<inter> base_bits = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>cteCap cte = capability.UntypedCap d base bits idx; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> global_refs' s \<inter> base_bits = {} proof (prove)
goal:
No subgoals!
theory Detype_R

lemma global_refs2:
  "global_refs' s \<subseteq> (- base_bits)" using global_refs by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs' s \<subseteq> - base_bits proof (prove)
using this:
global_refs' s \<inter> base_bits = {}

goal (1 subgoal):
 1. global_refs' s \<subseteq> - base_bits
theory Detype_R

lemma irq_nodes_range:
    "\<forall>irq :: 10 word. irq_node' s + (ucast irq) * 16 \<notin> base_bits" using irq_nodes_global global_refs by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>irq. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<notin> base_bits proof (prove)
using this:
\<forall>irq. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> global_refs' s
global_refs' s \<inter> base_bits = {}

goal (1 subgoal):
 1. \<forall>irq. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<notin> base_bits
theory Detype_R

lemma non_null_present:
  "cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) p s \<Longrightarrow> p \<notin> base_bits" apply (drule (1) if_unsafe_then_capD' [OF _ ifunsafe]) apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of
                  dest!: cte_refs_notRange simp del: atLeastAtMost_iff) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) p s \<Longrightarrow> p \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' (\<lambda>_. True) p s \<Longrightarrow> p \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>p \<in> cte_refs' (cteCap cte) (irq_node' s); cte_refs' (cteCap cte) (irq_node' s) \<inter> base_bits = {}; p \<in> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma cte_cap:
  "ex_cte_cap_to' p s \<Longrightarrow> ex_cte_cap_to' p state'" apply (clarsimp simp: ex_cte_cap_to'_def) apply (frule non_null_present [OF cte_wp_at_weakenE']) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' (\<lambda>_. True) p s \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p state' proof (prove)
goal (1 subgoal):
 1. \<And>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<and> (base \<le> cref \<longrightarrow> \<not> cref \<le> base + (2 ^ bits - 1)) proof (prove)
goal (2 subgoals):
 1. \<And>cref c. \<lbrakk>cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; p \<in> cte_refs' (cteCap c) (irq_node' s)\<rbrakk> \<Longrightarrow> cteCap c \<noteq> capability.NullCap
 2. \<And>cref. \<lbrakk>cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; cref \<notin> base_bits\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<and> (base \<le> cref \<longrightarrow> \<not> cref \<le> base + (2 ^ bits - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>cref. \<lbrakk>cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s; cref \<notin> base_bits\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<and> (base \<le> cref \<longrightarrow> \<not> cref \<le> base + (2 ^ bits - 1)) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma idle_notRange:
  "\<forall>cref. \<not> cte_wp_at' (\<lambda>c. ksIdleThread s \<in> capRange (cteCap c)) cref s
  \<Longrightarrow> ksIdleThread s \<notin> base_bits" apply (insert cap) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule_tac x=ptr in allE, clarsimp simp: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cref. \<not> cte_wp_at' (\<lambda>c. ksIdleThread s \<in> capRange (cteCap c)) cref s \<Longrightarrow> ksIdleThread s \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>cref. \<not> cte_wp_at' (\<lambda>c. ksIdleThread s \<in> capRange (cteCap c)) cref s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d base bits idx) ptr s\<rbrakk> \<Longrightarrow> ksIdleThread s \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>\<forall>cref cte. ctes_of s cref = Some cte \<longrightarrow> ksIdleThread s \<notin> capRange (cteCap cte); ctes_of s ptr = Some cte; cteCap cte = capability.UntypedCap d base bits idx; base \<le> ksIdleThread s; ksIdleThread s \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma map_to_ctesE[elim!]:
  "\<lbrakk> ctes' x = Some cte; \<lbrakk> ctes_of s x = Some cte; x \<notin> base_bits \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (clarsimp simp: tree_to_ctes split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes' x = Some cte; \<lbrakk>ctes_of s x = Some cte; x \<notin> base_bits\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Detype_R

lemma not_nullMDBNode:
  "\<lbrakk> ctes_of s x = Some cte; cteCap cte = NullCap; cteMDBNode cte = nullMDBNode \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" using nullcaps apply (cases cte) apply (simp add: valid_nullcaps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s x = Some cte; cteCap cte = capability.NullCap; cteMDBNode cte = nullMDBNode \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
valid_nullcaps (ctes_of s)

goal (1 subgoal):
 1. \<lbrakk>ctes_of s x = Some cte; cteCap cte = capability.NullCap; cteMDBNode cte = nullMDBNode \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>ctes_of s x = Some cte; cteCap cte = capability.NullCap; cteMDBNode cte = nullMDBNode \<Longrightarrow> P; valid_nullcaps (ctes_of s); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Detype_R

lemma mdb_src: "\<lbrakk> ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0 \<rbrakk> \<Longrightarrow> x \<notin> base_bits" apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0\<rbrakk> \<Longrightarrow> x \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; ctes_of s x = Some cte; y = mdbNext (cteMDBNode cte); cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>mdbNext (cteMDBNode cte) \<noteq> 0; y = mdbNext (cteMDBNode cte); cteCap cte = capability.NullCap; cteMDBNode cte = nullMDBNode\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma mdb_dest: "\<lbrakk> ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0 \<rbrakk> \<Longrightarrow> y \<notin> base_bits" apply (case_tac "x = 0") apply (insert no_0, simp add: next_unfold')[1] apply (drule(1) vdlist_nextD0 [OF _ _ dlist]) apply (rule non_null_present) apply (clarsimp simp: next_unfold' cte_wp_at_ctes_of mdb_prev_def) apply (erule(1) not_nullMDBNode) apply (simp add: nullMDBNode_def nullPointer_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0\<rbrakk> \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0; x = 0\<rbrakk> \<Longrightarrow> y \<notin> base_bits
 2. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> y; y \<noteq> 0; x \<noteq> 0\<rbrakk> \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> 0; x \<noteq> 0; ctes_of s \<turnstile> x \<leftarrow> y\<rbrakk> \<Longrightarrow> y \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> 0; x \<noteq> 0; ctes_of s \<turnstile> x \<leftarrow> y\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) y s proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>y \<noteq> 0; mdbPrev (cteMDBNode z) \<noteq> 0; ctes_of s y = Some z; x = mdbPrev (cteMDBNode z); cteCap z = capability.NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>y \<noteq> 0; mdbPrev (cteMDBNode z) \<noteq> 0; x = mdbPrev (cteMDBNode z); cteCap z = capability.NullCap; cteMDBNode z = nullMDBNode\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_R

lemma mdb_parent_notrange:
  "ctes_of s \<turnstile> x \<rightarrow> y \<Longrightarrow> x \<notin> base_bits \<and> y \<notin> base_bits" apply (erule subtree.induct) apply (frule(1) mdb_src, drule(1) mdb_dest, simp) apply (drule(1) mdb_dest, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s \<turnstile> x \<rightarrow> y \<Longrightarrow> x \<notin> base_bits \<and> y \<notin> base_bits proof (prove)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>ctes_of s \<turnstile> x \<leadsto> c'; c' \<noteq> 0; ctes_of s \<turnstile> x parentOf c'\<rbrakk> \<Longrightarrow> x \<notin> base_bits \<and> c' \<notin> base_bits
 2. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; x \<notin> base_bits \<and> c' \<notin> base_bits; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> x \<notin> base_bits \<and> c'' \<notin> base_bits proof (prove)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>ctes_of s \<turnstile> x \<rightarrow> c'; x \<notin> base_bits \<and> c' \<notin> base_bits; ctes_of s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; ctes_of s \<turnstile> x parentOf c''\<rbrakk> \<Longrightarrow> x \<notin> base_bits \<and> c'' \<notin> base_bits proof (prove)
goal:
No subgoals!
theory Detype_R

lemma trancl_next_rev:
  "ctes' \<turnstile> x \<leadsto>\<^sup>+ y \<Longrightarrow> ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y" apply (erule converse_trancl_induct) apply (rule r_into_trancl) apply (clarsimp simp: next_unfold') apply (rule_tac b=z in trancl_into_trancl2) apply (clarsimp simp: next_unfold') apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes' \<turnstile> x \<leadsto>\<^sup>+ y \<Longrightarrow> ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya. ctes' \<turnstile> ya \<leadsto> y \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto>\<^sup>+ y
 2. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya. ctes' \<turnstile> ya \<leadsto> y \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto> y
 2. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto>\<^sup>+ y proof (prove)
goal (2 subgoals):
 1. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> ya \<leadsto> z
 2. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal (1 subgoal):
 1. \<And>ya z. \<lbrakk>ctes' \<turnstile> ya \<leadsto> z; ctes' \<turnstile> z \<leadsto>\<^sup>+ y; ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> ctes_of s \<turnstile> z \<leadsto>\<^sup>+ y proof (prove)
goal:
No subgoals!
theory Detype_R

lemma exists_disj:
  "((\<exists>a. P a \<and> Q a)\<or>(\<exists>a. P a \<and> Q' a))
   = (\<exists>a. P a \<and> (Q a \<or> Q' a))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<exists>a. P a \<and> Q a) \<or> (\<exists>a. P a \<and> Q' a)) = (\<exists>a. P a \<and> (Q a \<or> Q' a))
theory Detype_R

lemma (in delete_locale) delete_ko_wp_at':
  assumes    objs: "ko_wp_at' P p s \<and> ex_nonz_cap_to' p s"
  shows      "ko_wp_at' P p state'" using objs by (clarsimp simp: ko_wp_at'_def ps_clear_def dom_if_None Diff_Int_distrib
    dest!: ex_nonz_cap_notRange)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p state' proof (prove)
using this:
ko_wp_at' P p s \<and> ex_nonz_cap_to' p s

goal (1 subgoal):
 1. ko_wp_at' P p state'
theory Detype_R

lemma (in delete_locale) delete_ex_cte_cap_to':
  assumes  exc: "ex_cte_cap_to' p s"
  shows    "ex_cte_cap_to' p state'" using exc by (clarsimp elim!: cte_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to' (\<lambda>_. True) p state' proof (prove)
using this:
ex_cte_cap_wp_to' (\<lambda>_. True) p s

goal (1 subgoal):
 1. ex_cte_cap_wp_to' (\<lambda>_. True) p state'
theory Detype_R

lemma deleteObjects_descendants:
  "\<lbrace>cte_wp_at' (\<lambda>c. cteCap c = UntypedCap d ptr bits idx) p
     and invs' and ct_active' and sch_act_simple
     and (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s))
     and (\<lambda>s. descendants_range_in' H p (ctes_of s))
     and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace>
  deleteObjects ptr bits
  \<lbrace>\<lambda>rv s.  descendants_range_in' H p (ctes_of s)\<rbrace>" apply (simp add:descendants_range_in'_def2) apply (wp deleteObjects_null_filter) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and (\<lambda>s. descendants_range_in' H p (ctes_of s)) and K (bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv s. descendants_range_in' H p (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and (\<lambda>s. \<forall>p'\<in>descendants_of' p (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> H = {}) and (\<lambda>y. bits < word_bits \<and> is_aligned ptr bits)\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv s. \<forall>p'\<in>descendants_of' p (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> H = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d ptr bits idx) p and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap d ptr bits idx) p (ctes_of s)) and (\<lambda>s. \<forall>p'\<in>descendants_of' p (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> H = {}) and (\<lambda>y. bits < word_bits \<and> is_aligned ptr bits)) s \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap ?d9 ptr bits ?idx9) ?p9 and invs' and ct_active' and sch_act_simple and (\<lambda>s. descendants_range' (capability.UntypedCap ?d9 ptr bits ?idx9) ?p9 (ctes_of s)) and (\<lambda>s. \<forall>p'\<in>descendants_of' p (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> H = {}) and K (bits < word_bits \<and> is_aligned ptr bits)) s proof (prove)
goal:
No subgoals!
theory Detype_R

lemma doMachineOp_modify:
  "doMachineOp (modify g) = modify (ksMachineState_update g)" apply (simp add: doMachineOp_def split_def select_f_returns) apply (rule ext) apply (simp add: simpler_gets_def simpler_modify_def bind_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (modify g) = modify (ksMachineState_update g) proof (prove)
goal (1 subgoal):
 1. do ms <- gets ksMachineState;
modify (ksMachineState_update (\<lambda>_. g ms))
od = modify (ksMachineState_update g) proof (prove)
goal (1 subgoal):
 1. \<And>x. (do ms <- gets ksMachineState;
modify (ksMachineState_update (\<lambda>_. g ms))
od) x = modify (ksMachineState_update g) x proof (prove)
goal:
No subgoals!