theory CNode_DR

lemma set_asid_pool_empty'_helper:
  "n < 1023 \<Longrightarrow>
   (if x = ucast ((1 :: word32) + of_nat n) then None else if x \<le> of_nat n then None else ap x) =
   (if (x :: 10 word) \<le> 1 + of_nat n then None else ap x)" apply (frule of_nat_mono_maybe[where x="2^10 - 1" and 'a=10, simplified]) apply (subgoal_tac "ucast (1 + of_nat n :: word32) = (1 + of_nat n :: 10 word)") prefer 2 apply (rule word_unat.Rep_eqD) apply (simp add: unat_word_ariths unat_ucast unat_of_nat) apply (subst word_le_make_less[where y="of_nat n"]) apply (auto simp: add.commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 1023 \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x)
 2. \<lbrakk>n < 1023; word_of_nat n < 0x3FF\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n
 2. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF\<rbrakk> \<Longrightarrow> unat (UCAST(32 \<rightarrow> 10) (1 + word_of_nat n)) = unat (1 + word_of_nat n)
 2. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x \<le> word_of_nat n then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> - 1
 2. \<lbrakk>n < 1023; word_of_nat n < 0x3FF; UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) = 1 + word_of_nat n\<rbrakk> \<Longrightarrow> (if x = UCAST(32 \<rightarrow> 10) (1 + word_of_nat n) then None else if x < word_of_nat n + 1 then None else ap x) = (if x \<le> 1 + word_of_nat n then None else ap x) proof (prove)
goal:
No subgoals!