diff --git a/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
new file mode 100644
index 000000000..7a2245d37
--- /dev/null
+++ b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
@@ -0,0 +1,386 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+(* Kernel init refinement. Currently axiomatised.
+*)
+
+theory ArchKernelInit_AI
+imports
+  "../ADT_AI"
+  "../Tcb_AI"
+  "../Arch_AI"
+begin
+
+context Arch begin global_naming ARM (*FIXME: arch_split*)
+
+text {*
+  Showing that there is a state that satisfies the abstract invariants.
+*}
+
+lemma [simp]: "is_aligned (0x1000 :: word32) 9" by (simp add: is_aligned_def)
+lemma [simp]: "is_aligned (0x2000 :: word32) 9" by (simp add: is_aligned_def)
+
+lemmas ptr_defs = init_tcb_ptr_def idle_thread_ptr_def init_irq_node_ptr_def 
+                  init_globals_frame_def init_global_pd_def
+lemmas state_defs = init_A_st_def init_kheap_def init_arch_state_def ptr_defs 
+
+lemma [simp]: "is_tcb (TCB t)" by (simp add: is_tcb_def)
+
+lemma [simp]: "ran (empty_cnode n) = {Structures_A.NullCap}"
+  apply (auto simp: ran_def empty_cnode_def)
+  apply (rule_tac x="replicate n False" in exI)
+  apply simp
+  done
+
+lemma empty_cnode_apply[simp]:
+  "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = Structures_A.NullCap)"
+  by (auto simp add: empty_cnode_def)
+
+lemma valid_cs_size_empty[simp]:
+  "valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits)"
+  apply (simp add: valid_cs_size_def)
+  apply (insert wf_empty_bits [of n])
+  apply fastforce
+  done
+
+lemma init_cdt [simp]:
+  "cdt init_A_st = init_cdt"
+  by (simp add: state_defs)
+
+lemma mdp_parent_empty [simp]:
+  "\<not>empty \<Turnstile> x \<rightarrow> y"
+  apply clarsimp
+  apply (drule tranclD)
+  apply (clarsimp simp: cdt_parent_of_def)
+  done
+
+lemma descendants_empty [simp]:
+  "descendants_of x empty = {}"
+  by (clarsimp simp: descendants_of_def)
+
+lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"
+  by (simp add: is_reply_cap_def)
+
+lemma [simp]: "cap_range Structures_A.NullCap = {}"
+  by (simp add: cap_range_def)
+
+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 simp
+  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  
+
+lemma mask_pde_mapping_bits:
+  "mask 20 = 2^pde_mapping_bits - 1"
+  by (simp add: mask_def pde_mapping_bits_def)
+
+
+
+lemma init_irq_ptrs_ineqs:
+  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
+  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
+                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
+  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
+                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
+proof -
+  have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)"
+    apply (rule order_le_less_trans[OF 
+        ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]])
+    apply (simp add: cte_level_bits_def minus_one_norm)
+    done
+  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
+    apply (rule is_aligned_no_wrap'[where sz=14])
+     apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def)
+    apply (rule shiftl_less_t2n[OF P])
+    apply simp
+    done
+  show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
+                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
+    apply (simp only: add_diff_eq[symmetric] add.assoc)
+    apply (rule word_add_le_mono2)
+     apply (simp only: trans [OF shiftl_t2n mult.commute])
+     apply (rule nasty_split_lt[OF P])
+      apply (simp_all add: cte_level_bits_def 
+        word_bits_def kernel_base_def init_irq_node_ptr_def)
+    done
+  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
+                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
+    apply (simp only: add_diff_eq[symmetric])
+    apply (rule word_add_le_mono2)
+     apply (rule minus_one_helper3, rule shiftl_less_t2n[OF P])
+     apply simp
+    apply (simp add: kernel_base_def
+      cte_level_bits_def word_bits_def init_irq_node_ptr_def)
+    done
+qed
+
+lemmas init_irq_ptrs_less_ineqs
+   = init_irq_ptrs_ineqs(1)[THEN order_less_le_trans[rotated]]
+     init_irq_ptrs_ineqs(2-3)[THEN order_le_less_trans]
+
+lemmas init_irq_ptrs_all_ineqs[unfolded init_irq_node_ptr_def cte_level_bits_def]
+   = init_irq_ptrs_ineqs(1)[THEN order_trans[rotated]]
+     init_irq_ptrs_ineqs(2-3)[THEN order_trans]
+     init_irq_ptrs_less_ineqs
+     init_irq_ptrs_less_ineqs[THEN less_imp_neq]
+     init_irq_ptrs_less_ineqs[THEN less_imp_neq, THEN not_sym]
+
+lemmas ucast_le_ucast_10_32 = ucast_le_ucast[where 'a=10 and 'b=32,simplified]
+lemma init_irq_ptrs_eq:
+  "((ucast (irq :: irq) << cte_level_bits)
+        = (ucast (irq' :: irq) << cte_level_bits :: word32))
+      = (irq = irq')"
+  apply safe
+  apply (rule ccontr)
+  apply (erule_tac bnd="ucast (max_word :: irq) + 1"
+              in shift_distinct_helper[rotated 3],
+         safe intro!: plus_one_helper2,
+         simp_all add: ucast_le_ucast_10_32 up_ucast_inj_eq,
+         simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
+                       max_word_def)
+  done
+
+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
+
+lemma pspace_aligned_init_A:
+  "pspace_aligned init_A_st"
+  apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
+                          dom_if_Some cte_level_bits_def)
+  apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
+           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
+  done
+
+lemma pspace_distinct_init_A:
+  "pspace_distinct init_A_st"
+  apply (clarsimp simp: pspace_distinct_def state_defs pageBits_def
+                        empty_cnode_bits kernel_base_def
+                        cte_level_bits_def linorder_not_le cong: if_cong)
+  apply (safe,
+         simp_all add: init_irq_ptrs_all_ineqs
+                       [simplified kernel_base_def, simplified])[1]
+  apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
+             and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
+             and sz=cte_level_bits in aligned_neq_into_no_overlap)
+     apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
+    apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
+    apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
+                     kernel_base_def)
+   apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
+   apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
+                    kernel_base_def)
+  apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def
+                   linorder_not_le)
+  done
+
+lemma caps_of_state_init_A_st_Null:
+  "caps_of_state (init_A_st::'z::state_ext state) x
+     = (if cte_at x (init_A_st::'z::state_ext state) then Some cap.NullCap else None)"
+  apply (subgoal_tac "\<not> cte_wp_at (op \<noteq> cap.NullCap) x init_A_st")
+   apply (auto simp add: cte_wp_at_caps_of_state)[1]
+  apply (clarsimp, erule cte_wp_atE)
+   apply (auto simp add: state_defs tcb_cap_cases_def split: split_if_asm)
+  done
+
+lemmas cte_wp_at_caps_of_state_eq
+    = cte_wp_at_caps_of_state[where P="op = cap" for cap]
+
+declare ptrFormPAddr_addFromPPtr[simp]
+
+lemma invs_A:
+  "invs init_A_st"
+
+  apply (simp add: invs_def)
+  apply (rule conjI)
+   prefer 2
+   apply (simp add: cur_tcb_def state_defs obj_at_def)
+  apply (simp add: valid_state_def)
+  apply (rule conjI)
+   apply (simp add: valid_pspace_def)
+   apply (rule conjI)
+    apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
+                          valid_obj_def valid_vm_rights_def vm_kernel_only_def
+                          dom_if_Some cte_level_bits_def)
+    apply (rule conjI)
+     apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def 
+                           valid_cap_def obj_at_def valid_tcb_state_def 
+                           cap_aligned_def word_bits_def)+
+    apply (clarsimp simp: valid_cs_def word_bits_def cte_level_bits_def
+                          init_irq_ptrs_all_ineqs valid_tcb_def
+                   split: split_if_asm)
+   apply (rule conjI)
+    apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
+                          dom_if_Some cte_level_bits_def)
+    apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
+           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
+   apply (rule conjI)
+    apply (simp add:pspace_distinct_init_A)
+   apply (rule conjI)
+    apply (clarsimp simp: if_live_then_nonz_cap_def obj_at_def state_defs)
+   apply (rule conjI)
+    apply (clarsimp simp: zombies_final_def cte_wp_at_cases state_defs 
+                          tcb_cap_cases_def is_zombie_def)
+   apply (clarsimp simp: sym_refs_def state_refs_of_def state_defs)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_mdb_def init_cdt_def no_mloop_def 
+                         mdb_cte_at_def)
+   apply (clarsimp simp: untyped_mdb_def caps_of_state_init_A_st_Null
+                         untyped_inc_def ut_revocable_def
+                         irq_revocable_def reply_master_revocable_def
+                         reply_mdb_def reply_caps_mdb_def
+                         reply_masters_mdb_def)
+   apply (simp add:descendants_inc_def)
+  apply (rule conjI)
+   apply (simp add: valid_ioc_def init_A_st_def init_ioc_def cte_wp_at_cases2)
+   apply (intro allI impI, elim exE conjE)
+   apply (case_tac obj, simp_all add: cap_of_def)
+   apply (clarsimp simp: init_kheap_def split: split_if_asm)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs)
+  apply (rule conjI)
+   apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs)
+  apply (rule conjI)
+   apply (clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null)
+  apply (clarsimp simp: valid_reply_caps_def unique_reply_caps_def
+                        has_reply_cap_def pred_tcb_at_def obj_at_def
+                        caps_of_state_init_A_st_Null
+                        cte_wp_at_caps_of_state_eq
+                        valid_reply_masters_def valid_global_refs_def
+                        valid_refs_def[unfolded cte_wp_at_caps_of_state])
+  apply (rule conjI)
+   apply (clarsimp simp: valid_arch_state_def)
+   apply (rule conjI)
+    apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs 
+                          a_type_def)
+   apply (rule conjI)
+    apply (clarsimp simp: valid_asid_table_def state_defs)
+   apply (rule conjI)
+    apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs 
+                          a_type_def)
+   apply (rule conjI)
+    apply (simp add: valid_global_pts_def state_defs)
+   apply (simp add: state_defs is_inv_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
+                         is_cap_table_def wf_empty_bits
+                         init_irq_ptrs_all_ineqs cte_level_bits_def
+                         init_irq_ptrs_eq[unfolded cte_level_bits_def])
+   apply (intro conjI)
+    apply (rule inj_onI)
+    apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def])
+   apply clarsimp
+   defer
+  apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
+                   ran_def cong: rev_conj_cong)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_irq_states_def init_A_st_def init_machine_state_def valid_irq_masks_def init_irq_masks_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_machine_state_def init_A_st_def
+                         init_machine_state_def init_underlying_memory_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_arch_objs_def obj_at_def state_defs)
+   apply (clarsimp simp: vs_lookup_def vs_asid_refs_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_arch_caps_def)
+   apply (rule conjI)
+    apply (clarsimp simp: valid_vs_lookup_def)
+    apply (clarsimp simp: vs_lookup_pages_def state_defs vs_asid_refs_def)
+   apply (clarsimp simp: valid_table_caps_def caps_of_state_init_A_st_Null
+                         unique_table_caps_def unique_table_refs_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_global_objs_def state_defs)
+   apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
+                         valid_pde_mappings_def)
+   apply (simp add: kernel_base_def kernel_mapping_slots_def 
+                    Platform.ARM.addrFromPPtr_def physMappingOffset_def
+                    kernelBase_addr_def physBase_def pageBits_def is_aligned_def)
+  apply (rule conjI)
+   apply (simp add: valid_kernel_mappings_def state_defs
+                         valid_kernel_mappings_if_pd_def pde_ref_def
+                         ran_def)
+   apply (auto simp: pde_ref_def split: split_if_asm)[1]
+  apply (rule conjI)
+   apply (clarsimp simp: equal_kernel_mappings_def state_defs obj_at_def)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_asid_map_def state_defs)
+  apply (rule conjI)
+   apply (clarsimp simp: valid_global_pd_mappings_def obj_at_def state_defs
+                         valid_pd_kernel_mappings_def mask_pde_mapping_bits)
+   apply (simp add: valid_pde_kernel_mappings_def kernel_base_def)
+   apply (rule conjI)
+    apply (fastforce simp:pde_mapping_bits_def)
+   apply (intro ballI impI)
+   apply (clarsimp simp:pde_mapping_bits_def)
+   apply word_bitwise
+   apply clarsimp
+  apply (rule conjI)
+   apply (clarsimp simp: pspace_in_kernel_window_def state_defs mask_def)
+   apply (intro conjI impI)
+            apply (rule in_kernel_base|simp)+
+         apply (erule exE,drule sym,simp add:field_simps)
+         apply (rule in_kernel_base[unfolded add.commute])
+          apply (rule word_less_add_right,simp add:cte_level_bits_def)
+           apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
+          apply simp
+         apply (simp add:cte_level_bits_def field_simps)
+         apply (subst add.commute)
+         apply (rule le_plus')
+          apply simp+
+          apply (rule less_imp_le)
+          apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
+     apply (rule in_kernel_base|simp)+
+  apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
+                  valid_refs_def[unfolded cte_wp_at_caps_of_state])
+  apply word_bitwise
+  done
+
+end
+
+end
diff --git a/proof/invariant-abstract/KernelInit_AI.thy b/proof/invariant-abstract/KernelInit_AI.thy
index 861e873e0..4cd6ff6cf 100644
--- a/proof/invariant-abstract/KernelInit_AI.thy
+++ b/proof/invariant-abstract/KernelInit_AI.thy
@@ -12,374 +12,10 @@
 *)
 
 theory KernelInit_AI
-imports ADT_AI Tcb_AI Arch_AI "../../lib/NICTATools"
+imports
+  "./$L4V_ARCH/ArchKernelInit_AI"
 begin
 
-context Arch begin global_naming ARM (*FIXME: arch_split*)
-
-text {*
-  Showing that there is a state that satisfies the abstract invariants.
-*}
-
-lemma [simp]: "is_aligned (0x1000 :: word32) 9" by (simp add: is_aligned_def)
-lemma [simp]: "is_aligned (0x2000 :: word32) 9" by (simp add: is_aligned_def)
-
-lemmas ptr_defs = init_tcb_ptr_def idle_thread_ptr_def init_irq_node_ptr_def 
-                  init_globals_frame_def init_global_pd_def
-lemmas state_defs = init_A_st_def init_kheap_def init_arch_state_def ptr_defs 
-
-lemma [simp]: "is_tcb (TCB t)" by (simp add: is_tcb_def)
-
-lemma [simp]: "ran (empty_cnode n) = {Structures_A.NullCap}"
-  apply (auto simp: ran_def empty_cnode_def)
-  apply (rule_tac x="replicate n False" in exI)
-  apply simp
-  done
-
-lemma empty_cnode_apply[simp]:
-  "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = Structures_A.NullCap)"
-  by (auto simp add: empty_cnode_def)
-
-lemma valid_cs_size_empty[simp]:
-  "valid_cs_size n (empty_cnode n) = (n < word_bits - cte_level_bits)"
-  apply (simp add: valid_cs_size_def)
-  apply (insert wf_empty_bits [of n])
-  apply fastforce
-  done
-
-lemma init_cdt [simp]:
-  "cdt init_A_st = init_cdt"
-  by (simp add: state_defs)
-
-lemma mdp_parent_empty [simp]:
-  "\<not>empty \<Turnstile> x \<rightarrow> y"
-  apply clarsimp
-  apply (drule tranclD)
-  apply (clarsimp simp: cdt_parent_of_def)
-  done
-
-lemma descendants_empty [simp]:
-  "descendants_of x empty = {}"
-  by (clarsimp simp: descendants_of_def)
-
-lemma [simp]: "\<not>is_reply_cap Structures_A.NullCap"
-  by (simp add: is_reply_cap_def)
-
-lemma [simp]: "cap_range Structures_A.NullCap = {}"
-  by (simp add: cap_range_def)
-
-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 simp
-  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  
-
-lemma mask_pde_mapping_bits:
-  "mask 20 = 2^pde_mapping_bits - 1"
-  by (simp add: mask_def pde_mapping_bits_def)
-
-
-
-lemma init_irq_ptrs_ineqs:
-  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
-  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
-                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
-  "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
-                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
-proof -
-  have P: "ucast irq < (2 ^ (14 - cte_level_bits) :: word32)"
-    apply (rule order_le_less_trans[OF 
-        ucast_le_ucast[where 'a=10 and 'b=32,simplified,THEN iffD2, OF word_n1_ge]])
-    apply (simp add: cte_level_bits_def minus_one_norm)
-    done
-  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) \<ge> init_irq_node_ptr"
-    apply (rule is_aligned_no_wrap'[where sz=14])
-     apply (simp add: is_aligned_def init_irq_node_ptr_def kernel_base_def)
-    apply (rule shiftl_less_t2n[OF P])
-    apply simp
-    done
-  show Q: "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits) + 2 ^ cte_level_bits - 1
-                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
-    apply (simp only: add_diff_eq[symmetric] add.assoc)
-    apply (rule word_add_le_mono2)
-     apply (simp only: trans [OF shiftl_t2n mult.commute])
-     apply (rule nasty_split_lt[OF P])
-      apply (simp_all add: cte_level_bits_def 
-        word_bits_def kernel_base_def init_irq_node_ptr_def)
-    done
-  show "init_irq_node_ptr + (ucast (irq :: irq) << cte_level_bits)
-                \<le> init_irq_node_ptr + 2 ^ 14 - 1"
-    apply (simp only: add_diff_eq[symmetric])
-    apply (rule word_add_le_mono2)
-     apply (rule minus_one_helper3, rule shiftl_less_t2n[OF P])
-     apply simp
-    apply (simp add: kernel_base_def
-      cte_level_bits_def word_bits_def init_irq_node_ptr_def)
-    done
-qed
-
-lemmas init_irq_ptrs_less_ineqs
-   = init_irq_ptrs_ineqs(1)[THEN order_less_le_trans[rotated]]
-     init_irq_ptrs_ineqs(2-3)[THEN order_le_less_trans]
-
-lemmas init_irq_ptrs_all_ineqs[unfolded init_irq_node_ptr_def cte_level_bits_def]
-   = init_irq_ptrs_ineqs(1)[THEN order_trans[rotated]]
-     init_irq_ptrs_ineqs(2-3)[THEN order_trans]
-     init_irq_ptrs_less_ineqs
-     init_irq_ptrs_less_ineqs[THEN less_imp_neq]
-     init_irq_ptrs_less_ineqs[THEN less_imp_neq, THEN not_sym]
-
-lemmas ucast_le_ucast_10_32 = ucast_le_ucast[where 'a=10 and 'b=32,simplified]
-lemma init_irq_ptrs_eq:
-  "((ucast (irq :: irq) << cte_level_bits)
-        = (ucast (irq' :: irq) << cte_level_bits :: word32))
-      = (irq = irq')"
-  apply safe
-  apply (rule ccontr)
-  apply (erule_tac bnd="ucast (max_word :: irq) + 1"
-              in shift_distinct_helper[rotated 3],
-         safe intro!: plus_one_helper2,
-         simp_all add: ucast_le_ucast_10_32 up_ucast_inj_eq,
-         simp_all add: cte_level_bits_def word_bits_def up_ucast_inj_eq
-                       max_word_def)
-  done
-
-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
-
-lemma pspace_aligned_init_A:
-  "pspace_aligned init_A_st"
-  apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
-                          dom_if_Some cte_level_bits_def)
-  apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
-           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
-  done
-
-lemma pspace_distinct_init_A:
-  "pspace_distinct init_A_st"
-  apply (clarsimp simp: pspace_distinct_def state_defs pageBits_def
-                        empty_cnode_bits kernel_base_def
-                        cte_level_bits_def linorder_not_le cong: if_cong)
-  apply (safe,
-         simp_all add: init_irq_ptrs_all_ineqs
-                       [simplified kernel_base_def, simplified])[1]
-  apply (cut_tac x="init_irq_node_ptr + (ucast irq << cte_level_bits)"
-             and y="init_irq_node_ptr + (ucast irqa << cte_level_bits)"
-             and sz=cte_level_bits in aligned_neq_into_no_overlap)
-     apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def)
-    apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
-    apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
-                     kernel_base_def)
-   apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl])
-   apply (simp add: is_aligned_def cte_level_bits_def init_irq_node_ptr_def
-                    kernel_base_def)
-  apply (simp add: init_irq_node_ptr_def kernel_base_def cte_level_bits_def
-                   linorder_not_le)
-  done
-
-lemma caps_of_state_init_A_st_Null:
-  "caps_of_state (init_A_st::'z::state_ext state) x
-     = (if cte_at x (init_A_st::'z::state_ext state) then Some cap.NullCap else None)"
-  apply (subgoal_tac "\<not> cte_wp_at (op \<noteq> cap.NullCap) x init_A_st")
-   apply (auto simp add: cte_wp_at_caps_of_state)[1]
-  apply (clarsimp, erule cte_wp_atE)
-   apply (auto simp add: state_defs tcb_cap_cases_def split: split_if_asm)
-  done
-
-lemmas cte_wp_at_caps_of_state_eq
-    = cte_wp_at_caps_of_state[where P="op = cap" for cap]
-
-declare ptrFormPAddr_addFromPPtr[simp]
-
-lemma invs_A:
-  "invs init_A_st"
-
-  apply (simp add: invs_def)
-  apply (rule conjI)
-   prefer 2
-   apply (simp add: cur_tcb_def state_defs obj_at_def)
-  apply (simp add: valid_state_def)
-  apply (rule conjI)
-   apply (simp add: valid_pspace_def)
-   apply (rule conjI)
-    apply (clarsimp simp: kernel_base_def valid_objs_def state_defs
-                          valid_obj_def valid_vm_rights_def vm_kernel_only_def
-                          dom_if_Some cte_level_bits_def)
-    apply (rule conjI)
-     apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def 
-                           valid_cap_def obj_at_def valid_tcb_state_def 
-                           cap_aligned_def word_bits_def)+
-    apply (clarsimp simp: valid_cs_def word_bits_def cte_level_bits_def
-                          init_irq_ptrs_all_ineqs valid_tcb_def
-                   split: split_if_asm)
-   apply (rule conjI)
-    apply (clarsimp simp: pspace_aligned_def state_defs wf_obj_bits [OF wf_empty_bits]
-                          dom_if_Some cte_level_bits_def)
-    apply (safe intro!: aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl],
-           simp_all add: is_aligned_def word_bits_def kernel_base_def)[1]
-   apply (rule conjI)
-    apply (simp add:pspace_distinct_init_A)
-   apply (rule conjI)
-    apply (clarsimp simp: if_live_then_nonz_cap_def obj_at_def state_defs)
-   apply (rule conjI)
-    apply (clarsimp simp: zombies_final_def cte_wp_at_cases state_defs 
-                          tcb_cap_cases_def is_zombie_def)
-   apply (clarsimp simp: sym_refs_def state_refs_of_def state_defs)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_mdb_def init_cdt_def no_mloop_def 
-                         mdb_cte_at_def)
-   apply (clarsimp simp: untyped_mdb_def caps_of_state_init_A_st_Null
-                         untyped_inc_def ut_revocable_def
-                         irq_revocable_def reply_master_revocable_def
-                         reply_mdb_def reply_caps_mdb_def
-                         reply_masters_mdb_def)
-   apply (simp add:descendants_inc_def)
-  apply (rule conjI)
-   apply (simp add: valid_ioc_def init_A_st_def init_ioc_def cte_wp_at_cases2)
-   apply (intro allI impI, elim exE conjE)
-   apply (case_tac obj, simp_all add: cap_of_def)
-   apply (clarsimp simp: init_kheap_def split: split_if_asm)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def state_defs)
-  apply (rule conjI)
-   apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def state_defs)
-  apply (rule conjI)
-   apply (clarsimp simp: if_unsafe_then_cap_def caps_of_state_init_A_st_Null)
-  apply (clarsimp simp: valid_reply_caps_def unique_reply_caps_def
-                        has_reply_cap_def pred_tcb_at_def obj_at_def
-                        caps_of_state_init_A_st_Null
-                        cte_wp_at_caps_of_state_eq
-                        valid_reply_masters_def valid_global_refs_def
-                        valid_refs_def[unfolded cte_wp_at_caps_of_state])
-  apply (rule conjI)
-   apply (clarsimp simp: valid_arch_state_def)
-   apply (rule conjI)
-    apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs 
-                          a_type_def)
-   apply (rule conjI)
-    apply (clarsimp simp: valid_asid_table_def state_defs)
-   apply (rule conjI)
-    apply (clarsimp simp: valid_arch_state_def obj_at_def state_defs 
-                          a_type_def)
-   apply (rule conjI)
-    apply (simp add: valid_global_pts_def state_defs)
-   apply (simp add: state_defs is_inv_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_irq_node_def obj_at_def state_defs
-                         is_cap_table_def wf_empty_bits
-                         init_irq_ptrs_all_ineqs cte_level_bits_def
-                         init_irq_ptrs_eq[unfolded cte_level_bits_def])
-   apply (intro conjI)
-    apply (rule inj_onI)
-    apply (simp add: init_irq_ptrs_eq[unfolded cte_level_bits_def])
-   apply clarsimp
-   defer
-  apply (simp add: valid_irq_handlers_def caps_of_state_init_A_st_Null
-                   ran_def cong: rev_conj_cong)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_irq_states_def init_A_st_def init_machine_state_def valid_irq_masks_def init_irq_masks_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_machine_state_def init_A_st_def
-                         init_machine_state_def init_underlying_memory_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_arch_objs_def obj_at_def state_defs)
-   apply (clarsimp simp: vs_lookup_def vs_asid_refs_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_arch_caps_def)
-   apply (rule conjI)
-    apply (clarsimp simp: valid_vs_lookup_def)
-    apply (clarsimp simp: vs_lookup_pages_def state_defs vs_asid_refs_def)
-   apply (clarsimp simp: valid_table_caps_def caps_of_state_init_A_st_Null
-                         unique_table_caps_def unique_table_refs_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_global_objs_def state_defs)
-   apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
-                         valid_pde_mappings_def)
-   apply (simp add: kernel_base_def kernel_mapping_slots_def 
-                    Platform.ARM.addrFromPPtr_def physMappingOffset_def
-                    kernelBase_addr_def physBase_def pageBits_def is_aligned_def)
-  apply (rule conjI)
-   apply (simp add: valid_kernel_mappings_def state_defs
-                         valid_kernel_mappings_if_pd_def pde_ref_def
-                         ran_def)
-   apply (auto simp: pde_ref_def split: split_if_asm)[1]
-  apply (rule conjI)
-   apply (clarsimp simp: equal_kernel_mappings_def state_defs obj_at_def)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_asid_map_def state_defs)
-  apply (rule conjI)
-   apply (clarsimp simp: valid_global_pd_mappings_def obj_at_def state_defs
-                         valid_pd_kernel_mappings_def mask_pde_mapping_bits)
-   apply (simp add: valid_pde_kernel_mappings_def kernel_base_def)
-   apply (rule conjI)
-    apply (fastforce simp:pde_mapping_bits_def)
-   apply (intro ballI impI)
-   apply (clarsimp simp:pde_mapping_bits_def)
-   apply word_bitwise
-   apply clarsimp
-  apply (rule conjI)
-   apply (clarsimp simp: pspace_in_kernel_window_def state_defs mask_def)
-   apply (intro conjI impI)
-            apply (rule in_kernel_base|simp)+
-         apply (erule exE,drule sym,simp add:field_simps)
-         apply (rule in_kernel_base[unfolded add.commute])
-          apply (rule word_less_add_right,simp add:cte_level_bits_def)
-           apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
-          apply simp
-         apply (simp add:cte_level_bits_def field_simps)
-         apply (subst add.commute)
-         apply (rule le_plus')
-          apply simp+
-          apply (rule less_imp_le)
-          apply (rule less_le_trans[OF shiftl_less_t2n'[OF ucast_less]],simp+)[1]
-     apply (rule in_kernel_base|simp)+
-  apply (simp add: cap_refs_in_kernel_window_def caps_of_state_init_A_st_Null
-                  valid_refs_def[unfolded cte_wp_at_caps_of_state])
-  apply word_bitwise
-  done
-
-end
-
 axiomatization where
   akernel_init_invs: "\<forall>((tc,s),m,e) \<in> Init_A. invs s \<and> ct_running s"