theory ArchAcc_AI

lemma pd_shifting_dual:
  "is_aligned (pd::word32) 14 \<Longrightarrow> pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2" apply (simp add: pd_bits_def pageBits_def) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) subgoal for n apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth) apply (spec n) apply (simp add: linorder_not_less) apply (drule test_bit_size)+ by (simp add: word_size) apply (rule word_eqI) 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 clarsimp apply (drule test_bit_size)+ apply (simp add: word_size) done

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