kings-crown/FVELER_Isabelle huggingface dataset:
theory SR_lemmas_C

lemma cmdbnode_relation_mdb_node_to_H [simp]:
  "cte_lift cte' = Some y
  \<Longrightarrow> cmdbnode_relation (mdb_node_to_H (cteMDBNode_CL y)) (cteMDBNode_C cte')" unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def by (fastforce split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_lift cte' = Some y \<Longrightarrow> cmdbnode_relation (mdb_node_to_H (cteMDBNode_CL y)) (cteMDBNode_C cte') proof (prove)
goal (1 subgoal):
 1. (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = \<lparr>mdbNext_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] << 0) && ~~ mask 3, mdbRevocable_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 1) && mask 1, mdbFirstBadged_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 0) && mask 1, mdbPrev_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[0] << 0) && ~~ mask 3\<rparr>\<rparr>) = Some y \<Longrightarrow> MDB (mdbNext_CL (cteMDBNode_CL y)) (mdbPrev_CL (cteMDBNode_CL y)) (to_bool (mdbRevocable_CL (cteMDBNode_CL y))) (to_bool (mdbFirstBadged_CL (cteMDBNode_CL y))) = MDB (mdbNext_CL \<lparr>mdbNext_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] << 0) && ~~ mask 3, mdbRevocable_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 1) && mask 1, mdbFirstBadged_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 0) && mask 1, mdbPrev_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[0] << 0) && ~~ mask 3\<rparr>) (mdbPrev_CL \<lparr>mdbNext_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] << 0) && ~~ mask 3, mdbRevocable_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 1) && mask 1, mdbFirstBadged_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 0) && mask 1, mdbPrev_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[0] << 0) && ~~ mask 3\<rparr>) (to_bool (mdbRevocable_CL \<lparr>mdbNext_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] << 0) && ~~ mask 3, mdbRevocable_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 1) && mask 1, mdbFirstBadged_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 0) && mask 1, mdbPrev_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[0] << 0) && ~~ mask 3\<rparr>)) (to_bool (mdbFirstBadged_CL \<lparr>mdbNext_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] << 0) && ~~ mask 3, mdbRevocable_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 1) && mask 1, mdbFirstBadged_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[1] >> 0) && mask 1, mdbPrev_CL = (mdb_node_C.words_C (cteMDBNode_C cte').[0] << 0) && ~~ mask 3\<rparr>))
theory SR_lemmas_C

lemma tcb_cte_cases_proj_eq [simp]:
  "tcb_cte_cases p = Some (getF, setF) \<Longrightarrow>
  tcb_no_ctes_proj tcb = tcb_no_ctes_proj (setF f tcb)" unfolding tcb_no_ctes_proj_def tcb_cte_cases_def by (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cte_cases p = Some (getF, setF) \<Longrightarrow> tcb_no_ctes_proj tcb = tcb_no_ctes_proj (setF f tcb) proof (prove)
goal (1 subgoal):
 1. [0 \<mapsto> (tcb.tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcb.tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcb.tcbReply, tcbReply_update), 0x30 \<mapsto> (tcb.tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] p = Some (getF, setF) \<Longrightarrow> (tcbState tcb, tcbFaultHandler tcb, tcbIPCBuffer tcb, tcbArch tcb, tcbQueued tcb, tcbMCP tcb, tcbPriority tcb, tcbDomain tcb, tcbTimeSlice tcb, tcbFault tcb, tcbBoundNotification tcb) = (tcbState (setF f tcb), tcbFaultHandler (setF f tcb), tcbIPCBuffer (setF f tcb), tcbArch (setF f tcb), tcbQueued (setF f tcb), tcbMCP (setF f tcb), tcbPriority (setF f tcb), tcbDomain (setF f tcb), tcbTimeSlice (setF f tcb), tcbFault (setF f tcb), tcbBoundNotification (setF f tcb))
theory SR_lemmas_C

lemma map_to_ctes_upd_tcb':
  "\<lbrakk> ksPSpace s p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits;
     ps_clear p tcbBlockSizeBits s \<rbrakk>
   \<Longrightarrow> map_to_ctes ((ksPSpace s)(p \<mapsto> KOTCB tcb)) =
       (\<lambda>x. if EX getF setF.
               tcb_cte_cases (x - p) = Some (getF, setF) &
               getF tcb \<noteq> getF tcb'
            then case tcb_cte_cases (x - p) of
               Some (getF, setF) \<Rightarrow> Some (getF tcb)
            else ctes_of s x)" apply (erule (1) map_to_ctes_upd_tcb) apply (simp add: field_simps ps_clear_def3 mask_def objBits_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> map_to_ctes ((ksPSpace s)(p \<mapsto> KOTCB tcb)) = (\<lambda>x. if \<exists>getF setF. tcb_cte_cases (x - p) = Some (getF, setF) \<and> getF tcb \<noteq> getF tcb' then case tcb_cte_cases (x - p) of Some (getF, setF) \<Rightarrow> Some (getF tcb) else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> {p + 1..p + mask tcbBlockSizeBits} \<inter> dom (ksPSpace s) = {} proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma in_alignCheck':
  "(z \<in> fst (alignCheck x n s)) = (snd z = s \<and> is_aligned x n)" by (cases z, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (z \<in> fst (alignCheck x n s)) = (snd z = s \<and> is_aligned x n)
theory SR_lemmas_C

lemma fst_alignCheck_empty [simp]:
   "(fst (alignCheck x n s) = {}) = (\<not> is_aligned x n)" apply (subst all_not_in_conv [symmetric]) apply (clarsimp simp: in_alignCheck') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (alignCheck x n s) = {}) = (\<not> is_aligned x n) proof (prove)
goal (1 subgoal):
 1. (\<forall>xa. xa \<notin> fst (alignCheck x n s)) = (\<not> is_aligned x n) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma pspace_alignedD' [intro?]:
  assumes  lu: "ksPSpace s x = Some v"
  and      al: "pspace_aligned' s"
  shows   "is_aligned x (objBitsKO v)" using al lu unfolding pspace_aligned'_def apply - apply (drule (1) bspec [OF _ domI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO v) proof (prove)
using this:
pspace_aligned' s
ksPSpace s x = Some v

goal (1 subgoal):
 1. is_aligned x (objBitsKO v) proof (prove)
using this:
\<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))
ksPSpace s x = Some v

goal (1 subgoal):
 1. is_aligned x (objBitsKO v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x))); ksPSpace s x = Some v\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; is_aligned x (objBitsKO (the (ksPSpace s x)))\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ctes_of_ksI [intro?]:
  fixes s :: "kernel_state"
  assumes ks: "ksPSpace s x = Some (KOCTE cte)"
  and     pa: "pspace_aligned' s"
  and     pd: "pspace_distinct' s"
  shows   "ctes_of s x = Some cte" proof (rule ctes_of_eq_cte_wp_at') from ks show "cte_wp_at' ((=) cte) x s" proof (rule cte_wp_at_cteI' [OF _ _ _ refl]) from ks pa have "is_aligned x (objBitsKO (KOCTE cte))" .. thus "is_aligned x cte_level_bits" unfolding cte_level_bits_def by (simp add: objBits_simps') from ks pd have "ps_clear x (objBitsKO (KOCTE cte)) s" .. thus "ps_clear x cte_level_bits s" unfolding cte_level_bits_def by (simp add: objBits_simps') qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s x = Some cte proof (state)
goal (1 subgoal):
 1. cte_wp_at' ((=) cte) x s proof (chain)
picking this:
ksPSpace s x = Some (KOCTE cte) proof (prove)
using this:
ksPSpace s x = Some (KOCTE cte)

goal (1 subgoal):
 1. cte_wp_at' ((=) cte) x s proof (state)
goal (2 subgoals):
 1. is_aligned x cte_level_bits
 2. ps_clear x cte_level_bits s proof (chain)
picking this:
ksPSpace s x = Some (KOCTE cte)
pspace_aligned' s proof (prove)
using this:
ksPSpace s x = Some (KOCTE cte)
pspace_aligned' s

goal (1 subgoal):
 1. is_aligned x (objBitsKO (KOCTE cte)) proof (state)
this:
is_aligned x (objBitsKO (KOCTE cte))

goal (2 subgoals):
 1. is_aligned x cte_level_bits
 2. ps_clear x cte_level_bits s proof (prove)
using this:
is_aligned x (objBitsKO (KOCTE cte))

goal (1 subgoal):
 1. is_aligned x cte_level_bits proof (prove)
using this:
is_aligned x (objBitsKO (KOCTE cte))

goal (1 subgoal):
 1. is_aligned x 4 proof (state)
this:
is_aligned x cte_level_bits

goal (1 subgoal):
 1. ps_clear x cte_level_bits s proof (chain)
picking this:
ksPSpace s x = Some (KOCTE cte)
pspace_distinct' s proof (prove)
using this:
ksPSpace s x = Some (KOCTE cte)
pspace_distinct' s

goal (1 subgoal):
 1. ps_clear x (objBitsKO (KOCTE cte)) s proof (state)
this:
ps_clear x (objBitsKO (KOCTE cte)) s

goal (1 subgoal):
 1. ps_clear x cte_level_bits s proof (prove)
using this:
ps_clear x (objBitsKO (KOCTE cte)) s

goal (1 subgoal):
 1. ps_clear x cte_level_bits s proof (prove)
using this:
ps_clear x (objBitsKO (KOCTE cte)) s

goal (1 subgoal):
 1. ps_clear x 4 s proof (state)
this:
ps_clear x cte_level_bits s

goal:
No subgoals! proof (state)
this:
cte_wp_at' ((=) cte) x s

goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_domE1:
  "\<lbrakk> f ` dom am = dom cm; am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (drule equalityD1) apply (drule subsetD) apply (erule imageI [OF domI]) apply (clarsimp simp: dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom cm; am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P; f ` dom am \<subseteq> dom cm\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> ?c2 \<in> f ` dom am
 2. \<lbrakk>am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P; ?c2 \<in> dom cm\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P; f x \<in> dom cm\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_domE2:
  "\<lbrakk> f ` dom am = dom cm; cm x = Some v'; \<And>x' v. \<lbrakk> x = f x'; am x' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (drule equalityD2) apply (drule subsetD) apply (erule domI) apply (clarsimp simp: dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom cm; cm x = Some v'; \<And>x' v. \<lbrakk>x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cm x = Some v'; \<And>x' v. \<lbrakk>x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P; dom cm \<subseteq> f ` dom am\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cm x = Some v'; \<And>x' v. \<lbrakk>x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> ?c2 \<in> dom cm
 2. \<lbrakk>cm x = Some v'; \<And>x' v. \<lbrakk>x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P; ?c2 \<in> f ` dom am\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cm x = Some v'; \<And>x' v. \<lbrakk>x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P; x \<in> f ` dom am\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_relationE2:
  "\<lbrakk> cmap_relation am cm f rel; cm x = Some y';
  \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" unfolding cmap_relation_def apply clarsimp apply (erule (1) cmap_domE2) apply (drule (1) bspec [OF _ domI]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm f rel; cm x = Some y'; \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); cm x = Some y'; \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cm x = Some y'; \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P; f ` dom am = dom cm; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>x' v. \<lbrakk>cm x = Some y'; \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P; \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))); x = f x'; am x' = Some v\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>x' v. \<lbrakk>cm x = Some y'; \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P; x = f x'; am x' = Some v; rel (the (am x')) (the (cm (f x')))\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_relationI:
  assumes doms:  "f ` dom am = dom cm"
  and     rel:   "\<And>x v v'. \<lbrakk>am x = Some v; cm (f x) = Some v' \<rbrakk> \<Longrightarrow> rel v v'"
  shows "cmap_relation am cm f rel" unfolding cmap_relation_def using doms proof (rule conjI) show "\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))" proof fix x assume "x \<in> dom am" then obtain v where "am x = Some v" .. moreover with doms obtain v' where "cm (f x) = Some v'" by (rule cmap_domE1) ultimately show "rel (the (am x)) (the (cm (f x)))" by (simp add: rel) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation am cm f rel proof (prove)
goal (1 subgoal):
 1. f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))) proof (prove)
using this:
f ` dom am = dom cm

goal (1 subgoal):
 1. f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))) proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))) proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x))) proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (state)
this:
x \<in> dom am

goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (chain)
picking this:
x \<in> dom am proof (prove)
using this:
x \<in> dom am

goal (1 subgoal):
 1. (\<And>v. am x = Some v \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
am x = Some v

goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (state)
this:
am x = Some v

goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (chain)
picking this:
f ` dom am = dom cm
am x = Some v proof (prove)
using this:
f ` dom am = dom cm
am x = Some v

goal (1 subgoal):
 1. (\<And>v'. cm (f x) = Some v' \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
cm (f x) = Some v'

goal (1 subgoal):
 1. \<And>x. x \<in> dom am \<Longrightarrow> rel (the (am x)) (the (cm (f x))) proof (chain)
picking this:
am x = Some v
cm (f x) = Some v' proof (prove)
using this:
am x = Some v
cm (f x) = Some v'

goal (1 subgoal):
 1. rel (the (am x)) (the (cm (f x))) proof (state)
this:
rel (the (am x)) (the (cm (f x)))

goal:
No subgoals! proof (state)
this:
\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))

goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_relation_relI:
  assumes "cmap_relation am cm f rel"
  and     "am x = Some v"
  and     "cm (f x) = Some v'"
  shows "rel v v'" using assms by (fastforce elim!: cmap_relationE1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel v v' proof (prove)
using this:
cmap_relation am cm f rel
am x = Some v
cm (f x) = Some v'

goal (1 subgoal):
 1. rel v v'
theory SR_lemmas_C

lemma cspace_cte_relationE:
  "\<lbrakk> cmap_relation am cm Ptr ccte_relation; am x = Some y;
  \<And>z k'. \<lbrakk>cm (Ptr x) = Some k'; cte_lift k' = Some z; cte_to_H z = y; c_valid_cte k' \<rbrakk> \<Longrightarrow> P
  \<rbrakk> \<Longrightarrow> P" apply (erule (1) cmap_relationE1) apply (clarsimp simp: ccte_relation_def map_option_Some_eq2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm cte_Ptr ccte_relation; am x = Some y; \<And>z k'. \<lbrakk>cm (cte_Ptr x) = Some k'; cte_lift k' = Some z; cte_to_H z = y; c_valid_cte k'\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>am x = Some y; \<And>z k'. \<lbrakk>cm (cte_Ptr x) = Some k'; cte_lift k' = Some z; cte_to_H z = y; c_valid_cte k'\<rbrakk> \<Longrightarrow> P; am x = Some y; ccte_relation y y'; cm (cte_Ptr x) = Some y'\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmdbnode_relationE:
  "\<lbrakk>cmdbnode_relation m v; m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" unfolding cmdbnode_relation_def apply (drule sym) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmdbnode_relation m v; m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = mdb_node_to_H (mdb_node_lift v); m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P; mdb_node_to_H (mdb_node_lift v) = m\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_relation_updI:
  fixes am :: "word32 \<rightharpoonup> 'a" and cm :: "'b typ_heap"
  assumes cr: "cmap_relation am cm f rel"
  and   cof: "am dest = Some v"
  and   cl:  "cm (f dest) = Some v'"
  and   cc:  "rel nv nv'"
  and   inj: "inj f"
  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel" using cr cof cl cc apply (rule cmap_relation_upd_relI) apply simp apply fact done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel proof (prove)
using this:
cmap_relation am cm f rel
am dest = Some v
cm (f dest) = Some v'
rel nv nv'

goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel proof (prove)
goal (2 subgoals):
 1. \<And>x ov ov'. \<lbrakk>x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov'\<rbrakk> \<Longrightarrow> rel ov ov'
 2. inj f proof (prove)
goal (1 subgoal):
 1. inj f proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cte_to_H_mdb_node_update [simp]:
  "cte_to_H (cteMDBNode_CL_update (\<lambda>_. m) cte) =
  cteMDBNode_update (\<lambda>_. mdb_node_to_H  m) (cte_to_H cte)" unfolding cte_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_to_H (cte\<lparr>cteMDBNode_CL := m\<rparr>) = cteMDBNode_update (\<lambda>_. mdb_node_to_H m) (cte_to_H cte) proof (prove)
goal (1 subgoal):
 1. CTE (cap_to_H (cap_CL (cte\<lparr>cteMDBNode_CL := m\<rparr>))) (mdb_node_to_H (cteMDBNode_CL (cte\<lparr>cteMDBNode_CL := m\<rparr>))) = cteMDBNode_update (\<lambda>_. mdb_node_to_H m) (CTE (cap_to_H (cap_CL cte)) (mdb_node_to_H (cteMDBNode_CL cte)))
theory SR_lemmas_C

lemma cspace_cte_relation_upd_mdbI:
  assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation"
  and   cof: "map_to_ctes am dest = Some cte"
  and   cl:  "clift cm (Ptr dest) = Some cte'"
  and   cc:  "cmdbnode_relation mdbl m"
  shows "cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte))
  ((clift cm)(Ptr dest \<mapsto> cte_C.cteMDBNode_C_update (\<lambda>_. m) cte')) Ptr ccte_relation" using cr cof cl cc apply - apply (frule (2) cmap_relation_relI) apply (erule (2) cmap_relation_updI) apply (clarsimp elim!: cmdbnode_relationE
           simp: map_comp_Some_iff ccte_relation_def c_valid_cte_def cl_valid_cte_def map_option_Some_eq2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cteMDBNode_C_update (\<lambda>_. m) cte')) cte_Ptr ccte_relation proof (prove)
using this:
cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation
map_to_ctes am dest = Some cte
clift cm (cte_Ptr dest) = Some cte'
cmdbnode_relation mdbl m

goal (1 subgoal):
 1. cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cteMDBNode_C_update (\<lambda>_. m) cte')) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation; map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; cmdbnode_relation mdbl m\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cteMDBNode_C_update (\<lambda>_. m) cte')) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation; map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; cmdbnode_relation mdbl m; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cteMDBNode_C_update (\<lambda>_. m) cte')) cte_Ptr ccte_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; cmdbnode_relation mdbl m; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> ccte_relation (cteMDBNode_update (\<lambda>_. mdbl) cte) (cteMDBNode_C_update (\<lambda>_. m) cte')
 2. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; cmdbnode_relation mdbl m; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; cmdbnode_relation mdbl m; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma mdb_node_to_H_mdbPrev_update[simp]:
  "mdb_node_to_H (mdbPrev_CL_update (\<lambda>_. x) m)
  = mdbPrev_update (\<lambda>_. x) (mdb_node_to_H m)" unfolding mdb_node_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_node_to_H (m\<lparr>mdbPrev_CL := x\<rparr>) = mdbPrev_update (\<lambda>_. x) (mdb_node_to_H m) proof (prove)
goal (1 subgoal):
 1. MDB (mdbNext_CL (m\<lparr>mdbPrev_CL := x\<rparr>)) (mdbPrev_CL (m\<lparr>mdbPrev_CL := x\<rparr>)) (to_bool (mdbRevocable_CL (m\<lparr>mdbPrev_CL := x\<rparr>))) (to_bool (mdbFirstBadged_CL (m\<lparr>mdbPrev_CL := x\<rparr>))) = mdbPrev_update (\<lambda>_. x) (MDB (mdbNext_CL m) (mdbPrev_CL m) (to_bool (mdbRevocable_CL m)) (to_bool (mdbFirstBadged_CL m)))
theory SR_lemmas_C

lemma mdb_node_to_H_mdbRevocable_update[simp]:
  "mdb_node_to_H (mdbRevocable_CL_update (\<lambda>_. x) m)
  = mdbRevocable_update (\<lambda>_. to_bool x) (mdb_node_to_H m)" unfolding mdb_node_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_node_to_H (m\<lparr>mdbRevocable_CL := x\<rparr>) = mdbRevocable_update (\<lambda>_. to_bool x) (mdb_node_to_H m) proof (prove)
goal (1 subgoal):
 1. MDB (mdbNext_CL (m\<lparr>mdbRevocable_CL := x\<rparr>)) (mdbPrev_CL (m\<lparr>mdbRevocable_CL := x\<rparr>)) (to_bool (mdbRevocable_CL (m\<lparr>mdbRevocable_CL := x\<rparr>))) (to_bool (mdbFirstBadged_CL (m\<lparr>mdbRevocable_CL := x\<rparr>))) = mdbRevocable_update (\<lambda>_. to_bool x) (MDB (mdbNext_CL m) (mdbPrev_CL m) (to_bool (mdbRevocable_CL m)) (to_bool (mdbFirstBadged_CL m)))