theory Detype_AI

lemma pre_helper:
  "\<And>base x n. \<lbrakk> is_aligned (base :: machine_word) (n + (a::nat)); n + a < word_bits \<rbrakk>
  \<Longrightarrow> base + (x && mask n) * 2^a \<in> {base .. base + 2 ^ (n + a) - 1}" apply (subgoal_tac "(x && mask n) * bit(a) < 2 ^ (n + a)") apply simp apply (rule context_conjI) apply (erule(1) is_aligned_no_wrap') apply (subst add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_wrap') apply simp apply (simp add: power_add) apply (rule word_mult_less_mono1) apply (rule and_mask_less_size, simp add: word_size word_bits_def) apply (simp add: p2_gt_0 word_bits_def) apply (simp add: word_bits_def) apply (drule power_strict_increasing[where a="2 :: nat"], simp_all) apply (simp add: power_add[where a="2::nat"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> base + (x && mask n) * 2 ^ a \<in> {base..base + 2 ^ (n + a) - 1} proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a)\<rbrakk> \<Longrightarrow> base + (x && mask n) * 2 ^ a \<in> {base..base + 2 ^ (n + a) - 1}
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a)\<rbrakk> \<Longrightarrow> base \<le> base + (x && mask n) * 2 ^ a \<and> base + (x && mask n) * 2 ^ a \<le> base + 2 ^ (n + a) - 1
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (3 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a)\<rbrakk> \<Longrightarrow> base \<le> base + (x && mask n) * 2 ^ a
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> base + (x && mask n) * 2 ^ a \<le> base + 2 ^ (n + a) - 1
 3. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> base + (x && mask n) * 2 ^ a \<le> base + 2 ^ (n + a) - 1
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> base + (x && mask n) * 2 ^ a \<le> base + (2 ^ (n + a) - 1)
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (3 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> (x && mask n) * 2 ^ a \<le> 2 ^ (n + a) - 1
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> base \<le> base + (2 ^ (n + a) - 1)
 3. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> base \<le> base + (2 ^ (n + a) - 1)
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>n + a < word_bits; (x && mask n) * 2 ^ a < 2 ^ (n + a); base \<le> base + (x && mask n) * 2 ^ a\<rbrakk> \<Longrightarrow> 2 ^ (n + a) - 1 < 2 ^ (n + a)
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (1 subgoal):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * HaskellLib_H.bit a < 2 ^ (n + a) proof (prove)
goal (1 subgoal):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> (x && mask n) * 2 ^ a < 2 ^ n * 2 ^ a proof (prove)
goal (3 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> x && mask n < 2 ^ n
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ a
 3. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ n) * unat (2 ^ a) < 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> 0 < 2 ^ a
 2. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ n) * unat (2 ^ a) < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>base x n. \<lbrakk>is_aligned base (n + a); n + a < word_bits\<rbrakk> \<Longrightarrow> unat (2 ^ n) * unat (2 ^ a) < 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>base n. \<lbrakk>is_aligned base (n + a); n + a < 32\<rbrakk> \<Longrightarrow> 2 ^ n * 2 ^ a < 4294967296 proof (prove)
goal (1 subgoal):
 1. \<And>base n. \<lbrakk>is_aligned base (n + a); 2 ^ (n + a) < 4294967296\<rbrakk> \<Longrightarrow> 2 ^ n * 2 ^ a < 4294967296 proof (prove)
goal:
No subgoals!