theory ArchKernelInit_AI

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
                        linorder_not_le cte_level_bits_def
                  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;
         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) apply (rule aligned_add_aligned[OF _ is_aligned_shiftl_self order_refl]) apply (simp add: is_aligned_def) apply (simp add: linorder_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct init_A_st proof (prove)
goal (1 subgoal):
 1. \<And>x. ((\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = x) \<longrightarrow> (x = 0xE0001000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE00011FF < y \<or> y + 0xF < 0xE0001000 \<or> y + 0xF < y)) \<and> (x \<noteq> 0xE0001000 \<longrightarrow> (x = 0xE0005000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE0005FFF < y \<or> y + 0xF < 0xE0005000 \<or> y + 0xF < y)) \<and> (x \<noteq> 0xE0005000 \<longrightarrow> (x = 0xE0060000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE0063FFF < y \<or> y + 0xF < 0xE0060000 \<or> y + 0xF < y)) \<and> (x \<noteq> 0xE0060000 \<longrightarrow> (\<forall>y. ((\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> (y = 0xE0001000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0001000 \<or> 0xE00011FF < x) \<and> (y \<noteq> 0xE0001000 \<longrightarrow> (y = 0xE0005000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0005000 \<or> 0xE0005FFF < x) \<and> (y \<noteq> 0xE0005000 \<longrightarrow> (y = 0xE0060000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0060000 \<or> 0xE0063FFF < x) \<and> (y \<noteq> 0xE0060000 \<longrightarrow> x \<noteq> y \<longrightarrow> x + 0xF < x \<or> x + 0xF < y \<or> y + 0xF < x \<or> y + 0xF < y)))) \<and> ((\<forall>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> y) \<longrightarrow> (y = 0xE0001000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0001000 \<or> 0xE00011FF < x) \<and> (y \<noteq> 0xE0001000 \<longrightarrow> (y = 0xE0005000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0005000 \<or> 0xE0005FFF < x) \<and> (y \<noteq> 0xE0005000 \<longrightarrow> y = 0xE0060000 \<longrightarrow> x + 0xF < x \<or> x + 0xF < 0xE0060000 \<or> 0xE0063FFF < x)))))))) \<and> ((\<forall>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<noteq> x) \<longrightarrow> (x = 0xE0001000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE00011FF < y \<or> y + 0xF < 0xE0001000 \<or> y + 0xF < y)) \<and> (x \<noteq> 0xE0001000 \<longrightarrow> (x = 0xE0005000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE0005FFF < y \<or> y + 0xF < 0xE0005000 \<or> y + 0xF < y)) \<and> (x \<noteq> 0xE0005000 \<longrightarrow> x = 0xE0060000 \<longrightarrow> (\<forall>y. (\<exists>irq. 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) = y) \<longrightarrow> y \<noteq> 0xE0001000 \<longrightarrow> y \<noteq> 0xE0005000 \<longrightarrow> y \<noteq> 0xE0060000 \<longrightarrow> 0xE0063FFF < y \<or> y + 0xF < 0xE0060000 \<or> y + 0xF < y)))) proof (prove)
goal (1 subgoal):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (3 subgoals):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned (0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4)) 4
 2. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned (0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)) 4
 3. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> \<not> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (3 subgoals):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 4
 2. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned (0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)) 4
 3. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> \<not> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (2 subgoals):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned (0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)) 4
 2. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> \<not> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (2 subgoals):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> is_aligned 0xE0008000 4
 2. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> \<not> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal (1 subgoal):
 1. \<And>irq irqa. \<lbrakk>UCAST(10 \<rightarrow> 32) irq << 4 \<noteq> UCAST(10 \<rightarrow> 32) irqa << 4; \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); \<not> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4); 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irq << 4) \<longrightarrow> \<not> 0xE0008000 + (UCAST(10 \<rightarrow> 32) irqa << 4) \<le> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4)\<rbrakk> \<Longrightarrow> 0xE000800F + (UCAST(10 \<rightarrow> 32) irqa << 4) < 0xE0008000 + (UCAST(10 \<rightarrow> 32) irq << 4) proof (prove)
goal:
No subgoals!