theory Recycle_C

lemma page_table_at_rf_sr_dom_s:
  "\<lbrakk> page_table_at' x s; (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> {x ..+ 2 ^ ptBits} \<times> {SIndexVal, SIndexTyp 0}
    \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" apply (rule_tac m=2 in intvl_2_power_times_decomp,
         simp_all add: shiftl_t2n field_simps ptBits_def pageBits_def
                       word_bits_def pteBits_def) apply (clarsimp simp: page_table_at'_def intvl_def) apply (drule spec, drule(1) mp) apply (simp add: typ_at_to_obj_at_arches) apply (drule obj_at_ko_at', clarsimp) apply (erule cmap_relationE1[OF rf_sr_cpte_relation]) apply (erule ko_at_projectKO_opt) apply (drule h_t_valid_clift) apply (drule h_t_valid_dom_s[OF _ refl refl]) apply (erule subsetD) apply (auto simp add: intvl_def shiftl_t2n)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' x s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> {x..+2 ^ ptBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' x s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<forall>y<0x100. {x + y * 4..+4} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k. \<lbrakk>(s, s') \<in> rf_sr; is_aligned x ptBits; \<forall>y<0x100. pte_at' (x + (y << 2)) s; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k. \<lbrakk>(s, s') \<in> rf_sr; is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; pte_at' (x + (y << 2)) s\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k. \<lbrakk>(s, s') \<in> rf_sr; is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; obj_at' (\<lambda>_. True) (x + (y << 2)) s\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k ko. \<lbrakk>(s, s') \<in> rf_sr; is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (2 subgoals):
 1. \<And>y b k ko. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s\<rbrakk> \<Longrightarrow> map_to_ptes (ksPSpace s) (?x22 y b k ko) = Some (?y22 y b k ko)
 2. \<And>y b k ko y'. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s; map_to_ptes (ksPSpace s) (?x22 y b k ko) = Some (?y22 y b k ko); cpte_relation (?y22 y b k ko) y'; cslift s' (pte_Ptr (?x22 y b k ko)) = Some y'\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k ko y'. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s; map_to_ptes (ksPSpace s) (x + (y << 2)) = Some ko; cpte_relation ko y'; cslift s' (pte_Ptr (x + (y << 2))) = Some y'\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k ko y'. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s; map_to_ptes (ksPSpace s) (x + (y << 2)) = Some ko; cpte_relation ko y'; s' \<Turnstile>\<^sub>c pte_Ptr (x + (y << 2))\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k ko y'. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s; map_to_ptes (ksPSpace s) (x + (y << 2)) = Some ko; cpte_relation ko y'; ptr_span (pte_Ptr (x + (y << 2))) \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y b k ko y'. \<lbrakk>is_aligned x ptBits; y < 0x100; b = SIndexVal \<or> b = SIndexTyp 0; k < 4; ko_at' ko (x + (y << 2)) s; map_to_ptes (ksPSpace s) (x + (y << 2)) = Some ko; cpte_relation ko y'\<rbrakk> \<Longrightarrow> (x + y * 4 + word_of_nat k, b) \<in> ptr_span (pte_Ptr (x + (y << 2))) \<times> {SIndexVal, SIndexTyp 0} proof (prove)
goal:
No subgoals!