theory CNode_DR

lemma set_asid_pool_empty:
  "set_asid_pool a Map.empty \<equiv>
   mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None))))
          [0 :: word32 .e. 2 ^ ARM_A.asid_low_bits - 1]" using set_asid_pool_empty' [of "2 ^ ARM_A.asid_low_bits - 1" a] apply - apply (rule eq_reflection) apply simp apply (subst (asm) empty_pool) apply (simp add: get_set_asid_pool) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_asid_pool a (\<lambda>x. None) \<equiv> mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
using this:
2 ^ local.asid_low_bits - 1 < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (2 ^ local.asid_low_bits - 1) then None else ap x)
od = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. word_of_nat (2 ^ local.asid_low_bits - 1)]

goal (1 subgoal):
 1. set_asid_pool a (\<lambda>x. None) \<equiv> mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. (2 ^ local.asid_low_bits - 1 < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (2 ^ local.asid_low_bits - 1) then None else ap x)
od = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. word_of_nat (2 ^ local.asid_low_bits - 1)]) \<Longrightarrow> set_asid_pool a (\<lambda>x. None) \<equiv> mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. (2 ^ local.asid_low_bits - 1 < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (2 ^ local.asid_low_bits - 1) then None else ap x)
od = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. word_of_nat (2 ^ local.asid_low_bits - 1)]) \<Longrightarrow> set_asid_pool a (\<lambda>x. None) = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> 2 ^ local.asid_low_bits - 1 then None else ap x)
od = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] \<Longrightarrow> set_asid_pool a (\<lambda>x. None) = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal (1 subgoal):
 1. do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. None)
od = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] \<Longrightarrow> set_asid_pool a (\<lambda>x. None) = mapM_x (\<lambda>slot. do pool <- get_asid_pool a;
set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) slot := None))
od) [0 .e. 2 ^ local.asid_low_bits - 1] proof (prove)
goal:
No subgoals!