theory Example_Valid_StateH

lemma tcb_offs_range_correct':
  "\<lbrakk>x \<in> tcb_offs_range ptr; is_aligned ptr 9\<rbrakk>
    \<Longrightarrow> \<exists>y. x = ptr + ucast (y:: 9 word)" apply (clarsimp simp: tcb_offs_range_def s0_ptr_defs cte_level_bits_def) apply (rule_tac x="ucast (x - ptr)" in exI) apply (clarsimp simp: ucast_ucast_mask) apply (rule_tac n=9 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 + 0x1FF" and n=9 in neg_mask_mono_le) apply (simp add: add.commute) apply (drule_tac n=9 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> tcb_offs_range ptr; is_aligned ptr 9\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + UCAST(9 \<rightarrow> 32) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> \<exists>y. x = ptr + UCAST(9 \<rightarrow> 32) y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x = ptr + UCAST(9 \<rightarrow> 32) (UCAST(32 \<rightarrow> 9) (x - ptr)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x = ptr + (x - ptr && mask 9) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = ptr + (x - ptr && mask 9) && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> is_aligned ptr 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = (x - ptr && mask 9) && mask 9
 3. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = (x - ptr && mask 9) && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = x - ptr && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = x + - ptr && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = - ptr + x && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> is_aligned (- ptr) 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = x && mask 9
 3. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && mask 9 = x && mask 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr + (x + - ptr && mask 9) && ~~ mask 9 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> is_aligned ptr 9
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>9. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 9) !! n'
 3. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>9. n' < LENGTH(32) \<longrightarrow> \<not> (x + - ptr && mask 9) !! n'
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr\<rbrakk> \<Longrightarrow> x \<le> ptr + 0x1FF
 2. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; ptr \<le> x; x \<le> 0x1FF + ptr; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr 9; x \<le> 0x1FF + ptr; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9\<rbrakk> \<Longrightarrow> is_aligned ptr 9
 2. \<lbrakk>is_aligned ptr 9; x \<le> 0x1FF + ptr; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9; ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; x \<le> 0x1FF + ptr; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9; ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; x \<le> ptr + 0x1FF; x && ~~ mask 9 \<le> ptr + 0x1FF && ~~ mask 9; ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 9; is_aligned ptr 9; x \<le> ptr + 0x1FF\<rbrakk> \<Longrightarrow> is_aligned ptr 9
 2. \<lbrakk>is_aligned ptr 9; x \<le> ptr + 0x1FF; x && ~~ mask 9 \<le> ptr + (0x1FF && ~~ mask 9); ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<le> x && ~~ mask 9; x \<le> ptr + 0x1FF\<rbrakk> \<Longrightarrow> 9 \<le> 9
 2. \<lbrakk>is_aligned ptr 9; x \<le> ptr + 0x1FF; x && ~~ mask 9 \<le> ptr + (0x1FF && ~~ mask 9); ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 9; x \<le> ptr + 0x1FF; x && ~~ mask 9 \<le> ptr + (0x1FF && ~~ mask 9); ptr \<le> x && ~~ mask 9\<rbrakk> \<Longrightarrow> x && ~~ mask 9 = ptr proof (prove)
goal:
No subgoals!