theory Arch_DR

lemma unat_map_upd:
  "unat_map (Some \<circ> transform_asid_table_entry \<circ> (asid_table as)(asid_high_bits_of base \<mapsto> frame)) =
   (unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table as))
     (unat (asid_high_bits_of base) \<mapsto> AsidPoolCap frame 0)" apply (rule ext) apply (clarsimp simp:unat_map_def asid_high_bits_of_def transform_asid_table_entry_def) apply (intro impI conjI) apply (subgoal_tac "x<256") apply (clarsimp simp: unat_map_def asid_high_bits_of_def asid_low_bits_def
                           transform_asid_table_entry_def transform_asid_def) apply (drule_tac x="of_nat x" in unat_cong) apply (subst (asm) word_unat.Abs_inverse) apply (clarsimp simp:unats_def unat_ucast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat_map (Some \<circ> transform_asid_table_entry \<circ> (asid_table as)(asid_high_bits_of base \<mapsto> frame)) = (unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table as))(unat (asid_high_bits_of base) \<mapsto> AsidPoolCap frame 0) proof (prove)
goal (1 subgoal):
 1. \<And>x. unat_map (Some \<circ> transform_asid_table_entry \<circ> (asid_table as)(asid_high_bits_of base \<mapsto> frame)) x = ((unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table as))(unat (asid_high_bits_of base) \<mapsto> AsidPoolCap frame 0)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits) \<longrightarrow> (x < 128 \<longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) \<longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)) \<and> (\<not> x < 128 \<longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)))) \<and> (word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits) \<longrightarrow> \<not> x < 128 \<longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)
 2. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))
 3. \<And>x. \<lbrakk>word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)); x < 256\<rbrakk> \<Longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)
 2. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x < 256
 3. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))
 4. \<And>x. \<lbrakk>word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> 10); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> 10))\<rbrakk> \<Longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> 10)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)
 2. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x < 256
 3. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))
 4. \<And>x. \<lbrakk>word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> 10)); unat (word_of_nat x) = unat (UCAST(32 \<rightarrow> 7) (base >> 10))\<rbrakk> \<Longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> 10)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)
 2. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x < 256
 3. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))
 4. \<And>x. \<lbrakk>word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) proof (prove)
goal (5 subgoals):
 1. \<And>x. \<lbrakk>x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> 10))\<rbrakk> \<Longrightarrow> x \<in> unats LENGTH(7)
 2. \<And>x. \<lbrakk>x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> 10)); x = unat (UCAST(32 \<rightarrow> 7) (base >> 10))\<rbrakk> \<Longrightarrow> AsidPoolCap frame 0 = (case asid_table as (UCAST(32 \<rightarrow> 7) (base >> 10)) of None \<Rightarrow> cdl_cap.NullCap | Some p \<Rightarrow> AsidPoolCap p 0)
 3. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); x < 128; x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> x < 256
 4. \<And>x. \<lbrakk>word_of_nat x = UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits))
 5. \<And>x. \<lbrakk>word_of_nat x \<noteq> UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits); \<not> x < 128\<rbrakk> \<Longrightarrow> x \<noteq> unat (UCAST(32 \<rightarrow> 7) (base >> local.asid_low_bits)) proof (prove)
goal:
No subgoals!