theory ArchAcc_AI

lemma pde_shifting:
  "\<lbrakk>is_aligned (vptr::word32) 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> x + (vptr >> 20) < 0x1000" apply (rule order_less_le_trans) apply (subst upper_bits_unset_is_l2p_32 [where n=12, symmetric]) apply (clarsimp simp: word_bits_def) prefer 2 apply simp apply (clarsimp simp: word_bits_def) subgoal premises prems for n' proof - have H: "(0xF::word32) < 2 ^ 4" by simp from prems show ?thesis apply (subst (asm) word_plus_and_or_coroll) apply word_eqI subgoal for n apply (spec "20 + n") apply (simp add: word_size) apply (insert H) apply (drule (1) order_le_less_trans) apply (drule bang_is_le) apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption) apply (drule word_power_increasing) by simp+ apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth) apply (erule disjE) apply (insert H)[1] apply (drule (1) order_le_less_trans) apply (drule bang_is_le) apply (drule order_le_less_trans[where z="2 ^ 4"], assumption) apply (drule word_power_increasing; simp) apply (spec "20 + n'") apply (frule test_bit_size) by (simp add: word_size) qed done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> x + (vptr >> 20) < 0x1000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> x + (vptr >> 20) < ?y
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> ?y \<le> 0x1000 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 12 < word_bits
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>12. n' < word_bits \<longrightarrow> \<not> (x + (vptr >> 20)) !! n'
 3. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 2 ^ 12 \<le> 0x1000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>12. n' < word_bits \<longrightarrow> \<not> (x + (vptr >> 20)) !! n'
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 2 ^ 12 \<le> 0x1000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> 2 ^ 12 \<le> 0x1000
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>12. n' < word_bits \<longrightarrow> \<not> (x + (vptr >> 20)) !! n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>12. n' < word_bits \<longrightarrow> \<not> (x + (vptr >> 20)) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>is_aligned vptr 24; x \<le> 0xF; 12 \<le> n'; n' < 32; (x + (vptr >> 20)) !! n'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. False proof (state)
goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. 0xF < 2 ^ 4 proof (state)
this:
0xF < 2 ^ 4

goal (1 subgoal):
 1. False proof (chain)
picking this:
is_aligned vptr 24
x \<le> 0xF
12 \<le> n'
n' < 32
(x + (vptr >> 20)) !! n' proof (prove)
using this:
is_aligned vptr 24
x \<le> 0xF
12 \<le> n'
n' < 32
(x + (vptr >> 20)) !! n'

goal (1 subgoal):
 1. False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF; 12 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> x && (vptr >> 20) = 0
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF; 12 \<le> n'; n' < 32; (x || (vptr >> 20)) !! n'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned vptr 24; x \<le> 0xF; 12 \<le> n'; n' < 32; (x || (vptr >> 20)) !! n'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n); 20 + n < 24 \<longrightarrow> \<not> vptr !! (20 + n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n); \<not> n < 4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>12 \<le> n'; n' < 32; x !! n; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>12 \<le> n'; n' < 32; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4; 2 ^ n \<le> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>12 \<le> n'; n' < 32; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4; 2 ^ n < 2 ^ 4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>12 \<le> n'; n' < 32; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4\<rbrakk> \<Longrightarrow> n < LENGTH(32)
 2. \<lbrakk>12 \<le> n'; n' < 32; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 3. \<lbrakk>12 \<le> n'; n' < 32; n < 12; vptr !! (20 + n); \<not> n < 4; 0xF < 2 ^ 4; x < 2 ^ 4; n < 4\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 24; x \<le> 0xF; 12 \<le> n'; n' < 32; (x || (vptr >> 20)) !! n'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n' \<or> vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; x !! n'; 0xF < 2 ^ 4\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; 12 \<le> n'; n' < 32; x !! n'; 0xF < 2 ^ 4; x < 2 ^ 4\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; 12 \<le> n'; n' < 32; 0xF < 2 ^ 4; x < 2 ^ 4; 2 ^ n' \<le> x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; 12 \<le> n'; n' < 32; 0xF < 2 ^ 4; x < 2 ^ 4; 2 ^ n' < 2 ^ 4\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n<24. \<not> vptr !! n; x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n'); 20 + n' < 24 \<longrightarrow> \<not> vptr !! (20 + n')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> 0xF; 12 \<le> n'; n' < 32; vptr !! (20 + n'); 20 + n' < 24 \<longrightarrow> \<not> vptr !! (20 + n'); 20 + n' < size vptr\<rbrakk> \<Longrightarrow> False proof (state)
this:
False

goal:
No subgoals! proof (prove)
goal:
No subgoals!