theory VSpace_R

lemma valid_duplicates'_non_pd_pt_I:
  "\<lbrakk>koTypeOf ko \<noteq> ArchT PDET; koTypeOf ko \<noteq> ArchT PTET;
   vs_valid_duplicates' (ksPSpace s) ; ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m\<rbrakk>
       \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(p \<mapsto> m))" apply (subst vs_valid_duplicates'_def) apply (intro allI impI) apply (clarsimp split:if_splits simp:duplicate_address_set_simp option.splits) apply (intro conjI impI allI) apply (frule_tac p = x and p' = p in valid_duplicates'_D) apply assumption apply simp apply (simp add:duplicate_address_set_simp)+ apply (drule_tac m = "ksPSpace s"
    and p = x in valid_duplicates'_D) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>koTypeOf ko \<noteq> ArchT PDET; koTypeOf ko \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(p \<mapsto> m)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>koTypeOf ko \<noteq> ArchT PDET; koTypeOf ko \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m\<rbrakk> \<Longrightarrow> \<forall>x y. case ((ksPSpace s)(p \<mapsto> m)) x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> ((ksPSpace s)(p \<mapsto> m)) x = ((ksPSpace s)(p \<mapsto> m)) y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>koTypeOf ko \<noteq> ArchT PDET; koTypeOf ko \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m\<rbrakk> \<Longrightarrow> case ((ksPSpace s)(p \<mapsto> m)) x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> ((ksPSpace s)(p \<mapsto> m)) x = ((ksPSpace s)(p \<mapsto> m)) y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m\<rbrakk> \<Longrightarrow> (y = p \<longrightarrow> (\<forall>x2. ksPSpace s x = Some x2 \<longrightarrow> x \<noteq> p \<longrightarrow> is_aligned p 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2) \<longrightarrow> x2 = m)) \<and> (y \<noteq> p \<longrightarrow> (\<forall>x2. ksPSpace s x = Some x2 \<longrightarrow> x \<noteq> p \<longrightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2) \<longrightarrow> Some x2 = ksPSpace s y)) proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x2 = m
 2. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (5 subgoals):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> ksPSpace s x = Some (?ko28 x y x2)
 2. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned p 2
 3. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (?ko28 x y x2)) = p && ~~ mask (vs_ptr_align (?ko28 x y x2))
 4. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2); ksPSpace s p = Some (?ko28 x y x2)\<rbrakk> \<Longrightarrow> x2 = m
 5. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned p 2
 2. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)
 3. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2); ksPSpace s p = Some x2\<rbrakk> \<Longrightarrow> x2 = m
 4. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (3 subgoals):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2)
 2. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y = p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned p 2; x && ~~ mask (vs_ptr_align x2) = p && ~~ mask (vs_ptr_align x2); ksPSpace s p = Some x2\<rbrakk> \<Longrightarrow> x2 = m
 3. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (1 subgoal):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; vs_valid_duplicates' (ksPSpace s); ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal (4 subgoals):
 1. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> ksPSpace s x = Some (?ko30 x y x2)
 2. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> is_aligned (?p'30 x y x2) 2
 3. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> x && ~~ mask (vs_ptr_align (?ko30 x y x2)) = ?p'30 x y x2 && ~~ mask (vs_ptr_align (?ko30 x y x2))
 4. \<And>x y x2. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET; ksPSpace s p = Some ko; koTypeOf ko = koTypeOf m; y \<noteq> p; ksPSpace s x = Some x2; x \<noteq> p; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); ksPSpace s (?p'30 x y x2) = Some (?ko30 x y x2)\<rbrakk> \<Longrightarrow> Some x2 = ksPSpace s y proof (prove)
goal:
No subgoals!