theory ArchKernelInit_AI

lemma pde_mapping_bits_shift:
  fixes x :: "12 word"
  shows "x \<noteq> 0 \<Longrightarrow> 2 ^ pde_mapping_bits - 1 < (ucast x << pde_mapping_bits :: word32)" apply (simp only:shiftl_t2n pde_mapping_bits_def) apply (unfold word_less_alt) apply simp apply (unfold word_mult_def) apply (subst int_word_uint) apply (subst mod_pos_pos_trivial) apply simp apply simp apply (subst uint_up_ucast) apply (simp add: is_up_def source_size_def target_size_def word_size) apply (cut_tac 'a = "12" and x = x in uint_lt2p) apply simp apply (rule order_less_le_trans) prefer 2 apply (rule pos_mult_pos_ge) apply (subst uint_up_ucast) apply (simp add: is_up_def source_size_def target_size_def word_size) apply (simp add: word_neq_0_conv word_less_alt) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 2 ^ pde_mapping_bits - 1 < UCAST(12 \<rightarrow> 32) x << pde_mapping_bits proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 2 ^ pageBitsForSize ARMSection - 1 < 2 ^ pageBitsForSize ARMSection * UCAST(12 \<rightarrow> 32) x proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> uint (2 ^ pageBitsForSize ARMSection - 1) < uint (2 ^ pageBitsForSize ARMSection * UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < uint (0x100000 * UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < uint (word_of_int (uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x))) proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) mod 2 ^ LENGTH(32) proof (prove)
goal (3 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<le> uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x)
 2. x \<noteq> 0 \<Longrightarrow> uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) < 2 ^ LENGTH(32)
 3. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) < 2 ^ LENGTH(32)
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> uint (UCAST(12 \<rightarrow> 32) x) < 4096
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (3 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> is_up UCAST(12 \<rightarrow> 32)
 2. x \<noteq> 0 \<Longrightarrow> uint x < 4096
 3. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> uint x < 4096
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 0; uint x < 2 ^ LENGTH(12)\<rbrakk> \<Longrightarrow> uint x < 4096
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < ?y46
 2. x \<noteq> 0 \<Longrightarrow> ?y46 \<le> uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x) proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> ?y46 \<le> uint 0x100000 * uint (UCAST(12 \<rightarrow> 32) x)
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < ?y46 proof (prove)
goal (3 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> 0 < uint (UCAST(12 \<rightarrow> 32) x)
 2. x \<noteq> 0 \<Longrightarrow> 0 \<le> uint 0x100000
 3. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * 1 proof (prove)
goal (4 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> is_up UCAST(12 \<rightarrow> 32)
 2. x \<noteq> 0 \<Longrightarrow> 0 < uint x
 3. x \<noteq> 0 \<Longrightarrow> 0 \<le> uint 0x100000
 4. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * 1 proof (prove)
goal (3 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> 0 < uint x
 2. x \<noteq> 0 \<Longrightarrow> 0 \<le> uint 0x100000
 3. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * 1 proof (prove)
goal (2 subgoals):
 1. x \<noteq> 0 \<Longrightarrow> 0 \<le> uint 0x100000
 2. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * 1 proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 1048575 < uint 0x100000 * 1 proof (prove)
goal:
No subgoals!