theory Example_Valid_StateH

lemma pd_offs_range_correct':
  "\<lbrakk>x \<in> pd_offs_range ptr; is_aligned ptr 14\<rbrakk>
    \<Longrightarrow> \<exists>y. x = ptr + (ucast (y:: 12 word) << 2)" apply (clarsimp simp: pd_offs_range_def s0_ptr_defs cte_level_bits_def) apply (rule_tac x="ucast ((x - ptr) >> 2)" in exI) apply (clarsimp simp: ucast_ucast_mask) apply (subst aligned_shiftr_mask_shiftl) apply (rule aligned_sub_aligned) apply assumption apply (erule is_aligned_weaken) apply simp apply simp apply simp apply (rule_tac n=14 in mask_eqI) apply (subst mask_add_aligned) apply (simp add: is_aligned_def) apply (simp add: mask_twice) apply (subst diff_conv_add_uminus) apply (subst add.commute[symmetric]) apply (subst mask_add_aligned) apply (simp add: is_aligned_minus) apply simp apply (subst diff_conv_add_uminus) apply (subst add_mask_lower_bits) apply (simp add: is_aligned_def) apply clarsimp apply (cut_tac x=x and y="ptr + 0x3FFF" and n=14 in neg_mask_mono_le) apply (simp add: add.commute) apply (drule_tac n=14 in aligned_le_sharp) apply (simp add: is_aligned_def) apply (simp add: add.commute) apply (subst(asm) mask_out_add_aligned[symmetric]) apply (erule is_aligned_weaken) apply simp apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> pd_offs_range ptr; is_aligned ptr 14\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + (UCAST(12 \<rightarrow> 32) y << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + (UCAST(12 \<rightarrow> 32) y << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (x - ptr >> 2)) << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + ((x - ptr >> 2) && mask 12 << 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (x - ptr) 2
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 4. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 2
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 \<le> 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask (12 + 2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask 14) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = ptr + (x - ptr && mask 14) && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = (x - ptr && mask 14) && mask 14
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = (x - ptr && mask 14) && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = x - ptr && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = x + - ptr && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = - ptr + x && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (- ptr) 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = x && mask 14
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && mask 14 = x && mask 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr + (x + - ptr && mask 14) && ~~ mask 14 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 14
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>14. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 14) !! n'
 3. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>14. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 14) !! n'
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x3FFF
 2. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; ptr \<le> x; x \<le> 0x3FFF + ptr; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 14; x \<le> 0x3FFF + ptr; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14\<rbrakk> \<Longrightarrow> is_aligned ptr 14
 2. \<lbrakk>is_aligned ptr 14; x \<le> 0x3FFF + ptr; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; x \<le> 0x3FFF + ptr; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; x \<le> ptr + 0x3FFF; is_aligned x 2; x && ~~ mask 14 \<le> ptr + 0x3FFF && ~~ mask 14; ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 14; is_aligned ptr 14; x \<le> ptr + 0x3FFF; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned ptr 14
 2. \<lbrakk>is_aligned ptr 14; x \<le> ptr + 0x3FFF; is_aligned x 2; x && ~~ mask 14 \<le> ptr + (0x3FFF && ~~ mask 14); ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 14; x \<le> ptr + 0x3FFF; is_aligned x 2\<rbrakk> \<Longrightarrow> 14 \<le> 14
 2. \<lbrakk>is_aligned ptr 14; x \<le> ptr + 0x3FFF; is_aligned x 2; x && ~~ mask 14 \<le> ptr + (0x3FFF && ~~ mask 14); ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 14; x \<le> ptr + 0x3FFF; is_aligned x 2; x && ~~ mask 14 \<le> ptr + (0x3FFF && ~~ mask 14); ptr \<le> x && ~~ mask 14\<rbrakk> \<Longrightarrow> x && ~~ mask 14 = ptr proof (prove)
goal:
No subgoals!