theory SR_lemmas_C

lemma page_directory_at_carray_map_relation:
  "\<lbrakk> page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp \<rbrakk>
    \<Longrightarrow> clift hp (pd_Ptr pd) \<noteq> None" apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) apply (drule spec, erule iffD1) apply (clarsimp simp: page_directory_at'_def) apply (drule_tac x="p' && mask pdBits >> 2" in spec) apply (clarsimp simp: shiftr_shiftl1) apply (drule mp) apply (simp add: shiftr_over_and_dist pdBits_def pageBits_def mask_def
                    order_le_less_trans[OF word_and_le1] pdeBits_def) apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def
                        is_aligned_andI1 add.commute word_plus_and_or_coroll2
                        pdeBits_def
                 dest!: obj_at_ko_at' ko_at_projectKO_opt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp\<rbrakk> \<Longrightarrow> clift hp (pd_Ptr pd) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_directory_at' pd s; \<forall>p. (is_aligned p pdBits \<and> (\<forall>p'. p' && ~~ mask pdBits = p \<and> is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))) \<longrightarrow> p' \<in> dom (map_to_pdes (ksPSpace s)))) = (\<exists>v. clift hp (pd_Ptr p) = Some v)\<rbrakk> \<Longrightarrow> \<exists>y. clift hp (pd_Ptr pd) = Some y proof (prove)
goal (1 subgoal):
 1. page_directory_at' pd s \<Longrightarrow> is_aligned pd pdBits \<and> (\<forall>p'. p' && ~~ mask pdBits = pd \<and> is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))) \<longrightarrow> p' \<in> dom (map_to_pdes (ksPSpace s))) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>\<forall>y<0x1000. pde_at' ((p' && ~~ mask pdBits) + (y << 2)) s; is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> \<exists>y. map_to_pdes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits; p' && mask pdBits >> 2 < 0x1000 \<longrightarrow> pde_at' ((p' && ~~ mask pdBits) + (p' && mask pdBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_pdes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits; p' && mask pdBits >> 2 < 0x1000 \<longrightarrow> pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_pdes (ksPSpace s) p' = Some y proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits\<rbrakk> \<Longrightarrow> p' && mask pdBits >> 2 < 0x1000
 2. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_pdes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_pdes (ksPSpace s) p'))); pd = p' && ~~ mask pdBits; pde_at' ((p' && ~~ mask pdBits) + ((p' && mask pdBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_pdes (ksPSpace s) p' = Some y proof (prove)
goal:
No subgoals!