kings-crown/FVELER_Isabelle huggingface dataset:
theory SR_lemmas_C

lemma rf_sr_heap_device_data_relation:
  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation
      (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s)))
      (cslift s') Ptr cuser_user_data_device_relation" by (clarsimp simp: user_word_at_def rf_sr_def
                     cstate_relation_def Let_def
                     cpspace_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation
theory SR_lemmas_C

lemma cap_get_tag_isCap_ArchObject:
  assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'"
  shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap"
  and "(cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap"
  and "(cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap"
  and "(cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap"
  and "(cap_get_tag cap' = scast cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = ARMSmallPage)"
  and "(cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> ARMSmallPage)" using cap_get_tag_isCap_ArchObject0 [OF cr] by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage) proof (prove)
using this:
(cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) \<and> (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage)

goal (1 subgoal):
 1. ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_control_cap) = isASIDControlCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = isASIDPoolCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = isPageTableCap cap) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = isPageDirectoryCap cap &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isPageCap cap \<and> capVPSize cap = Wellformed_C.ARMSmallPage) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isPageCap cap \<and> capVPSize cap \<noteq> Wellformed_C.ARMSmallPage)
theory SR_lemmas_C

lemma cap_get_tag_isCap_ArchObject2_worker:
  "\<lbrakk> \<And>cap''. ccap_relation (ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap'';
                ccap_relation cap cap'; isArchCap_tag n \<rbrakk>
        \<Longrightarrow> (cap_get_tag cap' = n)
              = (isArchObjectCap cap \<and> P (capCap cap))" apply (rule iffI) apply (clarsimp simp: cap_get_tag_isCap isCap_simps) apply (clarsimp simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap''. ccap_relation (capability.ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap''; ccap_relation cap cap'; isArchCap_tag n\<rbrakk> \<Longrightarrow> (cap_get_tag cap' = n) = (isArchObjectCap cap \<and> P (capCap cap)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>cap''. ccap_relation (capability.ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap''; ccap_relation cap cap'; isArchCap_tag n; cap_get_tag cap' = n\<rbrakk> \<Longrightarrow> isArchObjectCap cap \<and> P (capCap cap)
 2. \<lbrakk>\<And>cap''. ccap_relation (capability.ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap''; ccap_relation cap cap'; isArchCap_tag n; isArchObjectCap cap \<and> P (capCap cap)\<rbrakk> \<Longrightarrow> cap_get_tag cap' = n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap''. ccap_relation (capability.ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap''; ccap_relation cap cap'; isArchCap_tag n; isArchObjectCap cap \<and> P (capCap cap)\<rbrakk> \<Longrightarrow> cap_get_tag cap' = n proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma cap_get_tag_isCap_ArchObject2:
  assumes cr: "ccap_relation cap cap'"
  shows "(cap_get_tag cap' = scast cap_page_directory_cap)
           = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap))"
  and   "(cap_get_tag cap' = scast cap_asid_pool_cap)
           = (isArchObjectCap cap \<and> isASIDPoolCap (capCap cap))"
  and   "(cap_get_tag cap' = scast cap_page_table_cap)
           = (isArchObjectCap cap \<and> isPageTableCap (capCap cap))"
  and   "(cap_get_tag cap' = scast cap_small_frame_cap)
           = (isArchObjectCap cap \<and> isPageCap (capCap cap) \<and> capVPSize (capCap cap) = ARMSmallPage)"
  and   "(cap_get_tag cap' = scast cap_frame_cap)
           = (isArchObjectCap cap \<and> isPageCap (capCap cap) \<and> capVPSize (capCap cap) \<noteq> ARMSmallPage)" by (rule cap_get_tag_isCap_ArchObject2_worker [OF _ cr],
      simp add: cap_get_tag_isCap_ArchObject,
      simp add: isArchCap_tag_def2 cap_tag_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap) = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap)) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_asid_pool_cap) = (isArchObjectCap cap \<and> isASIDPoolCap (capCap cap))) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap) = (isArchObjectCap cap \<and> isPageTableCap (capCap cap)) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) = (isArchObjectCap cap \<and> isPageCap (capCap cap) \<and> capVPSize (capCap cap) = Wellformed_C.ARMSmallPage) &&& (cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) = (isArchObjectCap cap \<and> isPageCap (capCap cap) \<and> capVPSize (capCap cap) \<noteq> Wellformed_C.ARMSmallPage)
theory SR_lemmas_C

lemma rf_sr_armKSGlobalPD:
  "(s, s') \<in> rf_sr \<Longrightarrow> armKSGlobalPD (ksArchState s) = ptr_val armKSGlobalPD_Ptr" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> armKSGlobalPD (ksArchState s) = ptr_val armKSGlobalPD_Ptr
theory SR_lemmas_C

lemma ghost_assertion_size_logic':
  "unat (sz :: word32) \<le> gsMaxObjectSize s
    \<Longrightarrow> cstate_relation s gs
    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs) = 0 \<or>
            sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def ghost_size_rel_def
                     linorder_not_le word_less_nat_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat sz \<le> gsMaxObjectSize s; cstate_relation s gs\<rbrakk> \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs) = 0 \<or> sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs)
theory SR_lemmas_C

lemma ghost_assertion_size_logic:
  "unat (sz :: word32) \<le> gsMaxObjectSize s
    \<Longrightarrow> (s, \<sigma>) \<in> rf_sr
    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or>
            sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>))" by (clarsimp simp: rf_sr_def ghost_assertion_size_logic')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat sz \<le> gsMaxObjectSize s; (s, \<sigma>) \<in> rf_sr\<rbrakk> \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or> sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>))
theory SR_lemmas_C

lemma gs_set_assn_Delete_cstate_relation:
  "cstate_relation s (ghost'state_'_update (gs_set_assn cteDeleteOne_'proc v) gs)
    = cstate_relation s gs" apply (cases "ghost'state_' gs") by (auto simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def
                 cmachine_state_relation_def ghost_assertion_data_set_def
                 ghost_size_rel_def ghost_assertion_data_get_def
                 cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cstate_relation s (ghost'state_'_update (gs_set_assn cteDeleteOne_'proc v) gs) = cstate_relation s gs proof (prove)
goal (1 subgoal):
 1. \<And>a b c. ghost'state_' gs = (a, b, c) \<Longrightarrow> cstate_relation s (ghost'state_'_update (gs_set_assn cteDeleteOne_'proc v) gs) = cstate_relation s gs
theory SR_lemmas_C

lemma ptr_val_tcb_ptr_mask:
  "obj_at' (P :: tcb \<Rightarrow> bool) thread s
      \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits)
                  = thread" apply (clarsimp simp: obj_at'_def tcb_ptr_to_ctcb_ptr_def projectKOs) apply (simp add: is_aligned_add_helper ctcb_offset_defs objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P thread s \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && ~~ mask tcbBlockSizeBits = thread proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s thread = Some (KOTCB obj); is_aligned thread (objBitsKO (KOTCB obj)); P obj; ps_clear thread (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> thread + ctcb_offset && ~~ mask tcbBlockSizeBits = thread proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma typ_uinfo_t_diff_from_typ_name:
  "typ_name (typ_info_t TYPE ('a :: c_type)) \<noteq> typ_name (typ_info_t TYPE('b :: c_type))
    \<Longrightarrow> typ_uinfo_t (aty :: 'a itself) \<noteq> typ_uinfo_t (bty :: 'b itself)" by (clarsimp simp: typ_uinfo_t_def td_diff_from_typ_name)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_name (typ_info_t TYPE('a)) \<noteq> typ_name (typ_info_t TYPE('b)) \<Longrightarrow> typ_uinfo_t aty \<noteq> typ_uinfo_t bty
theory SR_lemmas_C

lemma page_directory_at_rf_sr:
   "\<lbrakk> page_directory_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> cslift s' (pd_Ptr pd) \<noteq> None" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                     cpspace_relation_def page_directory_at_carray_map_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' pd s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> cslift s' (pd_Ptr pd) \<noteq> None
theory SR_lemmas_C

lemma page_table_at_rf_sr:
   "\<lbrakk> page_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> cslift s' (Ptr pd :: (pte_C[256]) ptr) \<noteq> None" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                     cpspace_relation_def page_table_at_carray_map_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' pd s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> cslift s' (pt_Ptr pd) \<noteq> None
theory SR_lemmas_C

lemma ctes_of_untyped_zero_rf_sr:
  "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
      untyped_ranges_zero' s;
      untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk>
    \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" apply (erule gsUntypedZeroRanges_rf_sr[rotated]) apply (clarsimp simp: untyped_ranges_zero_inv_def) apply (rule_tac a=p in ranI) apply (simp add: map_comp_def cteCaps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s; untypedZeroRange (cteCap cte) = Some (start, end)\<rbrakk> \<Longrightarrow> region_actually_is_bytes start (unat (end + 1 - start)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; untyped_ranges_zero' s; untypedZeroRange (cteCap cte) = Some (start, end)\<rbrakk> \<Longrightarrow> (start, end) \<in> gsUntypedZeroRanges s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); untypedZeroRange (cteCap cte) = Some (start, end)\<rbrakk> \<Longrightarrow> (start, end) \<in> ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; gsUntypedZeroRanges s = ran (untypedZeroRange \<circ>\<^sub>m cteCaps_of s); untypedZeroRange (cteCap cte) = Some (start, end)\<rbrakk> \<Longrightarrow> (untypedZeroRange \<circ>\<^sub>m cteCaps_of s) p = Some (start, end) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma heap_list_is_zero_mono:
  "heap_list_is_zero hmem p n \<Longrightarrow> n' \<le> n
    \<Longrightarrow> heap_list_is_zero hmem p n'" apply (induct n arbitrary: n' p) apply simp apply clarsimp apply (case_tac n', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list hmem n p = replicate n 0; n' \<le> n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0 proof (prove)
goal (2 subgoals):
 1. \<And>n' p. \<lbrakk>heap_list hmem 0 p = replicate 0 0; n' \<le> 0\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0
 2. \<And>n n' p. \<lbrakk>\<And>n' p. \<lbrakk>heap_list hmem n p = replicate n 0; n' \<le> n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0; heap_list hmem (Suc n) p = replicate (Suc n) 0; n' \<le> Suc n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0 proof (prove)
goal (1 subgoal):
 1. \<And>n n' p. \<lbrakk>\<And>n' p. \<lbrakk>heap_list hmem n p = replicate n 0; n' \<le> n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0; heap_list hmem (Suc n) p = replicate (Suc n) 0; n' \<le> Suc n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0 proof (prove)
goal (1 subgoal):
 1. \<And>n n' p. \<lbrakk>\<And>n' p. \<lbrakk>heap_list hmem n p = replicate n 0; n' \<le> n\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0; n' \<le> Suc n; hmem p = 0; heap_list hmem n (p + 1) = replicate n 0\<rbrakk> \<Longrightarrow> heap_list hmem n' p = replicate n' 0 proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma heap_list_h_eq_better:
  "\<And>p. \<lbrakk> x \<in> {p..+q}; heap_list h q p = heap_list h' q p \<rbrakk>
      \<Longrightarrow> h x = h' x" proof (induct q) case 0 thus ?case by simp next case (Suc n) thus ?case by (force dest: intvl_neq_start) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>x \<in> {p..+0}; heap_list h 0 p = heap_list h' 0 p\<rbrakk> \<Longrightarrow> h x = h' x
 2. \<And>q p. \<lbrakk>\<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x; x \<in> {p..+Suc q}; heap_list h (Suc q) p = heap_list h' (Suc q) p\<rbrakk> \<Longrightarrow> h x = h' x proof (state)
this:
x \<in> {p..+0}
heap_list h 0 p = heap_list h' 0 p

goal (2 subgoals):
 1. \<And>p. \<lbrakk>x \<in> {p..+0}; heap_list h 0 p = heap_list h' 0 p\<rbrakk> \<Longrightarrow> h x = h' x
 2. \<And>q p. \<lbrakk>\<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x; x \<in> {p..+Suc q}; heap_list h (Suc q) p = heap_list h' (Suc q) p\<rbrakk> \<Longrightarrow> h x = h' x proof (prove)
using this:
x \<in> {p..+0}
heap_list h 0 p = heap_list h' 0 p

goal (1 subgoal):
 1. h x = h' x proof (state)
this:
h x = h' x

goal (1 subgoal):
 1. \<And>q p. \<lbrakk>\<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x; x \<in> {p..+Suc q}; heap_list h (Suc q) p = heap_list h' (Suc q) p\<rbrakk> \<Longrightarrow> h x = h' x proof (state)
goal (1 subgoal):
 1. \<And>q p. \<lbrakk>\<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x; x \<in> {p..+Suc q}; heap_list h (Suc q) p = heap_list h' (Suc q) p\<rbrakk> \<Longrightarrow> h x = h' x proof (state)
this:
\<lbrakk>x \<in> {?p..+n}; heap_list h n ?p = heap_list h' n ?p\<rbrakk> \<Longrightarrow> h x = h' x
x \<in> {p..+Suc n}
heap_list h (Suc n) p = heap_list h' (Suc n) p

goal (1 subgoal):
 1. \<And>q p. \<lbrakk>\<And>p. \<lbrakk>x \<in> {p..+q}; heap_list h q p = heap_list h' q p\<rbrakk> \<Longrightarrow> h x = h' x; x \<in> {p..+Suc q}; heap_list h (Suc q) p = heap_list h' (Suc q) p\<rbrakk> \<Longrightarrow> h x = h' x proof (prove)
using this:
\<lbrakk>x \<in> {?p..+n}; heap_list h n ?p = heap_list h' n ?p\<rbrakk> \<Longrightarrow> h x = h' x
x \<in> {p..+Suc n}
heap_list h (Suc n) p = heap_list h' (Suc n) p

goal (1 subgoal):
 1. h x = h' x proof (state)
this:
h x = h' x

goal:
No subgoals!
theory SR_lemmas_C

lemma heap_list_is_zero_mono2:
  "heap_list_is_zero hmem p n
    \<Longrightarrow> {p' ..+ n'} \<le> {p ..+ n}
    \<Longrightarrow> heap_list_is_zero hmem p' n'" using heap_list_h_eq2[where h'="\<lambda>_. 0"]
      heap_list_h_eq_better[where h'="\<lambda>_. 0"] apply (simp(no_asm_use) add: heap_list_rpbs) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list hmem n p = replicate n 0; {p'..+n'} \<subseteq> {p..+n}\<rbrakk> \<Longrightarrow> heap_list hmem n' p' = replicate n' 0 proof (prove)
using this:
(\<And>x. x \<in> {?p..+?n} \<Longrightarrow> ?h x = 0) \<Longrightarrow> heap_list ?h ?n ?p = heap_list (\<lambda>_. 0) ?n ?p
\<lbrakk>?x \<in> {?p..+?q}; heap_list ?h ?q ?p = heap_list (\<lambda>_. 0) ?q ?p\<rbrakk> \<Longrightarrow> ?h ?x = 0

goal (1 subgoal):
 1. \<lbrakk>heap_list hmem n p = replicate n 0; {p'..+n'} \<subseteq> {p..+n}\<rbrakk> \<Longrightarrow> heap_list hmem n' p' = replicate n' 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list hmem n p = replicate n 0; {p'..+n'} \<subseteq> {p..+n}; \<And>p n h. (\<And>x. x \<in> {p..+n} \<Longrightarrow> h x = 0) \<Longrightarrow> heap_list h n p = replicate n 0; \<And>x p q h. \<lbrakk>x \<in> {p..+q}; heap_list h q p = replicate q 0\<rbrakk> \<Longrightarrow> h x = 0\<rbrakk> \<Longrightarrow> heap_list hmem n' p' = replicate n' 0 proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma invs_urz[elim!]:
  "invs' s \<Longrightarrow> untyped_ranges_zero' s" by (clarsimp simp: invs'_def valid_state'_def)

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

lemma rf_sr_sched_action_relation:
  "(s, s') \<in> rf_sr
   \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))
theory SR_lemmas_C

lemma numDomains_sge_1_simp:
  "1 <s Kernel_C.numDomains \<longleftrightarrow> Suc 0 < Kernel_Config.numDomains" apply (simp add: word_sless_alt sint_numDomains_to_H) apply (subst nat_less_as_int, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (1 <s Kernel_C.numDomains) = (Suc 0 < numDomains) proof (prove)
goal (1 subgoal):
 1. (1 < int numDomains) = (Suc 0 < numDomains) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma unat_scast_numDomains:
  "unat (SCAST(32 signed \<rightarrow> machine_word_len) Kernel_C.numDomains) = unat Kernel_C.numDomains" by (simp add: scast_eq sint_numDomains_to_H unat_numDomains_to_H numDomains_machine_word_safe)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.numDomains) = unat Kernel_C.numDomains
theory SR_lemmas_C

lemma msgRegisters_size_sanity:
  "size_msgRegisters = unat (n_msgRegisters)" by (simp add: n_msgRegisters_def size_msgRegisters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size_msgRegisters = unat n_msgRegisters
theory SR_lemmas_C

lemma physBase_spec:
  "\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }" apply (rule allI, rule conseqPre, vcg) apply (simp add: Kernel_Config.physBase_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc \<lbrace>\<acute>ret__unsigned_long = physBase\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>SCAST(32 signed \<rightarrow> 32) 0x10000000 = physBase\<rbrace> proof (prove)
goal:
No subgoals!
theory Corres_C

lemma ccorres_cases:
  assumes "P \<Longrightarrow> ccorres_underlying srel Ga rrel xf arrel axf G G' hs a b"
  assumes "\<not>P \<Longrightarrow> ccorres_underlying srel Ga rrel xf arrel axf H H' hs  a b"
  shows "ccorres_underlying srel Ga rrel xf arrel axf
                            (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s))
                            ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'}) hs
                            a b" by (cases P, auto simp: assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel Ga rrel xf arrel axf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not> P \<longrightarrow> H s)) ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not> P \<longrightarrow> s \<in> H'}) hs a b