kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma src_next [simp]:
  "m \<turnstile> src \<leadsto> mdbNext src_node" by (simp add: next_unfold' src)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto> mdbNext src_node
theory CSpace_R

lemma dest_no_trancl_target [simp]:
  "m \<turnstile> x \<leadsto>\<^sup>+ dest = False" by (clarsimp dest!: tranclD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ dest = False
theory CSpace_R

lemma dest_loop:
  "n \<turnstile> dest \<rightarrow> dest = False" apply clarsimp apply (drule subtree_mdb_next) apply (drule mdb_next_from_dest) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> dest = False proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<rightarrow> dest \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<leadsto>\<^sup>+ dest \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. m \<turnstile> src \<leadsto>\<^sup>+ dest \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma descendants:
  "descendants_of' p m' =
  (if p = src
   then {}
   else if p = dest
   then descendants_of' src m
   else descendants_of' p m - {src} \<union>
        (if src \<in> descendants_of' p m then {dest} else {}))" apply (rule set_eqI) apply (simp add: descendants_of'_def m'_def) apply (auto simp: subtree_m_n intro: subtree_src_dest subtree_dest_src no_src_subtree_n_m) apply (auto simp: subtree_n_m) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p m' = (if p = src then {} else if p = dest then descendants_of' src m else descendants_of' p m - {src} \<union> (if src \<in> descendants_of' p m then {dest} else {})) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p m') = (x \<in> (if p = src then {} else if p = dest then descendants_of' src m else descendants_of' p m - {src} \<union> (if src \<in> descendants_of' p m then {dest} else {}))) proof (prove)
goal (1 subgoal):
 1. \<And>x. (m \<turnstile> p \<rightarrow> src \<longrightarrow> (p = dest \<longrightarrow> n \<turnstile> dest \<rightarrow> x = m \<turnstile> src \<rightarrow> x) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = (m \<turnstile> p \<rightarrow> x \<and> x \<noteq> src \<or> x = dest))) \<and> (\<not> m \<turnstile> p \<rightarrow> src \<longrightarrow> (p = dest \<longrightarrow> n \<turnstile> dest \<rightarrow> x = m \<turnstile> src \<rightarrow> x) \<and> (p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = (m \<turnstile> p \<rightarrow> x \<and> x \<noteq> src))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>m \<turnstile> p \<rightarrow> src; p \<noteq> dest; p \<noteq> src; n \<turnstile> p \<rightarrow> x; x \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> x proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateCap_dynamic_duo:
  "\<lbrakk> (rv, s') \<in> fst (updateCap x cap s); pspace_aligned' s; pspace_distinct' s \<rbrakk>
       \<Longrightarrow> pspace_aligned' s' \<and> pspace_distinct' s'" unfolding updateCap_def apply (rule conjI) apply (erule use_valid | wp | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(rv, s') \<in> fst (updateCap x cap s); pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_aligned' s' \<and> pspace_distinct' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(rv, s') \<in> fst ((do cte <- getCTE x;
setCTE x (cteCap_update (\<lambda>_. cap) cte)
od) s); pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_aligned' s' \<and> pspace_distinct' s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(rv, s') \<in> fst ((do cte <- getCTE x;
setCTE x (cteCap_update (\<lambda>_. cap) cte)
od) s); pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<lbrakk>(rv, s') \<in> fst ((do cte <- getCTE x;
setCTE x (cteCap_update (\<lambda>_. cap) cte)
od) s); pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> pspace_distinct' s' proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma next_slot_eq2:
  "\<lbrakk>case n q of None \<Rightarrow> next_slot p t' m' = x | Some q' \<Rightarrow> next_slot p (t'' q') (m'' q') = x;
    case n q of None \<Rightarrow> (t' = t \<and> m' = m) | Some q' \<Rightarrow> t'' q' = t \<and> m'' q' = m\<rbrakk>
    \<Longrightarrow> next_slot p t m = x" apply(simp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case n q of None \<Rightarrow> next_slot p t' m' = x | Some q' \<Rightarrow> next_slot p (t'' q') (m'' q') = x; case n q of None \<Rightarrow> t' = t \<and> m' = m | Some q' \<Rightarrow> t'' q' = t \<and> m'' q' = m\<rbrakk> \<Longrightarrow> next_slot p t m = x proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma valid_bitmapQ_lift:
  assumes prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  and     prqL1: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
  and     prqL2: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
  shows   "\<lbrace>Invariants_H.valid_bitmapQ\<rbrace> f \<lbrace>\<lambda>_. Invariants_H.valid_bitmapQ\<rbrace>" unfolding valid_bitmapQ_def bitmapQ_def apply (wp hoare_vcg_all_lift) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> f \<lbrace>\<lambda>_. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>d p. \<lbrace>?P2 d p\<rbrace> f \<lbrace>\<lambda>rv s. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace>
 2. \<And>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []) \<Longrightarrow> \<forall>x xa. ?P2 x xa s proof (prove)
goal (2 subgoals):
 1. \<And>d p prev_s. \<lbrace>?P3 d p prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. (ksReadyQueuesL1Bitmap prev_s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap prev_s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues prev_s (d, p) \<noteq> [])\<rbrace>
 2. \<And>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> []) \<Longrightarrow> \<forall>x xa. ?P3 x xa s s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma bitmapQ_no_L1_orphans_lift:
  assumes prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  and     prqL1: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
  and     prqL2: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
  shows   "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> f \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" unfolding valid_bitmapQ_def bitmapQ_def bitmapQ_no_L1_orphans_def apply (wp hoare_vcg_all_lift) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> f \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>d i. \<lbrace>?P2 d i\<rbrace> f \<lbrace>\<lambda>rv s. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace>
 2. \<And>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize \<Longrightarrow> \<forall>x xa. ?P2 x xa s proof (prove)
goal (2 subgoals):
 1. \<And>d i prev_s. \<lbrace>?P3 d i prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. ksReadyQueuesL1Bitmap prev_s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap prev_s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace>
 2. \<And>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize \<Longrightarrow> \<forall>x xa. ?P3 x xa s s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma bitmapQ_no_L2_orphans_lift:
  assumes prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  and     prqL1: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
  and     prqL2: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
  shows   "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> f \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" unfolding valid_bitmapQ_def bitmapQ_def bitmapQ_no_L2_orphans_def apply (wp hoare_vcg_all_lift) apply (wps prq prqL1 prqL2) apply (rule hoare_vcg_prop, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L2_orphans\<rbrace> f \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>d i j. \<lbrace>?P3 d i j\<rbrace> f \<lbrace>\<lambda>rv s. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i\<rbrace>
 2. \<And>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i \<Longrightarrow> \<forall>x xa xb. ?P3 x xa xb s proof (prove)
goal (2 subgoals):
 1. \<And>d i j prev_s. \<lbrace>?P4 d i j prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. ksReadyQueuesL2Bitmap prev_s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap prev_s d !! i\<rbrace>
 2. \<And>s. \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize \<longrightarrow> ksReadyQueuesL1Bitmap s d !! i \<Longrightarrow> \<forall>x xa xb. ?P4 x xa xb s s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma valid_queues_lift':
  assumes tat: "\<And>d p tcb. \<lbrace>\<lambda>s. \<not> obj_at' (inQ d p) tcb s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> obj_at' (inQ d p) tcb s\<rbrace>"
  and     prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>"
  shows   "\<lbrace>valid_queues'\<rbrace> f \<lbrace>\<lambda>_. valid_queues'\<rbrace>" unfolding valid_queues'_def imp_conv_disj by (wp hoare_vcg_all_lift hoare_vcg_disj_lift tat prq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> f \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace>
theory CSpace_R

lemma setCTE_norq [wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueues s) \<rbrace>" by (clarsimp simp: valid_def dest!: setCTE_pspace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueues s)\<rbrace>
theory CSpace_R

lemma setCTE_norqL1 [wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueuesL1Bitmap s) \<rbrace>" by (clarsimp simp: valid_def dest!: setCTE_pspace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueuesL1Bitmap s)\<rbrace>
theory CSpace_R

lemma setCTE_norqL2 [wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueuesL2Bitmap s) \<rbrace>" by (clarsimp simp: valid_def dest!: setCTE_pspace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> setCTE ptr cte \<lbrace>\<lambda>r s. P (ksReadyQueuesL2Bitmap s)\<rbrace>
theory CSpace_R

lemma setObject_cte_ct:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject t (v::cte) \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" by (clarsimp simp: valid_def setCTE_def[symmetric] dest!: setCTE_pspace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>
theory CSpace_R

lemma n_src_dest:
  "n \<turnstile> src \<leadsto> dest" by (simp add: n_direct_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<leadsto> dest
theory CSpace_R

lemma dest_chain_0 [simp, intro!]:
  "n \<turnstile> dest \<leadsto>\<^sup>+ 0" using chain_n n_dest by (simp add: mdb_chain_0_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> dest \<leadsto>\<^sup>+ 0 proof (prove)
using this:
mdb_chain_0 n
n dest = Some new_dest

goal (1 subgoal):
 1. n \<turnstile> dest \<leadsto>\<^sup>+ 0
theory CSpace_R

lemma n_trancl_eq:
  "n \<turnstile> p \<leadsto>\<^sup>+ p' =
  (if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src
   else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p'
   else m \<turnstile> p \<leadsto>\<^sup>+ p')" by (auto simp add: n_trancl_eq' rtrancl_eq_or_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = (if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p')
theory CSpace_R

lemma n_rtrancl_eq:
  "n \<turnstile> p \<leadsto>\<^sup>* p' =
  (if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src
   else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p'
   else m \<turnstile> p \<leadsto>\<^sup>* p')" by (auto simp: n_trancl_eq rtrancl_eq_or_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>* p' = (if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' else m \<turnstile> p \<leadsto>\<^sup>* p')
theory CSpace_R

lemma n_cap:
  "n p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node')
          else m p = Some (CTE cap node')" by (simp add: n src dest new_src_def new_dest_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node')
theory CSpace_R

lemma m_cap:
  "m p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then cap = dest_cap \<and> n p = Some (CTE c' node')
          else n p = Some (CTE cap node')" apply (simp add: n new_src_def new_dest_def) apply (cases "p=dest") apply (auto simp: src dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then cap = dest_cap \<and> n p = Some (CTE c' node') else n p = Some (CTE cap node') proof (prove)
goal (1 subgoal):
 1. m p = Some (CTE cap node) \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (p = dest \<longrightarrow> cap = dest_cap \<and> mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)) = node') \<and> (p \<noteq> dest \<longrightarrow> node = node'))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some (CTE cap node); p = dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (p = dest \<longrightarrow> cap = dest_cap \<and> mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)) = node') \<and> (p \<noteq> dest \<longrightarrow> node = node')))
 2. \<lbrakk>m p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> src_cap = cap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. (p = dest \<longrightarrow> cap = dest_cap \<and> mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)) = node') \<and> (p \<noteq> dest \<longrightarrow> node = node'))) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma chunked_m:
  "mdb_chunked m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. mdb_chunked m
theory CSpace_R

lemma derived_region1 [simp]:
  "badge_derived' c' src_cap \<Longrightarrow>
  sameRegionAs c' cap = sameRegionAs src_cap cap" by (clarsimp simp add: badge_derived'_def sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. badge_derived' c' src_cap \<Longrightarrow> global.sameRegionAs c' cap = global.sameRegionAs src_cap cap
theory CSpace_R

lemma derived_region2 [simp]:
  "badge_derived' c' src_cap \<Longrightarrow>
  sameRegionAs cap c' = sameRegionAs cap src_cap" by (clarsimp simp add: badge_derived'_def sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. badge_derived' c' src_cap \<Longrightarrow> global.sameRegionAs cap c' = global.sameRegionAs cap src_cap
theory CSpace_R

lemma untyped_c':
  "untypedRange c' = untypedRange src_cap"
  "isUntypedCap c' = isUntypedCap src_cap" using partial_is_derived' apply - apply (case_tac "isUntypedCap src_cap") by (clarsimp simp:isCap_simps freeIndex_update_def is_derived'_def
       badge_derived'_def capMasterCap_def split:if_splits capability.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange c' = untypedRange src_cap &&& isUntypedCap c' = isUntypedCap src_cap proof (prove)
using this:
is_derived' m src c' src_cap

goal (1 subgoal):
 1. untypedRange c' = untypedRange src_cap &&& isUntypedCap c' = isUntypedCap src_cap proof (prove)
goal (2 subgoals):
 1. is_derived' m src c' src_cap \<Longrightarrow> untypedRange c' = untypedRange src_cap
 2. is_derived' m src c' src_cap \<Longrightarrow> isUntypedCap c' = isUntypedCap src_cap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_derived' m src c' src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> untypedRange c' = untypedRange src_cap
 2. \<lbrakk>is_derived' m src c' src_cap; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> untypedRange c' = untypedRange src_cap
 3. is_derived' m src c' src_cap \<Longrightarrow> isUntypedCap c' = isUntypedCap src_cap
theory CSpace_R

lemma capRange_c':
  "capRange c' = capRange src_cap" using partial_is_derived' untyped_c' apply - apply (case_tac "isUntypedCap src_cap") apply (clarsimp simp:untypedCapRange) apply (rule master_eqI, rule capRange_Master) apply simp apply (rule arg_cong) apply (auto simp:isCap_simps freeIndex_update_def is_derived'_def
       badge_derived'_def capMasterCap_def split:if_splits capability.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange c' = capRange src_cap proof (prove)
using this:
is_derived' m src c' src_cap
untypedRange c' = untypedRange src_cap
isUntypedCap c' = isUntypedCap src_cap

goal (1 subgoal):
 1. capRange c' = capRange src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; isUntypedCap c' = isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange c' = capRange src_cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; isUntypedCap c' = isUntypedCap src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange c' = capRange src_cap
 2. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; isUntypedCap c' = isUntypedCap src_cap; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange c' = capRange src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; isUntypedCap c' = isUntypedCap src_cap; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange c' = capRange src_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; isUntypedCap c' = isUntypedCap src_cap; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange (capMasterCap c') = capRange (capMasterCap src_cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; \<not> isUntypedCap c'; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange (capMasterCap c') = capRange (capMasterCap src_cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived' m src c' src_cap; untypedRange c' = untypedRange src_cap; \<not> isUntypedCap c'; \<not> isUntypedCap src_cap\<rbrakk> \<Longrightarrow> capRange (capMasterCap c') = capRange (capMasterCap src_cap) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma untyped_no_parent:
  "isUntypedCap src_cap \<Longrightarrow> \<not> m \<turnstile> src \<rightarrow> p" using partial_is_derived' untyped_c' by (clarsimp simp: is_derived'_def isCap_simps freeIndex_update_def descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap src_cap \<Longrightarrow> \<not> m \<turnstile> src \<rightarrow> p proof (prove)
using this:
is_derived' m src c' src_cap
untypedRange c' = untypedRange src_cap
isUntypedCap c' = isUntypedCap src_cap

goal (1 subgoal):
 1. isUntypedCap src_cap \<Longrightarrow> \<not> m \<turnstile> src \<rightarrow> p