theory Untyped_AI

lemma nasty_range:
  fixes word :: "'a :: len word"
  assumes szb: "bz < len_of TYPE('a)"
  and al:  "is_aligned word bz"
  and br:  "ptr \<in> {word.. word+2^bz - 1}"
  and sr:  "sz \<le> bz"
  shows "\<exists>idx::'a :: len word. idx < (2::'a :: len word)^(bz - sz) \<and>
         ptr \<in> {word + idx * 2^ sz .. word + (idx * 2^ sz) + (2^ sz - 1)}" proof - have offset: "ptr - word < 2^ bz" using br szb apply (subst word_less_sub_le[symmetric],simp) apply (rule word_diff_ls') apply (clarsimp simp: field_simps)+ done have t2n_sym: "\<And>z. (2::'a :: len word)^z = (1:: 'a :: len word)<<z" by (simp add: shiftl_t2n) have le_helper: "\<And>b c. \<lbrakk>\<And>a. (a::'a :: len word)< b \<Longrightarrow> a< c\<rbrakk> \<Longrightarrow> b\<le>c" apply (rule ccontr) apply (clarsimp simp: not_le dest!: meta_spec) by auto have ptr_word: "(ptr - word >> sz) * 2 ^ sz = (ptr &&~~ mask sz) - word" apply (subst mult.commute) apply (clarsimp simp: shiftl_t2n[symmetric] shiftr_shiftl1 word_and_le2) apply (simp only: diff_conv_add_uminus) apply (subst add.commute[where a = "ptr && ~~ mask sz"]) apply (subst mask_out_add_aligned) defer apply (simp add: field_simps) apply (rule is_aligned_minus) apply (rule is_aligned_weaken[OF al sr]) done show ?thesis using szb sr br apply clarsimp apply (rule_tac x = "(ptr - word) >> sz" in exI) apply (intro conjI) apply (rule less_le_trans) apply (rule shiftr_less_t2n[where m = "bz - sz"]) apply (simp add: offset) apply simp apply (rule le_plus) apply (subst mult.commute) apply (simp add: shiftl_t2n[symmetric] shiftr_shiftl1 word_and_le2) apply clarsimp apply (simp add: ptr_word p_assoc_help) apply (rule order_trans[OF _ word_plus_mono_right]) apply (rule order_eq_refl) apply (subst word_plus_and_or_coroll2[where x = "ptr",symmetric]) apply (subst add.commute) apply simp apply (rule order_trans[OF word_and_le1]) apply (clarsimp simp: mask_def) apply (rule is_aligned_no_overflow'[OF is_aligned_neg_mask]) apply simp+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (state)
goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. ptr - word < 2 ^ bz proof (prove)
using this:
ptr \<in> {word..word + 2 ^ bz - 1}
bz < LENGTH('a)

goal (1 subgoal):
 1. ptr - word < 2 ^ bz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<in> {word..word + 2 ^ bz - 1}; bz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr - word \<le> 2 ^ bz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<in> {word..word + 2 ^ bz - 1}; bz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr \<le> 2 ^ bz - 1 + word
 2. \<lbrakk>ptr \<in> {word..word + 2 ^ bz - 1}; bz < LENGTH('a)\<rbrakk> \<Longrightarrow> word \<le> ptr proof (prove)
goal:
No subgoals! proof (state)
this:
ptr - word < 2 ^ bz

goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<And>z. 2 ^ z = 1 << z proof (state)
this:
2 ^ ?z = 1 << ?z

goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<And>b c. (\<And>a. a < b \<Longrightarrow> a < c) \<Longrightarrow> b \<le> c proof (prove)
goal (1 subgoal):
 1. \<And>b c. \<lbrakk>\<And>a. a < b \<Longrightarrow> a < c; \<not> b \<le> c\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>b c. \<lbrakk>c < b; ?a2 b c < b \<Longrightarrow> ?a2 b c < c\<rbrakk> \<Longrightarrow> False proof (state)
this:
(\<And>a. a < ?b \<Longrightarrow> a < ?c) \<Longrightarrow> ?b \<le> ?c

goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. (ptr - word >> sz) * 2 ^ sz = (ptr && ~~ mask sz) - word proof (prove)
goal (1 subgoal):
 1. 2 ^ sz * (ptr - word >> sz) = (ptr && ~~ mask sz) - word proof (prove)
goal (1 subgoal):
 1. ptr - word && ~~ mask sz = (ptr && ~~ mask sz) - word proof (prove)
goal (1 subgoal):
 1. ptr + - word && ~~ mask sz = (ptr && ~~ mask sz) + - word proof (prove)
goal (1 subgoal):
 1. ptr + - word && ~~ mask sz = - word + (ptr && ~~ mask sz) proof (prove)
goal (2 subgoals):
 1. is_aligned (- word) sz
 2. ptr + - word && ~~ mask sz = - word + ptr && ~~ mask sz proof (prove)
goal (2 subgoals):
 1. ptr + - word && ~~ mask sz = - word + ptr && ~~ mask sz
 2. is_aligned (- word) sz proof (prove)
goal (1 subgoal):
 1. is_aligned (- word) sz proof (prove)
goal (1 subgoal):
 1. is_aligned word sz proof (prove)
goal:
No subgoals! proof (state)
this:
(ptr - word >> sz) * 2 ^ sz = (ptr && ~~ mask sz) - word

goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
using this:
bz < LENGTH('a)
sz \<le> bz
ptr \<in> {word..word + 2 ^ bz - 1}

goal (1 subgoal):
 1. \<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> \<exists>idx<2 ^ (bz - sz). word + idx * 2 ^ sz \<le> ptr \<and> ptr \<le> word + idx * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr - word >> sz < 2 ^ (bz - sz) \<and> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr \<and> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr - word >> sz < 2 ^ (bz - sz)
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr - word >> sz < ?y7
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ?y7 \<le> 2 ^ (bz - sz)
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr
 4. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr - word < 2 ^ (sz + (bz - sz))
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> 2 ^ (bz - sz) \<le> 2 ^ (bz - sz)
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr
 4. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> 2 ^ (bz - sz) \<le> 2 ^ (bz - sz)
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word + (ptr - word >> sz) * 2 ^ sz \<le> ptr
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> (ptr - word >> sz) * 2 ^ sz \<le> ptr - word
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word \<le> ptr
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> 2 ^ sz * (ptr - word >> sz) \<le> ptr - word
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word \<le> ptr
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> word \<le> ptr
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + 2 ^ bz - 1\<rbrakk> \<Longrightarrow> ptr \<le> word + (ptr - word >> sz) * 2 ^ sz + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr \<le> (ptr && ~~ mask sz) + ?y18
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ?y18 \<le> 2 ^ sz - 1
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr = (ptr && ~~ mask sz) + ?y18
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ?y18 \<le> 2 ^ sz - 1
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> (ptr && ?w26) + (ptr && ~~ ?w26) = (ptr && ~~ mask sz) + ?y18
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ?y18 \<le> 2 ^ sz - 1
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> (ptr && ~~ ?w26) + (ptr && ?w26) = (ptr && ~~ mask sz) + ?y18
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ?y18 \<le> 2 ^ sz - 1
 3. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> 2 ^ sz - 1
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> mask sz \<le> 2 ^ sz - 1
 2. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bz < LENGTH('a); sz \<le> bz; word \<le> ptr; ptr \<le> word + (2 ^ bz - 1)\<rbrakk> \<Longrightarrow> sz \<le> sz proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>idx<2 ^ (bz - sz). ptr \<in> {word + idx * 2 ^ sz..word + idx * 2 ^ sz + (2 ^ sz - 1)}

goal:
No subgoals!