theory ArchArch_AI

lemma ucast_fst_hd_assocs:
  "- dom (\<lambda>x. pool (ucast (x::asid_low_index)::machine_word)) \<inter> {x. ucast x + (w::machine_word) \<noteq> 0} \<noteq> {}
  \<Longrightarrow>
  fst (hd [(x, y)\<leftarrow>assocs pool . x \<le> 2 ^ asid_low_bits - 1 \<and> x + w \<noteq> 0 \<and> y = None]) =
  ucast (fst (hd [(x, y)\<leftarrow>assocs (\<lambda>a::asid_low_index. pool (ucast a)) .
                          x \<le> 2 ^ asid_low_bits - 1 \<and>
                          ucast x + w \<noteq> 0 \<and> y = None]))" apply (simp add: ucast_assocs[unfolded o_def]) apply (simp add: filter_map split_def) apply (simp cong: conj_cong add: ucast_ucast_len) apply (simp add: asid_low_bits_def minus_one_norm) apply (simp add: ord_le_eq_trans [OF word_n1_ge]) apply (simp add: word_le_make_less) apply (subgoal_tac "P" for P)   (* cut_tac but more awesome *)
    apply (subst hd_map, assumption) apply simp apply (rule sym, rule ucast_ucast_len) apply (drule hd_in_set) apply simp apply (simp add: assocs_empty_dom_comp null_def split_def) apply (simp add: ucast_assocs[unfolded o_def] filter_map split_def) apply (simp cong: conj_cong add: ucast_ucast_len) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>(x, y). x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + w \<noteq> 0 \<and> y = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (filter (\<lambda>(x, y). x \<le> 2 ^ local.asid_low_bits - 1 \<and> UCAST(10 \<rightarrow> 32) x + w \<noteq> 0 \<and> y = None) (assocs (\<lambda>a. pool (UCAST(10 \<rightarrow> 32) a)))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>(x, y). x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + w \<noteq> 0 \<and> y = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (filter (\<lambda>(x, y). x \<le> 2 ^ local.asid_low_bits - 1 \<and> UCAST(10 \<rightarrow> 32) x + w \<noteq> 0 \<and> y = None) (map (\<lambda>(a, y). (UCAST(32 \<rightarrow> 10) a, y)) (filter (\<lambda>(a, y). a < 0x400) (assocs pool)))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p \<le> 2 ^ local.asid_low_bits - 1 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> UCAST(32 \<rightarrow> 10) (fst x) \<le> 2 ^ local.asid_low_bits - 1 \<and> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (fst x)) + w \<noteq> 0 \<and> snd x = None) (assocs pool))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p \<le> 2 ^ local.asid_low_bits - 1 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> UCAST(32 \<rightarrow> 10) (fst x) \<le> 2 ^ local.asid_low_bits - 1 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p \<le> 0x3FF \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> UCAST(32 \<rightarrow> 10) (fst x) \<le> 0x3FF \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p \<le> 0x3FF \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))))) proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p < 0x400 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; ?P25\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p < 0x400 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)))))
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> ?P25 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; ?P25\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p < 0x400 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (hd (map (\<lambda>p. (UCAST(32 \<rightarrow> 10) (fst p), snd p)) (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)))))
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> ?P25 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> []\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p < 0x400 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (fst (UCAST(32 \<rightarrow> 10) (fst (hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)))), snd (hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)))))
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> []\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>p. fst p < 0x400 \<and> fst p + w \<noteq> 0 \<and> snd p = None) (assocs pool))) = UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (fst (hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)))))
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> []\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))) < 2 ^ LENGTH(10)
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {}; hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool)) \<in> set (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))\<rbrakk> \<Longrightarrow> fst (hd (filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool))) < 2 ^ LENGTH(10)
 2. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. - dom (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + w \<noteq> 0} \<noteq> {} \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>p. UCAST(10 \<rightarrow> 32) (fst p) + w \<noteq> 0 \<and> snd p = None) (assocs (\<lambda>x. pool (UCAST(10 \<rightarrow> 32) x))) \<noteq> [] \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. fst x < 0x400 \<and> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) (fst x)) + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] \<Longrightarrow> filter (\<lambda>x. fst x < 0x400 \<and> fst x + w \<noteq> 0 \<and> snd x = None) (assocs pool) \<noteq> [] proof (prove)
goal:
No subgoals!