theory Example_Valid_StateH

lemma ucast_shiftr_3:
  "\<lbrakk>ucast (p - ptr >> 4) = (3::10 word); p \<le> 0x3FFF + ptr; ptr \<le> p;
    is_aligned ptr 14; is_aligned p 4\<rbrakk>
    \<Longrightarrow> p = (ptr::word32) + 0x30" apply (subst(asm) up_ucast_inj_eq[symmetric, where 'b=32]) apply simp apply simp apply (subst(asm) ucast_ucast_len) apply simp apply (rule shiftr_less_t2n[where m=10, simplified]) apply simp apply (rule word_leq_minus_one_le) apply simp apply simp apply (rule word_diff_ls') apply simp apply simp apply (drule shiftr_eqD[where y="0x30" and n=4 and 'a=32, simplified]) apply (erule(1) aligned_sub_aligned[OF _ is_aligned_weaken]) apply simp apply simp apply (simp add: is_aligned_def) apply (simp add: diff_eq_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(32 \<rightarrow> 10) (p - ptr >> 4) = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> LENGTH(10) \<le> LENGTH(32)
 2. \<lbrakk>UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p - ptr >> 4)) = UCAST(10 \<rightarrow> 32) 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p - ptr >> 4)) = UCAST(10 \<rightarrow> 32) 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (p - ptr >> 4)) = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr >> 4 < 2 ^ LENGTH(10)
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr >> 4 < 0x400
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr < 2 ^ (4 + 10)
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr < 0x4000
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> 0x4000 \<noteq> 0
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr \<le> 0x4000 - 1
 3. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr \<le> 0x4000 - 1
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p - ptr \<le> 0x3FFF
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p \<le> 0x3FFF + ptr
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> ptr \<le> p
 3. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> ptr \<le> p
 2. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p - ptr >> 4 = 3; p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> is_aligned (p - ptr) 4
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> is_aligned 0x30 4
 3. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4; p - ptr = 0x30\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14\<rbrakk> \<Longrightarrow> 4 \<le> 14
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 3. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> is_aligned 0x30 4
 4. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4; p - ptr = 0x30\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14\<rbrakk> \<Longrightarrow> 4 < LENGTH(32)
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> is_aligned 0x30 4
 3. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4; p - ptr = 0x30\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4\<rbrakk> \<Longrightarrow> is_aligned 0x30 4
 2. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4; p - ptr = 0x30\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<le> 0x3FFF + ptr; ptr \<le> p; is_aligned ptr 14; is_aligned p 4; p - ptr = 0x30\<rbrakk> \<Longrightarrow> p = ptr + 0x30 proof (prove)
goal:
No subgoals!