[STATEMENT]
lemma r:
  assumes e1: "e1 = (y + (q - b)) mod q"
    and s1: "s1 = (x*((y + (q - b)) mod q) + (q - r)) mod q"
    and b: "b < q"
    and x: "x < q"
    and y: "y < q"
    and r: "r < q"
  shows "r = (x*e1 + (q - s1)) mod q"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
have "s1 = (x*((y + (q - b))) + (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
using s1 b
[PROOF STATE]
proof (prove)
using this:
s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q
b < q

goal (1 subgoal):
 1. s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
by (metis mod_add_left_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
s1 = (x * (y + (q - b)) + (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
have s1_dist: "s1 = (x*y + x*(q - b) + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
s1 = (x * (y + (q - b)) + (q - r)) mod q

goal (1 subgoal):
 1. s1 = (x * y + x * (q - b) + (q - r)) mod q
[PROOF STEP]
by(metis distrib_left)
[PROOF STATE]
proof (state)
this:
s1 = (x * y + x * (q - b) + (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * y + x * (q - b) + (q - r)) mod q
[PROOF STEP]
have "?rhs = (x*((y + (q - b)) mod q) + (q - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + x * (q - b) + (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * ((y + (q - b)) mod q) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
using e1
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + x * (q - b) + (q - r)) mod q
e1 = (y + (q - b)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * ((y + (q - b)) mod q) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * ((y + (q - b)) mod q) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * ((y + (q - b)) mod q) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have "?rhs = (x*((y + (q - b))) + (q - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * ((y + (q - b)) mod q) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * (y + (q - b)) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by (metis mod_add_left_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * (y + (q - b)) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * (y + (q - b)) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have "?rhs = (x*y + x*(q - b) + (q - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * (y + (q - b)) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * (q - b) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by(metis distrib_left)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * (q - b) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * (q - b) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have a: "?rhs = (x*y + x*q - x*b + (q - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * (q - b) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
using distrib_left b diff_mult_distrib2
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * (q - b) + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
?a * (?b + ?c) = ?a * ?b + ?a * ?c
b < q
?k * (?m - ?n) = ?k * ?m - ?k * ?n

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have b: "?rhs = (x*y + x*q - x*b + (q*q + q*q + q  - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have "(x*y + x*q - x*b + (q - (x*y + x*(q - b) + (q - r)) mod q)) mod q = (x*y + x*q - x*b + (q*q + q*q + q - (x*y + x*(q - b) + (q - r)) mod q)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have f1: "\<forall>n na nb nc nd. (n::nat) mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n na nb nc nd. n mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na
[PROOF STEP]
by (meson mod_add_cong)
[PROOF STATE]
proof (state)
this:
\<forall>n na nb nc nd. n mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n na nb nc nd. n mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na
[PROOF STEP]
have "(q - (x * y + x*(q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x*(q - b) + (q - r)) mod q) mod q"
[PROOF STATE]
proof (prove)
using this:
\<forall>n na nb nc nd. n mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na

goal (1 subgoal):
 1. (q - (x * y + x * (q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q) mod q
[PROOF STEP]
by (metis Nat.diff_add_assoc mod_le_divisor q_gt_0 mod_mult_self4)
[PROOF STATE]
proof (state)
this:
(q - (x * y + x * (q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q) mod q

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q - (x * y + x * (q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q - (x * y + x * (q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q) mod q

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
(q - (x * y + x * (q - b) + (q - r)) mod q) mod q = (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q) mod q
\<forall>n na nb nc nd. n mod na \<noteq> nb mod na \<or> nc mod na \<noteq> nd mod na \<or> (n + nc) mod na = (nb + nd) mod na

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q
[PROOF STEP]
have "?rhs = (x*y + x*q - x*b + (q*q + q*q + q  - (x*y + x*(q - b) + (q - r)))) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have "(x*y + x*q - x*b + (q*q + q*q + q - (x*y + x*(q - b) + (q - r)) mod q)) mod q =
         (x*y + x*q - x*b + (q*q + q*q + q - (x*y + x*(q - b)+ (q - r)))) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
 2. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
 2. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
by (metis (no_types, lifting) assms(2) assms(4) True Nat.add_diff_assoc add.left_neutral
            cong_def diff_le_self minus_mod mult_is_0 not_gr_zero zero_eq_add_iff_both_eq_0 zero_less_diff)
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have qb: "q - b \<le> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - b \<le> q
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

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

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q - b \<le> q
[PROOF STEP]
have qb':"x*(q - b) < q*q"
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q

goal (1 subgoal):
 1. x * (q - b) < q * q
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q
x < q

goal (1 subgoal):
 1. x * (q - b) < q * q
[PROOF STEP]
by (metis mult_less_le_imp_less nat_0_less_mult_iff nat_less_le neq0_conv)
[PROOF STATE]
proof (state)
this:
x * (q - b) < q * q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have a: "x*y + x*(q - b) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x * y + x * (q - b)
[PROOF STEP]
using False assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
e1 = (y + (q - b)) mod q
s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q
b < q
x < q
y < q
r < q

goal (1 subgoal):
 1. 0 < x * y + x * (q - b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < x * y + x * (q - b)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have 1: "q*q > x*y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y < q * q
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * y < q * q
[PROOF STEP]
by (simp add: mult_strict_mono q_gt_0 x y)
[PROOF STATE]
proof (state)
this:
x * y < q * q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have 2: "q*q > x*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
by (simp add: mult_strict_mono q_gt_0 x y)
[PROOF STATE]
proof (state)
this:
x * q < q * q

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have b: "(q*q + q*q + q - (x*y + x*(q - b) + (q - r))) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))
[PROOF STEP]
using 1 qb'
[PROOF STATE]
proof (prove)
using this:
x * y < q * q
x * (q - b) < q * q

goal (1 subgoal):
 1. 0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
using a b mod_minus[of "x*y + x*q" "x*b" "q*q + q*q + q" "x*y + x*(q - b) + (q - r)"]
[PROOF STATE]
proof (prove)
using this:
0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))
0 < x * y + x * (q - b)
0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))
\<lbrakk>0 < x * y + x * q - x * b; 0 < q * q + q * q + q - (x * y + x * (q - b) + (q - r))\<rbrakk> \<Longrightarrow> (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
by (smt add.left_neutral cong_def gr0I minus_mod zero_less_diff)
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q
[PROOF STEP]
have d: "?rhs = (x*y + x*q - x*b + (q*q + q*q + q - x*y - x*(q - b) - (q - r))) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q
[PROOF STEP]
have e: "?rhs = (x*y + x*q - x*b + q*q + q*q + q - x*y - x*(q - b) - (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
proof(cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x = 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
 2. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x = 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
 2. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
using True d
[PROOF STATE]
proof (prove)
using this:
x = 0
x = 0
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have qb: "q - b \<le> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q - b \<le> q
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - (x * y + x * (q - b) + (q - r)) mod q)) mod q

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

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q - b \<le> q
[PROOF STEP]
have qb':"x*(q - b) < q*q"
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q

goal (1 subgoal):
 1. x * (q - b) < q * q
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
q - b \<le> q
x < q

goal (1 subgoal):
 1. x * (q - b) < q * q
[PROOF STEP]
by (metis mult_less_le_imp_less nat_0_less_mult_iff nat_less_le neq0_conv)
[PROOF STATE]
proof (state)
this:
x * (q - b) < q * q

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have a: "x*y + x*(q - b) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x * y + x * (q - b)
[PROOF STEP]
using False assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
e1 = (y + (q - b)) mod q
s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q
b < q
x < q
y < q
r < q

goal (1 subgoal):
 1. 0 < x * y + x * (q - b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < x * y + x * (q - b)

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have 1: "q*q > x*y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y < q * q
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * y < q * q
[PROOF STEP]
by (simp add: mult_strict_mono q_gt_0 x y)
[PROOF STATE]
proof (state)
this:
x * y < q * q

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have 2: "q*q > x*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * q < q * q
[PROOF STEP]
by (simp add: mult_strict_mono q_gt_0 x y)
[PROOF STATE]
proof (state)
this:
x * q < q * q

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have b: "q*q + q*q + q  - x*y - x*(q - b) - (q - r) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)
[PROOF STEP]
using 1 qb'
[PROOF STATE]
proof (prove)
using this:
x * y < q * q
x * (q - b) < q * q

goal (1 subgoal):
 1. 0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)

goal (1 subgoal):
 1. \<lbrakk>(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
using b d
[PROOF STATE]
proof (prove)
using this:
0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)
0 < q * q + q * q + q - x * y - x * (q - b) - (q - r)
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + (q * q + q * q + q - x * y - x * (q - b) - (q - r))) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
by (smt Nat.add_diff_assoc add.assoc diff_diff_left less_imp_le_nat zero_less_diff)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have "?rhs = (x*q - x*b + q*q + q*q + q - x*(q - b) - (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have "(x*y + x*q - x*b + q*q + q*q + q - x*y - x*(q - b) - (q - r)) mod q = (x*q - x*b + q*q + q*q + q - x*(q - b) - (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have 1: "q + n - b = q - b + n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q + n - b = q - b + n
[PROOF STEP]
by (simp add: assms(3) less_imp_le)
[PROOF STATE]
proof (state)
this:
q + ?n - b = q - b + ?n

goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have 2: "(c::nat) * b + (c * a + n) = c * (b + a) + n"
        for n a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * b + (c * a + n) = c * (b + a) + n
[PROOF STEP]
by (simp add: distrib_left)
[PROOF STATE]
proof (state)
this:
?c * ?b + (?c * ?a + ?n) = ?c * (?b + ?a) + ?n

goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have "(c::nat) + (b + a) - (n + a) = c + b - n" for n a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c + (b + a) - (n + a) = c + b - n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?c + (?b + ?a) - (?n + ?a) = ?c + ?b - ?n

goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?c + (?b + ?a) - (?n + ?a) = ?c + ?b - ?n
[PROOF STEP]
have "(q + (q * q + (q * q + x * (q + y - b))) - (q - r + x * (y + (q - b)))) mod q = (q + (q * q + (q * q + x * (q - b))) - (q - r + x * (q - b))) mod q"
[PROOF STATE]
proof (prove)
using this:
?c + (?b + ?a) - (?n + ?a) = ?c + ?b - ?n

goal (1 subgoal):
 1. (q + (q * q + (q * q + x * (q + y - b))) - (q - r + x * (y + (q - b)))) mod q = (q + (q * q + (q * q + x * (q - b))) - (q - r + x * (q - b))) mod q
[PROOF STEP]
by (metis (no_types) add.commute 1 2)
[PROOF STATE]
proof (state)
this:
(q + (q * q + (q * q + x * (q + y - b))) - (q - r + x * (y + (q - b)))) mod q = (q + (q * q + (q * q + x * (q - b))) - (q - r + x * (q - b))) mod q

goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q + (q * q + (q * q + x * (q + y - b))) - (q - r + x * (y + (q - b)))) mod q = (q + (q * q + (q * q + x * (q - b))) - (q - r + x * (q - b))) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q + (q * q + (q * q + x * (q + y - b))) - (q - r + x * (y + (q - b)))) mod q = (q + (q * q + (q * q + x * (q - b))) - (q - r + x * (q - b))) mod q

goal (1 subgoal):
 1. (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
by (simp add: add.commute diff_mult_distrib2 distrib_left)
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q \<Longrightarrow> (x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
(x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
(x * e1 + (q - s1)) mod q = (x * y + x * q - x * b + q * q + q * q + q - x * y - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have "?rhs = (x*(q - b) + q*q + q*q + q - x*(q - b) - (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * q - x * b + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (x * (q - b) + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
by(metis diff_mult_distrib2)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (x * (q - b) + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (x * (q - b) + q * q + q * q + q - x * (q - b) - (q - r)) mod q
[PROOF STEP]
have "?rhs = (q*q + q*q + q - (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * (q - b) + q * q + q * q + q - x * (q - b) - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (x * (q - b) + q * q + q * q + q - x * (q - b) - (q - r)) mod q
r < q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q
[PROOF STEP]
have "?rhs = (q*q + q*q + q - q + r) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (q * q + q * q + q - q + r) mod q
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - (q - r)) mod q
r < q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (q * q + q * q + q - q + r) mod q
[PROOF STEP]
by(simp add: Nat.diff_add_assoc2 less_imp_le)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - q + r) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - q + r) mod q
[PROOF STEP]
have "?rhs = (q*q + q*q  + r) mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + q - q + r) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = (q * q + q * q + r) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + r) mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + r) mod q
[PROOF STEP]
have "?rhs = r mod q"
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = (q * q + q * q + r) mod q

goal (1 subgoal):
 1. (x * e1 + (q - s1)) mod q = r mod q
[PROOF STEP]
by (metis add.commute distrib_right mod_mult_self1)
[PROOF STATE]
proof (state)
this:
(x * e1 + (q - s1)) mod q = r mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * e1 + (q - s1)) mod q = r mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = r mod q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
using assms(6)
[PROOF STATE]
proof (prove)
using this:
(x * e1 + (q - s1)) mod q = r mod q
r < q

goal (1 subgoal):
 1. r = (x * e1 + (q - s1)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = (x * e1 + (q - s1)) mod q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma r_P2:
  assumes b: "b < q" and x: "x < q" and y: "y < q" and r: "r < q"
  shows
    "((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) =
              ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q,
                      (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
have  "(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
have 1:"r = (x*((y + (q - b)) mod q) + (q - ((x*((y + (q - b)) mod q) + (q - r)) mod q))) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
using assms secure_mult.r secure_mult_axioms
[PROOF STATE]
proof (prove)
using this:
b < q
x < q
y < q
r < q
\<lbrakk>secure_mult ?q; ?e1.0 = (?y + (?q - ?b)) mod ?q; ?s1.0 = (?x * ((?y + (?q - ?b)) mod ?q) + (?q - ?r)) mod ?q; ?b < ?q; ?x < ?q; ?y < ?q; ?r < ?q\<rbrakk> \<Longrightarrow> ?r = (?x * ?e1.0 + (?q - ?s1.0)) mod ?q
secure_mult q

goal (1 subgoal):
 1. r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
have "?rhs = (x*((y + (q - b)) mod q) + (q - ((x*((y + (q - b)) mod q) + (q - r)) mod q))) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
b < q
x < q
y < q
r < q
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
using assms 1
[PROOF STATE]
proof (prove)
using this:
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q
b < q
x < q
y < q
r < q
r = (x * ((y + (q - b)) mod q) + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q

goal (1 subgoal):
 1. (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r

goal (1 subgoal):
 1. ((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r

goal (1 subgoal):
 1. ((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q = r
b < q
x < q
y < q
r < q

goal (1 subgoal):
 1. ((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((x, a, r, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((x, a, (x * ((y + q - b) mod q) + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q, (y + q - b) mod q), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem P1_security:
  assumes "x < q" "y < q"
  shows "sim_non_det_def.perfect_sec_P1 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 x y
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 x y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 x y
[PROOF STEP]
have "(funct x y) \<bind> (\<lambda> (s1',s2'). (sim_non_det_def.Ideal1 x y s1')) = R1 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "R1 x y = do {
    a :: nat \<leftarrow> sample_uniform q;
    b :: nat \<leftarrow> sample_uniform q;
    r :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    let d1 = r;
    let c2 = b;
    let d2 = ((a*b + (q - r)) mod q);
    let e2 = (x + c1) mod q;
    let e1 = (y + (q - c2)) mod q;
    let s1 = (x*e1 + (q - d1)) mod q;
    let s2 = (e2 * c2 + (q - d2)) mod q;
    return_spmf ((x, c1, d1, e1), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2))))
[PROOF STEP]
by(simp add: R1_def TI_def Let_def)
[PROOF STATE]
proof (state)
this:
R1 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R1 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "... = do {
    a :: nat \<leftarrow> sample_uniform q;
    b :: nat \<leftarrow> sample_uniform q;
    r :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    let c2 = b;
    let e1 = (y + (q - b)) mod q;
    let s1 = (x*((y + (q - b)) mod q) + (q - r)) mod q;
    let d1 = (x*e1 + (q - s1)) mod q;
    return_spmf ((x, c1, d1, e1), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: Let_def assms s1_s2_P1  r_P2 cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - d1)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((x, c1, d1, e1), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "... = do {
    a :: nat \<leftarrow> sample_uniform q;
    b :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    let c2 = b;
    let e1 = (y + (q - b)) mod q;
    s1 \<leftarrow> map_spmf (\<lambda> r. (x*((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q);
    let d1 = (x*e1 + (q - s1)) mod q;
    return_spmf ((x, c1, d1, e1), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: bind_map_spmf Let_def o_def)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q; s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "... = do {
    a :: nat \<leftarrow> sample_uniform q;
    b :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    let c2 = b;
    let e1 = (y + (q - b)) mod q;
    s1 \<leftarrow> sample_uniform q;
    let d1 = (x*e1 + (q - s1)) mod q;
    return_spmf ((x, c1, d1, e1), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: samp_uni_minus_one_time_pad)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "... = do {
    a :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    e1 \<leftarrow> map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q);
    s1 \<leftarrow> sample_uniform q;
    let d1 = (x*e1 + (q - s1)) mod q;
    return_spmf ((x, c1, d1, e1), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: bind_map_spmf Let_def o_def)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. let c1 = a; c2 = b; e1 = (y + (q - b)) mod q in sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
have "... = do {
    a :: nat \<leftarrow> sample_uniform q;
    let c1 = a;
    e1 \<leftarrow> sample_uniform q;
    s1 \<leftarrow> sample_uniform q;
    let d1 = (x*e1 + (q - s1)) mod q;
    return_spmf ((x, c1, d1, e1), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in sample_uniform q \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: samp_uni_minus_one_time_pad)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in sample_uniform q \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R1 x y = sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in sample_uniform q \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R1 x y = sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))
sample_uniform q \<bind> (\<lambda>a. let c1 = a in map_spmf (\<lambda>b. (y + (q - b)) mod q) (sample_uniform q) \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>a. let c1 = a in sample_uniform q \<bind> (\<lambda>e1. sample_uniform q \<bind> (\<lambda>s1. let d1 = (x * e1 + (q - s1)) mod q in return_spmf ((x, c1, d1, e1), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y
[PROOF STEP]
by(simp add: funct_def sim_non_det_def.Ideal1_def Let_def R1_def TI_def Out1_def S1_def)
[PROOF STATE]
proof (state)
this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y

goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 x y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal1 x y s1') = R1 x y

goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 x y
[PROOF STEP]
by(simp add: sim_non_det_def.perfect_sec_P1_def)
[PROOF STATE]
proof (state)
this:
local.sim_non_det_def.perfect_sec_P1 x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem P1_secure:
  assumes "x < q n" "y < q n"
  shows "sim_non_det_def.perfect_sec_P1 n x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P1 n x y
[PROOF STEP]
by (metis P1_security assms)


[STATEMENT]
theorem P2_secure:
  assumes "x < q n" "y < q n"
  shows "sim_non_det_def.perfect_sec_P2 n x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 n x y
[PROOF STEP]
by (metis P2_security assms)


[STATEMENT]
lemma inorder_upto_split:
  assumes "inorder \<langle>l,k,r\<rangle> = [i..j]"
  shows "inorder l = [i..k-1]" "inorder r = [k+1..j]" "i \<le> k" "k \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inorder l = [i..k - 1] &&& inorder r = [k + 1..j]) &&& i \<le> k &&& k \<le> j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
have k: "k\<in>set[i..j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> set [i..j]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>l, k, r\<rangle> = [i..j]

goal (1 subgoal):
 1. k \<in> set [i..j]
[PROOF STEP]
by (metis set_inorder tree.set_intros(2))
[PROOF STATE]
proof (state)
this:
k \<in> set [i..j]

goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
have "[i..k-1] @ k # [k+1..j] = [i..j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i..k - 1] @ k # [k + 1..j] = [i..j]
[PROOF STEP]
using k upto_rec1 upto_split1
[PROOF STATE]
proof (prove)
using this:
k \<in> set [i..j]
?i \<le> ?j \<Longrightarrow> [?i..?j] = ?i # [?i + 1..?j]
\<lbrakk>?i \<le> ?j; ?j \<le> ?k\<rbrakk> \<Longrightarrow> [?i..?k] = [?i..?j - 1] @ [?j..?k]

goal (1 subgoal):
 1. [i..k - 1] @ k # [k + 1..j] = [i..j]
[PROOF STEP]
by (metis atLeastAtMost_iff set_upto)
[PROOF STATE]
proof (state)
this:
[i..k - 1] @ k # [k + 1..j] = [i..j]

goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[i..k - 1] @ k # [k + 1..j] = [i..j]

goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
have "\<dots> = inorder l @ k # inorder r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i..j] = inorder l @ k # inorder r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>l, k, r\<rangle> = [i..j]

goal (1 subgoal):
 1. [i..j] = inorder l @ k # inorder r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[i..j] = inorder l @ k # inorder r

goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[i..k - 1] @ k # [k + 1..j] = inorder l @ k # inorder r
[PROOF STEP]
have "inorder l = [i..k-1] \<and> inorder r = [k+1..j]" (is "?A \<and> ?B")
[PROOF STATE]
proof (prove)
using this:
[i..k - 1] @ k # [k + 1..j] = inorder l @ k # inorder r

goal (1 subgoal):
 1. inorder l = [i..k - 1] \<and> inorder r = [k + 1..j]
[PROOF STEP]
by(auto simp: append_Cons_eq_iff)
[PROOF STATE]
proof (state)
this:
inorder l = [i..k - 1] \<and> inorder r = [k + 1..j]

goal (4 subgoals):
 1. inorder l = [i..k - 1]
 2. inorder r = [k + 1..j]
 3. i \<le> k
 4. k \<le> j
[PROOF STEP]
thus ?A ?B
[PROOF STATE]
proof (prove)
using this:
inorder l = [i..k - 1] \<and> inorder r = [k + 1..j]

goal (1 subgoal):
 1. inorder l = [i..k - 1] &&& inorder r = [k + 1..j]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]

goal (2 subgoals):
 1. i \<le> k
 2. k \<le> j
[PROOF STEP]
show "i \<le> k" "k \<le> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> k &&& k \<le> j
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<in> set [i..j]

goal (1 subgoal):
 1. i \<le> k &&& k \<le> j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> k
k \<le> j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_nodes: "finite (nodes t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (nodes t)
[PROOF STEP]
by(induction t) auto


[STATEMENT]
lemma finite_leaves: "finite (leaves i t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (leaves i t)
[PROOF STEP]
by(induction i t rule: leaves.induct) auto


[STATEMENT]
lemma notin_nodes0: "(k, 0) \<notin> nodes t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (k, 0) \<notin> nodes t
[PROOF STEP]
by(induction t) auto


[STATEMENT]
lemma sum_incr2: "sum f (incr2 ` A) = sum (\<lambda>xy. f(fst xy,snd xy+1)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
have "sum f (incr2 ` A) = sum (f o incr2) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f (incr2 ` A) = sum (f \<circ> incr2) A
[PROOF STEP]
by(subst sum.reindex)(auto simp: inj_on_def)
[PROOF STATE]
proof (state)
this:
sum f (incr2 ` A) = sum (f \<circ> incr2) A

goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f (incr2 ` A) = sum (f \<circ> incr2) A

goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
have "f o incr2 = (\<lambda>xy. f(fst xy,snd xy+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> incr2 = (\<lambda>xy. f (fst xy, snd xy + 1))
[PROOF STEP]
by(auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
f \<circ> incr2 = (\<lambda>xy. f (fst xy, snd xy + 1))

goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum f (incr2 ` A) = (\<Sum>a\<in>A. f (fst a, snd a + 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum f (incr2 ` A) = (\<Sum>a\<in>A. f (fst a, snd a + 1))

goal (1 subgoal):
 1. sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f (incr2 ` A) = (\<Sum>xy\<in>A. f (fst xy, snd xy + 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_nodes: "fst ` nodes t = set_tree t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` nodes t = set_tree t
[PROOF STEP]
apply(induction t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fst ` nodes \<langle>\<rangle> = set_tree \<langle>\<rangle>
 2. \<And>t1 x2 t2. \<lbrakk>fst ` nodes t1 = set_tree t1; fst ` nodes t2 = set_tree t2\<rbrakk> \<Longrightarrow> fst ` nodes \<langle>t1, x2, t2\<rangle> = set_tree \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t1 x2 t2. \<lbrakk>fst ` nodes t1 = set_tree t1; fst ` nodes t2 = set_tree t2\<rbrakk> \<Longrightarrow> fst ` nodes \<langle>t1, x2, t2\<rangle> = set_tree \<langle>t1, x2, t2\<rangle>
[PROOF STEP]
apply (fastforce simp: image_def set_eq_iff ball_Un)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fst_leaves: "\<lbrakk> inorder t = [i..j]; i \<le> j+1\<rbrakk> \<Longrightarrow> fst ` leaves i t = {i..j+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inorder t = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t = {i..j + 1}
[PROOF STEP]
proof(induction t arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>inorder \<langle>\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>\<rangle> = {i..j + 1}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
inorder \<langle>\<rangle> = [i..j]
i \<le> j + 1

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>inorder \<langle>\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>\<rangle> = {i..j + 1}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inorder \<langle>\<rangle> = [i..j]
i \<le> j + 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>\<rangle> = [i..j]
i \<le> j + 1

goal (1 subgoal):
 1. fst ` leaves i \<langle>\<rangle> = {i..j + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst ` leaves i \<langle>\<rangle> = {i..j + 1}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
case (Node t1 k t2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>inorder t1 = [?i..?j]; ?i \<le> ?j + 1\<rbrakk> \<Longrightarrow> fst ` leaves ?i t1 = {?i..?j + 1}
\<lbrakk>inorder t2 = [?i..?j]; ?i \<le> ?j + 1\<rbrakk> \<Longrightarrow> fst ` leaves ?i t2 = {?i..?j + 1}
inorder \<langle>t1, k, t2\<rangle> = [i..j]
i \<le> j + 1

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
note inorder = inorder_upto_split[OF Node.prems(1)]
[PROOF STATE]
proof (state)
this:
inorder t1 = [i..k - 1]
inorder t2 = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t1 = {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i t2 = {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> fst ` leaves i \<langle>t1, x2, t2\<rangle> = {i..j + 1}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` leaves i \<langle>t1, k, t2\<rangle> = {i..j + 1}
[PROOF STEP]
using  Node.IH(1)[OF inorder(1)] Node.IH(2)[OF inorder(2)] inorder(3,4) Node.prems(2)
[PROOF STATE]
proof (prove)
using this:
i \<le> k - 1 + 1 \<Longrightarrow> fst ` leaves i t1 = {i..k - 1 + 1}
k + 1 \<le> j + 1 \<Longrightarrow> fst ` leaves (k + 1) t2 = {k + 1..j + 1}
i \<le> k
k \<le> j
i \<le> j + 1

goal (1 subgoal):
 1. fst ` leaves i \<langle>t1, k, t2\<rangle> = {i..j + 1}
[PROOF STEP]
by (fastforce simp: image_def set_eq_iff bex_Un)
[PROOF STATE]
proof (state)
this:
fst ` leaves i \<langle>t1, k, t2\<rangle> = {i..j + 1}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_leaves: "\<lbrakk> inorder t = [i..j];  i \<le> j+1 \<rbrakk> \<Longrightarrow>
  (\<Sum>x\<in>leaves i t. (f(fst x) :: nat)) = sum f {i..j+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inorder t = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
proof(induction t arbitrary: i j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i j. \<lbrakk>inorder \<langle>\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>\<rangle>. f (fst x)) = sum f {i..j + 1}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
inorder \<langle>\<rangle> = [i..j]
i \<le> j + 1

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>inorder \<langle>\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>\<rangle>. f (fst x)) = sum f {i..j + 1}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
hence "i = j+1"
[PROOF STATE]
proof (prove)
using this:
inorder \<langle>\<rangle> = [i..j]
i \<le> j + 1

goal (1 subgoal):
 1. i = j + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i = j + 1

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>inorder \<langle>\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>\<rangle>. f (fst x)) = sum f {i..j + 1}
 2. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i = j + 1

goal (1 subgoal):
 1. (\<Sum>x\<in>leaves i \<langle>\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>leaves i \<langle>\<rangle>. f (fst x)) = sum f {i..j + 1}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
case (Node l k r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>inorder l = [?i..?j]; ?i \<le> ?j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves ?i l. f (fst x)) = sum f {?i..?j + 1}
\<lbrakk>inorder r = [?i..?j]; ?i \<le> ?j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves ?i r. f (fst x)) = sum f {?i..?j + 1}
inorder \<langle>l, k, r\<rangle> = [i..j]
i \<le> j + 1

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
note inorder = inorder_upto_split[OF Node.prems(1)]
[PROOF STATE]
proof (state)
this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
let ?Ll = "leaves i l"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
let ?Lr = "leaves (k+1) r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
let ?L = "?Ll \<union> ?Lr"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
have "fst ` ?Ll \<inter> fst ` ?Lr = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}
[PROOF STEP]
using inorder
[PROOF STATE]
proof (prove)
using this:
inorder l = [i..k - 1]
inorder r = [k + 1..j]
i \<le> k
k \<le> j

goal (1 subgoal):
 1. fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}
[PROOF STEP]
by(simp add: fst_leaves del: set_inorder add: set_inorder[symmetric])
[PROOF STATE]
proof (state)
this:
fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
hence l0: "?Ll \<inter> ?Lr = {}"
[PROOF STATE]
proof (prove)
using this:
fst ` leaves i l \<inter> fst ` leaves (k + 1) r = {}

goal (1 subgoal):
 1. leaves i l \<inter> leaves (k + 1) r = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
leaves i l \<inter> leaves (k + 1) r = {}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
have "{i..j+1} = {i..k} \<union> {k+1..j+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i..j + 1} = {i..k} \<union> {k + 1..j + 1}
[PROOF STEP]
using inorder(3,4)
[PROOF STATE]
proof (prove)
using this:
i \<le> k
k \<le> j

goal (1 subgoal):
 1. {i..j + 1} = {i..k} \<union> {k + 1..j + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}

goal (1 subgoal):
 1. \<And>t1 x2 t2 i j. \<lbrakk>\<And>i j. \<lbrakk>inorder t1 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t1. f (fst x)) = sum f {i..j + 1}; \<And>i j. \<lbrakk>inorder t2 = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i t2. f (fst x)) = sum f {i..j + 1}; inorder \<langle>t1, x2, t2\<rangle> = [i..j]; i \<le> j + 1\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>leaves i \<langle>t1, x2, t2\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}

goal (1 subgoal):
 1. (\<Sum>x\<in>leaves i \<langle>l, k, r\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
using Node.IH(1)[OF inorder(1)] Node.IH(2)[OF inorder(2)] inorder(3,4) Node.prems(2)
[PROOF STATE]
proof (prove)
using this:
{i..j + 1} = {i..k} \<union> {k + 1..j + 1}
i \<le> k - 1 + 1 \<Longrightarrow> (\<Sum>x\<in>leaves i l. f (fst x)) = sum f {i..k - 1 + 1}
k + 1 \<le> j + 1 \<Longrightarrow> (\<Sum>x\<in>leaves (k + 1) r. f (fst x)) = sum f {k + 1..j + 1}
i \<le> k
k \<le> j
i \<le> j + 1

goal (1 subgoal):
 1. (\<Sum>x\<in>leaves i \<langle>l, k, r\<rangle>. f (fst x)) = sum f {i..j + 1}
[PROOF STEP]
by(simp add: sum_incr2 sum_Un_nat finite_leaves l0)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>leaves i \<langle>l, k, r\<rangle>. f (fst x)) = sum f {i..j + 1}

goal:
No subgoals!
[PROOF STEP]
qed