[STATEMENT]
lemma core_argument:
  assumes "distinct (p\<^sub>0 # ps)" "sorted_snd (p\<^sub>0 # ps)" "0 \<le> \<delta>" "set (p\<^sub>0 # ps) = ps\<^sub>L \<union> ps\<^sub>R"
  assumes "\<forall>p \<in> set (p\<^sub>0 # ps). l - \<delta> \<le> fst p \<and> fst p \<le> l + \<delta>"
  assumes "\<forall>p \<in> ps\<^sub>L. fst p \<le> l" "\<forall>p \<in> ps\<^sub>R. l \<le> fst p"
  assumes "sparse \<delta> ps\<^sub>L" "sparse \<delta> ps\<^sub>R"
  assumes "p\<^sub>1 \<in> set ps" "dist p\<^sub>0 p\<^sub>1 < \<delta>"
  shows "p\<^sub>1 \<in> set (take 7 ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define PS where "PS = p\<^sub>0 # ps"
[PROOF STATE]
proof (state)
this:
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define R where "R = cbox (l - \<delta>, snd p\<^sub>0) (l + \<delta>, snd p\<^sub>0 + \<delta>)"
[PROOF STATE]
proof (state)
this:
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define RPS where "RPS = { p \<in> set PS. p \<in> R }"
[PROOF STATE]
proof (state)
this:
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define LSQ where "LSQ = cbox (l - \<delta>, snd p\<^sub>0) (l, snd p\<^sub>0 + \<delta>)"
[PROOF STATE]
proof (state)
this:
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define LSQPS where "LSQPS = { p \<in> ps\<^sub>L. p \<in> LSQ }"
[PROOF STATE]
proof (state)
this:
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define RSQ where "RSQ = cbox (l, snd p\<^sub>0) (l + \<delta>, snd p\<^sub>0 + \<delta>)"
[PROOF STATE]
proof (state)
this:
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
define RSQPS where "RSQPS = { p \<in> ps\<^sub>R. p \<in> RSQ }"
[PROOF STATE]
proof (state)
this:
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
note defs = PS_def R_def RPS_def LSQ_def LSQPS_def RSQ_def RSQPS_def
[PROOF STATE]
proof (state)
this:
PS = p\<^sub>0 # ps
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "R = LSQ \<union> RSQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = LSQ \<union> RSQ
[PROOF STEP]
using defs cbox_right_un
[PROOF STATE]
proof (prove)
using this:
PS = p\<^sub>0 # ps
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}
\<lbrakk>?x\<^sub>0 \<le> ?x\<^sub>1; ?x\<^sub>1 \<le> ?x\<^sub>2\<rbrakk> \<Longrightarrow> cbox (?x\<^sub>0, ?y\<^sub>0) (?x\<^sub>1, ?y\<^sub>1) \<union> cbox (?x\<^sub>1, ?y\<^sub>0) (?x\<^sub>2, ?y\<^sub>1) = cbox (?x\<^sub>0, ?y\<^sub>0) (?x\<^sub>2, ?y\<^sub>1)

goal (1 subgoal):
 1. R = LSQ \<union> RSQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R = LSQ \<union> RSQ

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R = LSQ \<union> RSQ

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "\<forall>p \<in> ps\<^sub>L. p \<in> RSQ \<longrightarrow> p \<in> LSQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ
[PROOF STEP]
using RSQ_def LSQ_def assms(6)
[PROOF STATE]
proof (prove)
using this:
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
\<forall>p\<in>ps\<^sub>L. fst p \<le> l

goal (1 subgoal):
 1. \<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "\<forall>p \<in> ps\<^sub>R. p \<in> LSQ \<longrightarrow> p \<in> RSQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ
[PROOF STEP]
using RSQ_def LSQ_def assms(7)
[PROOF STATE]
proof (prove)
using this:
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
\<forall>p\<in>ps\<^sub>R. l \<le> fst p

goal (1 subgoal):
 1. \<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R = LSQ \<union> RSQ
\<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ
\<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ
[PROOF STEP]
have "RPS = LSQPS \<union> RSQPS"
[PROOF STATE]
proof (prove)
using this:
R = LSQ \<union> RSQ
\<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ
\<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ

goal (1 subgoal):
 1. RPS = LSQPS \<union> RSQPS
[PROOF STEP]
using LSQPS_def RSQPS_def PS_def RPS_def assms(4)
[PROOF STATE]
proof (prove)
using this:
R = LSQ \<union> RSQ
\<forall>x\<in>ps\<^sub>L. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ
\<forall>x\<in>ps\<^sub>R. (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ \<longrightarrow> (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}
PS = p\<^sub>0 # ps
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
set (p\<^sub>0 # ps) = ps\<^sub>L \<union> ps\<^sub>R

goal (1 subgoal):
 1. RPS = LSQPS \<union> RSQPS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
RPS = LSQPS \<union> RSQPS

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "sparse \<delta> LSQPS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse \<delta> LSQPS
[PROOF STEP]
using assms(8) LSQPS_def sparse_def
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> ps\<^sub>L
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}
sparse ?\<delta> ?ps = (\<forall>p\<^sub>0\<in>?ps. \<forall>p\<^sub>1\<in>?ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> ?\<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)))

goal (1 subgoal):
 1. sparse \<delta> LSQPS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse \<delta> LSQPS

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
hence CLSQPS: "card LSQPS \<le> 4"
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> LSQPS

goal (1 subgoal):
 1. card LSQPS \<le> 4
[PROOF STEP]
using max_points_square[of LSQPS "l - \<delta>" "snd p\<^sub>0" \<delta>] assms(3) LSQ_def LSQPS_def
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> LSQPS
\<lbrakk>\<forall>p\<in>LSQPS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> cbox (real_of_int l - \<delta>, real_of_int (snd p\<^sub>0)) (real_of_int l - \<delta> + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>); sparse \<delta> LSQPS; 0 \<le> \<delta>\<rbrakk> \<Longrightarrow> card LSQPS \<le> 4
0 \<le> \<delta>
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}

goal (1 subgoal):
 1. card LSQPS \<le> 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card LSQPS \<le> 4

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "sparse \<delta> RSQPS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse \<delta> RSQPS
[PROOF STEP]
using assms(9) RSQPS_def sparse_def
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> ps\<^sub>R
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}
sparse ?\<delta> ?ps = (\<forall>p\<^sub>0\<in>?ps. \<forall>p\<^sub>1\<in>?ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> ?\<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)))

goal (1 subgoal):
 1. sparse \<delta> RSQPS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse \<delta> RSQPS

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
hence CRSQPS: "card RSQPS \<le> 4"
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> RSQPS

goal (1 subgoal):
 1. card RSQPS \<le> 4
[PROOF STEP]
using max_points_square[of RSQPS l "snd p\<^sub>0" \<delta>] assms(3) RSQ_def RSQPS_def
[PROOF STATE]
proof (prove)
using this:
sparse \<delta> RSQPS
\<lbrakk>\<forall>p\<in>RSQPS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> cbox (real_of_int l, real_of_int (snd p\<^sub>0)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>); sparse \<delta> RSQPS; 0 \<le> \<delta>\<rbrakk> \<Longrightarrow> card RSQPS \<le> 4
0 \<le> \<delta>
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}

goal (1 subgoal):
 1. card RSQPS \<le> 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card RSQPS \<le> 4

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have CRPS: "card RPS \<le> 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card RPS \<le> 8
[PROOF STEP]
using CLSQPS CRSQPS card_Un_le[of LSQPS RSQPS] \<open>RPS = LSQPS \<union> RSQPS\<close>
[PROOF STATE]
proof (prove)
using this:
card LSQPS \<le> 4
card RSQPS \<le> 4
card (LSQPS \<union> RSQPS) \<le> card LSQPS + card RSQPS
RPS = LSQPS \<union> RSQPS

goal (1 subgoal):
 1. card RPS \<le> 8
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card RPS \<le> 8

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "RPS \<subseteq> set (take 8 PS)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RPS \<subseteq> set (take 8 PS)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (RPS \<subseteq> set (take 8 PS))"
[PROOF STATE]
proof (state)
this:
\<not> RPS \<subseteq> set (take 8 PS)

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> RPS \<subseteq> set (take 8 PS)
[PROOF STEP]
obtain p where *: "p \<in> set PS" "p \<in> RPS" "p \<notin> set (take 8 PS)" "p \<in> R"
[PROOF STATE]
proof (prove)
using this:
\<not> RPS \<subseteq> set (take 8 PS)

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> set PS; p \<in> RPS; p \<notin> set (take 8 PS); (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using RPS_def
[PROOF STATE]
proof (prove)
using this:
\<not> RPS \<subseteq> set (take 8 PS)
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> set PS; p \<in> RPS; p \<notin> set (take 8 PS); (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> set PS
p \<in> RPS
p \<notin> set (take 8 PS)
(case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "\<forall>p\<^sub>0 \<in> set (take 8 PS). \<forall>p\<^sub>1 \<in> set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set (take 8 PS). \<forall>p\<^sub>1\<in>set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1
[PROOF STEP]
using sorted_wrt_take_drop[of "\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1" PS 8] assms(2) sorted_snd_def PS_def
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) PS \<Longrightarrow> \<forall>x\<in>set (take 8 PS). \<forall>y\<in>set (drop 8 PS). snd x \<le> snd y
sorted_snd (p\<^sub>0 # ps)
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set (take 8 PS). \<forall>p\<^sub>1\<in>set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>0\<in>set (take 8 PS). \<forall>p\<^sub>1\<in>set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence "\<forall>p' \<in> set (take 8 PS). snd p' \<le> snd p"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<^sub>0\<in>set (take 8 PS). \<forall>p\<^sub>1\<in>set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1

goal (1 subgoal):
 1. \<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p
[PROOF STEP]
using append_take_drop_id set_append Un_iff *(1,3)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<^sub>0\<in>set (take 8 PS). \<forall>p\<^sub>1\<in>set (drop 8 PS). snd p\<^sub>0 \<le> snd p\<^sub>1
take ?n ?xs @ drop ?n ?xs = ?xs
set (?xs @ ?ys) = set ?xs \<union> set ?ys
(?c \<in> ?A \<union> ?B) = (?c \<in> ?A \<or> ?c \<in> ?B)
p \<in> set PS
p \<notin> set (take 8 PS)

goal (1 subgoal):
 1. \<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "snd p \<le> snd p\<^sub>0 + \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
[PROOF STEP]
using \<open>p \<in> R\<close> R_def mem_cbox_2D
[PROOF STATE]
proof (prove)
using this:
(case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
(?x\<^sub>0 \<le> ?x \<and> ?x \<le> ?x\<^sub>1 \<and> ?y\<^sub>0 \<le> ?y \<and> ?y \<le> ?y\<^sub>1) = ((?x, ?y) \<in> cbox (?x\<^sub>0, ?y\<^sub>0) (?x\<^sub>1, ?y\<^sub>1))

goal (1 subgoal):
 1. real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
[PROOF STEP]
by (metis (mono_tags, lifting) prod.case_eq_if)
[PROOF STATE]
proof (state)
this:
real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p
real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
[PROOF STEP]
have "\<forall>p \<in> set (take 8 PS). snd p \<le> snd p\<^sub>0 + \<delta>"
[PROOF STATE]
proof (prove)
using this:
\<forall>p'\<in>set (take 8 PS). snd p' \<le> snd p
real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. \<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "\<forall>p \<in> set (take 8 PS). snd p\<^sub>0 \<le> snd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p
[PROOF STEP]
using sorted_wrt_hd_less_take[of "\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1" p\<^sub>0 ps 8] assms(2) sorted_snd_def PS_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) (p\<^sub>0 # ps); \<And>x. snd x \<le> snd x\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (take 8 (p\<^sub>0 # ps)). snd p\<^sub>0 \<le> snd y
sorted_snd (p\<^sub>0 # ps)
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. \<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "\<forall>p \<in> set (take 8 PS). l - \<delta> \<le> fst p \<and> fst p \<le> l + \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
[PROOF STEP]
using assms(5) PS_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (p\<^sub>0 # ps). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. \<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
[PROOF STEP]
by (meson in_set_takeD)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
\<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p
\<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
[PROOF STEP]
have "\<forall>p \<in> set (take 8 PS). p \<in> R"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
\<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p
\<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>

goal (1 subgoal):
 1. \<forall>x\<in>set (take 8 PS). (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
[PROOF STEP]
using R_def mem_cbox_2D
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (take 8 PS). real_of_int (snd p) \<le> real_of_int (snd p\<^sub>0) + \<delta>
\<forall>p\<in>set (take 8 PS). snd p\<^sub>0 \<le> snd p
\<forall>p\<in>set (take 8 PS). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
(?x\<^sub>0 \<le> ?x \<and> ?x \<le> ?x\<^sub>1 \<and> ?y\<^sub>0 \<le> ?y \<and> ?y \<le> ?y\<^sub>1) = ((?x, ?y) \<in> cbox (?x\<^sub>0, ?y\<^sub>0) (?x\<^sub>1, ?y\<^sub>1))

goal (1 subgoal):
 1. \<forall>x\<in>set (take 8 PS). (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (take 8 PS). (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence "set (take 8 PS) \<subseteq> RPS"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (take 8 PS). (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. set (take 8 PS) \<subseteq> RPS
[PROOF STEP]
using RPS_def set_take_subset
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (take 8 PS). (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
set (take ?n ?xs) \<subseteq> set ?xs

goal (1 subgoal):
 1. set (take 8 PS) \<subseteq> RPS
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
set (take 8 PS) \<subseteq> RPS

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence NINE: "{ p } \<union> set (take 8 PS) \<subseteq> RPS"
[PROOF STATE]
proof (prove)
using this:
set (take 8 PS) \<subseteq> RPS

goal (1 subgoal):
 1. {p} \<union> set (take 8 PS) \<subseteq> RPS
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
set (take 8 PS) \<subseteq> RPS
p \<in> set PS
p \<in> RPS
p \<notin> set (take 8 PS)
(case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. {p} \<union> set (take 8 PS) \<subseteq> RPS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{p} \<union> set (take 8 PS) \<subseteq> RPS

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "8 \<le> length PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 8 \<le> length PS
[PROOF STEP]
using *(1,3) nat_le_linear
[PROOF STATE]
proof (prove)
using this:
p \<in> set PS
p \<notin> set (take 8 PS)
?m \<le> ?n \<or> ?n \<le> ?m

goal (1 subgoal):
 1. 8 \<le> length PS
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
8 \<le> length PS

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence "length (take 8 PS) = 8"
[PROOF STATE]
proof (prove)
using this:
8 \<le> length PS

goal (1 subgoal):
 1. length (take 8 PS) = 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (take 8 PS) = 8

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "finite { p }" "finite (set (take 8 PS))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {p} &&& finite (set (take 8 PS))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
finite {p}
finite (set (take 8 PS))

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence "card ({ p } \<union> set (take 8 PS)) = card ({ p }) + card (set (take 8 PS))"
[PROOF STATE]
proof (prove)
using this:
finite {p}
finite (set (take 8 PS))

goal (1 subgoal):
 1. card ({p} \<union> set (take 8 PS)) = card {p} + card (set (take 8 PS))
[PROOF STEP]
using *(3) card_Un_disjoint
[PROOF STATE]
proof (prove)
using this:
finite {p}
finite (set (take 8 PS))
p \<notin> set (take 8 PS)
\<lbrakk>finite ?A; finite ?B; ?A \<inter> ?B = {}\<rbrakk> \<Longrightarrow> card (?A \<union> ?B) = card ?A + card ?B

goal (1 subgoal):
 1. card ({p} \<union> set (take 8 PS)) = card {p} + card (set (take 8 PS))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card ({p} \<union> set (take 8 PS)) = card {p} + card (set (take 8 PS))

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
hence "card ({ p } \<union> set (take 8 PS)) = 9"
[PROOF STATE]
proof (prove)
using this:
card ({p} \<union> set (take 8 PS)) = card {p} + card (set (take 8 PS))

goal (1 subgoal):
 1. card ({p} \<union> set (take 8 PS)) = 9
[PROOF STEP]
using assms(1) \<open>length (take 8 PS) = 8\<close> distinct_card[of "take 8 PS"] distinct_take[of PS] PS_def
[PROOF STATE]
proof (prove)
using this:
card ({p} \<union> set (take 8 PS)) = card {p} + card (set (take 8 PS))
distinct (p\<^sub>0 # ps)
length (take 8 PS) = 8
distinct (take 8 PS) \<Longrightarrow> card (set (take 8 PS)) = length (take 8 PS)
distinct PS \<Longrightarrow> distinct (take ?i PS)
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. card ({p} \<union> set (take 8 PS)) = 9
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card ({p} \<union> set (take 8 PS)) = 9

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({p} \<union> set (take 8 PS)) = 9

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
have "finite RPS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite RPS
[PROOF STEP]
using RPS_def
[PROOF STATE]
proof (prove)
using this:
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}

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

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card ({p} \<union> set (take 8 PS)) = 9
finite RPS
[PROOF STEP]
have "9 \<le> card RPS"
[PROOF STATE]
proof (prove)
using this:
card ({p} \<union> set (take 8 PS)) = 9
finite RPS

goal (1 subgoal):
 1. 9 \<le> card RPS
[PROOF STEP]
using NINE card_mono
[PROOF STATE]
proof (prove)
using this:
card ({p} \<union> set (take 8 PS)) = 9
finite RPS
{p} \<union> set (take 8 PS) \<subseteq> RPS
\<lbrakk>finite ?B; ?A \<subseteq> ?B\<rbrakk> \<Longrightarrow> card ?A \<le> card ?B

goal (1 subgoal):
 1. 9 \<le> card RPS
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
9 \<le> card RPS

goal (1 subgoal):
 1. \<not> RPS \<subseteq> set (take 8 PS) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
9 \<le> card RPS

goal (1 subgoal):
 1. False
[PROOF STEP]
using CRPS
[PROOF STATE]
proof (prove)
using this:
9 \<le> card RPS
card RPS \<le> 8

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
RPS \<subseteq> set (take 8 PS)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "dist (snd p\<^sub>0) (snd p\<^sub>1) < \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (real_of_int (snd p\<^sub>0)) (real_of_int (snd p\<^sub>1)) < \<delta>
[PROOF STEP]
using assms(11) dist_snd_le le_less_trans
[PROOF STATE]
proof (prove)
using this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
dist (snd ?x) (snd ?y) \<le> dist ?x ?y
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z

goal (1 subgoal):
 1. dist (real_of_int (snd p\<^sub>0)) (real_of_int (snd p\<^sub>1)) < \<delta>
[PROOF STEP]
by (metis (no_types, lifting) prod.case_eq_if snd_conv)
[PROOF STATE]
proof (state)
this:
dist (real_of_int (snd p\<^sub>0)) (real_of_int (snd p\<^sub>1)) < \<delta>

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
hence "snd p\<^sub>1 \<le> snd p\<^sub>0 + \<delta>"
[PROOF STATE]
proof (prove)
using this:
dist (real_of_int (snd p\<^sub>0)) (real_of_int (snd p\<^sub>1)) < \<delta>

goal (1 subgoal):
 1. real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>
[PROOF STEP]
by (simp add: dist_real_def)
[PROOF STATE]
proof (state)
this:
real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "l - \<delta> \<le> fst p\<^sub>1" "fst p\<^sub>1 \<le> l + \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1) &&& real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>
[PROOF STEP]
using assms(5,10)
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (p\<^sub>0 # ps). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
p\<^sub>1 \<in> set ps

goal (1 subgoal):
 1. real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1) &&& real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1)
real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1)
real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "snd p\<^sub>0 \<le> snd p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd p\<^sub>0 \<le> snd p\<^sub>1
[PROOF STEP]
using sorted_snd_def assms(2,10)
[PROOF STATE]
proof (prove)
using this:
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps
sorted_snd (p\<^sub>0 # ps)
p\<^sub>1 \<in> set ps

goal (1 subgoal):
 1. snd p\<^sub>0 \<le> snd p\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd p\<^sub>0 \<le> snd p\<^sub>1

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>
real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1)
real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>
snd p\<^sub>0 \<le> snd p\<^sub>1
[PROOF STEP]
have "p\<^sub>1 \<in> R"
[PROOF STATE]
proof (prove)
using this:
real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>
real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1)
real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>
snd p\<^sub>0 \<le> snd p\<^sub>1

goal (1 subgoal):
 1. (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
[PROOF STEP]
using mem_cbox_2D[of "l - \<delta>" "fst p\<^sub>1" "l + \<delta>" "snd p\<^sub>0" "snd p\<^sub>1" "snd p\<^sub>0 + \<delta>"] defs
[PROOF STATE]
proof (prove)
using this:
real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>
real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1)
real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta>
snd p\<^sub>0 \<le> snd p\<^sub>1
(real_of_int l - \<delta> \<le> real_of_int (fst p\<^sub>1) \<and> real_of_int (fst p\<^sub>1) \<le> real_of_int l + \<delta> \<and> real_of_int (snd p\<^sub>0) \<le> real_of_int (snd p\<^sub>1) \<and> real_of_int (snd p\<^sub>1) \<le> real_of_int (snd p\<^sub>0) + \<delta>) = ((real_of_int (fst p\<^sub>1), real_of_int (snd p\<^sub>1)) \<in> cbox (real_of_int l - \<delta>, real_of_int (snd p\<^sub>0)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>))
PS = p\<^sub>0 # ps
R = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
LSQ = cbox (case (real_of_int l - \<delta>, snd p\<^sub>0) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, real_of_int (snd p\<^sub>0) + \<delta>) of (x, y) \<Rightarrow> (real_of_int x, y))
LSQPS = {p \<in> ps\<^sub>L. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> LSQ}
RSQ = cbox (case (l, snd p\<^sub>0) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l + \<delta>, real_of_int (snd p\<^sub>0) + \<delta>)
RSQPS = {p \<in> ps\<^sub>R. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> RSQ}

goal (1 subgoal):
 1. (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
[PROOF STEP]
by (simp add: \<open>l - \<delta> \<le> fst p\<^sub>1\<close> \<open>snd p\<^sub>0 \<le> snd p\<^sub>1\<close> prod.case_eq_if)
[PROOF STATE]
proof (state)
this:
(case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
have "p\<^sub>1 \<in> set PS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>1 \<in> set PS
[PROOF STEP]
using PS_def assms(10)
[PROOF STATE]
proof (prove)
using this:
PS = p\<^sub>0 # ps
p\<^sub>1 \<in> set ps

goal (1 subgoal):
 1. p\<^sub>1 \<in> set PS
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p\<^sub>1 \<in> set PS

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
p\<^sub>1 \<in> set PS
[PROOF STEP]
have "p\<^sub>1 \<in> set (take 8 PS)"
[PROOF STATE]
proof (prove)
using this:
(case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
p\<^sub>1 \<in> set PS

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 8 PS)
[PROOF STEP]
using RPS_def \<open>RPS \<subseteq> set (take 8 PS)\<close>
[PROOF STATE]
proof (prove)
using this:
(case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R
p\<^sub>1 \<in> set PS
RPS = {p \<in> set PS. (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<in> R}
RPS \<subseteq> set (take 8 PS)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 8 PS)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p\<^sub>1 \<in> set (take 8 PS)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 \<in> set (take 8 PS)

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
using assms(1,10) PS_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 \<in> set (take 8 PS)
distinct (p\<^sub>0 # ps)
p\<^sub>1 \<in> set ps
PS = p\<^sub>0 # ps

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (take 7 ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p\<^sub>1 \<in> set (take 7 ps)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_closest_bf_dist_take_7:
  assumes "\<exists>p\<^sub>1 \<in> set ps. dist p\<^sub>0 p\<^sub>1 < \<delta>"
  assumes "distinct (p\<^sub>0 # ps)" "sorted_snd (p\<^sub>0 # ps)" "0 < length ps" "0 \<le> \<delta>" "set (p\<^sub>0 # ps) = ps\<^sub>L \<union> ps\<^sub>R"
  assumes "\<forall>p \<in> set (p\<^sub>0 # ps). l - \<delta> \<le> fst p \<and> fst p \<le> l + \<delta>"
  assumes "\<forall>p \<in> ps\<^sub>L. fst p \<le> l" "\<forall>p \<in> ps\<^sub>R. l \<le> fst p"
  assumes "sparse \<delta> ps\<^sub>L" "sparse \<delta> ps\<^sub>R"
  shows "\<forall>p\<^sub>1 \<in> set ps. dist p\<^sub>0 (find_closest_bf p\<^sub>0 (take 7 ps)) \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
have "dist p\<^sub>0 (find_closest_bf p\<^sub>0 ps) < \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
[PROOF STEP]
using assms(1) dual_order.strict_trans2 find_closest_bf_dist
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
\<lbrakk>?b < ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c < ?a
\<forall>q\<in>set ?ps. dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf ?p ?ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case q of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
have "find_closest_bf p\<^sub>0 ps \<in> set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_closest_bf p\<^sub>0 ps \<in> set ps
[PROOF STEP]
using assms(4) find_closest_bf_set
[PROOF STATE]
proof (prove)
using this:
0 < length ps
0 < length ?ps \<Longrightarrow> find_closest_bf ?p ?ps \<in> set ?ps

goal (1 subgoal):
 1. find_closest_bf p\<^sub>0 ps \<in> set ps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
find_closest_bf p\<^sub>0 ps \<in> set ps

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
find_closest_bf p\<^sub>0 ps \<in> set ps
[PROOF STEP]
have "find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)"
[PROOF STATE]
proof (prove)
using this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
find_closest_bf p\<^sub>0 ps \<in> set ps

goal (1 subgoal):
 1. find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
[PROOF STEP]
using core_argument[of p\<^sub>0 ps \<delta> ps\<^sub>L ps\<^sub>R l "find_closest_bf p\<^sub>0 ps"] assms
[PROOF STATE]
proof (prove)
using this:
dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
find_closest_bf p\<^sub>0 ps \<in> set ps
\<lbrakk>distinct (p\<^sub>0 # ps); sorted_snd (p\<^sub>0 # ps); 0 \<le> \<delta>; set (p\<^sub>0 # ps) = ps\<^sub>L \<union> ps\<^sub>R; \<forall>p\<in>set (p\<^sub>0 # ps). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>; \<forall>p\<in>ps\<^sub>L. fst p \<le> l; \<forall>p\<in>ps\<^sub>R. l \<le> fst p; sparse \<delta> ps\<^sub>L; sparse \<delta> ps\<^sub>R; find_closest_bf p\<^sub>0 ps \<in> set ps; dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>\<rbrakk> \<Longrightarrow> find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
\<exists>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
distinct (p\<^sub>0 # ps)
sorted_snd (p\<^sub>0 # ps)
0 < length ps
0 \<le> \<delta>
set (p\<^sub>0 # ps) = ps\<^sub>L \<union> ps\<^sub>R
\<forall>p\<in>set (p\<^sub>0 # ps). real_of_int l - \<delta> \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + \<delta>
\<forall>p\<in>ps\<^sub>L. fst p \<le> l
\<forall>p\<in>ps\<^sub>R. l \<le> fst p
sparse \<delta> ps\<^sub>L
sparse \<delta> ps\<^sub>R

goal (1 subgoal):
 1. find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
have "\<forall>p\<^sub>1 \<in> set (take 7 ps). dist p\<^sub>0 (find_closest_bf p\<^sub>0 (take 7 ps)) \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using find_closest_bf_dist
[PROOF STATE]
proof (prove)
using this:
\<forall>q\<in>set ?ps. dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf ?p ?ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case q of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
\<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
have "\<forall>p\<^sub>1 \<in> set ps. dist p\<^sub>0 (find_closest_bf p\<^sub>0 (take 7 ps)) \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
\<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using find_closest_bf_dist order.trans
[PROOF STATE]
proof (prove)
using this:
find_closest_bf p\<^sub>0 ps \<in> set (take 7 ps)
\<forall>p\<^sub>1\<in>set (take 7 ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<forall>q\<in>set ?ps. dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf ?p ?ps of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case q of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>1\<in>set ps. dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case find_closest_bf p\<^sub>0 (take 7 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_closest_pair_eq_val_find_closest_pair_tm:
  "val (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Monad.val (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps
[PROOF STEP]
by (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: c\<^sub>0 c\<^sub>1 rule: find_closest_pair.induct)
     (auto simp: Let_def find_closest_bf_eq_val_find_closest_bf_tm take_eq_val_take_tm)


[STATEMENT]
lemma find_closest_pair_set:
  assumes "(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps"
  shows "(C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps) \<or> (C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps

goal (1 subgoal):
 1. C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
proof (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 rule: find_closest_pair.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> C\<^sub>0 \<in> set [] \<and> C\<^sub>1 \<in> set [] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<Longrightarrow> C\<^sub>0 \<in> set [uu_] \<and> C\<^sub>1 \<in> set [uu_] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = p\<^sub>0 \<and> C\<^sub>1 = x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # v # va) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
case (3 c\<^sub>0 c\<^sub>1 p\<^sub>0 p\<^sub>2 ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<in> set (p\<^sub>2 # ps) \<and> ?C\<^sub>1 \<in> set (p\<^sub>2 # ps) \<or> ?C\<^sub>0 = c\<^sub>0 \<and> ?C\<^sub>1 = c\<^sub>1
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<in> set (p\<^sub>2 # ps) \<and> ?C\<^sub>1 \<in> set (p\<^sub>2 # ps) \<or> ?C\<^sub>0 = p\<^sub>0 \<and> ?C\<^sub>1 = ?x
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> C\<^sub>0 \<in> set [] \<and> C\<^sub>1 \<in> set [] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<Longrightarrow> C\<^sub>0 \<in> set [uu_] \<and> C\<^sub>1 \<in> set [uu_] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = p\<^sub>0 \<and> C\<^sub>1 = x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # v # va) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> C\<^sub>0 \<in> set [] \<and> C\<^sub>1 \<in> set [] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<Longrightarrow> C\<^sub>0 \<in> set [uu_] \<and> C\<^sub>1 \<in> set [uu_] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = p\<^sub>0 \<and> C\<^sub>1 = x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # v # va) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
hence A: "p\<^sub>1 \<in> set (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (p\<^sub>2 # ps)
[PROOF STEP]
using find_closest_bf_set[of "take 7 (p\<^sub>2 # ps)"] in_set_takeD
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 < length (take 7 (p\<^sub>2 # ps)) \<Longrightarrow> find_closest_bf ?p (take 7 (p\<^sub>2 # ps)) \<in> set (take 7 (p\<^sub>2 # ps))
?x \<in> set (take ?n ?xs) \<Longrightarrow> ?x \<in> set ?xs

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (p\<^sub>2 # ps)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p\<^sub>1 \<in> set (p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> C\<^sub>0 \<in> set [] \<and> C\<^sub>1 \<in> set [] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<Longrightarrow> C\<^sub>0 \<in> set [uu_] \<and> C\<^sub>1 \<in> set [uu_] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (v # va) \<and> C\<^sub>1 \<in> set (v # va) \<or> C\<^sub>0 = p\<^sub>0 \<and> C\<^sub>1 = x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # v # va) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # v # va) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
proof (cases "dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
hence "(C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps)) \<or> (C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1
[PROOF STEP]
using "3.hyps"(1) True p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<in> set (p\<^sub>2 # ps) \<and> ?C\<^sub>1 \<in> set (p\<^sub>2 # ps) \<or> ?C\<^sub>0 = c\<^sub>0 \<and> ?C\<^sub>1 = c\<^sub>1
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
have "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using defs True "3.prems"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = c\<^sub>0 \<and> C\<^sub>1' = c\<^sub>1
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
hence "(C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps)) \<or> (C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1)"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1
[PROOF STEP]
using "3.hyps"(2) p\<^sub>1_def False
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<in> set (p\<^sub>2 # ps) \<and> ?C\<^sub>1 \<in> set (p\<^sub>2 # ps) \<or> ?C\<^sub>0 = p\<^sub>0 \<and> ?C\<^sub>1 = ?x
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
have "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using defs False "3.prems"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0' \<in> set (p\<^sub>2 # ps) \<and> C\<^sub>1' \<in> set (p\<^sub>2 # ps) \<or> C\<^sub>0' = p\<^sub>0 \<and> C\<^sub>1' = p\<^sub>1
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
p\<^sub>1 \<in> set (p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<and> C\<^sub>1 \<in> set (p\<^sub>0 # p\<^sub>2 # ps) \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> C\<^sub>0 \<in> set [] \<and> C\<^sub>1 \<in> set [] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<Longrightarrow> C\<^sub>0 \<in> set [uu_] \<and> C\<^sub>1 \<in> set [uu_] \<or> C\<^sub>0 = c\<^sub>0 \<and> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
qed auto