theory ArchAcc_AI

lemma pd_shifting:
  "is_aligned (pd::word32) 14 \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd" apply (rule word_eqI[rule_format]) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) subgoal for \<dots> na apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth) apply (spec na) apply (simp add: linorder_not_less) apply (drule test_bit_size)+ by (simp add: word_size) subgoal for n apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth word_ops_nth_size
                          pd_bits_def pageBits_def linorder_not_less) apply (rule iffI) apply clarsimp apply (drule test_bit_size)+ apply (simp add: word_size) apply clarsimp apply (spec n) by simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd 14 \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> (pd + (vptr >> 20 << 2) && ~~ mask pd_bits) !! n = pd !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> pd && (vptr >> 20 << 2) = 0
 2. \<And>n. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> ((pd || (vptr >> 20 << 2)) && ~~ mask pd_bits) !! n = pd !! n proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> na < size (pd && (vptr >> 20 << 2)) \<longrightarrow> (pd && (vptr >> 20 << 2)) !! na = 0 !! na
 2. \<And>n. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> ((pd || (vptr >> 20 << 2)) && ~~ mask pd_bits) !! n = pd !! n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd 14; n_ < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> na < size (pd && (vptr >> 20 << 2)) \<longrightarrow> (pd && (vptr >> 20 << 2)) !! na = 0 !! na proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n_ < 32; na < 32; 2 \<le> na; pd !! na; vptr !! (18 + na)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n_ < 32; na < 32; 2 \<le> na; pd !! na; vptr !! (18 + na); na < 14 \<longrightarrow> \<not> pd !! na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n_ < 32; na < 32; pd !! na; vptr !! (18 + na); 14 \<le> na\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n_ < 32; na < 32; 14 \<le> na; na < size pd; 18 + na < size vptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> ((pd || (vptr >> 20 << 2)) && ~~ mask pd_bits) !! n = pd !! n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd 14; n < size (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)\<rbrakk> \<Longrightarrow> ((pd || (vptr >> 20 << 2)) && ~~ mask pd_bits) !! n = pd !! n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32\<rbrakk> \<Longrightarrow> ((pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n) = pd !! n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; (pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n\<rbrakk> \<Longrightarrow> pd !! n
 2. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; pd !! n\<rbrakk> \<Longrightarrow> (pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; 14 \<le> n; vptr !! (18 + n)\<rbrakk> \<Longrightarrow> pd !! n
 2. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; pd !! n\<rbrakk> \<Longrightarrow> (pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; 14 \<le> n; 18 + n < size vptr\<rbrakk> \<Longrightarrow> pd !! n
 2. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; pd !! n\<rbrakk> \<Longrightarrow> (pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; pd !! n\<rbrakk> \<Longrightarrow> (pd !! n \<or> 2 \<le> n \<and> vptr !! (20 + (n - 2))) \<and> 14 \<le> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<14. \<not> pd !! n; n < 32; pd !! n\<rbrakk> \<Longrightarrow> 14 \<le> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; pd !! n; n < 14 \<longrightarrow> \<not> pd !! n\<rbrakk> \<Longrightarrow> 14 \<le> n proof (prove)
goal:
No subgoals!