[STATEMENT]
lemma find_closest_pair_dist:
  assumes "sorted_snd ps" "distinct ps" "set ps = ps\<^sub>L \<union> ps\<^sub>R" "0 \<le> \<delta>"
  assumes "\<forall>p \<in> set 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" "dist c\<^sub>0 c\<^sub>1 \<le> \<delta>"
  assumes "(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps"
  shows "sparse (dist C\<^sub>0 C\<^sub>1) (set ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (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))) (set ps)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted_snd ps
distinct ps
set ps = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set 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
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps

goal (1 subgoal):
 1. sparse (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))) (set ps)
[PROOF STEP]
proof (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R 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 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd []; distinct []; set [] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set []. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> sparse (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))) (set [])
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd [uu_]; distinct [uu_]; set [uu_] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set [uu_]. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> sparse (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))) (set [uu_])
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
case (1 c\<^sub>0 c\<^sub>1)
[PROOF STATE]
proof (state)
this:
sorted_snd []
distinct []
set [] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set []. 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
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd []; distinct []; set [] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set []. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> sparse (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))) (set [])
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd [uu_]; distinct [uu_]; set [uu_] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set [uu_]. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> sparse (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))) (set [uu_])
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted_snd []
distinct []
set [] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set []. 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
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []

goal (1 subgoal):
 1. sparse (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))) (set [])
[PROOF STEP]
unfolding sparse_def
[PROOF STATE]
proof (prove)
using this:
sorted_snd []
distinct []
set [] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set []. 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
\<forall>p\<^sub>0\<in>ps\<^sub>L. \<forall>p\<^sub>1\<in>ps\<^sub>L. 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))
\<forall>p\<^sub>0\<in>ps\<^sub>R. \<forall>p\<^sub>1\<in>ps\<^sub>R. 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))
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []

goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set []. \<forall>p\<^sub>1\<in>set []. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> 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))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse (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))) (set [])

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd [uu_]; distinct [uu_]; set [uu_] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set [uu_]. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> sparse (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))) (set [uu_])
 2. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd [uu_]; distinct [uu_]; set [uu_] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set [uu_]. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> sparse (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))) (set [uu_])
 2. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
case (2 c\<^sub>0 c\<^sub>1 uu)
[PROOF STATE]
proof (state)
this:
sorted_snd [uu]
distinct [uu]
set [uu] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set [uu]. 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
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu]

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>sorted_snd [uu_]; distinct [uu_]; set [uu_] = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set [uu_]. 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> sparse (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))) (set [uu_])
 2. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted_snd [uu]
distinct [uu]
set [uu] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set [uu]. 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
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu]

goal (1 subgoal):
 1. sparse (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))) (set [uu])
[PROOF STEP]
unfolding sparse_def
[PROOF STATE]
proof (prove)
using this:
sorted_snd [uu]
distinct [uu]
set [uu] = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set [uu]. 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
\<forall>p\<^sub>0\<in>ps\<^sub>L. \<forall>p\<^sub>1\<in>ps\<^sub>L. 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))
\<forall>p\<^sub>0\<in>ps\<^sub>R. \<forall>p\<^sub>1\<in>ps\<^sub>R. 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))
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> \<delta>
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu]

goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set [uu]. \<forall>p\<^sub>1\<in>set [uu]. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> 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))
[PROOF STEP]
by (metis length_greater_0_conv length_pos_if_in_set set_ConsD)
[PROOF STATE]
proof (state)
this:
sparse (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))) (set [uu])

goal (1 subgoal):
 1. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[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)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = ?ps\<^sub>L \<union> ?ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (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)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = ?ps\<^sub>L \<union> ?ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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)) \<le> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>2 # ps))
sorted_snd (p\<^sub>0 # p\<^sub>2 # ps)
distinct (p\<^sub>0 # p\<^sub>2 # ps)
set (p\<^sub>0 # p\<^sub>2 # ps) = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set (p\<^sub>0 # p\<^sub>2 # 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
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> \<delta>
(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. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[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 (1 subgoal):
 1. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
define PS\<^sub>L where PS\<^sub>L_def: "PS\<^sub>L = ps\<^sub>L - { p\<^sub>0 }"
[PROOF STATE]
proof (state)
this:
PS\<^sub>L = ps\<^sub>L - {p\<^sub>0}

goal (1 subgoal):
 1. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
define PS\<^sub>R where PS\<^sub>R_def: "PS\<^sub>R = ps\<^sub>R - { p\<^sub>0 }"
[PROOF STATE]
proof (state)
this:
PS\<^sub>R = ps\<^sub>R - {p\<^sub>0}

goal (1 subgoal):
 1. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
have assms: "sorted_snd (p\<^sub>2 # ps)" "distinct (p\<^sub>2 # ps)" "set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R"
              "\<forall>p \<in> set (p\<^sub>2 # ps). l - \<delta> \<le> (fst p) \<and> (fst p) \<le> 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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((sorted_snd (p\<^sub>2 # ps) &&& distinct (p\<^sub>2 # ps)) &&& set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R &&& \<forall>p\<in>set (p\<^sub>2 # 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
[PROOF STEP]
using "3.prems"(1-9) sparse_def sorted_snd_def PS\<^sub>L_def PS\<^sub>R_def
[PROOF STATE]
proof (prove)
using this:
sorted_snd (p\<^sub>0 # p\<^sub>2 # ps)
distinct (p\<^sub>0 # p\<^sub>2 # ps)
set (p\<^sub>0 # p\<^sub>2 # ps) = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set (p\<^sub>0 # p\<^sub>2 # 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
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)))
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps
PS\<^sub>L = ps\<^sub>L - {p\<^sub>0}
PS\<^sub>R = ps\<^sub>R - {p\<^sub>0}

goal (1 subgoal):
 1. ((sorted_snd (p\<^sub>2 # ps) &&& distinct (p\<^sub>2 # ps)) &&& set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R &&& \<forall>p\<in>set (p\<^sub>2 # 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
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sorted_snd (p\<^sub>2 # ps)
distinct (p\<^sub>2 # ps)
set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R
\<forall>p\<in>set (p\<^sub>2 # 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. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); \<And>x C\<^sub>0 C\<^sub>1 ps\<^sub>L ps\<^sub>R. \<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)); sorted_snd (v # va); distinct (v # va); set (v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (v # va). 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; 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)) \<le> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (v # va)); sorted_snd (p\<^sub>0 # v # va); distinct (p\<^sub>0 # v # va); set (p\<^sub>0 # v # va) = ps\<^sub>L \<union> ps\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>0 # v # va). 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; 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> \<delta>; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # v # va))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C1: "\<exists>p \<in> set (p\<^sub>2 # ps). dist p\<^sub>0 p < \<delta>"
[PROOF STATE]
proof (state)
this:
\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence A: "\<forall>p \<in> set (p\<^sub>2 # ps). dist p\<^sub>0 p\<^sub>1 \<le> dist p\<^sub>0 p"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>

goal (1 subgoal):
 1. \<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using p\<^sub>1_def find_closest_bf_dist_take_7 "3.prems"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
\<lbrakk>\<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\<rbrakk> \<Longrightarrow> \<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))
sorted_snd (p\<^sub>0 # p\<^sub>2 # ps)
distinct (p\<^sub>0 # p\<^sub>2 # ps)
set (p\<^sub>0 # p\<^sub>2 # ps) = ps\<^sub>L \<union> ps\<^sub>R
0 \<le> \<delta>
\<forall>p\<in>set (p\<^sub>0 # p\<^sub>2 # 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
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> \<delta>
(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. \<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence B: "dist p\<^sub>0 p\<^sub>1 < \<delta>"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p 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 p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>
[PROOF STEP]
using C1
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>

goal (1 subgoal):
 1. 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>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
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>

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C2: "dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1"
[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. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where 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. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
using "3.hyps"(1)[of p\<^sub>1 PS\<^sub>L PS\<^sub>R] C2 p\<^sub>1_def "3.prems"(4,10) assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>p\<^sub>1 = 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 p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 \<le> \<delta>
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> \<delta>
sorted_snd (p\<^sub>2 # ps)
distinct (p\<^sub>2 # ps)
set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R
\<forall>p\<in>set (p\<^sub>2 # 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. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
have "dist C\<^sub>0' C\<^sub>1' \<le> dist c\<^sub>0 c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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 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))
[PROOF STEP]
using def find_closest_pair_dist_mono
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> 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 ?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))

goal (1 subgoal):
 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 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))
[PROOF STEP]
by blast
[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 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))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (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 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))
[PROOF STEP]
have "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>0 # p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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 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))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
using A C2 sparse_identity[of "dist C\<^sub>0' C\<^sub>1'" "p\<^sub>2 # ps" p\<^sub>0]
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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 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))
\<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
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))
\<lbrakk>sparse (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))) (set (p\<^sub>2 # ps)); \<forall>p\<in>set (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 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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 def "3.prems"(11) C2 p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # 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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. C\<^sub>0' = C\<^sub>0 &&& C\<^sub>1' = C\<^sub>1
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>0' = C\<^sub>0
 2. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>1' = C\<^sub>1
[PROOF STEP]
by (metis prod.inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C2: "\<not> dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1"
[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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
using "3.hyps"(2)[of p\<^sub>1 PS\<^sub>L PS\<^sub>R] C2 p\<^sub>1_def "3.prems"(4) assms B
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>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)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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)) \<le> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 \<le> \<delta>
sorted_snd (p\<^sub>2 # ps)
distinct (p\<^sub>2 # ps)
set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R
\<forall>p\<in>set (p\<^sub>2 # 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
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>

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
have "dist C\<^sub>0' C\<^sub>1' \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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))
[PROOF STEP]
using def find_closest_pair_dist_mono
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> 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 ?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))

goal (1 subgoal):
 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))
[PROOF STEP]
by blast
[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 (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (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))
[PROOF STEP]
have "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>0 # p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
using A sparse_identity order_trans
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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))
\<forall>p\<in>set (p\<^sub>2 # 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)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<lbrakk>sparse ?\<delta> (set ?ps); \<forall>p\<in>set ?ps. ?\<delta> \<le> dist (case ?p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> sparse ?\<delta> (set (?p\<^sub>0 # ?ps))
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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 def "3.prems"(11) C2 p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # 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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. C\<^sub>0' = C\<^sub>0 &&& C\<^sub>1' = C\<^sub>1
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (p\<^sub>2 # ps); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>0' = C\<^sub>0
 2. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (p\<^sub>2 # ps); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>1' = C\<^sub>1
[PROOF STEP]
by (metis prod.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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (1 subgoal):
 1. \<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>) \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>) \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C1: "\<not> (\<exists>p \<in> set (p\<^sub>2 # ps). dist p\<^sub>0 p < \<delta>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>)

goal (1 subgoal):
 1. \<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>) \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C2: "dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1"
[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. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where 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. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
using "3.hyps"(1)[of p\<^sub>1 PS\<^sub>L PS\<^sub>R] C2 p\<^sub>1_def "3.prems"(4,10) assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>p\<^sub>1 = 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 p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 \<le> \<delta>
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> \<delta>
sorted_snd (p\<^sub>2 # ps)
distinct (p\<^sub>2 # ps)
set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R
\<forall>p\<in>set (p\<^sub>2 # 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. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
have "dist C\<^sub>0' C\<^sub>1' \<le> dist c\<^sub>0 c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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 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))
[PROOF STEP]
using def find_closest_pair_dist_mono
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> 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 ?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))

goal (1 subgoal):
 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 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))
[PROOF STEP]
by blast
[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 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))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (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 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))
[PROOF STEP]
have "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>0 # p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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 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))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
using "3.prems"(10) C1 sparse_identity[of "dist C\<^sub>0' C\<^sub>1'" "p\<^sub>2 # ps" p\<^sub>0]
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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 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))
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> \<delta>
\<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>)
\<lbrakk>sparse (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))) (set (p\<^sub>2 # ps)); \<forall>p\<in>set (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 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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 def "3.prems"(11) C2 p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # 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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. C\<^sub>0' = C\<^sub>0 &&& C\<^sub>1' = C\<^sub>1
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>0' = C\<^sub>0
 2. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>1' = C\<^sub>1
[PROOF STEP]
by (metis prod.inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (2 subgoals):
 1. ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
 2. \<not> ?P \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
assume C2: "\<not> dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1"
[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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
hence "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
using "3.hyps"(2)[of p\<^sub>1 PS\<^sub>L PS\<^sub>R] C2 p\<^sub>1_def "3.prems"(4,10) assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>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)); sorted_snd (p\<^sub>2 # ps); distinct (p\<^sub>2 # ps); set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R; 0 \<le> \<delta>; \<forall>p\<in>set (p\<^sub>2 # 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; 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)) \<le> \<delta>; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> sparse (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))) (set (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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 \<le> \<delta>
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> \<delta>
sorted_snd (p\<^sub>2 # ps)
distinct (p\<^sub>2 # ps)
set (p\<^sub>2 # ps) = PS\<^sub>L \<union> PS\<^sub>R
\<forall>p\<in>set (p\<^sub>2 # 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. sparse (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))) (set (p\<^sub>2 # ps))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
have "dist C\<^sub>0' C\<^sub>1' \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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))
[PROOF STEP]
using def find_closest_pair_dist_mono
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> 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 ?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))

goal (1 subgoal):
 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))
[PROOF STEP]
by blast
[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 (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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (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))
[PROOF STEP]
have "sparse (dist C\<^sub>0' C\<^sub>1') (set (p\<^sub>0 # p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
using "3.prems"(10) C1 C2 sparse_identity[of "dist C\<^sub>0' C\<^sub>1'" "p\<^sub>2 # ps" p\<^sub>0]
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (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))
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> \<delta>
\<not> (\<exists>p\<in>set (p\<^sub>2 # ps). dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < \<delta>)
\<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))
\<lbrakk>sparse (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))) (set (p\<^sub>2 # ps)); \<forall>p\<in>set (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 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # 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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[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 def "3.prems"(11) C2 p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # 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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. C\<^sub>0' = C\<^sub>0 &&& C\<^sub>1' = C\<^sub>1
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (p\<^sub>2 # ps); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>0' = C\<^sub>0
 2. \<lbrakk>(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (p\<^sub>2 # ps); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)) (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 find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>1 = find_closest_bf p\<^sub>0 (p\<^sub>2 # take 6 ps)\<rbrakk> \<Longrightarrow> C\<^sub>1' = C\<^sub>1
[PROOF STEP]
by (metis prod.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> sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
C\<^sub>0' = C\<^sub>0
C\<^sub>1' = C\<^sub>1

goal (1 subgoal):
 1. sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sparse (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))) (set (p\<^sub>0 # p\<^sub>2 # ps))

goal:
No subgoals!
[PROOF STEP]
qed