theory CNode_DR

lemma set_asid_pool_empty':
  "n < 2 ^ asid_low_bits \<Longrightarrow>
   do ap \<leftarrow> get_asid_pool a; set_asid_pool a (\<lambda>x. if x \<le> of_nat n then None else ap x) od =
   mapM_x (\<lambda>slot. get_asid_pool a >>= (\<lambda>pool. set_asid_pool a (pool(ucast slot:=None))))
          [0 :: word32 .e. of_nat n]" apply (induct n) apply (simp add: mapM_x_Cons mapM_x_Nil fun_upd_def) apply (subgoal_tac "of_nat n < (2 :: word32) ^ word_bits - 1") prefer 2 apply (rule of_nat_mono_maybe[where x="2^word_bits - 1", simplified]) apply (simp add:word_bits_def) apply (simp add:asid_low_bits_def word_bits_def) apply (simp, drule sym) apply (simp add:upto_enum_inc_1 mapM_append_single bind_assoc fun_upd_def
                  set_get_set_asid_pool set_asid_pool_empty'_helper asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n] proof (prove)
goal (2 subgoals):
 1. 0 < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat 0 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 0]
 2. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)]
 2. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ word_bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ word_bits - 1
 2. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> 2 ^ word_bits - Suc 0 < 2 ^ LENGTH(32)
 2. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits - Suc 0
 3. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits - Suc 0
 2. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 2 ^ local.asid_low_bits \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n 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 n]; Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat (Suc n) 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 (Suc n)] proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Suc n < 2 ^ local.asid_low_bits; word_of_nat n < 2 ^ word_bits - 1; 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 n] = do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> word_of_nat n then None else ap x)
od\<rbrakk> \<Longrightarrow> do ap <- get_asid_pool a;
set_asid_pool a (\<lambda>x. if x \<le> 1 + word_of_nat n 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. 1 + word_of_nat n] proof (prove)
goal:
No subgoals!