[STATEMENT]
lemma P2_OT_14_TF: "R2_14 (m0,m1,m2,m3) (True,False) = funct_OT_14 (m0,m1,m2,m3) (True,False) \<bind> (\<lambda> (out1, out2). S2_14 (True,False) out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
have "R2_14 (m0,m1,m2,m3) (True,False) = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> map_spmf (\<lambda> S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> map_spmf (\<lambda> S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
apply(simp add: R2_14_def inf_th_OT12_P2 OT_12_P2_assm funct_OT_12_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. return_spmf ((True, False), (S0 = (S2 = m0), S0 = (S3 = m1), S1 = (S4 = m2), S1 = (S5 = m3)), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S0. map_spmf (\<lambda>S5. S1 = (S5 = m3)) coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S3. S0 = (S3 = m1)) coin_spmf \<bind> (\<lambda>a1. return_spmf ((True, False), (S0 = (S2 = m0), a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False y \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. return_spmf ((True, False), (S0 = (y = m0), S0 = (S3 = m1), S1 = (S4 = m2), S1 = (S5 = m3)), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S0. map_spmf (\<lambda>S5. S1 = (S5 = m3)) coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S3. S0 = (S3 = m1)) coin_spmf \<bind> (\<lambda>a1. return_spmf ((True, False), (S0 = (S2 = m0), a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 False y \<bind> (\<lambda>ya. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. return_spmf ((True, False), (S0 = (y = m0), S0 = (S3 = m1), S1 = (S4 = m2), S1 = (S5 = m3)), a, ya, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S0. map_spmf (\<lambda>S5. S1 = (S5 = m3)) coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S3. S0 = (S3 = m1)) coin_spmf \<bind> (\<lambda>a1. return_spmf ((True, False), (S0 = (S2 = m0), a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>"  in "bind_spmf _ \<hole>" in "\<hole> = _" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 False y \<bind> (\<lambda>ya. coin_spmf \<bind> (\<lambda>yb. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False yb \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S3. coin_spmf \<bind> (\<lambda>S5. return_spmf ((True, False), (S0 = (y = m0), S0 = (S3 = m1), S1 = (yb = m2), S1 = (S5 = m3)), a, ya, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S0. map_spmf (\<lambda>S5. S1 = (S5 = m3)) coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S3. S0 = (S3 = m1)) coin_spmf \<bind> (\<lambda>a1. return_spmf ((True, False), (S0 = (S2 = m0), a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
have "... = do {
    S0 :: bool \<leftarrow> coin_spmf;
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    let a0 = S0 \<oplus> S2 \<oplus> m0;
    a1 :: bool \<leftarrow> coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin'
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S3. ?S0.0 \<oplus> S3 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in map_spmf (\<lambda>S3. S0 \<oplus> S3 \<oplus> m1) coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in map_spmf (\<lambda>S5. S1 \<oplus> S5 \<oplus> m3) coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
have "... = do {
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> map_spmf (\<lambda> S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf;
    a1 :: bool \<leftarrow> coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S0. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. let a0 = S0 \<oplus> S2 \<oplus> m0 in coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
have "... = do {
    S1 :: bool \<leftarrow> coin_spmf;
    S2 :: bool \<leftarrow> coin_spmf;
    S4 :: bool \<leftarrow> coin_spmf;
    a0 :: bool \<leftarrow> coin_spmf;
    a1 :: bool \<leftarrow> coin_spmf;
    let a2 = S1 \<oplus> S4 \<oplus> m2;
    a3 \<leftarrow> coin_spmf;
    a :: 'v_OT122 \<leftarrow> S2_OT12 True S1;
    b :: 'v_OT122 \<leftarrow> S2_OT12 False S2;
    c :: 'v_OT122 \<leftarrow> S2_OT12 False S4;
    return_spmf ((True,False), (a0,a1,a2,a3), a,b,c)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
using coin_coin
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>S0. S0 \<oplus> ?S3.0 \<oplus> ?m1.0) coin_spmf = coin_spmf

goal (1 subgoal):
 1. coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))
coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. map_spmf (\<lambda>S0. S0 \<oplus> S2 \<oplus> m0) coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>S2. coin_spmf \<bind> (\<lambda>S4. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. let a2 = S1 \<oplus> S4 \<oplus> m2 in coin_spmf \<bind> (\<lambda>a3. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False S2 \<bind> (\<lambda>b. S2_OT12 False S4 \<bind> (\<lambda>c. return_spmf ((True, False), (a0, a1, a2, a3), a, b, c))))))))))

goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)
[PROOF STEP]
apply(simp add: funct_OT_14_def S2_14_def bind_spmf_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))); coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S0. S0 = (S2 = m0)) coin_spmf \<bind> (\<lambda>a0. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))\<rbrakk> \<Longrightarrow> coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>"  in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))); coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S0. S0 = (S2 = m0)) coin_spmf \<bind> (\<lambda>a0. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))\<rbrakk> \<Longrightarrow> coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False y \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))); coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S0. S0 = (S2 = m0)) coin_spmf \<bind> (\<lambda>a0. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))\<rbrakk> \<Longrightarrow> coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 False y \<bind> (\<lambda>y. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, y, c))))))))))
[PROOF STEP]
apply(rewrite in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "bind_spmf _ \<hole>" in "_ = \<hole>" bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R2_14 (m0, m1, m2, m3) (True, False) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))); coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. map_spmf (\<lambda>S0. S0 = (S2 = m0)) coin_spmf \<bind> (\<lambda>a0. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c))))))))))\<rbrakk> \<Longrightarrow> coin_spmf \<bind> (\<lambda>S2. S2_OT12 False S2 \<bind> (\<lambda>b. coin_spmf \<bind> (\<lambda>S4. S2_OT12 False S4 \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>S1. S2_OT12 True S1 \<bind> (\<lambda>a. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (S4 = m2), a3), a, b, c)))))))))) = coin_spmf \<bind> (\<lambda>S1. coin_spmf \<bind> (\<lambda>y. S2_OT12 False y \<bind> (\<lambda>y. coin_spmf \<bind> (\<lambda>ya. S2_OT12 True S1 \<bind> (\<lambda>a. S2_OT12 False ya \<bind> (\<lambda>c. coin_spmf \<bind> (\<lambda>a0. coin_spmf \<bind> (\<lambda>a1. coin_spmf \<bind> (\<lambda>a3. return_spmf ((True, False), (a0, a1, S1 = (ya = m2), a3), a, y, c))))))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
R2_14 (m0, m1, m2, m3) (True, False) = funct_OT_14 (m0, m1, m2, m3) (True, False) \<bind> (\<lambda>(out1, out2). S2_14 (True, False) out2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P2_sec_OT_14_split: "R2_14 (m0,m1,m2,m3) (c0,c1) = funct_OT_14 (m0,m1,m2,m3) (c0,c1) \<bind> (\<lambda> (out1, out2). S2_14 (c0,c1) out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 (m0, m1, m2, m3) (c0, c1) = funct_OT_14 (m0, m1, m2, m3) (c0, c1) \<bind> (\<lambda>(out1, out2). S2_14 (c0, c1) out2)
[PROOF STEP]
by(cases c0; cases c1; auto simp add: P2_OT_14_FF P2_OT_14_TF P2_OT_14_FT P2_OT_14_TT)


[STATEMENT]
lemma P2_sec_OT_14: "R2_14 M C = funct_OT_14 M C \<bind> (\<lambda> (out1, out2). S2_14 C out2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 M C = funct_OT_14 M C \<bind> (\<lambda>(out1, out2). S2_14 C out2)
[PROOF STEP]
by(metis P2_sec_OT_14_split surj_pair)


[STATEMENT]
lemma correctness_OT_14:
  shows "funct_OT_14 M C = protocol_14_OT M C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funct_OT_14 M C = protocol_14_OT M C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. funct_OT_14 M C = protocol_14_OT M C
[PROOF STEP]
have "S1 = (S5 = (S1 = (S5 = d))) = d" for S1 S5 d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S1 = (S5 = (S1 = (S5 = d)))) = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(?S1.0 = (?S5.0 = (?S1.0 = (?S5.0 = ?d)))) = ?d

goal (1 subgoal):
 1. funct_OT_14 M C = protocol_14_OT M C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?S1.0 = (?S5.0 = (?S1.0 = (?S5.0 = ?d)))) = ?d

goal (1 subgoal):
 1. funct_OT_14 M C = protocol_14_OT M C
[PROOF STEP]
by(cases "fst C"; cases "snd C"; simp add: funct_OT_14_def protocol_14_OT_def correct funct_OT_12_def lossless_funct_OT_12 bind_spmf_const split_def)
[PROOF STATE]
proof (state)
this:
funct_OT_14 M C = protocol_14_OT M C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma OT_14_correct: "OT_14.correctness M C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_14.correctness M C
[PROOF STEP]
unfolding OT_14.correctness_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. protocol_14_OT M C = funct_OT_14 M C
[PROOF STEP]
using correctness_OT_14
[PROOF STATE]
proof (prove)
using this:
funct_OT_14 ?M ?C = protocol_14_OT ?M ?C

goal (1 subgoal):
 1. protocol_14_OT M C = funct_OT_14 M C
[PROOF STEP]
by auto


[STATEMENT]
lemma OT_14_P2_sec: "OT_14.perfect_sec_P2 m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_14.perfect_sec_P2 m1 m2
[PROOF STEP]
unfolding OT_14.perfect_sec_P2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2_14 m1 m2 = funct_OT_14 m1 m2 \<bind> (\<lambda>(s1, s2). S2_14 m2 s2)
[PROOF STEP]
using P2_sec_OT_14
[PROOF STATE]
proof (prove)
using this:
R2_14 ?M ?C = funct_OT_14 ?M ?C \<bind> (\<lambda>(out1, out2). S2_14 ?C out2)

goal (1 subgoal):
 1. R2_14 m1 m2 = funct_OT_14 m1 m2 \<bind> (\<lambda>(s1, s2). S2_14 m2 s2)
[PROOF STEP]
by blast


[STATEMENT]
lemma OT_14_P1_sec: "OT_14.adv_P1 m1 m2 D \<le> 3 * adv_OT12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_14.adv_P1 m1 m2 D \<le> 3 * adv_OT12
[PROOF STEP]
unfolding OT_14.adv_P1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 m1 m2 \<bind> D) True - spmf (funct_OT_14 m1 m2 \<bind> (\<lambda>(o1, o2). S1_14 m1 o1 \<bind> D)) True\<bar> \<le> 3 * adv_OT12
[PROOF STEP]
by (metis reduction_P1 surj_pair)


[STATEMENT]
lemma OT_14_P1_sec: "OT_14.adv_P1 (R1_12_0T n) n m1 m2 D \<le> 3 * (adv_OT12 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D \<le> 3 * adv_OT12 n
[PROOF STEP]
unfolding OT_14.adv_P1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>spmf (R1_14 (R1_12_0T n) n m1 m2 \<bind> D) True - spmf (funct_OT_14 m1 m2 \<bind> (\<lambda>(o1, o2). S1_14 n m1 o1 \<bind> D)) True\<bar> \<le> 3 * adv_OT12 n
[PROOF STEP]
using reduction_P1 surj_pair
[PROOF STATE]
proof (prove)
using this:
\<bar>spmf (R1_14 ?R1_12_0T ?n ?M (?c0.0, ?c1.0) \<bind> ?D) True - spmf (funct_OT_14 ?M (?c0.0, ?c1.0) \<bind> (\<lambda>(out1, out2). S1_14 ?n ?M out1 \<bind> ?D)) True\<bar> \<le> 3 * adv_OT12 ?n
\<exists>x y. ?p = (x, y)

goal (1 subgoal):
 1. \<bar>spmf (R1_14 (R1_12_0T n) n m1 m2 \<bind> D) True - spmf (funct_OT_14 m1 m2 \<bind> (\<lambda>(o1, o2). S1_14 n m1 o1 \<bind> D)) True\<bar> \<le> 3 * adv_OT12 n
[PROOF STEP]
by metis


[STATEMENT]
theorem OT_14_P1_asym_sec: "negligible (\<lambda> n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)" if "negligible (\<lambda> n. adv_OT12 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
have adv_neg: "negligible (\<lambda>n. 3 * adv_OT12 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. 3 * adv_OT12 n)
[PROOF STEP]
using that negligible_cmultI
[PROOF STATE]
proof (prove)
using this:
Negligible.negligible adv_OT12
(?c \<noteq> 0 \<Longrightarrow> Negligible.negligible ?f) \<Longrightarrow> Negligible.negligible (\<lambda>\<eta>. ?c * ?f \<eta>)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. 3 * adv_OT12 n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Negligible.negligible (\<lambda>n. 3 * adv_OT12 n)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
have "\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * (adv_OT12 n)\<bar>" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 n\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 n\<bar>
[PROOF STEP]
have "\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n
[PROOF STEP]
using OT_14.adv_P1_def OT_14_P1_sec
[PROOF STATE]
proof (prove)
using this:
OT_14.adv_P1 ?R1_12_0T ?n ?m1.0 ?m2.0 ?D \<equiv> \<bar>spmf (R1_14 ?R1_12_0T ?n ?m1.0 ?m2.0 \<bind> ?D) True - spmf (funct_OT_14 ?m1.0 ?m2.0 \<bind> (\<lambda>(o1, o2). S1_14 ?n ?m1.0 o1 \<bind> ?D)) True\<bar>
OT_14.adv_P1 (?R1_12_0T ?n) ?n ?m1.0 ?m2.0 ?D \<le> 3 * adv_OT12 ?n

goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n

goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 n\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> 3 * adv_OT12 n

goal (1 subgoal):
 1. \<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 n\<bar>
[PROOF STEP]
by (meson abs_ge_self order_trans)
[PROOF STATE]
proof (state)
this:
\<bar>OT_14.adv_P1 (R1_12_0T n) n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 n\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>OT_14.adv_P1 (R1_12_0T ?n) ?n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 ?n\<bar>

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>OT_14.adv_P1 (R1_12_0T ?n) ?n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 ?n\<bar>

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
using OT_14_P1_sec negligible_le adv_neg
[PROOF STATE]
proof (prove)
using this:
\<bar>OT_14.adv_P1 (R1_12_0T ?n) ?n m1 m2 D\<bar> \<le> \<bar>3 * adv_OT12 ?n\<bar>
OT_14.adv_P1 (?R1_12_0T ?n) ?n ?m1.0 ?m2.0 ?D \<le> 3 * adv_OT12 ?n
\<lbrakk>Negligible.negligible ?g; \<And>\<eta>. \<bar>?f \<eta>\<bar> \<le> ?g \<eta>\<rbrakk> \<Longrightarrow> Negligible.negligible ?f
Negligible.negligible (\<lambda>n. 3 * adv_OT12 n)

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)
[PROOF STEP]
by (metis (no_types, lifting) negligible_absI)
[PROOF STATE]
proof (state)
this:
Negligible.negligible (\<lambda>n. OT_14.adv_P1 (R1_12_0T n) n m1 m2 D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem OT_14_P2_asym_sec: "OT_14.perfect_sec_P2 R2_OT12 n m1 m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OT_14.perfect_sec_P2 R2_OT12 n m1 m2
[PROOF STEP]
using OT_14_P2_sec
[PROOF STATE]
proof (prove)
using this:
OT_14.perfect_sec_P2 ?R2_12OT ?n ?m1.0 ?m2.0

goal (1 subgoal):
 1. OT_14.perfect_sec_P2 R2_OT12 n m1 m2
[PROOF STEP]
by simp


[STATEMENT]
lemma horner_sum_of_bool_2_concat:
  \<open>horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws\<close>
  for ws :: \<open>'a::len word list\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws
[PROOF STEP]
proof (induction ws)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []
 2. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []
 2. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) [])) = horner_sum uint (2 ^ LENGTH('a)) []

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
case (Cons w ws)
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
have \<open>horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w
[PROOF STEP]
fix k :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w
[PROOF STEP]
have \<open>map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]
      = map (bit k) [0..<LENGTH('a)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]

goal (1 subgoal):
 1. \<And>w. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit w n) [0..<LENGTH('a)]) = take_bit LENGTH('a) w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]
[PROOF STEP]
show \<open>horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)])
      = take_bit LENGTH('a) k\<close>
[PROOF STATE]
proof (prove)
using this:
map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)] = map (bit k) [0..<LENGTH('a)]

goal (1 subgoal):
 1. horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]) = take_bit LENGTH('a) k
[PROOF STEP]
by (simp only: horner_sum_bit_eq_take_bit)
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (map (\<lambda>n. n < LENGTH('a) \<and> bit k n) [0..<LENGTH('a)]) = take_bit LENGTH('a) k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w

goal (1 subgoal):
 1. \<And>a ws. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws \<Longrightarrow> horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (a # ws))) = horner_sum uint (2 ^ LENGTH('a)) (a # ws)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) ws)) = horner_sum uint (2 ^ LENGTH('a)) ws
horner_sum of_bool 2 (map (bit w) [0..<LENGTH('a)]) = uint w

goal (1 subgoal):
 1. horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (w # ws))) = horner_sum uint (2 ^ LENGTH('a)) (w # ws)
[PROOF STEP]
by (simp add: horner_sum_append)
[PROOF STATE]
proof (state)
this:
horner_sum of_bool 2 (concat (map (\<lambda>x. map (bit x) [0..<LENGTH('a)]) (w # ws))) = horner_sum uint (2 ^ LENGTH('a)) (w # ws)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_takefill: "m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill)
[PROOF STEP]
apply (induct n arbitrary: m l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m l. m < 0 \<Longrightarrow> takefill fill 0 l ! m = (if m < length l then l ! m else fill)
 2. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> takefill fill (Suc n) l ! m = (if m < length l then l ! m else fill)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> takefill fill (Suc n) l ! m = (if m < length l then l ! m else fill)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill)
[PROOF STEP]
apply (case_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m l. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = 0\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill)
 2. \<And>n m l nat. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = Suc nat\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill)
[PROOF STEP]
apply (simp split: list.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m l nat. \<lbrakk>\<And>m l. m < n \<Longrightarrow> takefill fill n l ! m = (if m < length l then l ! m else fill); m < Suc n; m = Suc nat\<rbrakk> \<Longrightarrow> (m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = l ! m) \<and> (\<not> m < length l \<longrightarrow> (case l of [] \<Rightarrow> fill # takefill fill n l | y # ys \<Rightarrow> y # takefill fill n ys) ! m = fill)
[PROOF STEP]
apply (simp split: list.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma takefill_alt: "takefill fill n l = take n l @ replicate (n - length l) fill"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill fill n l = take n l @ replicate (n - length l) fill
[PROOF STEP]
by (induct n arbitrary: l) (auto split: list.split)


[STATEMENT]
lemma takefill_replicate [simp]: "takefill fill n (replicate m fill) = replicate n fill"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill fill n (replicate m fill) = replicate n fill
[PROOF STEP]
by (simp add: takefill_alt replicate_add [symmetric])


[STATEMENT]
lemma takefill_le': "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l
[PROOF STEP]
by (induct m arbitrary: l n) (auto split: list.split)


[STATEMENT]
lemma length_takefill [simp]: "length (takefill fill n l) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takefill fill n l) = n
[PROOF STEP]
by (simp add: takefill_alt)


[STATEMENT]
lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w
[PROOF STEP]
by (induct k arbitrary: w n) (auto split: list.split)


[STATEMENT]
lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)
[PROOF STEP]
by (induct k arbitrary: w) (auto split: list.split)


[STATEMENT]
lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l
[PROOF STEP]
by (auto simp: le_iff_add takefill_le')


[STATEMENT]
lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w
[PROOF STEP]
by (auto simp: le_iff_add take_takefill')


[STATEMENT]
lemma takefill_append: "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill fill (m + length xs) (xs @ w) = xs @ takefill fill m w
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma takefill_same': "l = length xs \<Longrightarrow> takefill fill l xs = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l = length xs \<Longrightarrow> takefill fill l xs = xs
[PROOF STEP]
by (induct xs arbitrary: l) auto


[STATEMENT]
lemma tf_rev:
  "n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) =
    rev (takefill y m (rev (takefill x k (rev bl))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + k = m + length bl \<Longrightarrow> takefill x m (rev (takefill y n bl)) = rev (takefill y m (rev (takefill x k (rev bl))))
[PROOF STEP]
apply (rule nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n + k = m + length bl \<Longrightarrow> length (takefill x m (rev (takefill y n bl))) = length (rev (takefill y m (rev (takefill x k (rev bl)))))
 2. \<And>i. \<lbrakk>n + k = m + length bl; i < length (takefill x m (rev (takefill y n bl)))\<rbrakk> \<Longrightarrow> takefill x m (rev (takefill y n bl)) ! i = rev (takefill y m (rev (takefill x k (rev bl)))) ! i
[PROOF STEP]
apply (auto simp add: nth_takefill rev_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n + k = m + length bl; i < m; n - Suc i < length bl; k + i - m < length bl; i < n; m - Suc i < k\<rbrakk> \<Longrightarrow> bl ! (n - Suc i) = bl ! (length bl + m - Suc (k + i))
[PROOF STEP]
apply (rule_tac f = "\<lambda>n. bl ! n" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n + k = m + length bl; i < m; n - Suc i < length bl; k + i - m < length bl; i < n; m - Suc i < k\<rbrakk> \<Longrightarrow> n - Suc i = length bl + m - Suc (k + i)
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma takefill_minus: "0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> takefill fill (Suc (n - 1)) w = takefill fill n w
[PROOF STEP]
by auto


[STATEMENT]
lemma takefill_numeral_Nil [simp]:
  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma takefill_numeral_Cons [simp]:
  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs
[PROOF STEP]
by (simp add: numeral_eq_Suc)


[STATEMENT]
lemma bl_of_nth_simps [simp, code]:
  "bl_of_nth 0 f = []"
  "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_of_nth 0 f = [] &&& bl_of_nth (Suc n) f = f n # bl_of_nth n f
[PROOF STEP]
by (simp_all add: bl_of_nth_def)


[STATEMENT]
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bl_of_nth n f) = n
[PROOF STEP]
by (simp add: bl_of_nth_def)


[STATEMENT]
lemma nth_bl_of_nth [simp]: "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m
[PROOF STEP]
by (simp add: bl_of_nth_def rev_map)


[STATEMENT]
lemma bl_of_nth_inj: "(\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k < n \<Longrightarrow> f k = g k) \<Longrightarrow> bl_of_nth n f = bl_of_nth n g
[PROOF STEP]
by (simp add: bl_of_nth_def)


[STATEMENT]
lemma bl_of_nth_nth_le: "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs
[PROOF STEP]
apply (induct n arbitrary: xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs. 0 \<le> length xs \<Longrightarrow> bl_of_nth 0 ((!) (rev xs)) = drop (length xs - 0) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> bl_of_nth (Suc n) ((!) (rev xs)) = drop (length xs - Suc n) xs
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> bl_of_nth (Suc n) ((!) (rev xs)) = drop (length xs - Suc n) xs
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = drop (length xs - Suc n) xs
[PROOF STEP]
apply (rule trans [OF _ hd_Cons_tl])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = hd (drop (length xs - Suc n) xs) # tl (drop (length xs - Suc n) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> []
[PROOF STEP]
apply (frule Suc_le_lessD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs; n < length xs\<rbrakk> \<Longrightarrow> rev xs ! n # drop (length xs - n) xs = hd (drop (length xs - Suc n) xs) # tl (drop (length xs - Suc n) xs)
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> []
[PROOF STEP]
apply (simp add: rev_nth trans [OF drop_Suc drop_tl, symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = hd (drop (length xs - Suc n) xs) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> []
[PROOF STEP]
apply (subst hd_drop_conv_nth)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> length xs - Suc n < length xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = xs ! (length xs - Suc n) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 3. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> []
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> xs ! (length xs - Suc n) = xs ! (length xs - Suc n) \<and> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
 2. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; Suc n \<le> length xs\<rbrakk> \<Longrightarrow> drop (length xs - Suc n) xs \<noteq> []
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> drop (length xs - n) xs = drop (Suc (length xs - Suc n)) xs
[PROOF STEP]
apply (rule_tac f = "\<lambda>n. drop n xs" in arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n xs. \<lbrakk>\<And>xs. n \<le> length xs \<Longrightarrow> bl_of_nth n ((!) (rev xs)) = drop (length xs - n) xs; n < length xs\<rbrakk> \<Longrightarrow> length xs - n = Suc (length xs - Suc n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) ((!) (rev xs)) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_of_nth (length xs) ((!) (rev xs)) = xs
[PROOF STEP]
by (simp add: bl_of_nth_nth_le)


[STATEMENT]
lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater1 (l @ [a]) = a # l
[PROOF STEP]
by (cases l) (auto simp: rotater1_def)


[STATEMENT]
lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater1 (rotate1 l) = l
[PROOF STEP]
apply (unfold rotater1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
[PROOF STEP]
apply (cases "l")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 2. \<And>a list. l = a # list \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
[PROOF STEP]
apply (case_tac [2] "list")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l = [] \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 2. \<And>a list. \<lbrakk>l = a # list; list = []\<rbrakk> \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
 3. \<And>a list aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> (case rotate1 l of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (rotate1 l) # butlast (rotate1 l)) = l
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotate1 (rotater1 l) = l
[PROOF STEP]
by (cases l) (auto simp: rotater1_def)


[STATEMENT]
lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater1 (rev xs) = rev (rotate1 xs)
[PROOF STEP]
by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')


[STATEMENT]
lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater n (rev xs) = rev (rotate n xs)
[PROOF STEP]
by (induct n) (auto simp: rotater_def intro: rotater1_rev')


[STATEMENT]
lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater n ys = rev (rotate n (rev ys))
[PROOF STEP]
using rotater_rev' [where xs = "rev ys"]
[PROOF STATE]
proof (prove)
using this:
rotater ?n (rev (rev ys)) = rev (rotate ?n (rev ys))

goal (1 subgoal):
 1. rotater n ys = rev (rotate n (rev ys))
[PROOF STEP]
by simp


[STATEMENT]
lemma rotater_drop_take:
  "rotater n xs =
    drop (length xs - n mod length xs) xs @
    take (length xs - n mod length xs) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater n xs = drop (length xs - n mod length xs) xs @ take (length xs - n mod length xs) xs
[PROOF STEP]
by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)


[STATEMENT]
lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater (Suc n) xs = rotater1 (rotater n xs)
[PROOF STEP]
unfolding rotater_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rotater1 ^^ Suc n) xs = rotater1 ((rotater1 ^^ n) xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma nth_rotater:
  \<open>rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)\<close> if \<open>n < length xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
n < length xs

goal (1 subgoal):
 1. rotater m xs ! n = xs ! ((n + (length xs - m mod length xs)) mod length xs)
[PROOF STEP]
by (simp add: rotater_drop_take nth_append not_less less_diff_conv ac_simps le_mod_geq)


[STATEMENT]
lemma nth_rotater1:
  \<open>rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)\<close> if \<open>n < length xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)
[PROOF STEP]
using that nth_rotater [of n xs 1]
[PROOF STATE]
proof (prove)
using this:
n < length xs
n < length xs \<Longrightarrow> rotater 1 xs ! n = xs ! ((n + (length xs - 1 mod length xs)) mod length xs)

goal (1 subgoal):
 1. rotater1 xs ! n = xs ! ((n + (length xs - 1)) mod length xs)
[PROOF STEP]
by simp


[STATEMENT]
lemma rotate_inv_plus [rule_format]:
  "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
    rotate k (rotater n xs) = rotate m xs \<and>
    rotater n (rotate k xs) = rotate m xs \<and>
    rotate n (rotater k xs) = rotater m xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and> rotate k (rotater n xs) = rotate m xs \<and> rotater n (rotate k xs) = rotate m xs \<and> rotate n (rotater k xs) = rotater m xs
[PROOF STEP]
by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])


[STATEMENT]
lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rotater n xs = ys) = (rotate n ys = xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ys = rotater n xs) = (xs = rotate n ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma length_rotater [simp]: "length (rotater n xs) = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (rotater n xs) = length xs
[PROOF STEP]
by (simp add : rotater_rev)


[STATEMENT]
lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs
[PROOF STEP]
apply (rule box_equals)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m mod length xs = n mod length xs \<Longrightarrow> ?a = ?b
 2. m mod length xs = n mod length xs \<Longrightarrow> ?a = rotate m xs
 3. m mod length xs = n mod length xs \<Longrightarrow> ?b = rotate n xs
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. m mod length xs = n mod length xs \<Longrightarrow> ?a = rotate m xs
 2. m mod length xs = n mod length xs \<Longrightarrow> ?b = rotate n xs
 3. m mod length xs = n mod length xs \<Longrightarrow> ?a = ?b
[PROOF STEP]
apply (rule rotate_conv_mod [symmetric])+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m mod length xs = n mod length xs \<Longrightarrow> rotate (m mod length xs) xs = rotate (n mod length xs) xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<Longrightarrow> (x = z) = (y = z)
[PROOF STEP]
by simp


[STATEMENT]
lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)
[PROOF STEP]
by (induct xs) auto


[STATEMENT]
lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater1 (map f xs) = map f (rotater1 xs)
[PROOF STEP]
by (cases xs) (auto simp: rotater1_def last_map butlast_map)


[STATEMENT]
lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rotater n (map f xs) = map f (rotater n xs)
[PROOF STEP]
by (induct n) (auto simp: rotater_def rotater1_map)


[STATEMENT]
lemma but_last_zip [rule_format] :
  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
    last (zip xs ys) = (last xs, last ys) \<and>
    butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys)
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>ys. length [] = length ys \<longrightarrow> [] \<noteq> [] \<longrightarrow> last (zip [] ys) = (last [], last ys) \<and> butlast (zip [] ys) = zip (butlast []) (butlast ys)
 2. \<And>a xs. \<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys) \<Longrightarrow> \<forall>ys. length (a # xs) = length ys \<longrightarrow> a # xs \<noteq> [] \<longrightarrow> last (zip (a # xs) ys) = (last (a # xs), last ys) \<and> butlast (zip (a # xs) ys) = zip (butlast (a # xs)) (butlast ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a ys. Suc 0 = length ys \<Longrightarrow> last (zip [a] ys) = (a, last ys)
 2. \<And>a ys. Suc 0 = length ys \<Longrightarrow> butlast (zip [a] ys) = []
 3. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> last (zip (a # xs) ys) = (last xs, last ys)
 4. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (zip xs ys) = (last xs, last ys) \<and> butlast (zip xs ys) = zip (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> butlast (zip (a # xs) ys) = zip (a # butlast xs) (butlast ys)
[PROOF STEP]
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma but_last_map2 [rule_format] :
  "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
    last (map2 f xs ys) = f (last xs) (last ys) \<and>
    butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>ys. length [] = length ys \<longrightarrow> [] \<noteq> [] \<longrightarrow> last (map2 f [] ys) = f (last []) (last ys) \<and> butlast (map2 f [] ys) = map2 f (butlast []) (butlast ys)
 2. \<And>a xs. \<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys) \<Longrightarrow> \<forall>ys. length (a # xs) = length ys \<longrightarrow> a # xs \<noteq> [] \<longrightarrow> last (map2 f (a # xs) ys) = f (last (a # xs)) (last ys) \<and> butlast (map2 f (a # xs) ys) = map2 f (butlast (a # xs)) (butlast ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a ys. Suc 0 = length ys \<Longrightarrow> last (map2 f [a] ys) = f a (last ys)
 2. \<And>a ys. Suc 0 = length ys \<Longrightarrow> butlast (map2 f [a] ys) = []
 3. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> last (map2 f (a # xs) ys) = f (last xs) (last ys)
 4. \<And>a xs ys. \<lbrakk>\<forall>ys. length xs = length ys \<longrightarrow> last (map2 f xs ys) = f (last xs) (last ys) \<and> butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys); xs \<noteq> []; Suc (length xs) = length ys\<rbrakk> \<Longrightarrow> butlast (map2 f (a # xs) ys) = map2 f (a # butlast xs) (butlast ys)
[PROOF STEP]
apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rotater1_zip:
  "length xs = length ys \<Longrightarrow>
    rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)
[PROOF STEP]
apply (unfold rotater1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
[PROOF STEP]
apply (cases xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length xs = length ys; xs = []\<rbrakk> \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
 2. \<And>a list. \<lbrakk>length xs = length ys; xs = a # list\<rbrakk> \<Longrightarrow> (case zip xs ys of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last (zip xs ys) # butlast (zip xs ys)) = zip (case xs of [] \<Rightarrow> [] | x # xsa \<Rightarrow> last xs # butlast xs) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>Suc 0 = length ys; xs = [a]\<rbrakk> \<Longrightarrow> (case zip [a] ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (zip [a] ys) # butlast (zip [a] ys)) = zip [a] (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
 2. \<And>a list. \<lbrakk>Suc (length list) = length ys; xs = a # list; list \<noteq> []\<rbrakk> \<Longrightarrow> (case zip (a # list) ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last (zip (a # list) ys) # butlast (zip (a # list) ys)) = zip (last list # a # butlast list) (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)
[PROOF STEP]
apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rotater1_map2:
  "length xs = length ys \<Longrightarrow>
    rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)
[PROOF STEP]
by (simp add: rotater1_map rotater1_zip)


[STATEMENT]
lemma rotater_map2:
  "length xs = length ys \<Longrightarrow>
    rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)
[PROOF STEP]
by (induct n) (auto intro!: lrth)


[STATEMENT]
lemma rotate1_map2:
  "length xs = length ys \<Longrightarrow>
    rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)
[PROOF STEP]
by (cases xs; cases ys) auto


[STATEMENT]
lemma rotate_map2:
  "length xs = length ys \<Longrightarrow>
    rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)
[PROOF STEP]
by (induct n) (auto intro!: lth)


[STATEMENT]
lemma bin_to_bl_aux_zero_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = bin_to_bl_aux (n - 1) 0 (False # bl)
[PROOF STEP]
by (cases n) auto


[STATEMENT]
lemma bin_to_bl_aux_minus1_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (- 1) bl = bin_to_bl_aux (n - 1) (- 1) (True # bl)
[PROOF STEP]
by (cases n) auto


[STATEMENT]
lemma bin_to_bl_aux_one_minus_simp [simp]:
  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = bin_to_bl_aux (n - 1) 0 (True # bl)
[PROOF STEP]
by (cases n) auto


[STATEMENT]
lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
  "0 < n \<Longrightarrow>
    bin_to_bl_aux n (numeral (Num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (numeral (num.Bit0 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (False # bl)
[PROOF STEP]
by (cases n) simp_all


[STATEMENT]
lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
  "0 < n \<Longrightarrow>
    bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> bin_to_bl_aux n (numeral (num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)
[PROOF STEP]
by (cases n) simp_all


[STATEMENT]
lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)
[PROOF STEP]
by (induct bs arbitrary: w) auto


[STATEMENT]
lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)
[PROOF STEP]
by (induct n arbitrary: w bs) auto


[STATEMENT]
lemma bl_to_bin_append: "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)
[PROOF STEP]
unfolding bl_to_bin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin_aux (bs @ cs) 0 = bl_to_bin_aux cs (bl_to_bin_aux bs 0)
[PROOF STEP]
by (rule bl_to_bin_aux_append)


[STATEMENT]
lemma bin_to_bl_aux_alt: "bin_to_bl_aux n w bs = bin_to_bl n w @ bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n w bs = bin_to_bl n w @ bs
[PROOF STEP]
by (simp add: bin_to_bl_def bin_to_bl_aux_append)


[STATEMENT]
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl 0 bs = []
[PROOF STEP]
by (auto simp: bin_to_bl_def)


[STATEMENT]
lemma size_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl_aux n w bs) = n + length bs
[PROOF STEP]
by (induct n arbitrary: w bs) auto


[STATEMENT]
lemma size_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl n w) = n
[PROOF STEP]
by (simp add: bin_to_bl_def size_bin_to_bl_aux)


[STATEMENT]
lemma bl_bin_bl': "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs
[PROOF STEP]
apply (induct bs arbitrary: w n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w n. bin_to_bl (n + length []) (bl_to_bin_aux [] w) = bin_to_bl_aux n w []
 2. \<And>a bs w n. (\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs) \<Longrightarrow> bin_to_bl (n + length (a # bs)) (bl_to_bin_aux (a # bs) w) = bin_to_bl_aux n w (a # bs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w n. bin_to_bl n w = bin_to_bl_aux n w []
 2. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; a\<rbrakk> \<Longrightarrow> bin_to_bl (Suc (n + length bs)) (bl_to_bin_aux bs (1 + 2 * w)) = bin_to_bl_aux n w (True # bs)
 3. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; \<not> a\<rbrakk> \<Longrightarrow> bin_to_bl (Suc (n + length bs)) (bl_to_bin_aux bs (2 * w)) = bin_to_bl_aux n w (False # bs)
[PROOF STEP]
apply (simp_all only: add_Suc [symmetric])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>w n. bin_to_bl n w = bin_to_bl_aux n w []
 2. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; a\<rbrakk> \<Longrightarrow> bin_to_bl_aux (Suc n) (1 + 2 * w) bs = bin_to_bl_aux n w (True # bs)
 3. \<And>a bs w n. \<lbrakk>\<And>w n. bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = bin_to_bl_aux n w bs; \<not> a\<rbrakk> \<Longrightarrow> bin_to_bl_aux (Suc n) (2 * w) bs = bin_to_bl_aux n w (False # bs)
[PROOF STEP]
apply (auto simp add: bin_to_bl_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (length bs) (bl_to_bin bs) = bs
[PROOF STEP]
unfolding bl_to_bin_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (length bs) (bl_to_bin_aux bs 0) = bs
[PROOF STEP]
apply (rule box_equals)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ?a = ?b
 2. ?a = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
 3. ?b = bs
[PROOF STEP]
apply (rule bl_bin_bl')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bin_to_bl (?n4 + length ?bs4) (bl_to_bin_aux ?bs4 ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
 2. bin_to_bl_aux ?n4 ?w4 ?bs4 = bs
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bin_to_bl_aux ?n4 ?w4 ?bs4 = bs
 2. bin_to_bl (?n4 + length ?bs4) (bl_to_bin_aux ?bs4 ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
[PROOF STEP]
apply (rule bin_to_bl_aux.Z)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl (0 + length bs) (bl_to_bin_aux bs ?w4) = bin_to_bl (length bs) (bl_to_bin_aux bs 0)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_to_bin_inj: "bl_to_bin bs = bl_to_bin cs \<Longrightarrow> length bs = length cs \<Longrightarrow> bs = cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bs = cs
[PROOF STEP]
apply (rule_tac box_equals)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = ?b
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = bs
 3. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = bs
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs
 3. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?a = ?b
[PROOF STEP]
apply (rule bl_bin_bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> ?b = cs
 2. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bin_to_bl (length bs) (bl_to_bin bs) = ?b
[PROOF STEP]
apply (rule bl_bin_bl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bl_to_bin bs = bl_to_bin cs; length bs = length cs\<rbrakk> \<Longrightarrow> bin_to_bl (length bs) (bl_to_bin bs) = bin_to_bl (length cs) (bl_to_bin cs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (False # bl) = bl_to_bin bl
[PROOF STEP]
by (auto simp: bl_to_bin_def)


[STATEMENT]
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin [] = 0
[PROOF STEP]
by (auto simp: bl_to_bin_def)


[STATEMENT]
lemma bin_to_bl_zero_aux: "bin_to_bl_aux n 0 bl = replicate n False @ bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n 0 bl = replicate n False @ bl
[PROOF STEP]
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)


[STATEMENT]
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n 0 = replicate n False
[PROOF STEP]
by (simp add: bin_to_bl_def bin_to_bl_zero_aux)


[STATEMENT]
lemma bin_to_bl_minus1_aux: "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (- 1) bl = replicate n True @ bl
[PROOF STEP]
by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)


[STATEMENT]
lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (- 1) = replicate n True
[PROOF STEP]
by (simp add: bin_to_bl_def bin_to_bl_minus1_aux)


[STATEMENT]
lemma bin_bl_bin': "bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (take_bit n w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl_aux n w bs) = bl_to_bin_aux bs (take_bit n w)
[PROOF STEP]
by (induct n arbitrary: w bs) (auto simp: bl_to_bin_def take_bit_Suc ac_simps mod_2_eq_odd)


[STATEMENT]
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = take_bit n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (bin_to_bl n w) = take_bit n w
[PROOF STEP]
by (auto simp: bin_to_bl_def bin_bl_bin')


[STATEMENT]
lemma bl_to_bin_rep_F: "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (replicate n False @ bl) = bl_to_bin bl
[PROOF STEP]
by (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin') (simp add: bl_to_bin_def)


[STATEMENT]
lemma bin_to_bl_trunc [simp]: "n \<le> m \<Longrightarrow> bin_to_bl n (take_bit m w) = bin_to_bl n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> bin_to_bl n (take_bit m w) = bin_to_bl n w
[PROOF STEP]
by (auto intro: bl_to_bin_inj)


[STATEMENT]
lemma bin_to_bl_aux_bintr:
  "bin_to_bl_aux n (take_bit m bin) bl =
    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl
[PROOF STEP]
apply (induct n arbitrary: m bin bl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m bin bl. bin_to_bl_aux 0 (take_bit m bin) bl = replicate (0 - m) False @ bin_to_bl_aux (min 0 m) bin bl
 2. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux (Suc n) (take_bit m bin) bl = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux (Suc n) (take_bit m bin) bl = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n m bin bl. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply (case_tac "m")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n m bin bl. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = 0\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply (clarsimp simp: bin_to_bl_zero_aux)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. (\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl) \<Longrightarrow> replicate n False @ [False] = False # replicate n False
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply (erule thin_rl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. replicate n False @ [False] = False # replicate n False
 2. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. replicate 0 False @ [False] = False # replicate 0 False
 2. \<And>n na. replicate na False @ [False] = False # replicate na False \<Longrightarrow> replicate (Suc na) False @ [False] = False # replicate (Suc na) False
 3. \<And>n m bin bl nat. \<lbrakk>\<And>m bin bl. bin_to_bl_aux n (take_bit m bin) bl = replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl; m = Suc nat\<rbrakk> \<Longrightarrow> bin_to_bl_aux n (take_bit m bin div 2) ((0 < m \<and> odd bin) # bl) = replicate (Suc n - m) False @ bin_to_bl_aux (min (Suc n) m) bin bl
[PROOF STEP]
apply (auto simp add: take_bit_Suc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bin_to_bl_bintr:
  "bin_to_bl n (take_bit m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl n (take_bit m bin) = replicate (n - m) False @ bin_to_bl (min n m) bin
[PROOF STEP]
unfolding bin_to_bl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_to_bl_aux n (take_bit m bin) [] = replicate (n - m) False @ bin_to_bl_aux (min n m) bin []
[PROOF STEP]
by (rule bin_to_bl_aux_bintr)


[STATEMENT]
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl_to_bin (replicate n False) = 0
[PROOF STEP]
by (induct n) auto


[STATEMENT]
lemma len_bin_to_bl_aux: "length (bin_to_bl_aux n w bs) = n + length bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl_aux n w bs) = n + length bs
[PROOF STEP]
by (fact size_bin_to_bl_aux)


[STATEMENT]
lemma len_bin_to_bl: "length (bin_to_bl n w) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bin_to_bl n w) = n
[PROOF STEP]
by (fact size_bin_to_bl)


[STATEMENT]
lemma sign_bl_bin': "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (bl_to_bin_aux bs w) = bin_sign w
[PROOF STEP]
by (induction bs arbitrary: w) (simp_all add: bin_sign_def)


[STATEMENT]
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bin_sign (bl_to_bin bs) = 0
[PROOF STEP]
by (simp add: bl_to_bin_def sign_bl_bin')


[STATEMENT]
lemma bl_sbin_sign_aux: "hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (signed_take_bit n w) = -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl_aux (Suc n) w bs) = (bin_sign (signed_take_bit n w) = - 1)
[PROOF STEP]
by (induction n arbitrary: w bs) (auto simp add: bin_sign_def even_iff_mod_2_eq_zero bit_Suc)


[STATEMENT]
lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (signed_take_bit n w) = -1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl (Suc n) w) = (bin_sign (signed_take_bit n w) = - 1)
[PROOF STEP]
unfolding bin_to_bl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (bin_to_bl_aux (Suc n) w []) = (bin_sign (signed_take_bit n w) = - 1)
[PROOF STEP]
by (rule bl_sbin_sign_aux)