theory ArchKernelInit_AI

lemma in_kernel_base:
"\<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF\<rbrakk> \<Longrightarrow> (\<forall>y\<in>{kernel_base + m .. n + kernel_base}.
              kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF)" apply (clarsimp simp:) apply (intro conjI) apply (rule ccontr,simp add:not_le) apply (drule(1) le_less_trans) apply (cut_tac is_aligned_no_wrap'[where ptr = kernel_base and off = m
     and sz = 28,simplified]) apply (drule(1) less_le_trans) apply simp apply (simp add:kernel_base_def is_aligned_def) apply (rule ccontr,simp add:not_less) apply (drule less_le_trans[where z = "0x10000000"]) apply simp apply simp apply (erule order_trans) apply (simp add:field_simps) apply (rule word_plus_mono_right) apply simp apply (simp add:kernel_base_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF\<rbrakk> \<Longrightarrow> \<forall>y\<in>{kernel_base + m..n + kernel_base}. kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> kernel_base \<le> y \<and> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> kernel_base \<le> y
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base; y < kernel_base\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base; kernel_base \<le> kernel_base + m\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> is_aligned kernel_base 28
 3. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> m < 0x10000000
 4. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; kernel_base + m < kernel_base; kernel_base \<le> kernel_base + m; y < kernel_base + m\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> is_aligned kernel_base 28
 3. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> m < 0x10000000
 4. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> is_aligned kernel_base 28
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> m < 0x10000000
 3. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base\<rbrakk> \<Longrightarrow> m < 0x10000000
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base; 0x10000000 \<le> m\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base; 0x10000000 \<le> m\<rbrakk> \<Longrightarrow> 0xFFFFF \<le> 0x10000000
 2. \<And>y. \<lbrakk>n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base; 0x10000000 \<le> m; m < 0x10000000\<rbrakk> \<Longrightarrow> False
 3. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>n \<le> 0xFFFFF; y \<le> n + kernel_base; y < kernel_base; kernel_base + m < kernel_base; 0x10000000 \<le> m; m < 0x10000000\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y; y \<le> n + kernel_base\<rbrakk> \<Longrightarrow> y \<le> kernel_base + 0xFFFFF proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y\<rbrakk> \<Longrightarrow> n + kernel_base \<le> kernel_base + 0xFFFFF proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y\<rbrakk> \<Longrightarrow> kernel_base + n \<le> kernel_base + 0xFFFFF proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y\<rbrakk> \<Longrightarrow> n \<le> 0xFFFFF
 2. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y\<rbrakk> \<Longrightarrow> kernel_base \<le> kernel_base + 0xFFFFF proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>m < 0xFFFFF; n \<le> 0xFFFFF; kernel_base + m \<le> y\<rbrakk> \<Longrightarrow> kernel_base \<le> kernel_base + 0xFFFFF proof (prove)
goal:
No subgoals!