kings-crown/FVELER_Isabelle huggingface dataset:
theory SR_lemmas_C

lemma rf_sr_upd_safe[simp]:
  assumes rl: "(t_hrs_' (globals (g y))) = (t_hrs_' (globals y))"
  and     rq: "(ksReadyQueues_' (globals (g y))) = (ksReadyQueues_' (globals y))"
  and     rqL1: "(ksReadyQueuesL1Bitmap_' (globals (g y))) = (ksReadyQueuesL1Bitmap_' (globals y))"
  and     rqL2: "(ksReadyQueuesL2Bitmap_' (globals (g y))) = (ksReadyQueuesL2Bitmap_' (globals y))"
  and     sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))"
  and     ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))"
  and     it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))"
  and     isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)"
  and     ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)"
  and     dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)"
  and     cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)"
  and     dt: "ksDomainTime_' (globals (g y)) = ksDomainTime_' (globals y)"
  and arch:
    "armKSHWASIDTable_' (globals (g y)) = armKSHWASIDTable_' (globals y)"
    "armKSASIDTable_' (globals (g y)) = armKSASIDTable_' (globals y)"
    "armKSNextASID_' (globals (g y)) = armKSNextASID_' (globals y)"
    "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)"
  and    gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)"
  and     wu:  "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))"
  shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)" using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, g y) \<in> rf_sr) = ((a, y) \<in> rf_sr) proof (prove)
using this:
t_hrs_' (globals (g y)) = t_hrs_' (globals y)
ksReadyQueues_' (globals (g y)) = ksReadyQueues_' (globals y)
ksReadyQueuesL1Bitmap_' (globals (g y)) = ksReadyQueuesL1Bitmap_' (globals y)
ksReadyQueuesL2Bitmap_' (globals (g y)) = ksReadyQueuesL2Bitmap_' (globals y)
ksSchedulerAction_' (globals (g y)) = ksSchedulerAction_' (globals y)
ksCurThread_' (globals (g y)) = ksCurThread_' (globals y)
ksIdleThread_' (globals (g y)) = ksIdleThread_' (globals y)
intStateIRQNode_' (globals (g y)) = intStateIRQNode_' (globals y)
intStateIRQTable_' (globals (g y)) = intStateIRQTable_' (globals y)
armKSHWASIDTable_' (globals (g y)) = armKSHWASIDTable_' (globals y)
armKSASIDTable_' (globals (g y)) = armKSASIDTable_' (globals y)
armKSNextASID_' (globals (g y)) = armKSNextASID_' (globals y)
phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)
ksWorkUnitsCompleted_' (globals (g y)) = ksWorkUnitsCompleted_' (globals y)
ghost'state_' (globals (g y)) = ghost'state_' (globals y)
ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)
ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)
ksDomainTime_' (globals (g y)) = ksDomainTime_' (globals y)

goal (1 subgoal):
 1. ((a, g y) \<in> rf_sr) = ((a, y) \<in> rf_sr)
theory SR_lemmas_C

lemma rf_sr_cte_at_valid:
  "\<lbrakk> cte_wp_at' P (ptr_val p) s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (p :: cte_C ptr)" apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule (1) rf_sr_ctes_of_clift) apply (clarsimp simp add: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P (ptr_val p) s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s (ptr_val p) = Some cte; P cte\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>ctes_of s (ptr_val p) = Some cte; P cte; \<exists>cte'. cslift s' (cte_Ptr (ptr_val p)) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c p proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma rf_sr_cte_at_validD:
  "\<lbrakk> cte_wp_at' P p s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (Ptr p :: cte_C ptr)" by (simp add: rf_sr_cte_at_valid)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c cte_Ptr p
theory SR_lemmas_C

lemma ccap_relation_NullCap_iff:
  "(ccap_relation NullCap cap') = (cap_get_tag cap' = scast cap_null_cap)" unfolding ccap_relation_def apply (clarsimp simp: map_option_Some_eq2 c_valid_cap_def cl_valid_cap_def
            cap_to_H_def cap_lift_def Let_def cap_tag_defs split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation capability.NullCap cap' = (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) proof (prove)
goal (1 subgoal):
 1. (Some capability.NullCap = map_option cap_to_H (cap_lift cap') \<and> c_valid_cap cap') = (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_null_cap) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ko_at_valid_ntfn':
  "\<lbrakk> ko_at' ntfn p s; valid_objs' s \<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s" apply (erule obj_atE') apply (erule (1) valid_objsE') apply (simp add: projectKOs valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>valid_objs' s; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = ntfn; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = ntfn; ps_clear p (objBitsKO ko) s; valid_obj' ko s\<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cmap_relation_ko_atE:
  fixes ko :: "'a :: pspace_storable" and  mp :: "word32 \<rightharpoonup> 'a"
  assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel"
  and     ko: "ko_at' ko ptr s"
  and     rl: "\<And>ko'. \<lbrakk>cslift s' (f ptr) = Some ko'; rel ko ko'\<rbrakk> \<Longrightarrow> P"
  shows   P using ps ko apply - apply (drule (1) cmap_relation_ko_atD) apply (clarsimp) apply (erule (1) rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
cmap_relation (projectKO_opt \<circ>\<^sub>m ksPSpace s) (cslift s') f rel
ko_at' ko ptr s

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (projectKO_opt \<circ>\<^sub>m ksPSpace s) (cslift s') f rel; ko_at' ko ptr s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko ptr s; \<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko'\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ko_at' ko ptr s; cslift s' (f ptr) = Some ko'; rel ko ko'\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma map_to_tcbs_from_tcb_at:
  "tcb_at' thread s \<Longrightarrow> map_to_tcbs (ksPSpace s) thread \<noteq> None" unfolding obj_at'_def by (clarsimp simp: projectKOs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' thread s \<Longrightarrow> map_to_tcbs (ksPSpace s) thread \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<exists>ko obj. ksPSpace s thread = Some ko \<and> is_aligned thread (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> True \<and> ps_clear thread (objBitsKO ko) s \<Longrightarrow> map_to_tcbs (ksPSpace s) thread \<noteq> None
theory SR_lemmas_C

lemma st_tcb_at_h_t_valid:
  "\<lbrakk> st_tcb_at' P thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread" apply (drule pred_tcb_at') apply (erule (1) tcb_at_h_t_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' P thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma exs_getObject:
  assumes x: "\<And>q n ko. loadObject p q n ko =
                (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s"
  shows      "\<lbrace>(=) s\<rbrace> getObject p \<exists>\<lbrace>\<lambda>r :: ('a :: pspace_storable). (=) s\<rbrace>" using objat unfolding exs_valid_def obj_at'_def apply clarsimp apply (rule_tac x = "(the (projectKO_opt ko), s)" in bexI) apply (clarsimp simp: split_def) apply (simp add: projectKO_def fail_def split: option.splits) apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1
                        split_def x P lookupAround2_char1 projectKOs
                        objBits_def[symmetric] in_magnitude_check project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> getObject p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. \<lbrace>(=) s\<rbrace> getObject p \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
using this:
\<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s

goal (1 subgoal):
 1. \<forall>sa. s = sa \<longrightarrow> (\<exists>(rv, s')\<in>fst (getObject p sa). s = s') proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (getObject p s). case x of (rv, x) \<Rightarrow> s = x proof (prove)
goal (2 subgoals):
 1. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> case (the (projectKO_opt ko), s) of (rv, x) \<Rightarrow> s = x
 2. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (the (projectKO_opt ko), s) \<in> fst (getObject p s) proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (the (projectKO_opt ko), s) \<in> fst (getObject p s) proof (prove)
goal (1 subgoal):
 1. \<And>ko obj x2. \<lbrakk>P obj; ps_clear p (objBitsKO ko) s; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); projectKO_opt ko = Some x2; fst (return x2 s) = {(obj, s)}\<rbrakk> \<Longrightarrow> (x2, s) \<in> fst (getObject p s) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma getObject_eq:
  fixes ko :: "'a :: pspace_storable"
  assumes x: "\<And>q n ko. loadObject p q n ko =
                (loadObject_default p q n ko :: 'a kernel)"
  assumes P: "\<And>(v::'a). (1 :: word32) < 2 ^ (objBits v)"
  and objat: "ko_at' ko p s"
  shows      "(ko, s) \<in> fst (getObject p s)" using objat unfolding exs_valid_def obj_at'_def apply clarsimp apply (simp add: projectKO_def fail_def split: option.splits) apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1
                        split_def x P lookupAround2_char2 projectKOs
                        objBits_def[symmetric] in_magnitude_check project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ko, s) \<in> fst (getObject p s) proof (prove)
using this:
ko_at' ko p s

goal (1 subgoal):
 1. (ko, s) \<in> fst (getObject p s) proof (prove)
using this:
\<exists>koa obj. ksPSpace s p = Some koa \<and> is_aligned p (objBitsKO koa) \<and> fst (projectKO koa s) = {(obj, s)} \<and> obj = ko \<and> ps_clear p (objBitsKO koa) s

goal (1 subgoal):
 1. (ko, s) \<in> fst (getObject p s) proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); fst (projectKO koa s) = {(ko, s)}; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> (ko, s) \<in> fst (getObject p s) proof (prove)
goal (1 subgoal):
 1. \<And>koa x2. \<lbrakk>ps_clear p (objBitsKO koa) s; ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); projectKO_opt koa = Some x2; fst (return x2 s) = {(ko, s)}\<rbrakk> \<Longrightarrow> (ko, s) \<in> fst (getObject p s) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma null_sched_queue:
  "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'
  \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'" apply (rule ext) apply (erule_tac x = x in map_option_comp_eqE) apply simp apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_sched_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp' proof (prove)
goal (1 subgoal):
 1. \<And>x. map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>mp x = None; mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x
 2. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_sched_ptrs v = tcb_null_sched_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma null_ep_queue:
  "map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp'
  \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'" apply (rule ext) apply (erule_tac x = x in map_option_comp_eqE) apply simp apply (case_tac v, case_tac v') apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_ep_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp' \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp' proof (prove)
goal (1 subgoal):
 1. \<And>x. map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp' \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>mp x = None; mp' x = None\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x
 2. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_ep_ptrs v = tcb_null_ep_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal (1 subgoal):
 1. \<And>x v v'. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_ep_ptrs v = tcb_null_ep_ptrs v'\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal (1 subgoal):
 1. \<And>x v v' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>mp x = Some v; mp' x = Some v'; tcb_null_ep_ptrs v = tcb_null_ep_ptrs v'; v = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; v' = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> (map_option tcb_null_queue_ptrs \<circ> mp) x = (map_option tcb_null_queue_ptrs \<circ> mp') x proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ctcb_relation_null_queue_ptrs:
  assumes rel: "cmap_relation mp mp' tcb_ptr_to_ctcb_ptr ctcb_relation"
  and same: "map_option tcb_null_queue_ptrs \<circ> mp'' = map_option tcb_null_queue_ptrs \<circ> mp'"
  shows "cmap_relation mp mp'' tcb_ptr_to_ctcb_ptr ctcb_relation" using rel apply (rule iffD1 [OF cmap_relation_cong, OF _ map_option_eq_dom_eq, rotated -1]) apply simp apply (rule same [symmetric]) apply (drule compD [OF same]) apply (case_tac b, case_tac b') apply (simp add: ctcb_relation_def tcb_null_queue_ptrs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation mp mp'' tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
using this:
cmap_relation mp mp' tcb_ptr_to_ctcb_ptr ctcb_relation

goal (1 subgoal):
 1. cmap_relation mp mp'' tcb_ptr_to_ctcb_ptr ctcb_relation proof (prove)
goal (3 subgoals):
 1. dom mp = dom mp
 2. map_option ?f2 \<circ> mp' = map_option ?f2 \<circ> mp''
 3. \<And>p a a' b b'. \<lbrakk>mp p = Some a; mp p = Some a'; mp' (tcb_ptr_to_ctcb_ptr p) = Some b; mp'' (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (2 subgoals):
 1. map_option ?f2 \<circ> mp' = map_option ?f2 \<circ> mp''
 2. \<And>p a a' b b'. \<lbrakk>mp p = Some a; mp p = Some a'; mp' (tcb_ptr_to_ctcb_ptr p) = Some b; mp'' (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. \<And>p a a' b b'. \<lbrakk>mp p = Some a; mp p = Some a'; mp' (tcb_ptr_to_ctcb_ptr p) = Some b; mp'' (tcb_ptr_to_ctcb_ptr p) = Some b'\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. \<And>p a a' b b'. \<lbrakk>mp p = Some a; mp p = Some a'; mp' (tcb_ptr_to_ctcb_ptr p) = Some b; map_option tcb_null_queue_ptrs (mp' (tcb_ptr_to_ctcb_ptr p)) = map_option tcb_null_queue_ptrs (Some b')\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal (1 subgoal):
 1. \<And>p a a' b b' x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a. \<lbrakk>mp p = Some a; mp p = Some a'; mp' (tcb_ptr_to_ctcb_ptr p) = Some b; map_option tcb_null_queue_ptrs (mp' (tcb_ptr_to_ctcb_ptr p)) = map_option tcb_null_queue_ptrs (Some b'); b = tcb_C.tcb_C x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15; b' = tcb_C.tcb_C x1a x2a x3a x4a x5a x6a x7a x8a x9a x10a x11a x12a x13a x14a x15a\<rbrakk> \<Longrightarrow> ctcb_relation a b = ctcb_relation a' b' proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ntfnQueue_tail_mask_4 [simp]:
  "ntfnQueue_tail_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_tail_CL (notification_lift ko')" unfolding notification_lift_def by (clarsimp simp: mask_def word_bw_assocs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfnQueue_tail_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_tail_CL (notification_lift ko') proof (prove)
goal (1 subgoal):
 1. ntfnQueue_tail_CL \<lparr>ntfnBoundTCB_CL = (notification_C.words_C ko'.[3] << 0) && ~~ mask 4, ntfnMsgIdentifier_CL = notification_C.words_C ko'.[2] >> 0, ntfnQueue_head_CL = (notification_C.words_C ko'.[1] << 0) && ~~ mask 4, ntfnQueue_tail_CL = (notification_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (notification_C.words_C ko'.[0] >> 0) && mask 2\<rparr> && ~~ mask 4 = ntfnQueue_tail_CL \<lparr>ntfnBoundTCB_CL = (notification_C.words_C ko'.[3] << 0) && ~~ mask 4, ntfnMsgIdentifier_CL = notification_C.words_C ko'.[2] >> 0, ntfnQueue_head_CL = (notification_C.words_C ko'.[1] << 0) && ~~ mask 4, ntfnQueue_tail_CL = (notification_C.words_C ko'.[0] << 0) && ~~ mask 4, state_CL = (notification_C.words_C ko'.[0] >> 0) && mask 2\<rparr>
theory SR_lemmas_C

lemma update_ntfn_map_tos:
  fixes P :: "Structures_H.notification \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_eps ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_eps (ksPSpace s)"
  and     "map_to_tcbs ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_tcbs (ksPSpace s)"
  and     "map_to_ctes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_ctes (ksPSpace s)"
  and     "map_to_pdes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_pdes (ksPSpace s)"
  and     "map_to_ptes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_ptes (ksPSpace s)"
  and     "map_to_asidpools ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_asidpools (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_eps ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_eps (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KONotification ko)) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((map_to_eps ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_eps (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KONotification ko)) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KONotification ko)) = map_to_user_data_device (ksPSpace s)