theory Finalise_DR

lemma transform_page_table_contents_upd:
  "(transform_page_table_contents fun)(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte) =
   transform_page_table_contents (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))" apply (rule ext) apply (clarsimp simp: transform_page_table_contents_def unat_map_def) apply (subgoal_tac "unat (y && mask pt_bits >> 2) < 256") apply (rule conjI|clarsimp)+ apply (simp only: ucast_nat_def[symmetric]) apply (drule word_of_nat_inj[rotated -1]; clarsimp simp: mask_pt_bits_less) apply simp apply (rule unat_less_helper) apply (subst shiftr_div_2n_w) apply (clarsimp simp:word_size)+ apply (rule word_div_mult,simp) apply (clarsimp simp:pt_bits_def pageBits_def) apply (rule and_mask_less_size[where n = 10,simplified],simp add:word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (transform_page_table_contents fun)(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte) = transform_page_table_contents (fun(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := pte)) proof (prove)
goal (1 subgoal):
 1. \<And>x. ((transform_page_table_contents fun)(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte)) x = transform_page_table_contents (fun(UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) := pte)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (word_of_nat x = UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> (x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256) \<and> (x \<noteq> unat (y && mask pt_bits >> 2) \<longrightarrow> x < 256 \<longrightarrow> transform_pte (fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = transform_pte pte)) \<and> (word_of_nat x \<noteq> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256) proof (prove)
goal (2 subgoals):
 1. \<And>x. unat (y && mask pt_bits >> 2) < 256 \<Longrightarrow> (word_of_nat x = UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> (x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256) \<and> (x \<noteq> unat (y && mask pt_bits >> 2) \<longrightarrow> x < 256 \<longrightarrow> transform_pte (fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = transform_pte pte)) \<and> (word_of_nat x \<noteq> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256)
 2. \<And>x. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>unat (y && mask pt_bits >> 2) < 256; word_of_nat x = UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2); x \<noteq> unat (y && mask pt_bits >> 2); x < 256\<rbrakk> \<Longrightarrow> transform_pte (fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))) = transform_pte pte
 2. \<And>x. unat (y && mask pt_bits >> 2) < 256 \<Longrightarrow> word_of_nat x \<noteq> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256
 3. \<And>x. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>unat (y && mask pt_bits >> 2) < 256; word_of_nat x = word_of_nat (unat (y && mask pt_bits >> 2)); x \<noteq> unat (y && mask pt_bits >> 2); x < 256\<rbrakk> \<Longrightarrow> transform_pte (fun (word_of_nat (unat (y && mask pt_bits >> 2)))) = transform_pte pte
 2. \<And>x. unat (y && mask pt_bits >> 2) < 256 \<Longrightarrow> word_of_nat x \<noteq> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256
 3. \<And>x. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (2 subgoals):
 1. \<And>x. unat (y && mask pt_bits >> 2) < 256 \<Longrightarrow> word_of_nat x \<noteq> UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2) \<longrightarrow> x = unat (y && mask pt_bits >> 2) \<longrightarrow> unat (y && mask pt_bits >> 2) < 256
 2. \<And>x. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. \<And>x. unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. \<And>x. y && mask pt_bits >> 2 < word_of_nat 256 proof (prove)
goal (1 subgoal):
 1. \<And>x. (y && mask pt_bits) div 2\<^sup>2 < word_of_nat 256 proof (prove)
goal (1 subgoal):
 1. (y && mask pt_bits) div 4 < 0x100 proof (prove)
goal (1 subgoal):
 1. y && mask pt_bits < 0x100 * 4 proof (prove)
goal (1 subgoal):
 1. y && mask 10 < 0x400 proof (prove)
goal:
No subgoals!