theory Example_Valid_State

lemma pspace_in_kernel_window_s0[simp]:
  "pspace_in_kernel_window s0_internal" apply (clarsimp simp: pspace_in_kernel_window_def s0_internal_def) apply (drule kh0_SomeD) apply (erule disjE | simp add: arch_state0_def kh0_obj_def s0_ptr_defs mask_def
                                 irq_node_offs_range_def cte_level_bits_def | rule conjI
                     | rule order_trans_rules(23)[rotated] order_trans_rules(23), force, force)+ apply (force intro: order_trans_rules(23)[rotated]) apply clarsimp apply (drule_tac x=y in le_less_trans) apply (rule neq_le_trans[rotated]) apply (rule word_plus_mono_right) apply (rule less_imp_le) apply simp+ apply (force intro: less_imp_le less_le_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_in_kernel_window s0_internal proof (prove)
goal (1 subgoal):
 1. \<And>x ko y. \<lbrakk>kh0 x = Some ko; x \<le> y; y \<le> x + 2 ^ obj_bits ko - 1\<rbrakk> \<Longrightarrow> arm_kernel_vspace arch_state0 y = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>x ko y. \<lbrakk>x \<le> y; y \<le> x + 2 ^ obj_bits ko - 1; x = init_globals_frame \<and> ko = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> ko = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> ko = idle_tcb \<or> x = High_tcb_ptr \<and> ko = High_tcb \<or> x = Low_tcb_ptr \<and> ko = Low_tcb \<or> x = High_pt_ptr \<and> ko = High_pt \<or> x = Low_pt_ptr \<and> ko = Low_pt \<or> x = High_pd_ptr \<and> ko = High_pd \<or> x = Low_pd_ptr \<and> ko = Low_pd \<or> x = irq_cnode_ptr \<and> ko = irq_cnode \<or> x = ntfn_ptr \<and> ko = ntfn \<or> x = Silc_cnode_ptr \<and> ko = Silc_cnode \<or> x = High_cnode_ptr \<and> ko = High_cnode \<or> x = Low_cnode_ptr \<and> ko = Low_cnode \<or> x \<in> irq_node_offs_range \<and> ko = CNode 0 (empty_cnode 0)\<rbrakk> \<Longrightarrow> arm_kernel_vspace arch_state0 y = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; y \<le> 0xF + x; 0xE0008000 \<le> x \<and> x < 0xE000C000 \<and> is_aligned x 4\<rbrakk> \<Longrightarrow> 0xE0000000 \<le> y
 2. \<And>x y. \<lbrakk>x \<le> y; y \<le> 0xF + x; 0xE0008000 \<le> x \<and> x < 0xE000C000 \<and> is_aligned x 4\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> y; y \<le> 0xF + x; 0xE0008000 \<le> x \<and> x < 0xE000C000 \<and> is_aligned x 4\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> y; y \<le> 0xF + x; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF + x < ?z453 x y
 2. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; y < ?z453 x y\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF + x \<le> ?z453 x y
 2. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF + x \<noteq> ?z453 x y
 3. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; y < ?z453 x y\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x \<le> ?z458 x y
 2. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF \<le> 0xF + ?z458 x y
 3. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF + x \<noteq> 0xF + ?z458 x y
 4. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; y < 0xF + ?z458 x y\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> x < ?z458 x y
 2. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF \<le> 0xF + ?z458 x y
 3. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4\<rbrakk> \<Longrightarrow> 0xF + x \<noteq> 0xF + ?z458 x y
 4. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; y < 0xF + ?z458 x y\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<le> y; 0xE0008000 \<le> x; x < 0xE000C000; is_aligned x 4; y < 0xE000C00F\<rbrakk> \<Longrightarrow> y \<le> 0xE00FFFFF proof (prove)
goal:
No subgoals!