theory ArchFinalise_AI

lemma word32_ucast_enumerates_word8:
  "\<lbrakk>is_aligned (word :: word32) pt_bits\<rbrakk>
  \<Longrightarrow> (x :: word8) \<in> (\<lambda>sl. ucast (sl && mask pt_bits >> 2))
     ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1]" apply (rule_tac x="word + (ucast x << 2)" in image_eqI) apply (frule_tac ae="x" in pt_shifting) apply simp apply (rule sym) apply (rule pd_casting_shifting) apply (simp add: word_size len32) apply (clarsimp simp: upto_enum_step_def) apply (rule conjI) apply (subgoal_tac
     " word + 2 ^ pt_bits - 1 \<ge> word", simp) apply (rule is_aligned_no_overflow) apply (simp, simp add: pt_bits_def pageBits_def word_bits_def) apply clarsimp apply (rule_tac x="ucast x" in image_eqI) apply (simp add: word_shift_by_2) apply (clarsimp simp: pt_bits_def pageBits_def) apply (rule order_trans) apply (rule word_le_minus_one_leq) apply (rule ucast_less) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned word pt_bits \<Longrightarrow> x \<in> (\<lambda>sl. UCAST(32 \<rightarrow> 8) (sl && mask pt_bits >> 2)) ` set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (2 subgoals):
 1. is_aligned word pt_bits \<Longrightarrow> x = UCAST(32 \<rightarrow> 8) (word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits >> 2)
 2. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pt_bits; word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits = UCAST(8 \<rightarrow> 32) x << 2\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 8) (word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits >> 2)
 2. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pt_bits; word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits = UCAST(8 \<rightarrow> 32) x << 2\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x << 2 >> 2)
 2. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pt_bits; word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits = UCAST(8 \<rightarrow> 32) x << 2\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 8) (UCAST(8 \<rightarrow> 32) x << 2 >> 2) = x
 2. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pt_bits; word + (UCAST(8 \<rightarrow> 32) x << 2) && mask pt_bits = UCAST(8 \<rightarrow> 32) x << 2\<rbrakk> \<Longrightarrow> size x + 2 < LENGTH(32)
 2. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (1 subgoal):
 1. is_aligned word pt_bits \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> set [word , word + 4 .e. word + 2 ^ pt_bits - 1] proof (prove)
goal (1 subgoal):
 1. is_aligned word pt_bits \<Longrightarrow> \<not> word + 2 ^ pt_bits - 1 < word \<and> (\<not> word + 2 ^ pt_bits - 1 < word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> (2 ^ pt_bits - 1) div 4}) proof (prove)
goal (2 subgoals):
 1. is_aligned word pt_bits \<Longrightarrow> \<not> word + 2 ^ pt_bits - 1 < word
 2. is_aligned word pt_bits \<Longrightarrow> \<not> word + 2 ^ pt_bits - 1 < word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> (2 ^ pt_bits - 1) div 4} proof (prove)
goal (2 subgoals):
 1. is_aligned word pt_bits \<Longrightarrow> word \<le> word + 2 ^ pt_bits - 1
 2. is_aligned word pt_bits \<Longrightarrow> \<not> word + 2 ^ pt_bits - 1 < word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> (2 ^ pt_bits - 1) div 4} proof (prove)
goal (2 subgoals):
 1. is_aligned word pt_bits \<Longrightarrow> is_aligned word pt_bits
 2. is_aligned word pt_bits \<Longrightarrow> \<not> word + 2 ^ pt_bits - 1 < word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> (2 ^ pt_bits - 1) div 4} proof (prove)
goal (1 subgoal):
 1. is_aligned word 10 \<Longrightarrow> \<not> 0x3FF + word < word \<longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> 0xFF} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) \<in> (\<lambda>x. word + x * 4) ` {x. x \<le> 0xFF} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> word + (UCAST(8 \<rightarrow> 32) x << 2) = word + UCAST(8 \<rightarrow> 32) x * 4
 2. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<in> {x. x \<le> 0xFF} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<in> {x. x \<le> 0xFF} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<le> 0xFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x \<le> ?y29
 2. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> ?y29 \<le> 0xFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) x < ?y32
 2. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> ?y32 - 1 \<le> 0xFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> LENGTH(8) < LENGTH(32)
 2. \<lbrakk>is_aligned word 10; \<not> 0x3FF + word < word\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(8) - 1 \<le> 0xFF proof (prove)
goal:
No subgoals!