theory ADT_C

lemma mask_pageBits_shift_sum:
  "unat n = unat (p && mask 2) \<Longrightarrow>
  (p && ~~ mask pageBits) + (p && mask pageBits >> 2) * 4 + n = (p::word32)" apply (clarsimp simp: word_shift_by_2) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size) apply arith apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size) apply (rule word_eqI) apply (clarsimp simp: word_size pageBits_def nth_shiftl nth_shiftr word_ops_nth_size) apply (auto simp: linorder_not_less SucSucMinus) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat n = unat (p && mask 2) \<Longrightarrow> (p && ~~ mask pageBits) + (p && mask pageBits >> 2) * 4 + n = p proof (prove)
goal (1 subgoal):
 1. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits) + (p && mask pageBits >> 2 << 2) + (p && mask 2) = p proof (prove)
goal (2 subgoals):
 1. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits) && (p && mask pageBits >> 2 << 2) = 0
 2. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) + (p && mask 2) = p proof (prove)
goal (2 subgoals):
 1. \<And>na. n = p && mask 2 \<Longrightarrow> na < size ((p && ~~ mask pageBits) && (p && mask pageBits >> 2 << 2)) \<longrightarrow> ((p && ~~ mask pageBits) && (p && mask pageBits >> 2 << 2)) !! na = 0 !! na
 2. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) + (p && mask 2) = p proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>n = p && mask 2; na < 32; p !! Suc (Suc 0); p !! na; \<not> na < 12; na - 2 < 10\<rbrakk> \<Longrightarrow> False
 2. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) + (p && mask 2) = p proof (prove)
goal (1 subgoal):
 1. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) + (p && mask 2) = p proof (prove)
goal (2 subgoals):
 1. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) && p && mask 2 = 0
 2. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) || p && mask 2 = p proof (prove)
goal (2 subgoals):
 1. \<And>na. n = p && mask 2 \<Longrightarrow> na < size ((p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) && p && mask 2) \<longrightarrow> ((p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) && p && mask 2) !! na = 0 !! na
 2. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) || p && mask 2 = p proof (prove)
goal (1 subgoal):
 1. n = p && mask 2 \<Longrightarrow> (p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) || p && mask 2 = p proof (prove)
goal (1 subgoal):
 1. \<And>na. n = p && mask 2 \<Longrightarrow> na < size ((p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) || p && mask 2) \<longrightarrow> ((p && ~~ mask pageBits || (p && mask pageBits >> 2 << 2)) || p && mask 2) !! na = p !! na proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>n = p && mask 2; na < 32\<rbrakk> \<Longrightarrow> (p !! na \<and> \<not> na < 12 \<or> 2 \<le> na \<and> p !! Suc (Suc (na - 2)) \<and> na - 2 < 30 \<and> na - 2 < 10 \<or> p !! na \<and> na < 2) = p !! na proof (prove)
goal:
No subgoals!