theory SR_lemmas_C

lemma page_table_at_carray_map_relation:
  "\<lbrakk> page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp \<rbrakk>
    \<Longrightarrow> clift hp (pt_Ptr pt) \<noteq> None" apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) apply (drule spec, erule iffD1) apply (clarsimp simp: page_table_at'_def) apply (drule_tac x="p' && mask ptBits >> 2" in spec) apply (clarsimp simp: shiftr_shiftl1) apply (drule mp) apply (simp add: shiftr_over_and_dist ptBits_def pageBits_def mask_def
                    order_le_less_trans[OF word_and_le1] pteBits_def) apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def
                        is_aligned_andI1 add.commute word_plus_and_or_coroll2
                        pteBits_def
                 dest!: obj_at_ko_at' ko_at_projectKO_opt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp\<rbrakk> \<Longrightarrow> clift hp (pt_Ptr pt) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' pt s; \<forall>p. (is_aligned p ptBits \<and> (\<forall>p'. p' && ~~ mask ptBits = p \<and> is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))) \<longrightarrow> p' \<in> dom (map_to_ptes (ksPSpace s)))) = (\<exists>v. clift hp (pt_Ptr p) = Some v)\<rbrakk> \<Longrightarrow> \<exists>y. clift hp (pt_Ptr pt) = Some y proof (prove)
goal (1 subgoal):
 1. page_table_at' pt s \<Longrightarrow> is_aligned pt ptBits \<and> (\<forall>p'. p' && ~~ mask ptBits = pt \<and> is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))) \<longrightarrow> p' \<in> dom (map_to_ptes (ksPSpace s))) proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>\<forall>y<0x100. pte_at' ((p' && ~~ mask ptBits) + (y << 2)) s; is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ptes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits; p' && mask ptBits >> 2 < 0x100 \<longrightarrow> pte_at' ((p' && ~~ mask ptBits) + (p' && mask ptBits >> 2 << 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ptes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits; p' && mask ptBits >> 2 < 0x100 \<longrightarrow> pte_at' ((p' && ~~ mask ptBits) + ((p' && mask ptBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ptes (ksPSpace s) p' = Some y proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits\<rbrakk> \<Longrightarrow> p' && mask ptBits >> 2 < 0x100
 2. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits; pte_at' ((p' && ~~ mask ptBits) + ((p' && mask ptBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ptes (ksPSpace s) p' = Some y proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>is_aligned p' (objBits (the (map_to_ptes (ksPSpace s) p'))); pt = p' && ~~ mask ptBits; pte_at' ((p' && ~~ mask ptBits) + ((p' && mask ptBits) && ~~ mask 2)) s\<rbrakk> \<Longrightarrow> \<exists>y. map_to_ptes (ksPSpace s) p' = Some y proof (prove)
goal:
No subgoals!