[STATEMENT]
lemma delta_weak_complexity_carrier:
  assumes d0: "def > 0"
  shows "weak_complexity_linear_poly_order_carrier (>) def delta_mono"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_complexity_linear_poly_order_carrier (\<lambda>x y. y < x) def delta_mono
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
fix xys :: "('a \<times> 'a) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
assume ass: "\<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x"
[PROOF STATE]
proof (state)
this:
\<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
let ?cs = "map (\<lambda> (x,y). x - y) xys"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
let ?ds = "def # ?cs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
define d where "d = Min (set ?ds)"
[PROOF STATE]
proof (state)
this:
d = Min (set (def # map (\<lambda>(x, y). x - y) xys))

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
have d: "d \<le> def" and dcs: "\<And> x. x \<in> set ?cs \<Longrightarrow> d \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<le> def &&& (\<And>x. x \<in> set (map (\<lambda>(x, y). x - y) xys) \<Longrightarrow> d \<le> x)
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (def # map (\<lambda>(x, y). x - y) xys)) \<le> def &&& (\<And>x. x \<in> set (map (\<lambda>(x, y). x - y) xys) \<Longrightarrow> Min (set (def # map (\<lambda>(x, y). x - y) xys)) \<le> x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<le> def
?x \<in> set (map (\<lambda>(x, y). x - y) xys) \<Longrightarrow> d \<le> ?x

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
have "d \<in> set ?ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> set (def # map (\<lambda>(x, y). x - y) xys)
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (def # map (\<lambda>(x, y). x - y) xys)) \<in> set (def # map (\<lambda>(x, y). x - y) xys)
[PROOF STEP]
by (rule Min_in, auto)
[PROOF STATE]
proof (state)
this:
d \<in> set (def # map (\<lambda>(x, y). x - y) xys)

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
hence "d = def \<or> d \<in> set ?cs"
[PROOF STATE]
proof (prove)
using this:
d \<in> set (def # map (\<lambda>(x, y). x - y) xys)

goal (1 subgoal):
 1. d = def \<or> d \<in> set (map (\<lambda>(x, y). x - y) xys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d = def \<or> d \<in> set (map (\<lambda>(x, y). x - y) xys)

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
hence d0: "d > 0"
[PROOF STATE]
proof (prove)
using this:
d = def \<or> d \<in> set (map (\<lambda>(x, y). x - y) xys)

goal (1 subgoal):
 1. (0::'a) < d
[PROOF STEP]
by (cases, insert d0 ass, auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(0::'a) < d

goal (1 subgoal):
 1. \<And>xys. \<forall>x y. (x, y) \<in> set xys \<longrightarrow> y < x \<Longrightarrow> \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
show "\<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)
[PROOF STEP]
by (intro exI conjI, rule delta_complexity[OF d0 d], insert dcs, force simp: delta_gt_def)
[PROOF STATE]
proof (state)
this:
\<exists>gt bound. mono_matrix_carrier gt def bound delta_mono \<and> (\<forall>x y. (x, y) \<in> set xys \<longrightarrow> gt x y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arctic_delta_weak_carrier:
  "weak_SN_both_mono_ordered_semiring_1 weak_gt_arctic_delta 1 pos_arctic_delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_SN_both_mono_ordered_semiring_1 weak_gt_arctic_delta 1 pos_arctic_delta
[PROOF STEP]
..


[STATEMENT]
lemma arctic_weak_carrier:
  "weak_SN_both_mono_ordered_semiring_1 (>) 1 pos_arctic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_SN_both_mono_ordered_semiring_1 (\<lambda>x y. y < x) 1 pos_arctic
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. weak_SN_both_mono_ordered_semiring_1 (\<lambda>x y. y < x) 1 pos_arctic
[PROOF STEP]
have SN: "SN_both_mono_ordered_semiring_1 1 (>) pos_arctic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SN_both_mono_ordered_semiring_1 1 (\<lambda>x y. y < x) pos_arctic
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
SN_both_mono_ordered_semiring_1 1 (\<lambda>x y. y < x) pos_arctic

goal (1 subgoal):
 1. weak_SN_both_mono_ordered_semiring_1 (\<lambda>x y. y < x) 1 pos_arctic
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_SN_both_mono_ordered_semiring_1 (\<lambda>x y. y < x) 1 pos_arctic
[PROOF STEP]
by (unfold_locales, intro conjI exI, rule SN, auto)
[PROOF STATE]
proof (state)
this:
weak_SN_both_mono_ordered_semiring_1 (\<lambda>x y. y < x) 1 pos_arctic

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<phi>_def2:
"\<phi> (Trans s a ou s') \<longleftrightarrow>
 (\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = (\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK)
[PROOF STEP]
by (cases "Trans s a ou s'" rule: \<phi>.cases) auto


[STATEMENT]
lemma comReceivePost_out:
assumes 1: "step s a = (ou,s')" and a: "a = COMact (comReceivePost AID p PID pst uid vs)" and 2: "ou = outOK"
shows "p = serverPass s AID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = serverPass s AID
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
ou = outOK

goal (1 subgoal):
 1. p = serverPass s AID
[PROOF STEP]
unfolding a
[PROOF STATE]
proof (prove)
using this:
step s (COMact (comReceivePost AID p PID pst uid vs)) = (ou, s')
ou = outOK

goal (1 subgoal):
 1. p = serverPass s AID
[PROOF STEP]
by (auto simp: com_defs)


[STATEMENT]
lemma \<phi>_def3:
assumes "step s a = (ou,s')"
shows
"\<phi> (Trans s a ou s') \<longleftrightarrow>
 (\<exists>uid pst vs. a = COMact (comReceivePost AID (serverPass s AID) PID pst uid vs) \<and> ou = outOK)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = (\<exists>uid pst vs. a = COMact (comReceivePost AID (serverPass s AID) PID pst uid vs) \<and> ou = outOK)
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK) = (\<exists>uid pst vs. a = COMact (comReceivePost AID (serverPass s AID) PID pst uid vs) \<and> ou = outOK)
[PROOF STEP]
using comReceivePost_out[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a = COMact (comReceivePost AID ?p PID ?pst ?uid ?vs); ou = outOK\<rbrakk> \<Longrightarrow> ?p = serverPass s AID

goal (1 subgoal):
 1. (\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK) = (\<exists>uid pst vs. a = COMact (comReceivePost AID (serverPass s AID) PID pst uid vs) \<and> ou = outOK)
[PROOF STEP]
by blast


[STATEMENT]
lemma \<phi>_cases:
assumes "\<phi> (Trans s a ou s')"
and "step s a = (ou, s')"
and "reach s"
obtains
  (Recv) uid sp aID pID pst vs where "a = COMact (comReceivePost aID sp pID pst uid vs)" "ou = outOK"
                                 "sp = serverPass s AID"
                                  "aID = AID" "pID = PID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>aID sp pID pst uid vs. \<lbrakk>a = COMact (comReceivePost aID sp pID pst uid vs); ou = outOK; sp = serverPass s AID; aID = AID; pID = PID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>aID sp pID pst uid vs. \<lbrakk>a = COMact (comReceivePost aID sp pID pst uid vs); ou = outOK; sp = serverPass s AID; aID = AID; pID = PID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<phi> (Trans s a ou s')
[PROOF STEP]
obtain sp pst uid vs where "a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK"
[PROOF STATE]
proof (prove)
using this:
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. (\<And>sp pst uid vs. a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. (\<And>sp pst uid vs. a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. (\<And>aID sp pID pst uid vs. \<lbrakk>a = COMact (comReceivePost aID sp pID pst uid vs); ou = outOK; sp = serverPass s AID; aID = AID; pID = PID\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK \<Longrightarrow> thesis
[PROOF STEP]
assume "a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK"
[PROOF STATE]
proof (state)
this:
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK

goal (1 subgoal):
 1. a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK \<Longrightarrow> thesis
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
a = COMact (comReceivePost AID sp PID pst uid vs) \<and> ou = outOK

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButPID_step_\<phi>_imp:
assumes ss1: "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and \<phi>: "\<phi> (Trans s a ou s')"
shows "\<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
have s's1': "eqButPID s' s1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButPID s' s1'
[PROOF STEP]
using eqButPID_step local.step ss1 step1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>eqButPID ?s ?s1.0; step ?s ?a = (?ou, ?s'); step ?s1.0 ?a = (?ou1.0, ?s1')\<rbrakk> \<Longrightarrow> eqButPID ?s' ?s1'
step s a = (ou, s')
eqButPID s s1
step s1 a = (ou1, s1')

goal (1 subgoal):
 1. eqButPID s' s1'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
eqButPID s' s1'

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using step step1 \<phi>
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
step s1 a = (ou1, s1')
\<phi> (Trans s a ou s')

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
using eqButPID_stateSelectors[OF ss1]
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
step s1 a = (ou1, s1')
\<phi> (Trans s a ou s')
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> pendingFReqs s = pendingFReqs s1 \<and> friendReq s = friendReq s1 \<and> friendIDs s = friendIDs s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> eeqButPID (outerPost s) (outerPost s1) \<and> outerOwner s = outerOwner s1 \<and> outerVis s = outerVis s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1 \<and> IDsOK s = IDsOK s1

goal (1 subgoal):
 1. \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
unfolding \<phi>_def2
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
step s1 a = (ou1, s1')
\<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou = outOK
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> pendingFReqs s = pendingFReqs s1 \<and> friendReq s = friendReq s1 \<and> friendIDs s = friendIDs s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> owner s = owner s1 \<and> vis s = vis s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> eeqButPID (outerPost s) (outerPost s1) \<and> outerOwner s = outerOwner s1 \<and> outerVis s = outerVis s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1 \<and> IDsOK s = IDsOK s1

goal (1 subgoal):
 1. \<exists>uid p pst vs. a = COMact (comReceivePost AID p PID pst uid vs) \<and> ou1 = outOK
[PROOF STEP]
by (auto simp: u_defs com_defs)
[PROOF STATE]
proof (state)
this:
\<phi> (Trans s1 a ou1 s1')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButPID_step_\<phi>:
assumes s's1': "eqButPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
shows "\<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (Trans s a ou s') = \<phi> (Trans s1 a ou1 s1')
[PROOF STEP]
by (metis eqButPID_step_\<phi>_imp eqButPID_sym assms)


[STATEMENT]
lemma crypts_union_1:
 "crypts (H \<union> H') \<subseteq> crypts H \<union> crypts H'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crypts (H \<union> H') \<subseteq> crypts H \<union> crypts H'
[PROOF STEP]
by (rule subsetI, erule crypts.induct, auto)


[STATEMENT]
lemma crypts_union_2:
 "crypts H \<union> crypts H' \<subseteq> crypts (H \<union> H')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crypts H \<union> crypts H' \<subseteq> crypts (H \<union> H')
[PROOF STEP]
by (rule subsetI, erule UnE, erule_tac [!] crypts.induct, auto)


[STATEMENT]
lemma crypts_hash_1:
 "crypts {Hash X} \<subseteq> insert (Hash X) (crypts {X})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crypts {Hash X} \<subseteq> insert (Hash X) (crypts {X})
[PROOF STEP]
by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp,
 rule list.induct, simp_all, blast, (drule crypts_hash, simp)?)+)


[STATEMENT]
lemma crypts_hash_2:
 "insert (Hash X) (crypts {X}) \<subseteq> crypts {Hash X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (Hash X) (crypts {X}) \<subseteq> crypts {Hash X}
[PROOF STEP]
by (rule subsetI, simp, erule disjE, blast, erule crypts.induct, simp,
 subst id_apply [symmetric], subst foldr_Nil [symmetric], rule crypts_hash, simp,
 blast+)


[STATEMENT]
lemma crypts_crypt_1:
 "crypts {Crypt K X} \<subseteq> Crypt K ` crypts {X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crypts {Crypt K X} \<subseteq> Crypt K ` crypts {X}
[PROOF STEP]
by (rule subsetI, erule crypts.induct, fastforce, rotate_tac [!], erule_tac [!] rev_mp,
 rule_tac [!] list.induct, auto)


[STATEMENT]
lemma crypts_crypt_2:
 "Crypt K ` crypts {X} \<subseteq> crypts {Crypt K X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Crypt K ` crypts {X} \<subseteq> crypts {Crypt K X}
[PROOF STEP]
by (rule subsetI, simp add: image_iff, erule bexE, drule crypts_comp, simp)


[STATEMENT]
lemma crypts_mpair_1:
 "crypts {\<lbrace>X, Y\<rbrace>} \<subseteq> insert \<lbrace>X, Y\<rbrace> (crypts {X} \<union> crypts {Y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crypts {\<lbrace>X, Y\<rbrace>} \<subseteq> insert \<lbrace>X, Y\<rbrace> (crypts {X} \<union> crypts {Y})
[PROOF STEP]
by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp,
 rule list.induct, (simp+, blast)+)+)


[STATEMENT]
lemma crypts_mpair_2:
 "insert \<lbrace>X, Y\<rbrace> (crypts {X} \<union> crypts {Y}) \<subseteq> crypts {\<lbrace>X, Y\<rbrace>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert \<lbrace>X, Y\<rbrace> (crypts {X} \<union> crypts {Y}) \<subseteq> crypts {\<lbrace>X, Y\<rbrace>}
[PROOF STEP]
by (rule subsetI, simp, erule disjE, blast, erule disjE, (erule crypts.induct, simp,
 subst id_apply [symmetric], subst foldr_Nil [symmetric], (rule crypts_fst [of _ X] |
 rule crypts_snd), rule crypts_used, simp, blast+)+)


[STATEMENT]
lemma key_sets_crypt_1:
 "X \<noteq> Crypt K Y \<Longrightarrow>
    key_sets X {Crypt K Y} \<subseteq> insert (InvKey K) ` key_sets X {Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<noteq> Crypt K Y \<Longrightarrow> key_sets X {Crypt K Y} \<subseteq> insert (InvKey K) ` key_sets X {Y}
[PROOF STEP]
by (rule subsetI, simp add: key_sets_def, erule exE, rotate_tac, erule rev_mp,
 rule list.induct, auto)


[STATEMENT]
lemma key_sets_crypt_2:
 "insert (InvKey K) ` key_sets X {Y} \<subseteq> key_sets X {Crypt K Y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (InvKey K) ` key_sets X {Y} \<subseteq> key_sets X {Crypt K Y}
[PROOF STEP]
by (rule subsetI, simp add: key_sets_def image_iff, (erule exE, erule conjE)+,
 drule arg_cong [where f = "Crypt K"], simp only: comp_apply
 [symmetric, of "Crypt K"] foldr_Cons [symmetric], subst conj_commute,
 rule exI, rule conjI, assumption, simp)


[STATEMENT]
lemma log_spied_1:
 "\<lbrakk>s \<turnstile> s';
    Log X \<in> parts (used s) \<longrightarrow> Log X \<in> spied s;
    Log X \<in> parts (used s')\<rbrakk> \<Longrightarrow>
  Log X \<in> spied s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> s'; Log X \<in> parts (used s) \<longrightarrow> Log X \<in> spied s; Log X \<in> parts (used s')\<rbrakk> \<Longrightarrow> Log X \<in> spied s'
[PROOF STEP]
by (simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: parts_insert,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec |
 drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+)


[STATEMENT]
lemma idinfo_spied_1:
 "\<lbrakk>s \<turnstile> s';
    \<langle>n, X\<rangle> \<in> parts (used s) \<longrightarrow> \<langle>n, X\<rangle> \<in> spied s;
    \<langle>n, X\<rangle> \<in> parts (used s')\<rbrakk> \<Longrightarrow>
  \<langle>n, X\<rangle> \<in> spied s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> s'; \<langle>n, X\<rangle> \<in> parts (used s) \<longrightarrow> \<langle>n, X\<rangle> \<in> spied s; \<langle>n, X\<rangle> \<in> parts (used s')\<rbrakk> \<Longrightarrow> \<langle>n, X\<rangle> \<in> spied s'
[PROOF STEP]
by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec |
 drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+,
 auto simp add: parts_insert)


[STATEMENT]
lemma idinfo_msg_1:
  assumes A: "s\<^sub>0 \<Turnstile> s"
  shows "\<lbrakk>s \<turnstile> s'; \<langle>n, X\<rangle> \<in> spied s \<longrightarrow> X \<in> spied s; \<langle>n, X\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
    X \<in> spied s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> s'; \<langle>n, X\<rangle> \<in> spied s \<longrightarrow> X \<in> spied s; \<langle>n, X\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow> X \<in> spied s'
[PROOF STEP]
by (simp add: rel_def, (erule disjE, (erule exE)+, simp, ((subst (asm) disj_assoc
 [symmetric])?, erule disjE, (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]),
 simp+ | erule disjE, (simp add: image_iff)+, blast?)?)+)


[STATEMENT]
lemma idinfo_init_1 [rule_format]:
  assumes A: "s\<^sub>0 \<Turnstile> s"
  shows "\<lbrakk>s \<turnstile> s'; n \<notin> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey;
    \<forall>X. \<langle>n, X\<rangle> \<notin> spied s\<rbrakk> \<Longrightarrow>
  \<langle>n, X\<rangle> \<notin> spied s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> s'; n \<notin> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey; \<forall>X. \<langle>n, X\<rangle> \<notin> spied s\<rbrakk> \<Longrightarrow> \<langle>n, X\<rangle> \<notin> spied s'
[PROOF STEP]
by (rule notI, simp add: rel_def, ((erule disjE)?, (erule exE)+, (blast | simp,
 ((drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast |
 (erule conjE)+, drule parts_agent [OF A], blast))?)+)


[STATEMENT]
lemma idinfo_mpair_1 [rule_format]:
 "\<lbrakk>(s, s') \<in> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con;
    \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
      key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {};
    \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
  key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con; \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow> key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {}; \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow> key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}
[PROOF STEP]
by ((erule disjE)?, clarify?, simp add: image_iff Image_def, (drule subsetD
 [OF key_sets_crypts_hash] | drule key_sets_range, blast | (drule spec)+,
 drule mp, simp, simp add: ex_in_conv [symmetric], erule exE, frule subsetD
 [OF key_sets_crypts_fst], drule subsetD [OF key_sets_crypts_snd])?)+


[STATEMENT]
lemma idinfo_mpair_2 [rule_format]:
  assumes A: "s\<^sub>0 \<Turnstile> s"
  shows "\<lbrakk>s \<turnstile> s'; (s, s') \<notin> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con;
    \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow>
      key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {};
    \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow>
  key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> s'; (s, s') \<notin> rel_id_hash \<union> rel_id_crypt \<union> rel_id_sep \<union> rel_id_con; \<forall>X Y. \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s \<longrightarrow> key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s)) \<noteq> {}; \<langle>n, \<lbrace>X, Y\<rbrace>\<rangle> \<in> spied s'\<rbrakk> \<Longrightarrow> key_sets \<lbrace>X, Y\<rbrace> (crypts (Log -` spied s')) \<noteq> {}
[PROOF STEP]
by (simp only: rel_def Un_iff de_Morgan_disj, simp, ((erule disjE)?, (erule exE)+,
 simp add: Image_def, (simp only: Collect_disj_eq crypts_union key_sets_union, simp)?,
 ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule idinfo_dec [OF A] |
 drule idinfo_sep [OF A]), simp+)?)+)


[STATEMENT]
lemma pwd_anonymous_1 [rule_format]:
 "\<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_id_password\<rbrakk> \<Longrightarrow>
    \<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow>
  (\<exists>SK. SesKey SK \<in> spied s \<and>
    ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
     (Asset n, Crypt (SesK SK) (Num 0)) \<in> s))"
  (is "\<lbrakk>_; _\<rbrakk> \<Longrightarrow> _ \<longrightarrow> ?P s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s\<^sub>0 \<Turnstile> s; n \<notin> bad_id_password\<rbrakk> \<Longrightarrow> \<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow> (\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s))
[PROOF STEP]
proof (erule rtrancl_induct, simp add: image_def, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<notin> bad_id_password; s\<^sub>0 \<Turnstile> y; y \<turnstile> z; \<langle>n, Pwd n\<rangle> \<in> spied y \<longrightarrow> (\<exists>SK. SesKey SK \<in> spied y \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> y \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> y)); \<langle>n, Pwd n\<rangle> \<in> spied z\<rbrakk> \<Longrightarrow> \<exists>SK. SesKey SK \<in> spied z \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> z \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> z)
[PROOF STEP]
fix s s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<notin> bad_id_password; s\<^sub>0 \<Turnstile> y; y \<turnstile> z; \<langle>n, Pwd n\<rangle> \<in> spied y \<longrightarrow> (\<exists>SK. SesKey SK \<in> spied y \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> y \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> y)); \<langle>n, Pwd n\<rangle> \<in> spied z\<rbrakk> \<Longrightarrow> \<exists>SK. SesKey SK \<in> spied z \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> z \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> z)
[PROOF STEP]
assume
    A: "s\<^sub>0 \<Turnstile> s" and
    B: "s \<turnstile> s'" and
    C: "\<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow> ?P s" and
    D: "\<langle>n, Pwd n\<rangle> \<in> spied s'"
[PROOF STATE]
proof (state)
this:
s\<^sub>0 \<Turnstile> s
s \<turnstile> s'
\<langle>n, Pwd n\<rangle> \<in> spied s \<longrightarrow> (\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s))
\<langle>n, Pwd n\<rangle> \<in> spied s'

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<notin> bad_id_password; s\<^sub>0 \<Turnstile> y; y \<turnstile> z; \<langle>n, Pwd n\<rangle> \<in> spied y \<longrightarrow> (\<exists>SK. SesKey SK \<in> spied y \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> y \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> y)); \<langle>n, Pwd n\<rangle> \<in> spied z\<rbrakk> \<Longrightarrow> \<exists>SK. SesKey SK \<in> spied z \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> z \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> z)
[PROOF STEP]
show "?P s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>SK. SesKey SK \<in> spied s' \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s' \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s')
[PROOF STEP]
by (insert B C D, simp add: rel_def, ((erule disjE)?, (erule exE)+, simp add:
     image_iff, blast?, ((subst (asm) disj_assoc [symmetric])?, erule disjE,
     (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast+ |
     insert key_sets_pwd_empty [OF A], clarsimp)?, (((erule disjE)?, erule
     conjE, drule sym, simp, (drule key_sets_pwd_seskey [OF A] | drule
     idinfo_mpair [OF A, simplified]), simp)+ | drule key_sets_range, blast)?)+)
[PROOF STATE]
proof (state)
this:
\<exists>SK. SesKey SK \<in> spied s' \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s' \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem pwd_anonymous:
  assumes
    A: "s\<^sub>0 \<Turnstile> s" and
    B: "n \<notin> bad_id_password" and
    C: "n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey) \<inter> (bad_id_pubkey \<union> bad_id_shak)"
  shows "\<langle>n, Pwd n\<rangle> \<notin> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<notin> spied s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
assume D: "\<langle>n, Pwd n\<rangle> \<in> spied s"
[PROOF STATE]
proof (state)
this:
\<langle>n, Pwd n\<rangle> \<in> spied s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
[PROOF STATE]
proof (prove)
using this:
\<langle>n, Pwd n\<rangle> \<in> spied s

goal (1 subgoal):
 1. n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
[PROOF STEP]
by (rule contrapos_pp, rule_tac idinfo_init [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
have "\<exists>SK. SesKey SK \<in> spied s \<and>
    ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
     (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)"
    (is "\<exists>SK. ?P SK \<and> (?Q SK \<or> ?R SK)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)
[PROOF STEP]
by (rule pwd_anonymous_1 [OF A B D])
[PROOF STATE]
proof (state)
this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)
[PROOF STEP]
obtain SK where "?P SK" and "?Q SK \<or> ?R SK"
[PROOF STATE]
proof (prove)
using this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)

goal (1 subgoal):
 1. (\<And>SK. \<lbrakk>SesKey SK \<in> spied s; (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
assume "?Q SK"
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_shakey \<inter> bad_prikey"
[PROOF STATE]
proof (prove)
using this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s

goal (1 subgoal):
 1. n \<in> bad_shakey \<inter> bad_prikey
[PROOF STEP]
by (rule_tac contrapos_pp [OF \<open>?P SK\<close>], rule_tac owner_seskey_secret [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
assume "?R SK"
[PROOF STATE]
proof (state)
this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)"
[PROOF STATE]
proof (prove)
using this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)
[PROOF STEP]
by (rule_tac contrapos_pp [OF \<open>?P SK\<close>], rule_tac asset_seskey_secret [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. \<langle>n, Pwd n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. False
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)
n \<notin> bad_id_password
n \<notin> bad_shakey \<inter> (bad_pwd \<union> bad_prikey) \<inter> (bad_id_pubkey \<union> bad_id_shak)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem auth_prikey_anonymous:
  assumes
    A: "s\<^sub>0 \<Turnstile> s" and
    B: "n \<notin> bad_id_prikey" and
    C: "n \<notin> bad_shakey \<inter> bad_prikey \<inter> (bad_id_password \<union> bad_id_shak)"
  shows "\<langle>n, Auth_PriKey n\<rangle> \<notin> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<notin> spied s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
assume D: "\<langle>n, Auth_PriKey n\<rangle> \<in> spied s"
[PROOF STATE]
proof (state)
this:
\<langle>n, Auth_PriKey n\<rangle> \<in> spied s

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
[PROOF STATE]
proof (prove)
using this:
\<langle>n, Auth_PriKey n\<rangle> \<in> spied s

goal (1 subgoal):
 1. n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
[PROOF STEP]
by (rule contrapos_pp, rule_tac idinfo_init [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
have "Auth_PriKey n \<in> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Auth_PriKey n \<in> spied s
[PROOF STEP]
by (rule idinfo_msg [OF A D])
[PROOF STATE]
proof (state)
this:
Auth_PriKey n \<in> spied s

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_prikey"
[PROOF STATE]
proof (prove)
using this:
Auth_PriKey n \<in> spied s

goal (1 subgoal):
 1. n \<in> bad_prikey
[PROOF STEP]
by (rule contrapos_pp, rule_tac auth_prikey_secret [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> bad_prikey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
n \<in> bad_prikey
[PROOF STEP]
have E: "n \<notin> bad_id_pubkey"
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_pubkey
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_prikey
n \<notin> bad_id_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_pubkey
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<notin> bad_id_pubkey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<notin> bad_id_pubkey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
have "n \<in> bad_shakey"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<in> bad_shakey
[PROOF STEP]
proof (cases "n \<in> bad_id_shakey", simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<notin> bad_id_shakey

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
with D and E
[PROOF STATE]
proof (chain)
picking this:
\<langle>n, Auth_PriKey n\<rangle> \<in> spied s
n \<notin> bad_id_pubkey
n \<notin> bad_id_shakey
[PROOF STEP]
have "\<exists>SK. SesKey SK \<in> spied s \<and>
      ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or>
       (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)"
      (is "\<exists>SK. ?P SK \<and> (?Q SK \<or> ?R SK)")
[PROOF STATE]
proof (prove)
using this:
\<langle>n, Auth_PriKey n\<rangle> \<in> spied s
n \<notin> bad_id_pubkey
n \<notin> bad_id_shakey

goal (1 subgoal):
 1. \<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)
[PROOF STEP]
by (rule_tac idinfo_pwd [OF A], rule_tac exI [of _ "Auth_PriKey n"], simp_all)
[PROOF STATE]
proof (state)
this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)
[PROOF STEP]
obtain SK where "?P SK" and "?Q SK \<or> ?R SK"
[PROOF STATE]
proof (prove)
using this:
\<exists>SK. SesKey SK \<in> spied s \<and> ((Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s)

goal (1 subgoal):
 1. (\<And>SK. \<lbrakk>SesKey SK \<in> spied s; (Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
assume "?Q SK"
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
hence "n \<in> bad_shakey \<inter> bad_prikey"
[PROOF STATE]
proof (prove)
using this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s

goal (1 subgoal):
 1. n \<in> bad_shakey \<inter> bad_prikey
[PROOF STEP]
by (rule_tac contrapos_pp [OF \<open>?P SK\<close>], rule_tac owner_seskey_secret
         [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
assume "?R SK"
[PROOF STATE]
proof (state)
this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
hence "n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)"
[PROOF STATE]
proof (prove)
using this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s

goal (1 subgoal):
 1. n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)
[PROOF STEP]
by (rule_tac contrapos_pp [OF \<open>?P SK\<close>], rule_tac asset_seskey_secret
         [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. n \<notin> bad_id_shakey \<Longrightarrow> n \<in> bad_shakey
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
SesKey SK \<in> spied s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<or> (Asset n, Crypt (SesK SK) (Num 0)) \<in> s
(Owner n, Crypt (SesK SK) (Pwd n)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> bad_prikey
(Asset n, Crypt (SesK SK) (Num 0)) \<in> s \<Longrightarrow> n \<in> bad_shakey \<inter> (bad_pwd \<union> bad_prikey)

goal (1 subgoal):
 1. n \<in> bad_shakey
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey

goal (1 subgoal):
 1. \<langle>n, Auth_PriKey n\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_prikey
n \<notin> bad_id_pubkey
n \<in> bad_shakey
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_prikey
n \<notin> bad_id_pubkey
n \<in> bad_shakey

goal (1 subgoal):
 1. False
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_prikey
n \<notin> bad_id_pubkey
n \<in> bad_shakey
n \<notin> bad_shakey \<inter> bad_prikey \<inter> (bad_id_password \<union> bad_id_shak)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem auth_shakey_anonymous:
  assumes
    A: "s\<^sub>0 \<Turnstile> s" and
    B: "n \<notin> bad_id_shakey" and
    C: "n \<notin> bad_shakey \<inter> (bad_id_password \<union> bad_id_pubkey)"
  shows "\<langle>n, Key (Auth_ShaKey n)\<rangle> \<notin> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<notin> spied s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
assume D: "\<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s"
[PROOF STATE]
proof (state)
this:
\<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s

goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey"
[PROOF STATE]
proof (prove)
using this:
\<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s

goal (1 subgoal):
 1. n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
[PROOF STEP]
by (rule contrapos_pp, rule_tac idinfo_init [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey

goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
have "Key (Auth_ShaKey n) \<in> spied s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Key (Auth_ShaKey n) \<in> spied s
[PROOF STEP]
by (rule idinfo_msg [OF A D])
[PROOF STATE]
proof (state)
this:
Key (Auth_ShaKey n) \<in> spied s

goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
hence "n \<in> bad_shakey"
[PROOF STATE]
proof (prove)
using this:
Key (Auth_ShaKey n) \<in> spied s

goal (1 subgoal):
 1. n \<in> bad_shakey
[PROOF STEP]
by (rule contrapos_pp, rule_tac auth_shakey_secret [OF A])
[PROOF STATE]
proof (state)
this:
n \<in> bad_shakey

goal (1 subgoal):
 1. \<langle>n, Key (Auth_ShaKey n)\<rangle> \<in> spied s \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_shakey
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_shakey

goal (1 subgoal):
 1. False
[PROOF STEP]
using B and C
[PROOF STATE]
proof (prove)
using this:
n \<in> bad_id_password \<union> bad_id_pubkey \<union> bad_id_shakey
n \<in> bad_shakey
n \<notin> bad_id_shakey
n \<notin> bad_shakey \<inter> (bad_id_password \<union> bad_id_pubkey)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_last_def:
  "(odd :: int \<Rightarrow> bool) w \<longleftrightarrow> w mod 2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd w = (w mod 2 = 1)
[PROOF STEP]
by (fact odd_iff_mod_2_eq_one)


[STATEMENT]
lemma bin_last_numeral_simps [simp]:
  "\<not> odd (0 :: int)"
  "odd (1 :: int)"
  "odd (- 1 :: int)"
  "odd (Numeral1 :: int)"
  "\<not> odd (numeral (Num.Bit0 w) :: int)"
  "odd (numeral (Num.Bit1 w) :: int)"
  "\<not> odd (- numeral (Num.Bit0 w) :: int)"
  "odd (- numeral (Num.Bit1 w) :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<not> odd 0 &&& \<not> is_unit 2) &&& odd (- 1) &&& odd Numeral1) &&& (\<not> odd (numeral (num.Bit0 w)) &&& odd (numeral (num.Bit1 w))) &&& \<not> odd (- numeral (num.Bit0 w)) &&& odd (- numeral (num.Bit1 w))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma bin_rest_numeral_simps [simp]:
  "(\<lambda>k::int. k div 2) 0 = 0"
  "(\<lambda>k::int. k div 2) 1 = 0"
  "(\<lambda>k::int. k div 2) (- 1) = - 1"
  "(\<lambda>k::int. k div 2) Numeral1 = 0"
  "(\<lambda>k::int. k div 2) (numeral (Num.Bit0 w)) = numeral w"
  "(\<lambda>k::int. k div 2) (numeral (Num.Bit1 w)) = numeral w"
  "(\<lambda>k::int. k div 2) (- numeral (Num.Bit0 w)) = - numeral w"
  "(\<lambda>k::int. k div 2) (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0 div 2 = 0 &&& 1 div 2 = 0) &&& - 1 div 2 = - 1 &&& Numeral1 div 2 = 0) &&& (numeral (num.Bit0 w) div 2 = numeral w &&& numeral (num.Bit1 w) div 2 = numeral w) &&& - numeral (num.Bit0 w) div 2 = - numeral w &&& - numeral (num.Bit1 w) div 2 = - numeral (w + num.One)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma bin_rl_eqI: "\<lbrakk>(\<lambda>k::int. k div 2) x = (\<lambda>k::int. k div 2) y; odd x = odd y\<rbrakk> \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x div 2 = y div 2; odd x = odd y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (auto elim: oddE)


[STATEMENT]
lemma [simp]:
  shows bin_rest_lt0: "(\<lambda>k::int. k div 2) i < 0 \<longleftrightarrow> i < 0"
  and  bin_rest_ge_0: "(\<lambda>k::int. k div 2) i \<ge> 0 \<longleftrightarrow> i \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i div 2 < 0) = (i < 0) &&& (0 \<le> i div 2) = (0 \<le> i)
[PROOF STEP]
by auto


[STATEMENT]
lemma bin_rest_gt_0 [simp]: "(\<lambda>k::int. k div 2) x > 0 \<longleftrightarrow> x > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < x div 2) = (1 < x)
[PROOF STEP]
by auto


[STATEMENT]
lemma bin_nth_eq_iff: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) x = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bit x = bit y) = (x = y)
[PROOF STEP]
by (simp add: bit_eq_iff fun_eq_iff)


[STATEMENT]
lemma bin_eqI:
  "x = y" if "\<And>n. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
bit x ?n = bit y ?n

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (rule bit_eqI)


[STATEMENT]
lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x n = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = y) = (\<forall>n. bit x n = bit y n)
[PROOF STEP]
by (metis bit_eq_iff)


[STATEMENT]
lemma bin_nth_zero [simp]: "\<not> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) 0 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> bit 0 n
[PROOF STEP]
by simp


[STATEMENT]
lemma bin_nth_1 [simp]: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) 1 n \<longleftrightarrow> n = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit 1 n = (n = 0)
[PROOF STEP]
by (cases n) (simp_all add: bit_Suc)


[STATEMENT]
lemma bin_nth_minus1 [simp]: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (- 1) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (- 1) n
[PROOF STEP]
by simp


[STATEMENT]
lemma bin_nth_numeral: "(\<lambda>k::int. k div 2) x = y \<Longrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (numeral n) = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y (pred_numeral n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x div 2 = y \<Longrightarrow> bit x (numeral n) = bit y (pred_numeral n)
[PROOF STEP]
by (simp add: numeral_eq_Suc bit_Suc)


[STATEMENT]
lemma nth_2p_bin: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (2 ^ n) m = (m = n)" \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (2 ^ n) m = (m = n)
[PROOF STEP]
by (auto simp add: bit_exp_iff)


[STATEMENT]
lemma nth_rest_power_bin: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (((\<lambda>k::int. k div 2) ^^ k) w) n = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w (n + k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)
[PROOF STEP]
apply (induct k arbitrary: n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. bit (((\<lambda>k. k div 2) ^^ 0) w) n = bit w (n + 0)
 2. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ Suc k) w) n = bit w (n + Suc k)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ Suc k) w) n = bit w (n + Suc k)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k n. (\<And>n. bit (((\<lambda>k. k div 2) ^^ k) w) n = bit w (n + k)) \<Longrightarrow> bit (((\<lambda>k. k div 2) ^^ k) w div 2) n = bit w (Suc (n + k))
[PROOF STEP]
apply (simp only: bit_Suc [symmetric] add_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_nth_numeral_unfold:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (num.Bit0 x)) n \<longleftrightarrow> n > 0 \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral x) (n - 1)"
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (num.Bit1 x)) n \<longleftrightarrow> (n > 0 \<longrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral x) (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (numeral (num.Bit0 x)) n = (0 < n \<and> bit (numeral x) (n - 1)) &&& bit (numeral (num.Bit1 x)) n = (0 < n \<longrightarrow> bit (numeral x) (n - 1))
[PROOF STEP]
by (cases n; simp)+


[STATEMENT]
lemma bin_sign_simps [simp]:
  "bin_sign 0 = 0"
  "bin_sign 1 = 0"
  "bin_sign (- 1) = - 1"
  "bin_sign (numeral k) = 0"
  "bin_sign (- numeral k) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bin_sign 0 = 0 &&& bin_sign 1 = 0) &&& bin_sign (- 1) = - 1 &&& bin_sign (numeral k) = 0 &&& bin_sign (- numeral k) = - 1
[PROOF STEP]
by (simp_all add: bin_sign_def)


[STATEMENT]
lemma bin_sign_rest [simp]: "bin_sign ((\<lambda>k::int. k div 2) w) = bin_sign w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (w div 2) = bin_sign w
[PROOF STEP]
by (simp add: bin_sign_def)


[STATEMENT]
lemma bintrunc_mod2p: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w = w mod 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n w = w mod 2 ^ n
[PROOF STEP]
by (fact take_bit_eq_mod)


[STATEMENT]
lemma sbintrunc_mod2p: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n w = (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n
[PROOF STEP]
by (simp add: bintrunc_mod2p signed_take_bit_eq_take_bit_shift)


[STATEMENT]
lemma sbintrunc_eq_take_bit:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n
[PROOF STEP]
by (fact signed_take_bit_eq_take_bit_shift)


[STATEMENT]
lemma sign_bintr: "bin_sign ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (take_bit n w) = 0
[PROOF STEP]
by (simp add: bin_sign_def)


[STATEMENT]
lemma bintrunc_n_0: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n 0 = 0
[PROOF STEP]
by (fact take_bit_of_0)


[STATEMENT]
lemma sbintrunc_n_0: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n 0 = 0
[PROOF STEP]
by (fact signed_take_bit_of_0)


[STATEMENT]
lemma sbintrunc_n_minus1: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (- 1) = - 1
[PROOF STEP]
by (fact signed_take_bit_of_minus_1)


[STATEMENT]
lemma bintrunc_Suc_numeral:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) 1 = 1"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- 1) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral (w + Num.One))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (take_bit (Suc n) 1 = 1 &&& take_bit (Suc n) (- 1) = 1 + 2 * take_bit n (- 1) &&& take_bit (Suc n) (numeral (num.Bit0 w)) = 2 * take_bit n (numeral w)) &&& take_bit (Suc n) (numeral (num.Bit1 w)) = 1 + 2 * take_bit n (numeral w) &&& take_bit (Suc n) (- numeral (num.Bit0 w)) = 2 * take_bit n (- numeral w) &&& take_bit (Suc n) (- numeral (num.Bit1 w)) = 1 + 2 * take_bit n (- numeral (w + num.One))
[PROOF STEP]
by (simp_all add: take_bit_Suc del: take_bit_minus_one_eq_mask)


[STATEMENT]
lemma sbintrunc_0_numeral [simp]:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 1 = -1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (numeral (Num.Bit0 w)) = 0"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (numeral (Num.Bit1 w)) = -1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (- numeral (Num.Bit0 w)) = 0"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) 0 (- numeral (Num.Bit1 w)) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit 0 1 = - 1 &&& signed_take_bit 0 (numeral (num.Bit0 w)) = 0) &&& signed_take_bit 0 (numeral (num.Bit1 w)) = - 1 &&& signed_take_bit 0 (- numeral (num.Bit0 w)) = 0 &&& signed_take_bit 0 (- numeral (num.Bit1 w)) = - 1
[PROOF STEP]
by simp_all


[STATEMENT]
lemma sbintrunc_Suc_numeral:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) 1 = 1"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit0 w)) = 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- numeral (Num.Bit1 w)) = 1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- numeral (w + Num.One))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit (Suc n) 1 = 1 &&& signed_take_bit (Suc n) (numeral (num.Bit0 w)) = 2 * signed_take_bit n (numeral w)) &&& signed_take_bit (Suc n) (numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit n (numeral w) &&& signed_take_bit (Suc n) (- numeral (num.Bit0 w)) = 2 * signed_take_bit n (- numeral w) &&& signed_take_bit (Suc n) (- numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit n (- numeral (w + num.One))
[PROOF STEP]
by (simp_all add: signed_take_bit_Suc)


[STATEMENT]
lemma bin_sign_lem: "(bin_sign ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = -1) = bit bin n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bin_sign (signed_take_bit n bin) = - 1) = bit bin n
[PROOF STEP]
by (simp add: bin_sign_def)


[STATEMENT]
lemma nth_bintr: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) n \<longleftrightarrow> n < m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (take_bit m w) n = (n < m \<and> bit w n)
[PROOF STEP]
by (fact bit_take_bit_iff)


[STATEMENT]
lemma nth_sbintr: "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) n = (if n < m then (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w n else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) w m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (signed_take_bit m w) n = (if n < m then bit w n else bit w m)
[PROOF STEP]
by (simp add: bit_signed_take_bit_iff min_def)


[STATEMENT]
lemma bin_nth_Bit0:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (Num.Bit0 w)) n \<longleftrightarrow>
    (\<exists>m. n = Suc m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral w) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (numeral (num.Bit0 w)) n = (\<exists>m. n = Suc m \<and> bit (numeral w) m)
[PROOF STEP]
using bit_double_iff [of \<open>numeral w :: int\<close> n]
[PROOF STATE]
proof (prove)
using this:
bit (2 * numeral w) n = (bit (numeral w) (n - 1) \<and> n \<noteq> 0 \<and> possible_bit TYPE(int) n)

goal (1 subgoal):
 1. bit (numeral (num.Bit0 w)) n = (\<exists>m. n = Suc m \<and> bit (numeral w) m)
[PROOF STEP]
by (auto intro: exI [of _ \<open>n - 1\<close>])


[STATEMENT]
lemma bin_nth_Bit1:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral (Num.Bit1 w)) n \<longleftrightarrow>
    n = 0 \<or> (\<exists>m. n = Suc m \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) (numeral w) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (numeral (num.Bit1 w)) n = (n = 0 \<or> (\<exists>m. n = Suc m \<and> bit (numeral w) m))
[PROOF STEP]
using even_bit_succ_iff [of \<open>2 * numeral w :: int\<close> n]
    bit_double_iff [of \<open>numeral w :: int\<close> n]
[PROOF STATE]
proof (prove)
using this:
even (2 * numeral w) \<Longrightarrow> bit (1 + 2 * numeral w) n = (bit (2 * numeral w) n \<or> n = 0)
bit (2 * numeral w) n = (bit (numeral w) (n - 1) \<and> n \<noteq> 0 \<and> possible_bit TYPE(int) n)

goal (1 subgoal):
 1. bit (numeral (num.Bit1 w)) n = (n = 0 \<or> (\<exists>m. n = Suc m \<and> bit (numeral w) m))
[PROOF STEP]
by auto


[STATEMENT]
lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> take_bit m (take_bit n w) = take_bit n w
[PROOF STEP]
by simp


[STATEMENT]
lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> signed_take_bit m (signed_take_bit n w) = signed_take_bit n w
[PROOF STEP]
by simp


[STATEMENT]
lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> take_bit n (take_bit m w) = take_bit n w
[PROOF STEP]
by (rule bin_eqI) (auto simp: nth_bintr)


[STATEMENT]
lemma bintrunc_bintrunc_min [simp]: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (min m n) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit m (take_bit n w) = take_bit (min m n) w
[PROOF STEP]
by (rule take_bit_take_bit)


[STATEMENT]
lemma sbintrunc_sbintrunc_min [simp]: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (min m n) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit m (signed_take_bit n w) = signed_take_bit (min m n) w
[PROOF STEP]
by (rule signed_take_bit_signed_take_bit)


[STATEMENT]
lemma bintrunc_minus: "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc (n - 1)) w = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> take_bit (Suc (n - 1)) w = take_bit n w
[PROOF STEP]
by auto


[STATEMENT]
lemma sbintrunc_minus: "0 < n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc (n - 1)) w = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> signed_take_bit (Suc (n - 1)) w = signed_take_bit n w
[PROOF STEP]
by auto


[STATEMENT]
lemma sbintrunc_BIT_I:
  \<open>0 < n \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) 0 = y \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n 0 = 2 * y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; signed_take_bit (n - 1) 0 = y\<rbrakk> \<Longrightarrow> signed_take_bit n 0 = 2 * y
[PROOF STEP]
by simp


[STATEMENT]
lemma sbintrunc_Suc_Is:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = y \<Longrightarrow>
  (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) (- 1) = 1 + 2 * y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (- 1) = y \<Longrightarrow> signed_take_bit (Suc n) (- 1) = 1 + 2 * y
[PROOF STEP]
by auto


[STATEMENT]
lemma sbintrunc_Suc_lem: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>signed_take_bit (Suc n) x = y; m = Suc n\<rbrakk> \<Longrightarrow> signed_take_bit m x = y
[PROOF STEP]
by (rule ssubst)


[STATEMENT]
lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> signed_take_bit n (take_bit m w) = signed_take_bit n w
[PROOF STEP]
by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)


[STATEMENT]
lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) m w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> Suc n \<Longrightarrow> take_bit m (signed_take_bit n w) = take_bit m w
[PROOF STEP]
by (rule take_bit_signed_take_bit)


[STATEMENT]
lemma bintrunc_sbintrunc' [simp]: "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) w) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> take_bit n (signed_take_bit (n - 1) w) = take_bit n w
[PROOF STEP]
by (cases n) simp_all


[STATEMENT]
lemma sbintrunc_bintrunc' [simp]: "0 < n \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> signed_take_bit (n - 1) (take_bit n w) = signed_take_bit (n - 1) w
[PROOF STEP]
by (cases n) simp_all


[STATEMENT]
lemma bin_sbin_eq_iff: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) y \<longleftrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (take_bit (Suc n) x = take_bit (Suc n) y) = (signed_take_bit n x = signed_take_bit n y)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. take_bit (Suc n) x = take_bit (Suc n) y \<Longrightarrow> signed_take_bit n x = signed_take_bit n y
 2. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y
[PROOF STEP]
apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. take_bit (Suc n) x = take_bit (Suc n) y \<Longrightarrow> signed_take_bit n (take_bit (Suc n) x) = signed_take_bit n (take_bit (Suc n) y)
 2. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) x = take_bit (Suc n) y
[PROOF STEP]
apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n x = signed_take_bit n y \<Longrightarrow> take_bit (Suc n) (signed_take_bit n x) = take_bit (Suc n) (signed_take_bit n y)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_sbin_eq_iff':
  "0 < n \<Longrightarrow> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n y \<longleftrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (take_bit n x = take_bit n y) = (signed_take_bit (n - 1) x = signed_take_bit (n - 1) y)
[PROOF STEP]
by (cases n) (simp_all add: bin_sbin_eq_iff)


[STATEMENT]
lemma bintrunc_numeral:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit (numeral k) x = of_bool (odd x) + 2 * take_bit (pred_numeral k) (x div 2)
[PROOF STEP]
by (simp add: numeral_eq_Suc take_bit_Suc mod_2_eq_odd)


[STATEMENT]
lemma sbintrunc_numeral:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) x = of_bool (odd x) + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (x div 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit (numeral k) x = of_bool (odd x) + 2 * signed_take_bit (pred_numeral k) (x div 2)
[PROOF STEP]
by (simp add: numeral_eq_Suc signed_take_bit_Suc mod2_eq_if)


[STATEMENT]
lemma bintrunc_numeral_simps [simp]:
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit0 w)) =
    2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit1 w)) =
    1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit0 w)) =
    2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral w)"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit1 w)) =
    1 + 2 * (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral (w + Num.One))"
  "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (take_bit (numeral k) (numeral (num.Bit0 w)) = 2 * take_bit (pred_numeral k) (numeral w) &&& take_bit (numeral k) (numeral (num.Bit1 w)) = 1 + 2 * take_bit (pred_numeral k) (numeral w)) &&& take_bit (numeral k) (- numeral (num.Bit0 w)) = 2 * take_bit (pred_numeral k) (- numeral w) &&& take_bit (numeral k) (- numeral (num.Bit1 w)) = 1 + 2 * take_bit (pred_numeral k) (- numeral (w + num.One)) &&& take_bit (numeral k) 1 = 1
[PROOF STEP]
by (simp_all add: bintrunc_numeral)


[STATEMENT]
lemma sbintrunc_numeral_simps [simp]:
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit0 w)) =
    2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (numeral (Num.Bit1 w)) =
    1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit0 w)) =
    2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral w)"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) (- numeral (Num.Bit1 w)) =
    1 + 2 * (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (pred_numeral k) (- numeral (w + Num.One))"
  "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (numeral k) 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit (numeral k) (numeral (num.Bit0 w)) = 2 * signed_take_bit (pred_numeral k) (numeral w) &&& signed_take_bit (numeral k) (numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit (pred_numeral k) (numeral w)) &&& signed_take_bit (numeral k) (- numeral (num.Bit0 w)) = 2 * signed_take_bit (pred_numeral k) (- numeral w) &&& signed_take_bit (numeral k) (- numeral (num.Bit1 w)) = 1 + 2 * signed_take_bit (pred_numeral k) (- numeral (w + num.One)) &&& signed_take_bit (numeral k) 1 = 1
[PROOF STEP]
by (simp_all add: sbintrunc_numeral)


[STATEMENT]
lemma no_bintr_alt1: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>w. w mod 2 ^ n :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n = (\<lambda>w. w mod 2 ^ n)
[PROOF STEP]
by (rule ext) (rule bintrunc_mod2p)


[STATEMENT]
lemma range_bintrunc: "range ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n) = {i. 0 \<le> i \<and> i < 2 ^ n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (take_bit n) = {i. 0 \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
by (auto simp add: take_bit_eq_mod image_iff) (metis mod_pos_pos_trivial)


[STATEMENT]
lemma no_sbintr_alt2: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n = (\<lambda>w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n)
[PROOF STEP]
by (rule ext) (simp add : sbintrunc_mod2p)


[STATEMENT]
lemma range_sbintrunc: "range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
have \<open>surj (\<lambda>k::int. k + 2 ^ n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj (\<lambda>k. k + 2 ^ n)
[PROOF STEP]
by (rule surjI [of _ \<open>(\<lambda>k. k - 2 ^ n)\<close>]) simp
[PROOF STATE]
proof (state)
this:
surj (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
surj (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
have \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = ((\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)
[PROOF STEP]
by (simp add: sbintrunc_eq_take_bit fun_eq_iff)
[PROOF STATE]
proof (state)
this:
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
surj (\<lambda>k. k + 2 ^ n)
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
surj (\<lambda>k. k + 2 ^ n)
signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)

goal (1 subgoal):
 1. range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
apply (simp only: fun.set_map range_bintrunc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surj (\<lambda>k. k + 2 ^ n); signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n)\<rbrakk> \<Longrightarrow> (\<lambda>k. k - 2 ^ n) ` {i. 0 \<le> i \<and> i < 2 ^ Suc n} = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}
[PROOF STEP]
apply (auto simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>surj (\<lambda>k. k + 2 ^ n); signed_take_bit n = (\<lambda>k. k - 2 ^ n) \<circ> take_bit (Suc n) \<circ> (\<lambda>k. k + 2 ^ n); - (2 ^ n) \<le> x; x < 2 ^ n\<rbrakk> \<Longrightarrow> \<exists>xa\<ge>0. xa < 2 * 2 ^ n \<and> x = xa - 2 ^ n
[PROOF STEP]
apply presburger
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
range (signed_take_bit n) = {i. - (2 ^ n) \<le> i \<and> i < 2 ^ n}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sbintrunc_inc:
  \<open>k + 2 ^ Suc n \<le> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k\<close> if \<open>k < - (2 ^ n)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + 2 ^ Suc n \<le> signed_take_bit n k
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
k < - (2 ^ n)

goal (1 subgoal):
 1. k + 2 ^ Suc n \<le> signed_take_bit n k
[PROOF STEP]
by (fact signed_take_bit_int_greater_eq)


[STATEMENT]
lemma sbintrunc_dec:
  \<open>(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n k \<le> k - 2 ^ (Suc n)\<close> if \<open>k \<ge> 2 ^ n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n k \<le> k - 2 ^ Suc n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> k

goal (1 subgoal):
 1. signed_take_bit n k \<le> k - 2 ^ Suc n
[PROOF STEP]
by (fact signed_take_bit_int_less_eq)


[STATEMENT]
lemma bintr_ge0: "0 \<le> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> take_bit n w
[PROOF STEP]
by (simp add: bintrunc_mod2p)


[STATEMENT]
lemma bintr_lt2p: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w < 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n w < 2 ^ n
[PROOF STEP]
by (simp add: bintrunc_mod2p)


[STATEMENT]
lemma bintr_Min: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n (- 1) = 2 ^ n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n (- 1) = 2 ^ n - 1
[PROOF STEP]
by (simp add: stable_imp_take_bit_eq mask_eq_exp_minus_1)


[STATEMENT]
lemma sbintr_ge: "- (2 ^ n) \<le> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (2 ^ n) \<le> signed_take_bit n w
[PROOF STEP]
by (fact signed_take_bit_int_greater_eq_minus_exp)


[STATEMENT]
lemma sbintr_lt: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n w < 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n w < 2 ^ n
[PROOF STEP]
by (fact signed_take_bit_int_less_exp)


[STATEMENT]
lemma sign_Pls_ge_0: "bin_sign bin = 0 \<longleftrightarrow> bin \<ge> 0"
  for bin :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bin_sign bin = 0) = (0 \<le> bin)
[PROOF STEP]
by (simp add: bin_sign_def)


[STATEMENT]
lemma sign_Min_lt_0: "bin_sign bin = -1 \<longleftrightarrow> bin < 0"
  for bin :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bin_sign bin = - 1) = (bin < 0)
[PROOF STEP]
by (simp add: bin_sign_def)


[STATEMENT]
lemma bin_rest_trunc: "(\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - 1) ((\<lambda>k::int. k div 2) bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n bin div 2 = take_bit (n - 1) (bin div 2)
[PROOF STEP]
by (simp add: take_bit_rec [of n bin])


[STATEMENT]
lemma bin_rest_power_trunc:
  "((\<lambda>k::int. k div 2) ^^ k) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin) = (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (n - k) (((\<lambda>k::int. k div 2) ^^ k) bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>k. k div 2) ^^ k) (take_bit n bin) = take_bit (n - k) (((\<lambda>k. k div 2) ^^ k) bin)
[PROOF STEP]
by (induct k) (auto simp: bin_rest_trunc)


[STATEMENT]
lemma bin_rest_trunc_i: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) bin) = (\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n (bin div 2) = take_bit (Suc n) bin div 2
[PROOF STEP]
by (auto simp add: take_bit_Suc)


[STATEMENT]
lemma bin_rest_strunc: "(\<lambda>k::int. k div 2) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) (Suc n) bin) = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit (Suc n) bin div 2 = signed_take_bit n (bin div 2)
[PROOF STEP]
by (simp add: signed_take_bit_Suc)


[STATEMENT]
lemma bintrunc_rest [simp]: "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)) = (\<lambda>k::int. k div 2) ((take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n (take_bit n bin div 2) = take_bit n bin div 2
[PROOF STEP]
by (induct n arbitrary: bin) (simp_all add: take_bit_Suc)


[STATEMENT]
lemma sbintrunc_rest [simp]: "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n ((\<lambda>k::int. k div 2) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)) = (\<lambda>k::int. k div 2) ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n bin)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n (signed_take_bit n bin div 2) = signed_take_bit n bin div 2
[PROOF STEP]
by (induct n arbitrary: bin) (simp_all add: signed_take_bit_Suc mod2_eq_if)


[STATEMENT]
lemma bintrunc_rest': "(take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n \<circ> (\<lambda>k::int. k div 2) \<circ> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>k::int. k div 2) \<circ> (take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take_bit n \<circ> (\<lambda>k. k div 2) \<circ> take_bit n = (\<lambda>k. k div 2) \<circ> take_bit n
[PROOF STEP]
by (rule ext) auto


[STATEMENT]
lemma sbintrunc_rest': "(signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n \<circ> (\<lambda>k::int. k div 2) \<circ> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n = (\<lambda>k::int. k div 2) \<circ> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. signed_take_bit n \<circ> (\<lambda>k. k div 2) \<circ> signed_take_bit n = (\<lambda>k. k div 2) \<circ> signed_take_bit n
[PROOF STEP]
by (rule ext) auto


[STATEMENT]
lemma rco_lem: "f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> f \<circ> (g \<circ> f) ^^ n = g ^^ n \<circ> f
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. f \<circ> g \<circ> f = g \<circ> f \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ 0) x = (g ^^ 0 \<circ> f) x
 2. \<And>x n. \<lbrakk>f \<circ> g \<circ> f = g \<circ> f; (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x\<rbrakk> \<Longrightarrow> (f \<circ> (g \<circ> f) ^^ Suc n) x = (g ^^ Suc n \<circ> f) x
[PROOF STEP]
apply (simp_all (no_asm))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>f \<circ> g \<circ> f = g \<circ> f; (f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x))
[PROOF STEP]
apply (drule fun_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>(f \<circ> (g \<circ> f) ^^ n) x = (g ^^ n \<circ> f) x; (f \<circ> g \<circ> f) (?x3 x n) = (g \<circ> f) (?x3 x n)\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x))
[PROOF STEP]
apply (unfold o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. \<lbrakk>f (((\<lambda>a. g (f a)) ^^ n) x) = (g ^^ n) (f x); f (g (f (?x3 x n))) = g (f (?x3 x n))\<rbrakk> \<Longrightarrow> f (g (f (((\<lambda>a. g (f a)) ^^ n) x))) = g ((g ^^ n) (f x))
[PROOF STEP]
apply (erule trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x n. f (((\<lambda>a. g (f a)) ^^ n) x) = (g ^^ n) (f x) \<Longrightarrow> g (f (((\<lambda>a. g (f a)) ^^ n) x)) = g ((g ^^ n) (f x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [code]:
  "bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2))"
  "bin_split 0 w = (w, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_split (Suc n) w = (let (w1, w2) = bin_split n (w div 2) in (w1, of_bool (odd w) + 2 * w2)) &&& bin_split 0 w = (w, 0)
[PROOF STEP]
by (simp_all add: drop_bit_Suc take_bit_Suc mod_2_eq_odd)


[STATEMENT]
lemma bin_cat_eq_push_bit_add_take_bit:
  \<open>concat_bit n l k = push_bit n k + take_bit n l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n l k = push_bit n k + take_bit n l
[PROOF STEP]
by (simp add: concat_bit_eq)


[STATEMENT]
lemma bin_sign_cat: "bin_sign ((\<lambda>k n l. concat_bit n l k) x n y) = bin_sign x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x
[PROOF STEP]
have \<open>0 \<le> x\<close> if \<open>0 \<le> x * 2 ^ n + y mod 2 ^ n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
have \<open>y mod 2 ^ n < 2 ^ n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y mod 2 ^ n < 2 ^ n
[PROOF STEP]
using pos_mod_bound [of \<open>2 ^ n\<close> y]
[PROOF STATE]
proof (prove)
using this:
0 < 2 ^ n \<Longrightarrow> y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. y mod 2 ^ n < 2 ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y mod 2 ^ n < 2 ^ n
[PROOF STEP]
have \<open>\<not> y mod 2 ^ n \<ge> 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. \<not> 2 ^ n \<le> y mod 2 ^ n
[PROOF STEP]
by (simp add: less_le)
[PROOF STATE]
proof (state)
this:
\<not> 2 ^ n \<le> y mod 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n
\<not> 2 ^ n \<le> y mod 2 ^ n
[PROOF STEP]
have \<open>x \<noteq> - 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n
\<not> 2 ^ n \<le> y mod 2 ^ n

goal (1 subgoal):
 1. x \<noteq> - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> - 1

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
have *: \<open>- 1 \<le> (- (y mod 2 ^ n)) div 2 ^ n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1 \<le> - (y mod 2 ^ n) div 2 ^ n
[PROOF STEP]
by (simp add: zdiv_zminus1_eq_if)
[PROOF STATE]
proof (state)
this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n
[PROOF STEP]
have \<open>- (y mod 2 ^ n) \<le> x * 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n

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

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- (y mod 2 ^ n) \<le> x * 2 ^ n
[PROOF STEP]
have \<open>(- (y mod 2 ^ n)) div 2 ^ n \<le> (x * 2 ^ n) div 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
- (y mod 2 ^ n) \<le> x * 2 ^ n

goal (1 subgoal):
 1. - (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n
[PROOF STEP]
using zdiv_mono1 zero_less_numeral zero_less_power
[PROOF STATE]
proof (prove)
using this:
- (y mod 2 ^ n) \<le> x * 2 ^ n
\<lbrakk>?a \<le> ?a'; 0 < ?b\<rbrakk> \<Longrightarrow> ?a div ?b \<le> ?a' div ?b
(0::?'a) < numeral ?n
(0::?'a) < ?a \<Longrightarrow> (0::?'a) < ?a ^ ?n

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

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n
- (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n
[PROOF STEP]
have \<open>- 1 \<le> x * 2 ^ n div 2 ^ n\<close>
[PROOF STATE]
proof (prove)
using this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n
- (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n

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

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
with \<open>x \<noteq> - 1\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> - 1
- 1 \<le> x * 2 ^ n div 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1
- 1 \<le> x * 2 ^ n div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x

goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x

goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x
[PROOF STEP]
by (simp add: bin_sign_def not_le not_less bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult take_bit_eq_mod)
[PROOF STATE]
proof (state)
this:
bin_sign (concat_bit n y x) = bin_sign x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_cat_assoc: "(\<lambda>k n l. concat_bit n l k) ((\<lambda>k n l. concat_bit n l k) x m y) n z = (\<lambda>k n l. concat_bit n l k) x (m + n) ((\<lambda>k n l. concat_bit n l k) y n z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit n z (concat_bit m y x) = concat_bit (m + n) (concat_bit n z y) x
[PROOF STEP]
by (fact concat_bit_assoc)


[STATEMENT]
lemma bin_cat_assoc_sym: "(\<lambda>k n l. concat_bit n l k) x m ((\<lambda>k n l. concat_bit n l k) y n z) = (\<lambda>k n l. concat_bit n l k) ((\<lambda>k n l. concat_bit n l k) x (m - n) y) (min m n) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_bit m (concat_bit n z y) x = concat_bit (min m n) z (concat_bit (m - n) y x)
[PROOF STEP]
by (fact concat_bit_assoc_sym)


[STATEMENT]
lemma bin_rcat_eq_foldl:
  \<open>bin_rcat n = foldl (\<lambda>u v. (\<lambda>k n l. concat_bit n l k) u n v) 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_rcat n = foldl (\<lambda>u v. concat_bit n v u) 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bin_rcat n x = foldl (\<lambda>u v. concat_bit n v u) 0 x
[PROOF STEP]
fix ks :: \<open>int list\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. bin_rcat n x = foldl (\<lambda>u v. concat_bit n v u) 0 x
[PROOF STEP]
show \<open>bin_rcat n ks = foldl (\<lambda>u v. (\<lambda>k n l. concat_bit n l k) u n v) 0 ks\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_rcat n ks = foldl (\<lambda>u v. concat_bit n v u) 0 ks
[PROOF STEP]
by (induction ks rule: rev_induct)
      (simp_all add: bin_rcat_def concat_bit_eq push_bit_eq_mult)
[PROOF STATE]
proof (state)
this:
bin_rcat n ks = foldl (\<lambda>u v. concat_bit n v u) 0 ks

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_nth_cat:
  "(bit :: int \<Rightarrow> nat \<Rightarrow> bool) ((\<lambda>k n l. concat_bit n l k) x k y) n =
    (if n < k then (bit :: int \<Rightarrow> nat \<Rightarrow> bool) y n else (bit :: int \<Rightarrow> nat \<Rightarrow> bool) x (n - k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (concat_bit k y x) n = (if n < k then bit y n else bit x (n - k))
[PROOF STEP]
by (simp add: bit_concat_bit_iff)


[STATEMENT]
lemma bin_nth_drop_bit_iff:
  \<open>(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (drop_bit n c) k \<longleftrightarrow> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c (n + k)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (drop_bit n c) k = bit c (n + k)
[PROOF STEP]
by (simp add: bit_drop_bit_eq)


[STATEMENT]
lemma bin_nth_take_bit_iff:
  \<open>(bit :: int \<Rightarrow> nat \<Rightarrow> bool) (take_bit n c) k \<longleftrightarrow> k < n \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (take_bit n c) k = (k < n \<and> bit c k)
[PROOF STEP]
by (fact bit_take_bit_iff)


[STATEMENT]
lemma bin_nth_split:
  "bin_split n c = (a, b) \<Longrightarrow>
    (\<forall>k. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) a k = (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c (n + k)) \<and>
    (\<forall>k. (bit :: int \<Rightarrow> nat \<Rightarrow> bool) b k = (k < n \<and> (bit :: int \<Rightarrow> nat \<Rightarrow> bool) c k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_split n c = (a, b) \<Longrightarrow> (\<forall>k. bit a k = bit c (n + k)) \<and> (\<forall>k. bit b k = (k < n \<and> bit c k))
[PROOF STEP]
by (auto simp add: bin_nth_drop_bit_iff bin_nth_take_bit_iff)