theory ArchFinalise_AI

lemma pd_shifting_kernel_mapping_slots:
  "\<lbrakk>is_aligned word pd_bits;
    (sl :: word32) \<le> (kernel_base >> (20::nat)) - (1::word32)\<rbrakk>
   \<Longrightarrow> ucast ((sl << (2::nat)) + word && mask pd_bits >> (2::nat))
      \<notin> kernel_mapping_slots" apply (subst pd_shifting_again5) apply assumption+ prefer 2 apply (simp add:not_le kernel_mapping_slots_def) apply (subst (asm) le_m1_iff_lt[THEN iffD1]) apply (simp add: kernel_base_def) apply (rule shiftr_20_less[where x = "sl << 20",THEN iffD2]) apply (subst shiftl_shiftr_id) apply (simp add:word_bits_def) defer apply assumption apply (subst shiftl_shiftr_id) apply (simp add:word_bits_def) defer apply (simp add: ucast_bl word_rep_drop of_drop_to_bl word_size) apply (subst eq_commute) apply (subst and_mask_eq_iff_le_mask) apply (rule order_trans) apply ((simp add: kernel_base_def mask_def)+)[2] apply (rule_tac x="sl" and y="kernel_base >> 20" in less_trans) apply ((simp add: kernel_base_def word_bits_def)+)[2] apply (subst (asm) le_m1_iff_lt[THEN iffD1]) apply (simp add: kernel_base_def) apply (rule_tac x="sl" and y="kernel_base >> 20" in less_trans) apply ((simp add: kernel_base_def word_bits_def)+)[2] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((sl << 2) + word && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> is_aligned word pd_bits
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> ?y \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> ?y \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> ?y \<notin> kernel_mapping_slots
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> ?y < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y proof (prove)
goal (3 subgoals):
 1. is_aligned word pd_bits \<Longrightarrow> 0 < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> ?y < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> ?y < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) ?y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl << 20 >> 20 < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (sl << 20 >> 20)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < kernel_base >> 20
 4. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (sl << 20 >> 20)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < kernel_base >> 20
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (sl << 20 >> 20)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (sl << 20 >> 20))
 3. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (sl << 20 >> 20))
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) sl)
 4. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) sl)
 3. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) sl)
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl = sl && mask 12
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl && mask 12 = sl
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl \<le> mask 12
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl \<le> ?y76
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> ?y76 \<le> mask 12
 3. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 4. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20)
 2. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> kernel_base >> 20 < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word pd_bits; sl \<le> (kernel_base >> 20) - 1\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (2 subgoals):
 1. is_aligned word pd_bits \<Longrightarrow> 0 < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < 2 ^ (LENGTH(32) - 20) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> sl < kernel_base >> 20
 2. \<lbrakk>is_aligned word pd_bits; sl < kernel_base >> 20\<rbrakk> \<Longrightarrow> kernel_base >> 20 < 2 ^ (LENGTH(32) - 20) proof (prove)
goal:
No subgoals!