[STATEMENT]
lemma mset_del_min: assumes "braun t" "t \<noteq> Leaf"
shows "mset_tree(del_min t) = mset_tree t - {#get_min t#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
proof(cases t rule: del_min.cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. t = \<langle>\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 2. \<And>x r. t = \<langle>\<langle>\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 3. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
t = \<langle>\<rangle>

goal (3 subgoals):
 1. t = \<langle>\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 2. \<And>x r. t = \<langle>\<langle>\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 3. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
braun t
t \<noteq> \<langle>\<rangle>
t = \<langle>\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
braun t
t \<noteq> \<langle>\<rangle>
t = \<langle>\<rangle>

goal (1 subgoal):
 1. mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mset_tree (del_min t) = mset_tree t - {#get_min t#}

goal (2 subgoals):
 1. \<And>x r. t = \<langle>\<langle>\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 2. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x r. t = \<langle>\<langle>\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 2. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
t = \<langle>\<langle>\<rangle>, x_, r_\<rangle>

goal (2 subgoals):
 1. \<And>x r. t = \<langle>\<langle>\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
 2. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
braun t
t \<noteq> \<langle>\<rangle>
t = \<langle>\<langle>\<rangle>, x_, r_\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
braun t
t \<noteq> \<langle>\<rangle>
t = \<langle>\<langle>\<rangle>, x_, r_\<rangle>

goal (1 subgoal):
 1. mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
mset_tree (del_min t) = mset_tree t - {#get_min t#}

goal (1 subgoal):
 1. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
case [simp]: (3 ll b lr a r)
[PROOF STATE]
proof (state)
this:
t = \<langle>\<langle>ll, b, lr\<rangle>, a, r\<rangle>

goal (1 subgoal):
 1. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
have "mset_tree(sift_down r y l') = mset_tree t - {#a#}"
    if del: "del_left (Node ll b lr) = (y,l')" for y l'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset_tree (sift_down r y l') = mset_tree t - {#a#}
[PROOF STEP]
using assms del_left_mset[OF del] del_left_size[OF del]
      del_left_braun[OF del] del_left_mset_plus[OF del]
[PROOF STATE]
proof (prove)
using this:
braun t
t \<noteq> \<langle>\<rangle>
\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> y \<in># mset_tree \<langle>ll, b, lr\<rangle> \<and> mset_tree l' = mset_tree \<langle>ll, b, lr\<rangle> - {#y#}
\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> size \<langle>ll, b, lr\<rangle> = size l' + 1
\<lbrakk>\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle>; braun \<langle>ll, b, lr\<rangle>\<rbrakk> \<Longrightarrow> braun l'
\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> mset_tree \<langle>ll, b, lr\<rangle> = {#y#} + mset_tree l'

goal (1 subgoal):
 1. mset_tree (sift_down r y l') = mset_tree t - {#a#}
[PROOF STEP]
apply (subst mset_sift_down)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>braun t; t \<noteq> \<langle>\<rangle>; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> y \<in># mset_tree \<langle>ll, b, lr\<rangle> \<and> mset_tree l' = mset_tree \<langle>ll, b, lr\<rangle> - {#y#}; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> size \<langle>ll, b, lr\<rangle> = size l' + 1; \<lbrakk>\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle>; braun \<langle>ll, b, lr\<rangle>\<rbrakk> \<Longrightarrow> braun l'; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> mset_tree \<langle>ll, b, lr\<rangle> = {#y#} + mset_tree l'\<rbrakk> \<Longrightarrow> braun \<langle>r, y, l'\<rangle>
 2. \<lbrakk>braun t; t \<noteq> \<langle>\<rangle>; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> y \<in># mset_tree \<langle>ll, b, lr\<rangle> \<and> mset_tree l' = mset_tree \<langle>ll, b, lr\<rangle> - {#y#}; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> size \<langle>ll, b, lr\<rangle> = size l' + 1; \<lbrakk>\<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle>; braun \<langle>ll, b, lr\<rangle>\<rbrakk> \<Longrightarrow> braun l'; \<langle>ll, b, lr\<rangle> \<noteq> \<langle>\<rangle> \<Longrightarrow> mset_tree \<langle>ll, b, lr\<rangle> = {#y#} + mset_tree l'\<rbrakk> \<Longrightarrow> {#y#} + (mset_tree r + mset_tree l') = mset_tree t - {#a#}
[PROOF STEP]
apply (auto simp: ac_simps del_left_mset_plus[OF del])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
del_left \<langle>ll, b, lr\<rangle> = (?y, ?l') \<Longrightarrow> mset_tree (sift_down r ?y ?l') = mset_tree t - {#a#}

goal (1 subgoal):
 1. \<And>v va vb x r. t = \<langle>\<langle>v, va, vb\<rangle>, x, r\<rangle> \<Longrightarrow> mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
del_left \<langle>ll, b, lr\<rangle> = (?y, ?l') \<Longrightarrow> mset_tree (sift_down r ?y ?l') = mset_tree t - {#a#}

goal (1 subgoal):
 1. mset_tree (del_min t) = mset_tree t - {#get_min t#}
[PROOF STEP]
by(auto split: prod.split)
[PROOF STATE]
proof (state)
this:
mset_tree (del_min t) = mset_tree t - {#get_min t#}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma approximating_imp_booloan_semantics_nospoofing:
      assumes "matcher_agree_on_exact_matches \<gamma> common_matcher"
      and "simple_ruleset rs"
      and no_spoofing: "no_spoofing TYPE('pkt_ext) ipassmt rs"
      shows "\<forall> iface \<in> dom ipassmt. \<forall>p::('i::len,'pkt_ext) tagged_packet_scheme.
                (\<Gamma>,\<gamma>,p\<lparr>p_iiface:=iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<longrightarrow>
                    p_src p \<in> (ipcidr_union_set (set (the (ipassmt iface))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>iface\<in>dom ipassmt. \<forall>p. \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
unfolding no_spoofing_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>iface\<in>dom ipassmt. \<forall>p. \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
proof(intro ballI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
fix iface p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
assume i: "iface \<in> dom ipassmt"
           and a: "\<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow"
[PROOF STATE]
proof (state)
this:
iface \<in> dom ipassmt
\<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow

goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
from no_spoofing[unfolded no_spoofing_def] i
[PROOF STATE]
proof (chain)
picking this:
\<forall>iface\<in>dom ipassmt. \<forall>p. (common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
iface \<in> dom ipassmt
[PROOF STEP]
have no_spoofing':
          "(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow>
           p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>iface\<in>dom ipassmt. \<forall>p. (common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
iface \<in> dom ipassmt

goal (1 subgoal):
 1. (common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))

goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
from assms simple_imp_good_ruleset FinalAllows_subseteq_in_doubt_allow[where rs=rs]
[PROOF STATE]
proof (chain)
picking this:
matcher_agree_on_exact_matches \<gamma> common_matcher
simple_ruleset rs
no_spoofing TYPE('pkt_ext) ipassmt rs
simple_ruleset ?rs \<Longrightarrow> good_ruleset ?rs
\<lbrakk>matcher_agree_on_exact_matches ?\<gamma> ?\<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> _Collect p (?\<Gamma>,?\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((?\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)
[PROOF STEP]
have
          "{p. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow} \<subseteq> {p. (common_matcher, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow}"
[PROOF STATE]
proof (prove)
using this:
matcher_agree_on_exact_matches \<gamma> common_matcher
simple_ruleset rs
no_spoofing TYPE('pkt_ext) ipassmt rs
simple_ruleset ?rs \<Longrightarrow> good_ruleset ?rs
\<lbrakk>matcher_agree_on_exact_matches ?\<gamma> ?\<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> _Collect p (?\<Gamma>,?\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((?\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)

goal (1 subgoal):
 1. _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((common_matcher, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
_Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((common_matcher, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)

goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
_Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((common_matcher, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)
[PROOF STEP]
have "(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
_Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((common_matcher, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)

goal (1 subgoal):
 1. (common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (1 subgoal):
 1. \<And>iface p. \<lbrakk>iface \<in> dom ipassmt; \<Gamma>,\<gamma>,p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
with no_spoofing'
[PROOF STATE]
proof (chain)
picking this:
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
[PROOF STEP]
show "p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))"
[PROOF STATE]
proof (prove)
using this:
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<longrightarrow> p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
(common_matcher, in_doubt_allow),p\<lparr>p_iiface := iface_sel iface\<rparr>\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow

goal (1 subgoal):
 1. p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p_src p \<in> ipcidr_union_set (set (the (ipassmt iface)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_iff_udvd:
  \<open>is_aligned w n \<longleftrightarrow> 2 ^ n udvd w\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (2 ^ n udvd w)
[PROOF STEP]
by transfer (simp flip: take_bit_eq_0_iff add: min_def)


[STATEMENT]
lemma is_aligned_iff_take_bit_eq_0:
  \<open>is_aligned w n \<longleftrightarrow> take_bit n w = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (take_bit n w = 0)
[PROOF STEP]
by (simp add: is_aligned_iff_udvd take_bit_eq_0_iff exp_dvd_iff_exp_udvd)


[STATEMENT]
lemma is_aligned_iff_dvd_int:
  \<open>is_aligned ptr n \<longleftrightarrow> 2 ^ n dvd uint ptr\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr n = (2 ^ n dvd uint ptr)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma is_aligned_0 [simp]:
  \<open>is_aligned 0 n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned 0 n
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma is_aligned_at_0 [simp]:
  \<open>is_aligned w 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w 0
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma is_aligned_beyond_length:
  \<open>is_aligned w n \<longleftrightarrow> w = 0\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (w = 0)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
LENGTH('a) \<le> n

goal (1 subgoal):
 1. is_aligned w n = (w = 0)
[PROOF STEP]
apply (simp add: is_aligned_iff_udvd)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> n \<Longrightarrow> (2 ^ n udvd w) = (w = 0)
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n w. LENGTH('a) \<le> n \<Longrightarrow> (take_bit LENGTH('a) (2 ^ n) dvd take_bit LENGTH('a) w) = (take_bit LENGTH('a) w = take_bit LENGTH('a) 0)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_alignedI [intro?]:
  \<open>is_aligned x n\<close> if \<open>x = 2 ^ n * k\<close> for x :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned x n
[PROOF STEP]
proof (unfold is_aligned_iff_udvd)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ n udvd x
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
x = 2 ^ n * k
[PROOF STEP]
show \<open>2 ^ n udvd x\<close>
[PROOF STATE]
proof (prove)
using this:
x = 2 ^ n * k

goal (1 subgoal):
 1. 2 ^ n udvd x
[PROOF STEP]
using dvd_triv_left exp_dvd_iff_exp_udvd
[PROOF STATE]
proof (prove)
using this:
x = 2 ^ n * k
?a dvd ?a * ?b
(2 ^ ?n dvd ?w) = (2 ^ ?n udvd ?w)

goal (1 subgoal):
 1. 2 ^ n udvd x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2 ^ n udvd x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_alignedE:
  fixes w :: \<open>'a::len word\<close>
  assumes \<open>is_aligned w n\<close>
  obtains q where \<open>w = 2 ^ n * word_of_nat q\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases \<open>n < LENGTH('a)\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n < LENGTH('a)

goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_aligned w n
\<not> n < LENGTH('a)
[PROOF STEP]
have \<open>w = 0\<close>
[PROOF STATE]
proof (prove)
using this:
is_aligned w n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. w = 0
[PROOF STEP]
by (simp add: is_aligned_beyond_length)
[PROOF STATE]
proof (state)
this:
w = 0

goal (2 subgoals):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with that [of 0]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>w = 2 ^ n * word_of_nat 0; 0 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = 0
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w = 2 ^ n * word_of_nat 0; 0 < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = 0

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define m where \<open>m = LENGTH('a) - n\<close>
[PROOF STATE]
proof (state)
this:
m = LENGTH('a) - n

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
m = LENGTH('a) - n
[PROOF STEP]
have l: \<open>LENGTH('a) = n + m\<close> and \<open>m \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)
m = LENGTH('a) - n

goal (1 subgoal):
 1. LENGTH('a) = n + m &&& m \<noteq> 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
LENGTH('a) = n + m
m \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>n < LENGTH('a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n < LENGTH('a)
[PROOF STEP]
have *: \<open>unat (2 ^ n :: 'a word) = 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
n < LENGTH('a)

goal (1 subgoal):
 1. unat (2 ^ n) = 2 ^ n
[PROOF STEP]
by transfer simp
[PROOF STATE]
proof (state)
this:
unat (2 ^ n) = 2 ^ n

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_aligned w n
[PROOF STEP]
have \<open>2 ^ n udvd w\<close>
[PROOF STATE]
proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. 2 ^ n udvd w
[PROOF STEP]
by (simp add: is_aligned_iff_udvd)
[PROOF STATE]
proof (state)
this:
2 ^ n udvd w

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ n udvd w
[PROOF STEP]
obtain v :: \<open>'a word\<close>
    where \<open>unat w = unat (2 ^ n :: 'a word) * unat v\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ n udvd w

goal (1 subgoal):
 1. (\<And>v. unat w = unat (2 ^ n) * unat v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
unat w = unat (2 ^ n) * unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
unat w = unat (2 ^ n) * unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
define q where \<open>q = unat v\<close>
[PROOF STATE]
proof (state)
this:
q = unat v

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
unat w = unat (2 ^ n) * unat v
q = unat v
[PROOF STEP]
have unat_w: \<open>unat w = 2 ^ n * q\<close>
[PROOF STATE]
proof (prove)
using this:
unat w = unat (2 ^ n) * unat v
q = unat v

goal (1 subgoal):
 1. unat w = 2 ^ n * q
[PROOF STEP]
by (simp add: *)
[PROOF STATE]
proof (state)
this:
unat w = 2 ^ n * q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat w = 2 ^ n * q
[PROOF STEP]
have \<open>word_of_nat (unat w) = (word_of_nat (2 ^ n * q) :: 'a word)\<close>
[PROOF STATE]
proof (prove)
using this:
unat w = 2 ^ n * q

goal (1 subgoal):
 1. word_of_nat (unat w) = word_of_nat (2 ^ n * q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q)
[PROOF STEP]
have w: \<open>w = 2 ^ n * word_of_nat q\<close>
[PROOF STATE]
proof (prove)
using this:
word_of_nat (unat w) = word_of_nat (2 ^ n * q)

goal (1 subgoal):
 1. w = 2 ^ n * word_of_nat q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w = 2 ^ n * word_of_nat q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w = 2 ^ n * word_of_nat q

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (state)
this:
\<not> q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
have \<open>2 ^ (LENGTH('a) - n) \<le> q\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - n) \<le> q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (LENGTH('a) - n) \<le> q

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ (LENGTH('a) - n) \<le> q
[PROOF STEP]
have \<open>2 ^ LENGTH('a) \<le> 2 ^ n * q\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ (LENGTH('a) - n) \<le> q

goal (1 subgoal):
 1. 2 ^ LENGTH('a) \<le> 2 ^ n * q
[PROOF STEP]
by (simp add: l power_add)
[PROOF STATE]
proof (state)
this:
2 ^ LENGTH('a) \<le> 2 ^ n * q

goal (1 subgoal):
 1. \<not> q < 2 ^ (LENGTH('a) - n) \<Longrightarrow> False
[PROOF STEP]
with unat_w [symmetric]
[PROOF STATE]
proof (chain)
picking this:
2 ^ n * q = unat w
2 ^ LENGTH('a) \<le> 2 ^ n * q
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
2 ^ n * q = unat w
2 ^ LENGTH('a) \<le> 2 ^ n * q

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis le_antisym nat_less_le unsigned_less)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<lbrakk>\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis; n < LENGTH('a)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)
\<lbrakk>w = 2 ^ n * word_of_nat ?q; ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_alignedE' [elim?]:
  fixes w :: \<open>'a::len word\<close>
  assumes \<open>is_aligned w n\<close>
  obtains q where \<open>w = push_bit n (word_of_nat q)\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_aligned w n
[PROOF STEP]
obtain q where \<open>w = 2 ^ n * word_of_nat q\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = 2 ^ n * word_of_nat q; q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_alignedE)
[PROOF STATE]
proof (state)
this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
have \<open>w = push_bit n (word_of_nat q)\<close>
[PROOF STATE]
proof (prove)
using this:
w = 2 ^ n * word_of_nat q
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. w = push_bit n (word_of_nat q)
[PROOF STEP]
by (simp add: push_bit_eq_mult)
[PROOF STATE]
proof (state)
this:
w = push_bit n (word_of_nat q)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>w = push_bit n (word_of_nat ?q); ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = push_bit n (word_of_nat q)
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w = push_bit n (word_of_nat ?q); ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = push_bit n (word_of_nat q)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>w = push_bit n (word_of_nat ?q); ?q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_mask:
  \<open>is_aligned w n \<longleftrightarrow> w AND mask n = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned w n = (w AND mask n = 0)
[PROOF STEP]
by (simp add: is_aligned_iff_take_bit_eq_0 take_bit_eq_mask)


[STATEMENT]
lemma is_aligned_imp_not_bit:
  \<open>\<not> bit w m\<close> if \<open>is_aligned w n\<close> and \<open>m < n\<close>
  for w :: \<open>'a::len word\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
from \<open>is_aligned w n\<close>
[PROOF STATE]
proof (chain)
picking this:
is_aligned w n
[PROOF STEP]
obtain q where \<open>w = push_bit n (word_of_nat q)\<close> \<open>q < 2 ^ (LENGTH('a) - n)\<close>
[PROOF STATE]
proof (prove)
using this:
is_aligned w n

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>w = push_bit n (word_of_nat q); q < 2 ^ (LENGTH('a) - n)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)

goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
have \<open>\<not> bit (push_bit n (word_of_nat q :: 'a word)) m\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit (push_bit n (word_of_nat q)) m
[PROOF STEP]
using \<open>m < n\<close>
[PROOF STATE]
proof (prove)
using this:
m < n

goal (1 subgoal):
 1. \<not> bit (push_bit n (word_of_nat q)) m
[PROOF STEP]
by (simp add: bit_simps)
[PROOF STATE]
proof (state)
this:
\<not> bit (push_bit n (word_of_nat q)) m

goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)
\<not> bit (push_bit n (word_of_nat q)) m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = push_bit n (word_of_nat q)
q < 2 ^ (LENGTH('a) - n)
\<not> bit (push_bit n (word_of_nat q)) m

goal (1 subgoal):
 1. \<not> bit w m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> bit w m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_weaken:
  "\<lbrakk> is_aligned w x; x \<ge> y \<rbrakk> \<Longrightarrow> is_aligned w y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w x; y \<le> x\<rbrakk> \<Longrightarrow> is_aligned w y
[PROOF STEP]
unfolding is_aligned_iff_dvd_nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ x dvd unat w; y \<le> x\<rbrakk> \<Longrightarrow> 2 ^ y dvd unat w
[PROOF STEP]
by (erule dvd_trans [rotated]) (simp add: le_imp_power_dvd)


[STATEMENT]
lemma is_alignedE_pre:
  fixes w::"'a::len word"
  assumes aligned: "is_aligned w n"
  shows        rl: "\<exists>q. w = 2 ^ n * (of_nat q) \<and> q < 2 ^ (LENGTH('a) - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>q. w = 2 ^ n * word_of_nat q \<and> q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
using aligned is_alignedE
[PROOF STATE]
proof (prove)
using this:
is_aligned w n
\<lbrakk>is_aligned ?w ?n; \<And>q. \<lbrakk>?w = 2 ^ ?n * word_of_nat q; q < 2 ^ (LENGTH(?'a) - ?n)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<exists>q. w = 2 ^ n * word_of_nat q \<and> q < 2 ^ (LENGTH('a) - n)
[PROOF STEP]
by blast


[STATEMENT]
lemma aligned_add_aligned:
  fixes x::"'a::len word"
  assumes aligned1: "is_aligned x n"
  and     aligned2: "is_aligned y m"
  and           lt: "m \<le> n"
  shows   "is_aligned (x + y) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (x + y) m
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (x + y) m
 2. \<not> ?P \<Longrightarrow> is_aligned (x + y) m
[PROOF STEP]
assume nlt: "n < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (x + y) m
 2. \<not> ?P \<Longrightarrow> is_aligned (x + y) m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (x + y) m
[PROOF STEP]
unfolding is_aligned_iff_dvd_nat dvd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
from aligned2
[PROOF STATE]
proof (chain)
picking this:
is_aligned y m
[PROOF STEP]
obtain q2 where yv: "y = 2 ^ m * of_nat q2"
      and q2v: "q2 < 2 ^ (LENGTH('a) - m)"
[PROOF STATE]
proof (prove)
using this:
is_aligned y m

goal (1 subgoal):
 1. (\<And>q2. \<lbrakk>y = 2 ^ m * word_of_nat q2; q2 < 2 ^ (LENGTH('a) - m)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
y = 2 ^ m * word_of_nat q2
q2 < 2 ^ (LENGTH('a) - m)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
from lt
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
[PROOF STEP]
obtain k where kv: "m + k = n"
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. (\<And>k. m + k = n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: le_iff_add)
[PROOF STATE]
proof (state)
this:
m + k = n

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
with aligned1
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
m + k = n
[PROOF STEP]
obtain q1 where xv: "x = 2 ^ (m + k) * of_nat q1"
      and q1v: "q1 < 2 ^ (LENGTH('a) - (m + k))"
[PROOF STATE]
proof (prove)
using this:
is_aligned x n
m + k = n

goal (1 subgoal):
 1. (\<And>q1. \<lbrakk>x = 2 ^ (m + k) * word_of_nat q1; q1 < 2 ^ (LENGTH('a) - (m + k))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
x = 2 ^ (m + k) * word_of_nat q1
q1 < 2 ^ (LENGTH('a) - (m + k))

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
have l1: "2 ^ (m + k) * q1 < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (m + k) * q1 < 2 ^ LENGTH('a)
[PROOF STEP]
by (rule nat_less_power_trans [OF q1v])
         (subst kv, rule order_less_imp_le [OF nlt])
[PROOF STATE]
proof (state)
this:
2 ^ (m + k) * q1 < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
have l2: "2 ^ m * q2 < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ m * q2 < 2 ^ LENGTH('a)
[PROOF STEP]
by (rule nat_less_power_trans [OF q2v],
          rule order_less_imp_le [OF order_le_less_trans])
         fact+
[PROOF STATE]
proof (state)
this:
2 ^ m * q2 < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
have "x = of_nat (2 ^ (m + k) *  q1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = word_of_nat (2 ^ (m + k) * q1)
[PROOF STEP]
using xv
[PROOF STATE]
proof (prove)
using this:
x = 2 ^ (m + k) * word_of_nat q1

goal (1 subgoal):
 1. x = word_of_nat (2 ^ (m + k) * q1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = word_of_nat (2 ^ (m + k) * q1)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = word_of_nat (2 ^ (m + k) * q1)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
have "y = of_nat (2 ^ m * q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = word_of_nat (2 ^ m * q2)
[PROOF STEP]
using yv
[PROOF STATE]
proof (prove)
using this:
y = 2 ^ m * word_of_nat q2

goal (1 subgoal):
 1. y = word_of_nat (2 ^ m * q2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = word_of_nat (2 ^ m * q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = word_of_nat (2 ^ (m + k) * q1)
y = word_of_nat (2 ^ m * q2)
[PROOF STEP]
have upls: "unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)"
[PROOF STATE]
proof (prove)
using this:
x = word_of_nat (2 ^ (m + k) * q1)
y = word_of_nat (2 ^ m * q2)

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
have f1: "unat x = 2 ^ (m + k) * q1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x = 2 ^ (m + k) * q1
[PROOF STEP]
using q1v unat_mult_power_lem xv
[PROOF STATE]
proof (prove)
using this:
q1 < 2 ^ (LENGTH('a) - (m + k))
?k < 2 ^ (LENGTH(?'a) - ?sz) \<Longrightarrow> unat (2 ^ ?sz * word_of_nat ?k) = 2 ^ ?sz * ?k
x = 2 ^ (m + k) * word_of_nat q1

goal (1 subgoal):
 1. unat x = 2 ^ (m + k) * q1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
unat x = 2 ^ (m + k) * q1

goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
have "unat y = 2 ^ m * q2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat y = 2 ^ m * q2
[PROOF STEP]
using q2v unat_mult_power_lem yv
[PROOF STATE]
proof (prove)
using this:
q2 < 2 ^ (LENGTH('a) - m)
?k < 2 ^ (LENGTH(?'a) - ?sz) \<Longrightarrow> unat (2 ^ ?sz * word_of_nat ?k) = 2 ^ ?sz * ?k
y = 2 ^ m * word_of_nat q2

goal (1 subgoal):
 1. unat y = 2 ^ m * q2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
unat y = 2 ^ m * q2

goal (1 subgoal):
 1. \<lbrakk>x = word_of_nat (2 ^ (m + k) * q1); y = word_of_nat (2 ^ m * q2)\<rbrakk> \<Longrightarrow> unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unat y = 2 ^ m * q2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unat y = 2 ^ m * q2

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
unat y = 2 ^ m * q2
unat x = 2 ^ (m + k) * q1

goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
by (simp add: power_add semiring_normalization_rules(34))
[PROOF STATE]
proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
(* (2 ^ k * q1 + q2) *)
[PROOF STATE]
proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>k. unat (x + y) = 2 ^ m * k
[PROOF STEP]
show "\<exists>d. unat (x + y) = 2 ^ m * d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
proof (cases "unat x + unat y < 2 ^ LENGTH('a)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
unat x + unat y < 2 ^ LENGTH('a)

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
have "unat (x + y) = unat x + unat y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (x + y) = unat x + unat y
[PROOF STEP]
by (subst unat_plus_if', rule if_P) fact
[PROOF STATE]
proof (state)
this:
unat (x + y) = unat x + unat y

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unat (x + y) = unat x + unat y

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
have "\<dots> = 2 ^ m * (2 ^ k * q1 + q2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
by (rule upls)
[PROOF STATE]
proof (state)
this:
unat x + unat y = 2 ^ m * (2 ^ k * q1 + q2)

goal (2 subgoals):
 1. unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
 2. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unat (x + y) = 2 ^ m * (2 ^ k * q1 + q2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unat (x + y) = 2 ^ m * (2 ^ k * q1 + q2)

goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> unat x + unat y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> unat x + unat y < 2 ^ LENGTH('a)
[PROOF STEP]
have "unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
using this:
\<not> unat x + unat y < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)
[PROOF STEP]
by (subst unat_word_ariths(1)) simp
[PROOF STATE]
proof (state)
this:
unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unat (x + y) = (unat x + unat y) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
have "\<dots> = (2 ^ m * (2 ^ k * q1 + q2)) mod 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a)
[PROOF STEP]
by (subst upls, rule refl)
[PROOF STATE]
proof (state)
this:
(unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(unat x + unat y) mod 2 ^ LENGTH('a) = 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
have "\<dots> = 2 ^ m * ((2 ^ k * q1 +  q2) mod 2 ^ (LENGTH('a) - m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))
[PROOF STEP]
have "m \<le> len_of (TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> LENGTH('a)
[PROOF STEP]
by (meson le_trans less_imp_le_nat lt nlt)
[PROOF STATE]
proof (state)
this:
m \<le> LENGTH('a)

goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<le> LENGTH('a)

goal (1 subgoal):
 1. 2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))
[PROOF STEP]
by (metis mult_mod_right ordered_cancel_comm_monoid_diff_class.add_diff_inverse power_add)
[PROOF STATE]
proof (state)
this:
2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ m * (2 ^ k * q1 + q2) mod 2 ^ LENGTH('a) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal (1 subgoal):
 1. \<not> unat x + unat y < 2 ^ LENGTH('a) \<Longrightarrow> \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unat (x + y) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unat (x + y) = 2 ^ m * ((2 ^ k * q1 + q2) mod 2 ^ (LENGTH('a) - m))

goal (1 subgoal):
 1. \<exists>d. unat (x + y) = 2 ^ m * d
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>d. unat (x + y) = 2 ^ m * d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_aligned (x + y) m

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m
[PROOF STEP]
assume "\<not> n < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> is_aligned (x + y) m
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
is_aligned x n
is_aligned y m
m \<le> n
\<not> n < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned x n
is_aligned y m
m \<le> n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. is_aligned (x + y) m
[PROOF STEP]
by (simp add: is_aligned_mask not_less take_bit_eq_mod power_overflow word_arith_nat_defs(7) flip: take_bit_eq_mask)
[PROOF STATE]
proof (state)
this:
is_aligned (x + y) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_shift:
  fixes k::"'a::len word"
  shows "is_aligned (k << m) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (k << m) m
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
assume mv: "m < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
m < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
from mv
[PROOF STATE]
proof (chain)
picking this:
m < LENGTH('a)
[PROOF STEP]
obtain q where mq: "m + q = LENGTH('a)" and "0 < q"
[PROOF STATE]
proof (prove)
using this:
m < LENGTH('a)

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>m + q = LENGTH('a); 0 < q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: less_imp_add_positive)
[PROOF STATE]
proof (state)
this:
m + q = LENGTH('a)
0 < q

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
have "(2::nat) ^ m dvd unat (push_bit m k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ m dvd unat (push_bit m k)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
have kv: "(unat k div 2 ^ q) * 2 ^ q + unat k mod 2 ^ q = unat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat k div 2 ^ q * 2 ^ q + unat k mod 2 ^ q = unat k
[PROOF STEP]
by (rule div_mult_mod_eq)
[PROOF STATE]
proof (state)
this:
unat k div 2 ^ q * 2 ^ q + unat k mod 2 ^ q = unat k

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
have "unat (push_bit m k) = unat (2 ^ m * k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (push_bit m k) = unat (2 ^ m * k)
[PROOF STEP]
by (simp add: push_bit_eq_mult ac_simps)
[PROOF STATE]
proof (state)
this:
unat (push_bit m k) = unat (2 ^ m * k)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unat (push_bit m k) = unat (2 ^ m * k)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
have "\<dots> = (2 ^ m * unat k) mod (2 ^ LENGTH('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a)
[PROOF STEP]
using mv
[PROOF STATE]
proof (prove)
using this:
m < LENGTH('a)

goal (1 subgoal):
 1. unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a)
[PROOF STEP]
by (simp add: unat_word_ariths(2))
[PROOF STATE]
proof (state)
this:
unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
unat (2 ^ m * k) = 2 ^ m * unat k mod 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
have "\<dots> = 2 ^ m * (unat k mod 2 ^ q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ m * unat k mod 2 ^ LENGTH('a) = 2 ^ m * (unat k mod 2 ^ q)
[PROOF STEP]
by (subst mq [symmetric], subst power_add, subst mod_mult2_eq) simp
[PROOF STATE]
proof (state)
this:
2 ^ m * unat k mod 2 ^ LENGTH('a) = 2 ^ m * (unat k mod 2 ^ q)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * ?k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)
[PROOF STEP]
show "unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)"
[PROOF STATE]
proof (prove)
using this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)

goal (1 subgoal):
 1. unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
unat (push_bit m k) = 2 ^ m * (unat k mod 2 ^ q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ m dvd unat (push_bit m k)

goal (2 subgoals):
 1. ?P \<Longrightarrow> is_aligned (k << m) m
 2. \<not> ?P \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ m dvd unat (push_bit m k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ m dvd unat (push_bit m k)

goal (1 subgoal):
 1. is_aligned (k << m) m
[PROOF STEP]
by (unfold is_aligned_iff_dvd_nat shiftl_def)
[PROOF STATE]
proof (state)
this:
is_aligned (k << m) m

goal (1 subgoal):
 1. \<not> m < LENGTH('a) \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> m < LENGTH('a) \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
assume "\<not> m < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> m < LENGTH('a)

goal (1 subgoal):
 1. \<not> m < LENGTH('a) \<Longrightarrow> is_aligned (k << m) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> m < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> m < LENGTH('a)

goal (1 subgoal):
 1. is_aligned (k << m) m
[PROOF STEP]
by (simp add: not_less power_overflow is_aligned_mask word_size shiftl_def)
[PROOF STATE]
proof (state)
this:
is_aligned (k << m) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma aligned_mod_eq_0:
  fixes p::"'a::len word"
  assumes al: "is_aligned p sz"
  shows   "p mod 2 ^ sz = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p mod 2 ^ sz = 0
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> p mod 2 ^ sz = 0
 2. \<not> ?P \<Longrightarrow> p mod 2 ^ sz = 0
[PROOF STEP]
assume szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> p mod 2 ^ sz = 0
 2. \<not> ?P \<Longrightarrow> p mod 2 ^ sz = 0
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned p sz
sz < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned p sz
sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0
[PROOF STEP]
unfolding is_aligned_iff_dvd_nat
[PROOF STATE]
proof (prove)
using this:
2 ^ sz dvd unat p
sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0
[PROOF STEP]
by (simp add: and_mask_dvd_nat p2_gt_0 word_mod_2p_is_mask)
[PROOF STATE]
proof (state)
this:
p mod 2 ^ sz = 0

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0
[PROOF STEP]
assume "\<not> sz < LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. \<not> sz < LENGTH('a) \<Longrightarrow> p mod 2 ^ sz = 0
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned p sz
\<not> sz < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned p sz
\<not> sz < LENGTH('a)

goal (1 subgoal):
 1. p mod 2 ^ sz = 0
[PROOF STEP]
by (simp add: is_aligned_mask flip: take_bit_eq_mask take_bit_eq_mod)
[PROOF STATE]
proof (state)
this:
p mod 2 ^ sz = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_triv: "is_aligned (2 ^ n ::'a::len word) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (2 ^ n) n
[PROOF STEP]
by (rule is_alignedI [where k = 1], simp)


[STATEMENT]
lemma is_aligned_mult_triv1: "is_aligned (2 ^ n * x  ::'a::len word) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (2 ^ n * x) n
[PROOF STEP]
by (rule is_alignedI [OF refl])


[STATEMENT]
lemma is_aligned_mult_triv2: "is_aligned (x * 2 ^ n ::'a::len word) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned (x * 2 ^ n) n
[PROOF STEP]
by (subst mult.commute, simp add: is_aligned_mult_triv1)


[STATEMENT]
lemma word_power_less_0_is_0:
  fixes x :: "'a::len word"
  shows "x < a ^ 0 \<Longrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < a ^ 0 \<Longrightarrow> x = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma is_aligned_no_wrap:
  fixes off :: "'a::len word"
  fixes ptr :: "'a::len word"
  assumes al: "is_aligned ptr sz"
  and    off: "off < 2 ^ sz"
  shows  "unat ptr + unat off < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
have szv: "sz < LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a)
[PROOF STEP]
using off p2_gt_0 word_neq_0_conv
[PROOF STATE]
proof (prove)
using this:
off < 2 ^ sz
(0 < 2 ^ ?n) = (?n < LENGTH(?'a))
(?w \<noteq> 0) = (0 < ?w)

goal (1 subgoal):
 1. sz < LENGTH('a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
from al
[PROOF STATE]
proof (chain)
picking this:
is_aligned ptr sz
[PROOF STEP]
obtain q where ptrq: "ptr = 2 ^ sz * of_nat q" and
    qv: "q < 2 ^ (LENGTH('a) - sz)"
[PROOF STATE]
proof (prove)
using this:
is_aligned ptr sz

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>ptr = 2 ^ sz * word_of_nat q; q < 2 ^ (LENGTH('a) - sz)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: is_alignedE)
[PROOF STATE]
proof (state)
this:
ptr = 2 ^ sz * word_of_nat q
q < 2 ^ (LENGTH('a) - sz)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
proof (cases "sz = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sz = 0

goal (2 subgoals):
 1. sz = 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
 2. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sz = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sz = 0

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
using off ptrq qv
[PROOF STATE]
proof (prove)
using this:
sz = 0
off < 2 ^ sz
ptr = 2 ^ sz * word_of_nat q
q < 2 ^ (LENGTH('a) - sz)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
sz \<noteq> 0

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sz \<noteq> 0
[PROOF STEP]
have sne: "0 < sz"
[PROOF STATE]
proof (prove)
using this:
sz \<noteq> 0

goal (1 subgoal):
 1. 0 < sz
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
0 < sz

goal (1 subgoal):
 1. sz \<noteq> 0 \<Longrightarrow> unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
have uq: "unat (of_nat q ::'a::len word) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat q) = q
[PROOF STEP]
apply (subst unat_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q mod 2 ^ LENGTH('a) = q
[PROOF STEP]
apply (rule mod_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule order_less_trans [OF qv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (LENGTH('a) - sz) < 2 ^ LENGTH('a)
[PROOF STEP]
apply (rule power_strict_increasing [OF diff_less [OF sne]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < LENGTH('a)
 2. 1 < 2
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat (word_of_nat q) = q

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
have uptr: "unat ptr = 2 ^ sz * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr = 2 ^ sz * q
[PROOF STEP]
apply (subst ptrq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz * word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst iffD1 [OF unat_mult_lem])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. unat (2 ^ sz) * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst unat_power_lower [OF szv])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * unat (word_of_nat q) < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst uq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 2 ^ sz * q < 2 ^ LENGTH('a)
 2. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (rule nat_less_power_trans [OF qv order_less_imp_le [OF szv]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * unat (word_of_nat q) = 2 ^ sz * q
[PROOF STEP]
apply (subst uq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat (2 ^ sz) * q = 2 ^ sz * q
[PROOF STEP]
apply (subst unat_power_lower [OF szv])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ sz * q = 2 ^ sz * q
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat ptr = 2 ^ sz * q

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
show "unat ptr + unat off < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
using szv
[PROOF STATE]
proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. unat ptr + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst uptr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz * q + unat off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst mult.commute, rule nat_add_offset_less [OF _ qv])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat off < 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz
[PROOF STEP]
apply (rule order_less_le_trans [OF unat_mono [OF off] order_eq_refl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (2 ^ sz) = 2 ^ sz
 2. sz < LENGTH('a) \<Longrightarrow> LENGTH('a) = LENGTH('a) - sz + sz
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unat ptr + unat off < 2 ^ LENGTH('a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_no_wrap':
  fixes ptr :: "'a::len word"
  assumes al: "is_aligned ptr sz"
  and    off: "off < 2 ^ sz"
  shows  "ptr \<le> ptr + off"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ptr \<le> ptr + off
[PROOF STEP]
by (subst no_plus_overflow_unat_size, subst word_size, rule is_aligned_no_wrap) fact+


[STATEMENT]
lemma is_aligned_no_overflow':
  fixes p :: "'a::len word"
  assumes al: "is_aligned p n"
  shows "p \<le> p + (2 ^ n - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
assume "n<LENGTH('a)"
[PROOF STATE]
proof (state)
this:
n < LENGTH('a)

goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned p n
n < LENGTH('a)
[PROOF STEP]
have "2^n - (1::'a::len word) < 2^n"
[PROOF STATE]
proof (prove)
using this:
is_aligned p n
n < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ n - 1 < 2 ^ n
[PROOF STEP]
by (simp add: word_less_nat_alt unat_sub_if_size)
[PROOF STATE]
proof (state)
this:
2 ^ n - 1 < 2 ^ n

goal (2 subgoals):
 1. ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<not> ?P \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned p n
2 ^ n - 1 < 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned p n
2 ^ n - 1 < 2 ^ n

goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1)
[PROOF STEP]
by (rule is_aligned_no_wrap')
[PROOF STATE]
proof (state)
this:
p \<le> p + (2 ^ n - 1)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
assume "\<not> n<LENGTH('a)"
[PROOF STATE]
proof (state)
this:
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. \<not> n < LENGTH('a) \<Longrightarrow> p \<le> p + (2 ^ n - 1)
[PROOF STEP]
with al
[PROOF STATE]
proof (chain)
picking this:
is_aligned p n
\<not> n < LENGTH('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_aligned p n
\<not> n < LENGTH('a)

goal (1 subgoal):
 1. p \<le> p + (2 ^ n - 1)
[PROOF STEP]
by (simp add: not_less power_overflow is_aligned_mask mask_2pm1)
[PROOF STATE]
proof (state)
this:
p \<le> p + (2 ^ n - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_no_overflow:
  "is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2^sz - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> ptr \<le> ptr + 2 ^ sz - 1
[PROOF STEP]
by (drule is_aligned_no_overflow') (simp add: field_simps)


[STATEMENT]
lemma replicate_not_True:
  "\<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. xs = replicate n False \<Longrightarrow> True \<notin> set xs
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma map_zip_replicate_False_xor:
  "n = length xs \<Longrightarrow> map (\<lambda>(x, y). x = (\<not> y)) (zip xs (replicate n False)) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = xs
[PROOF STEP]
by (induct xs arbitrary: n, auto)


[STATEMENT]
lemma drop_minus_lem:
  "\<lbrakk> n \<le> length xs; 0 < n; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1)  # drop (Suc (n' - n)) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs
[PROOF STEP]
proof (induct xs arbitrary: n n')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>n \<le> length []; 0 < n; n' = length []\<rbrakk> \<Longrightarrow> drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []
 2. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n \<le> length []
0 < n
n' = length []

goal (2 subgoals):
 1. \<And>n n'. \<lbrakk>n \<le> length []; 0 < n; n' = length []\<rbrakk> \<Longrightarrow> drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []
 2. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> length []
0 < n
n' = length []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> length []
0 < n
n' = length []

goal (1 subgoal):
 1. drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
drop (n' - n) [] = rev [] ! (n - 1) # drop (Suc (n' - n)) []

goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs)
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?n \<le> length ys; 0 < ?n; ?n' = length ys\<rbrakk> \<Longrightarrow> drop (?n' - ?n) ys = rev ys ! (?n - 1) # drop (Suc (?n' - ?n)) ys
n \<le> length (y # ys)
0 < n
n' = length (y # ys)

goal (1 subgoal):
 1. \<And>a xs n n'. \<lbrakk>\<And>n n'. \<lbrakk>n \<le> length xs; 0 < n; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - n) xs = rev xs ! (n - 1) # drop (Suc (n' - n)) xs; n \<le> length (a # xs); 0 < n; n' = length (a # xs)\<rbrakk> \<Longrightarrow> drop (n' - n) (a # xs) = rev (a # xs) ! (n - 1) # drop (Suc (n' - n)) (a # xs)
[PROOF STEP]
from Cons.prems
[PROOF STATE]
proof (chain)
picking this:
n \<le> length (y # ys)
0 < n
n' = length (y # ys)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n \<le> length (y # ys)
0 < n
n' = length (y # ys)

goal (1 subgoal):
 1. drop (n' - n) (y # ys) = rev (y # ys) ! (n - 1) # drop (Suc (n' - n)) (y # ys)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys
[PROOF STEP]
apply (cases "n = Suc (length ys)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n = Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys
 2. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys
[PROOF STEP]
apply (simp add: nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> drop (Suc (length ys) - n) (y # ys) = (rev ys @ [y]) ! (n - Suc 0) # drop (Suc (length ys) - n) ys
[PROOF STEP]
apply (simp add: Suc_diff_le Cons.hyps nth_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys)\<rbrakk> \<Longrightarrow> \<not> n - Suc 0 < length ys \<longrightarrow> rev ys ! 0 = y
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> Suc (length ys); 0 < n; n' = Suc (length ys); n \<noteq> Suc (length ys); \<not> n - Suc 0 < length ys\<rbrakk> \<Longrightarrow> rev ys ! 0 = y
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
drop (n' - n) (y # ys) = rev (y # ys) ! (n - 1) # drop (Suc (n' - n)) (y # ys)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma drop_minus:
  "\<lbrakk> n < length xs; n' = length xs \<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n  # drop (n' - n) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> drop (n' - Suc n) xs = rev xs ! n # drop (n' - n) xs
[PROOF STEP]
apply (subst drop_minus_lem)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> Suc n \<le> length xs
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> 0 < Suc n
 3. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 4. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> 0 < Suc n
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 3. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> n' = length xs
 2. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> rev xs ! (Suc n - 1) # drop (Suc (n' - Suc n)) xs = rev xs ! n # drop (n' - n) xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; n' = length xs\<rbrakk> \<Longrightarrow> drop (Suc (length xs - Suc n)) xs = drop (length xs - n) xs
[PROOF STEP]
apply (cases "length xs", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>n < length xs; n' = length xs; length xs = Suc nat\<rbrakk> \<Longrightarrow> drop (Suc (length xs - Suc n)) xs = drop (length xs - n) xs
[PROOF STEP]
apply (simp add: Suc_diff_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_add_xor:
  \<open>(x + 2 ^ n) XOR 2 ^ n = x\<close>
  if al: \<open>is_aligned (x::'a::len word) n'\<close> and le: \<open>n < n'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
have \<open>\<not> bit x n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit x n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
is_aligned x n'
n < n'

goal (1 subgoal):
 1. \<not> bit x n
[PROOF STEP]
by (rule is_aligned_imp_not_bit)
[PROOF STATE]
proof (state)
this:
\<not> bit x n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> bit x n
[PROOF STEP]
have \<open>x + 2 ^ n = x OR 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> bit x n

goal (1 subgoal):
 1. x + 2 ^ n = x OR 2 ^ n
[PROOF STEP]
by (subst disjunctive_add) (auto simp add: bit_simps disjunctive_add)
[PROOF STATE]
proof (state)
this:
x + 2 ^ n = x OR 2 ^ n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x + 2 ^ n = x OR 2 ^ n

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
have \<open>(x OR 2 ^ n) XOR 2 ^ n = x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x OR 2 ^ n) XOR 2 ^ n = x
[PROOF STEP]
by (rule bit_word_eqI) (auto simp add: bit_simps \<open>\<not> bit x n\<close>)
[PROOF STATE]
proof (state)
this:
(x OR 2 ^ n) XOR 2 ^ n = x

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x + 2 ^ n = x OR 2 ^ n
(x OR 2 ^ n) XOR 2 ^ n = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x + 2 ^ n = x OR 2 ^ n
(x OR 2 ^ n) XOR 2 ^ n = x

goal (1 subgoal):
 1. x + 2 ^ n XOR 2 ^ n = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x + 2 ^ n XOR 2 ^ n = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_aligned_add_mult_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n * z) n'
[PROOF STEP]
apply (erule aligned_add_aligned)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (x * 2 ^ n * z) n'
 2. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> n' \<le> m
[PROOF STEP]
apply (auto intro: is_alignedI [where k="x*z"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_add_multI:
  fixes p :: "'a::len word"
  shows "\<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p m; n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (p + x * 2 ^ n) n'
[PROOF STEP]
apply (erule aligned_add_aligned)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> is_aligned (x * 2 ^ n) n'
 2. \<lbrakk>n \<le> m; n' = n\<rbrakk> \<Longrightarrow> n' \<le> m
[PROOF STEP]
apply (auto intro: is_alignedI [where k="x"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_no_wrap''':
  fixes ptr :: "'a::len word"
  shows"\<lbrakk> is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz \<rbrakk>
         \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (drule is_aligned_no_wrap[where off="of_nat off"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> word_of_nat off < 2 ^ sz
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: word_less_nat_alt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (word_of_nat off) < 2 ^ sz
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule order_le_less_trans[rotated])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> unat (word_of_nat off) \<le> off
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (simp add: take_bit_eq_mod unsigned_of_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + unat (word_of_nat off) < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (subst(asm) unat_of_nat_len)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz\<rbrakk> \<Longrightarrow> off < 2 ^ LENGTH('a)
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule order_less_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sz < LENGTH('a) \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a)
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply (erule power_strict_increasing)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1 < 2
 2. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH('a); off < 2 ^ sz; unat ptr + off < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + off < 2 ^ LENGTH('a)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_get_word_bits:
  fixes p :: "'a::len word"
  shows "\<lbrakk> is_aligned p n; \<lbrakk> is_aligned p n; n < LENGTH('a) \<rbrakk> \<Longrightarrow> P;
           \<lbrakk> p = 0; n \<ge> LENGTH('a) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (cases "n < LENGTH('a)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<lbrakk>is_aligned p n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> P; \<lbrakk>p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; p = 0 \<Longrightarrow> P; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (erule meta_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> p = 0
[PROOF STEP]
apply (simp add: is_aligned_mask power_add power_overflow not_less
    flip: take_bit_eq_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_bit n p = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> p = 0
[PROOF STEP]
apply (metis take_bit_length_eq take_bit_of_0 take_bit_tightened)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aligned_small_is_0:
  "\<lbrakk> is_aligned x n; x < 2 ^ n \<rbrakk> \<Longrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x < 2 ^ n\<rbrakk> \<Longrightarrow> x = 0
[PROOF STEP]
by (simp add: is_aligned_mask less_mask_eq)


[STATEMENT]
lemma aligned_at_least_t2n_diff:
  "\<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; is_aligned y n; x < y\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (erule is_aligned_get_word_bits[where p=y])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); \<not> x \<le> y - 2 ^ n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (clarsimp simp: linorder_not_le)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (subgoal_tac "y - x = 0")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x; y - x = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x = 0
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x = 0
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (rule aligned_small_is_0)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> is_aligned (y - x) ?n8
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ ?n8
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply (erule(1) aligned_sub_aligned)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> n \<le> n
 2. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ n
 3. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; x < y; is_aligned y n; n < LENGTH('a); y - 2 ^ n < x\<rbrakk> \<Longrightarrow> y - x < 2 ^ n
 2. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply unat_arith
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x < y; y = 0; LENGTH('a) \<le> n\<rbrakk> \<Longrightarrow> x \<le> y - 2 ^ n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_no_overflow'':
  "\<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n
[PROOF STEP]
apply (frule is_aligned_no_overflow')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0; x \<le> x + (2 ^ n - 1)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ n
[PROOF STEP]
apply (erule order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x + (2 ^ n - 1) \<le> x + 2 ^ n
[PROOF STEP]
apply (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; x + 2 ^ n \<noteq> 0\<rbrakk> \<Longrightarrow> x + 2 ^ n - 1 \<le> x + 2 ^ n
[PROOF STEP]
apply (erule word_sub_1_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_bitI:
  \<open>is_aligned p m\<close> if \<open>\<And>n. n < m \<Longrightarrow> \<not> bit p n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p m
[PROOF STEP]
apply (simp add: is_aligned_mask)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p AND mask m = 0
[PROOF STEP]
apply (rule bit_word_eqI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (p AND mask m) n = bit 0 n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?n < m \<Longrightarrow> \<not> bit p ?n

goal (1 subgoal):
 1. \<And>n. n < LENGTH('a) \<Longrightarrow> bit (p AND mask m) n = bit 0 n
[PROOF STEP]
apply (auto simp add: bit_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_aligned_nth:
  "is_aligned p m = (\<forall>n < m. \<not> bit p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_aligned p m = (\<forall>n<m. \<not> bit p n)
[PROOF STEP]
apply (auto intro: is_aligned_bitI simp add: is_aligned_mask bit_eq_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). \<not> bit (p AND mask m) n; n < m; bit p n\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>\<forall>n<m. \<not> bit p n; n < LENGTH('a); bit (p AND mask m) n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp: bit_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). bit p n \<longrightarrow> \<not> n < m; n < m; bit p n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using bit_imp_le_length not_less
[PROOF STATE]
proof (prove)
using this:
bit ?w ?n \<Longrightarrow> ?n < LENGTH(?'a)
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<LENGTH('a). bit p n \<longrightarrow> \<not> n < m; n < m; bit p n\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma range_inter:
  "({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not>(a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a..b} \<inter> {c..d} = {}) = (\<forall>x. \<not> (a \<le> x \<and> x \<le> b \<and> c \<le> x \<and> x \<le> d))
[PROOF STEP]
by auto


[STATEMENT]
lemma aligned_inter_non_empty:
  "\<lbrakk> {p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {};
     is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{p..p + (2 ^ n - 1)} \<inter> {p..p + 2 ^ m - 1} = {}; is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (clarsimp simp only: range_inter)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<not> (p \<le> x \<and> x \<le> p + (2 ^ n - 1) \<and> p \<le> x \<and> x \<le> p + 2 ^ m - 1); is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule_tac x=p in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; \<not> (p \<le> p \<and> p \<le> p + (2 ^ n - 1) \<and> p \<le> p \<and> p \<le> p + 2 ^ m - 1)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; p \<le> p + (2 ^ n - 1) \<longrightarrow> \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule impE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> p \<le> p + (2 ^ n - 1)
 2. \<lbrakk>is_aligned p n; is_aligned p m; \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule is_aligned_no_overflow')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m; \<not> p \<le> p + 2 ^ m - 1\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p m\<rbrakk> \<Longrightarrow> p \<le> p + 2 ^ m - 1
[PROOF STEP]
apply (erule is_aligned_no_overflow)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_aligned_mod_nz:
  assumes al: "\<not> is_aligned a n"
  shows "a mod 2 ^ n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n \<noteq> 0
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
using al
[PROOF STATE]
proof (prove)
using this:
\<not> is_aligned a n

goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
apply (rule notE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> a mod 2 ^ n \<noteq> 0 \<Longrightarrow> is_aligned a n
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n = 0 \<Longrightarrow> is_aligned a n
[PROOF STEP]
apply (rule is_alignedI [of _ _ \<open>a div 2 ^ n\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod 2 ^ n = 0 \<Longrightarrow> a = 2 ^ n * (a div 2 ^ n)
[PROOF STEP]
apply (metis add.right_neutral mult.commute word_mod_div_equality)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nat_add_offset_le:
  fixes x :: nat
  assumes yv: "y \<le> 2 ^ n"
  and     xv: "x < 2 ^ m"
  and     mn: "sz = m + n"
  shows   "x * 2 ^ n + y \<le> 2 ^ sz"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ sz
[PROOF STEP]
proof (subst mn)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
from yv
[PROOF STATE]
proof (chain)
picking this:
y \<le> 2 ^ n
[PROOF STEP]
obtain qy where "y + qy = 2 ^ n"
[PROOF STATE]
proof (prove)
using this:
y \<le> 2 ^ n

goal (1 subgoal):
 1. (\<And>qy. y + qy = 2 ^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: le_iff_add)
[PROOF STATE]
proof (state)
this:
y + qy = 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
have "x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n
[PROOF STEP]
using yv xv
[PROOF STATE]
proof (prove)
using this:
y \<le> 2 ^ n
x < 2 ^ m

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * 2 ^ n + y \<le> x * 2 ^ n + 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
have "\<dots> = (x + 1) * 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * 2 ^ n + 2 ^ n = (x + 1) * 2 ^ n

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
have "\<dots> \<le> 2 ^ (m + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + 1) * 2 ^ n \<le> 2 ^ (m + n)
[PROOF STEP]
using xv
[PROOF STATE]
proof (prove)
using this:
x < 2 ^ m

goal (1 subgoal):
 1. (x + 1) * 2 ^ n \<le> 2 ^ (m + n)
[PROOF STEP]
by (subst power_add) (rule mult_le_mono1, simp)
[PROOF STATE]
proof (state)
this:
(x + 1) * 2 ^ n \<le> 2 ^ (m + n)

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
show "x * 2 ^ n + y \<le> 2 ^ (m + n)"
[PROOF STATE]
proof (prove)
using this:
x * 2 ^ n + y \<le> 2 ^ (m + n)

goal (1 subgoal):
 1. x * 2 ^ n + y \<le> 2 ^ (m + n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x * 2 ^ n + y \<le> 2 ^ (m + n)

goal:
No subgoals!
[PROOF STEP]
qed