[STATEMENT]
lemma closest_pair_rec_dist:
  assumes "1 < length xs" "distinct xs" "sorted_fst xs" "(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs"
  shows "sparse (dist c\<^sub>0 c\<^sub>1) (set xs)"
[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 xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < length xs
distinct xs
sorted_fst xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs

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 xs)
[PROOF STEP]
proof (induction xs arbitrary: ys c\<^sub>0 c\<^sub>1 rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys)); 1 < length xs; distinct xs; sorted_fst xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs\<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 xs)
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys))
1 < length xs
distinct xs
sorted_fst xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs

goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys)); 1 < length xs; distinct xs; sorted_fst xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs\<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 xs)
[PROOF STEP]
let ?n = "length xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys)); 1 < length xs; distinct xs; sorted_fst xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs\<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 xs)
[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 xs)
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<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 xs)
 2. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

goal (2 subgoals):
 1. length xs \<le> 3 \<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 xs)
 2. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
hence "(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs"
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

goal (1 subgoal):
 1. (c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
[PROOF STEP]
using "1.prems"(4) closest_pair_rec.simps
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
closest_pair_rec ?xs = (let n = length ?xs in if n \<le> 3 then (mergesort snd ?xs, closest_pair_bf ?xs) else let (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) ?xs; (ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) = closest_pair_rec xs\<^sub>L; (ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) = closest_pair_rec xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (fst (hd xs\<^sub>R)) ys))

goal (1 subgoal):
 1. (c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs

goal (2 subgoals):
 1. length xs \<le> 3 \<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 xs)
 2. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs

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 xs)
[PROOF STEP]
using "1.prems"(1,4) closest_pair_bf_dist
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
1 < length xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
\<lbrakk>1 < length ?ps; (?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf ?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 ?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 xs)
[PROOF STEP]
by metis
[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 xs)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs \<le> 3

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
obtain XS\<^sub>L XS\<^sub>R where XS\<^sub>L\<^sub>R_def: "(XS\<^sub>L, XS\<^sub>R) = split_at (?n div 2) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>XS\<^sub>L XS\<^sub>R. (XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs \<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>XS\<^sub>L XS\<^sub>R. (XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
define L where "L = fst (hd XS\<^sub>R)"
[PROOF STATE]
proof (state)
this:
L = fst (hd XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
obtain YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L where YSC\<^sub>0\<^sub>1\<^sub>L_def: "(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L. (YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L \<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>YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L. (YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
obtain YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R where YSC\<^sub>0\<^sub>1\<^sub>R_def: "(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R. (YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R \<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>YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R. (YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
define YS where "YS = merge (\<lambda>p. snd p) YS\<^sub>L YS\<^sub>R"
[PROOF STATE]
proof (state)
this:
YS = Common.merge snd YS\<^sub>L YS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 where C\<^sub>0\<^sub>1_def: "(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS \<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) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSC\<^sub>0\<^sub>1\<^sub>L_def YSC\<^sub>0\<^sub>1\<^sub>R_def YS_def C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have XSLR: "XS\<^sub>L = take (?n div 2) xs" "XS\<^sub>R = drop (?n div 2) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XS\<^sub>L = take (length xs div 2) xs &&& XS\<^sub>R = drop (length xs div 2) xs
[PROOF STEP]
using defs
[PROOF STATE]
proof (prove)
using this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. XS\<^sub>L = take (length xs div 2) xs &&& XS\<^sub>R = drop (length xs div 2) xs
[PROOF STEP]
by (auto simp: split_at_take_drop_conv)
[PROOF STATE]
proof (state)
this:
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "1 < length XS\<^sub>L" "length XS\<^sub>L < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length xs
[PROOF STEP]
using False XSLR
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs

goal (1 subgoal):
 1. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "distinct XS\<^sub>L" "sorted_fst XS\<^sub>L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct XS\<^sub>L &&& sorted_fst XS\<^sub>L
[PROOF STEP]
using "1.prems"(2,3) XSLR
[PROOF STATE]
proof (prove)
using this:
distinct xs
sorted_fst xs
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs

goal (1 subgoal):
 1. distinct XS\<^sub>L &&& sorted_fst XS\<^sub>L
[PROOF STEP]
by (auto simp: sorted_fst_def sorted_wrt_take)
[PROOF STATE]
proof (state)
this:
distinct XS\<^sub>L
sorted_fst XS\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L
sorted_fst XS\<^sub>L
[PROOF STEP]
have L: "sparse (dist C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L) (set XS\<^sub>L)"
                       "set XS\<^sub>L = set YS\<^sub>L"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L
sorted_fst XS\<^sub>L

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>L) &&& set XS\<^sub>L = set YS\<^sub>L
[PROOF STEP]
using 1 closest_pair_rec_set_length_sorted_snd closest_pair_rec_c0_c1
              YSC\<^sub>0\<^sub>1\<^sub>L_def
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L
sorted_fst XS\<^sub>L
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys))
1 < length xs
distinct xs
sorted_fst xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
\<lbrakk>1 < length ?xs; distinct ?xs; (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec ?xs\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<in> set ?xs \<and> ?c\<^sub>1 \<in> set ?xs \<and> ?c\<^sub>0 \<noteq> ?c\<^sub>1
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>L) &&& set XS\<^sub>L = set YS\<^sub>L
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>L)
set XS\<^sub>L = set YS\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
hence IHL: "sparse (dist C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L) (set YS\<^sub>L)"
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>L)
set XS\<^sub>L = set YS\<^sub>L

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^sub>L)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^sub>L)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "1 < length XS\<^sub>R" "length XS\<^sub>R < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length xs
[PROOF STEP]
using False XSLR
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs

goal (1 subgoal):
 1. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "distinct XS\<^sub>R" "sorted_fst XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct XS\<^sub>R &&& sorted_fst XS\<^sub>R
[PROOF STEP]
using "1.prems"(2,3) XSLR
[PROOF STATE]
proof (prove)
using this:
distinct xs
sorted_fst xs
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs

goal (1 subgoal):
 1. distinct XS\<^sub>R &&& sorted_fst XS\<^sub>R
[PROOF STEP]
by (auto simp: sorted_fst_def sorted_wrt_drop)
[PROOF STATE]
proof (state)
this:
distinct XS\<^sub>R
sorted_fst XS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R
sorted_fst XS\<^sub>R
[PROOF STEP]
have R: "sparse (dist C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R) (set XS\<^sub>R)"
                       "set XS\<^sub>R = set YS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R
sorted_fst XS\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>R) &&& set XS\<^sub>R = set YS\<^sub>R
[PROOF STEP]
using 1 closest_pair_rec_set_length_sorted_snd closest_pair_rec_c0_c1
              YSC\<^sub>0\<^sub>1\<^sub>R_def
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R
sorted_fst XS\<^sub>R
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> sorted_fst ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> sparse (dist (case xa of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case xb of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ys))
1 < length xs
distinct xs
sorted_fst xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
\<lbrakk>1 < length ?xs; distinct ?xs; (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec ?xs\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<in> set ?xs \<and> ?c\<^sub>1 \<in> set ?xs \<and> ?c\<^sub>0 \<noteq> ?c\<^sub>1
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>R) &&& set XS\<^sub>R = set YS\<^sub>R
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>R)
set XS\<^sub>R = set YS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
hence IHR: "sparse (dist C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R) (set YS\<^sub>R)"
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set XS\<^sub>R)
set XS\<^sub>R = set YS\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^sub>R)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^sub>R)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have *: "(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
[PROOF STEP]
using False closest_pair_rec_simps defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
\<lbrakk>?n = length ?xs; \<not> ?n \<le> 3\<rbrakk> \<Longrightarrow> closest_pair_rec ?xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (?n div 2) ?xs; (ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) = closest_pair_rec xs\<^sub>L; (ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) = closest_pair_rec xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (fst (hd xs\<^sub>R)) ys))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
[PROOF STEP]
by (auto simp: Let_def split: prod.split)
[PROOF STATE]
proof (state)
this:
(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "set xs = set YS" "distinct YS" "sorted_snd YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set YS &&& distinct YS &&& sorted_snd YS
[PROOF STEP]
using "1.prems"(2) closest_pair_rec_set_length_sorted_snd closest_pair_rec_distinct *
[PROOF STATE]
proof (prove)
using this:
distinct xs
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
\<lbrakk>distinct ?xs; (?ys, ?p) = closest_pair_rec ?xs\<rbrakk> \<Longrightarrow> distinct ?ys
(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs

goal (1 subgoal):
 1. set xs = set YS &&& distinct YS &&& sorted_snd YS
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
set xs = set YS
distinct YS
sorted_snd YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs = set YS
distinct YS
sorted_snd YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "\<forall>p \<in> set YS\<^sub>L. fst p \<le> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set YS\<^sub>L. fst p \<le> L
[PROOF STEP]
using False "1.prems"(3) XSLR L_def L(2) sorted_fst_take_less_hd_drop
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
sorted_fst xs
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs
L = fst (hd XS\<^sub>R)
set XS\<^sub>L = set YS\<^sub>L
\<lbrakk>sorted_fst ?ps; ?n < length ?ps\<rbrakk> \<Longrightarrow> \<forall>p\<in>set (take ?n ?ps). fst p \<le> fst (hd (drop ?n ?ps))

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set YS\<^sub>L. fst p \<le> L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "\<forall>p \<in> set YS\<^sub>R. L \<le> fst p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set YS\<^sub>R. L \<le> fst p
[PROOF STEP]
using False "1.prems"(3) XSLR L_def R(2) sorted_fst_hd_drop_less_drop
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
sorted_fst xs
XS\<^sub>L = take (length xs div 2) xs
XS\<^sub>R = drop (length xs div 2) xs
L = fst (hd XS\<^sub>R)
set XS\<^sub>R = set YS\<^sub>R
sorted_fst ?ps \<Longrightarrow> \<forall>p\<in>set (drop ?n ?ps). fst (hd (drop ?n ?ps)) \<le> fst p

goal (1 subgoal):
 1. \<forall>p\<in>set YS\<^sub>R. L \<le> fst p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set YS\<^sub>R. L \<le> fst p

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set YS\<^sub>R. L \<le> fst p

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "set YS = set YS\<^sub>L \<union> set YS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set YS = set YS\<^sub>L \<union> set YS\<^sub>R
[PROOF STEP]
using set_merge defs
[PROOF STATE]
proof (prove)
using this:
set (Common.merge ?f ?xs ?ys) = set ?xs \<union> set ?ys
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. set YS = set YS\<^sub>L \<union> set YS\<^sub>R
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set YS = set YS\<^sub>L \<union> set YS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set YS = set YS\<^sub>L \<union> set YS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
[PROOF STEP]
by (auto simp add: defs)
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set xs = set YS
distinct YS
sorted_snd YS
\<forall>p\<in>set YS\<^sub>L. fst p \<le> L
\<forall>p\<in>set YS\<^sub>R. L \<le> fst p
set YS = set YS\<^sub>L \<union> set YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
[PROOF STEP]
have "sparse (dist C\<^sub>0 C\<^sub>1) (set xs)"
[PROOF STATE]
proof (prove)
using this:
set xs = set YS
distinct YS
sorted_snd YS
\<forall>p\<in>set YS\<^sub>L. fst p \<le> L
\<forall>p\<in>set YS\<^sub>R. L \<le> fst p
set YS = set YS\<^sub>L \<union> set YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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 xs)
[PROOF STEP]
using combine_dist IHL IHR
[PROOF STATE]
proof (prove)
using this:
set xs = set YS
distinct YS
sorted_snd YS
\<forall>p\<in>set YS\<^sub>L. fst p \<le> L
\<forall>p\<in>set YS\<^sub>R. L \<le> fst p
set YS = set YS\<^sub>L \<union> set YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
\<lbrakk>distinct ?ps; sorted_snd ?ps; set ?ps = ?ps\<^sub>L \<union> ?ps\<^sub>R; \<forall>p\<in>?ps\<^sub>L. fst p \<le> ?l; \<forall>p\<in>?ps\<^sub>R. ?l \<le> fst p; sparse (dist (case ?p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ?ps\<^sub>L; sparse (dist (case ?p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ?ps\<^sub>R; (?c\<^sub>0, ?c\<^sub>1) = combine (?p\<^sub>0\<^sub>L, ?p\<^sub>1\<^sub>L) (?p\<^sub>0\<^sub>R, ?p\<^sub>1\<^sub>R) ?l ?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 ?ps)
sparse (dist (case C\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^sub>L)
sparse (dist (case C\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set YS\<^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 xs)
[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 xs)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[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 xs)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[PROOF STEP]
have "(YS, C\<^sub>0, C\<^sub>1) = (ys, c\<^sub>0, c\<^sub>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = (ys, c\<^sub>0, c\<^sub>1)
[PROOF STEP]
using "1.prems"(4) *
[PROOF STATE]
proof (prove)
using this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs

goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = (ys, c\<^sub>0, c\<^sub>1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(YS, C\<^sub>0, C\<^sub>1) = (ys, c\<^sub>0, c\<^sub>1)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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 xs)
[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 xs)
(YS, C\<^sub>0, C\<^sub>1) = (ys, c\<^sub>0, 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 xs)
(YS, C\<^sub>0, C\<^sub>1) = (ys, 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 xs)
[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 xs)

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 xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_eq_val_closest_pair_tm:
  "val (closest_pair_tm ps) = closest_pair ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Monad.val (closest_pair_tm ps) = closest_pair ps
[PROOF STEP]
by (induction ps rule: induct_list012)
     (auto simp del: closest_pair_rec_tm.simps mergesort_tm.simps
           simp add: closest_pair_rec_eq_val_closest_pair_rec_tm mergesort_eq_val_mergesort_tm
           split: prod.split)


[STATEMENT]
lemma closest_pair_simps:
  "1 < length ps \<Longrightarrow> closest_pair ps = (let (_, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst ps) in (c\<^sub>0, c\<^sub>1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length ps \<Longrightarrow> closest_pair ps = (let (uu_, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst ps) in (c\<^sub>0, c\<^sub>1))
[PROOF STEP]
by (induction ps rule: induct_list012) auto


[STATEMENT]
theorem closest_pair_c0_c1:
  assumes "1 < length ps" "distinct ps" "(c\<^sub>0, c\<^sub>1) = closest_pair ps"
  shows "c\<^sub>0 \<in> set ps" "c\<^sub>1 \<in> set ps" "c\<^sub>0 \<noteq> c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 \<in> set ps &&& c\<^sub>1 \<in> set ps &&& c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
using assms closest_pair_rec_c0_c1[of "mergesort fst ps"]
[PROOF STATE]
proof (prove)
using this:
1 < length ps
distinct ps
(c\<^sub>0, c\<^sub>1) = closest_pair ps
\<lbrakk>1 < length (mergesort fst ps); distinct (mergesort fst ps); (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec (mergesort fst ps)\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<in> set (mergesort fst ps) \<and> ?c\<^sub>1 \<in> set (mergesort fst ps) \<and> ?c\<^sub>0 \<noteq> ?c\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<in> set ps &&& c\<^sub>1 \<in> set ps &&& c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
by (auto simp: mergesort closest_pair_simps split: prod.splits)


[STATEMENT]
theorem closest_pair_dist:
  assumes "1 < length ps" "distinct ps" "(c\<^sub>0, c\<^sub>1) = closest_pair 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 closest_pair_rec_dist[of "mergesort fst ps"] closest_pair_rec_c0_c1[of "mergesort fst ps"]
[PROOF STATE]
proof (prove)
using this:
1 < length ps
distinct ps
(c\<^sub>0, c\<^sub>1) = closest_pair ps
\<lbrakk>1 < length (mergesort fst ps); distinct (mergesort fst ps); sorted_fst (mergesort fst ps); (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec (mergesort fst 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 (mergesort fst ps))
\<lbrakk>1 < length (mergesort fst ps); distinct (mergesort fst ps); (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec (mergesort fst ps)\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<in> set (mergesort fst ps) \<and> ?c\<^sub>1 \<in> set (mergesort fst ps) \<and> ?c\<^sub>0 \<noteq> ?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 ps)
[PROOF STEP]
by (auto simp: sorted_fst_def mergesort closest_pair_simps split: prod.splits)


[STATEMENT]
lemma time_find_closest_pair_tm:
  "time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps) \<le> 17 * length ps + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps) \<le> 17 * length ps + 1
[PROOF STEP]
proof (induction ps rule: find_closest_pair_tm.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va. \<lbrakk>\<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (v # va)) \<le> 17 * length (v # va) + 1; \<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); \<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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, vc) (v # va)) \<le> 17 * length (v # va) + 1\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)) \<le> 17 * length (p\<^sub>0 # v # va) + 1
[PROOF STEP]
case (3 c\<^sub>0 c\<^sub>1 p\<^sub>0 p\<^sub>2 ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?vb = Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)); ?vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 ?vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 ?vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>2 # ps) + 1
\<lbrakk>?vb = Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)); ?vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 ?vb); \<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 ?vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, ?vc) (p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>2 # ps) + 1

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va. \<lbrakk>\<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (v # va)) \<le> 17 * length (v # va) + 1; \<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); \<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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, vc) (v # va)) \<le> 17 * length (v # va) + 1\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)) \<le> 17 * length (p\<^sub>0 # v # va) + 1
[PROOF STEP]
let ?ps = "p\<^sub>2 # ps"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va. \<lbrakk>\<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (v # va)) \<le> 17 * length (v # va) + 1; \<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); \<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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, vc) (v # va)) \<le> 17 * length (v # va) + 1\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)) \<le> 17 * length (p\<^sub>0 # v # va) + 1
[PROOF STEP]
let ?p\<^sub>1 = "val (find_closest_bf_tm p\<^sub>0 (val (take_tm 7 ?ps)))"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va. \<lbrakk>\<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (v # va)) \<le> 17 * length (v # va) + 1; \<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); \<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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, vc) (v # va)) \<le> 17 * length (v # va) + 1\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)) \<le> 17 * length (p\<^sub>0 # v # va) + 1
[PROOF STEP]
have *: "length (val (take_tm 7 ?ps)) \<le> 7"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) \<le> 7
[PROOF STEP]
by (subst take_eq_val_take_tm, simp)
[PROOF STATE]
proof (state)
this:
length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) \<le> 7

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va. \<lbrakk>\<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (v # va)) \<le> 17 * length (v # va) + 1; \<And>vb vc. \<lbrakk>vb = Time_Monad.val (take_tm 7 (v # va)); vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 vb); \<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 vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, vc) (v # va)) \<le> 17 * length (v # va) + 1\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)) \<le> 17 * length (p\<^sub>0 # v # va) + 1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
assume C1: "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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
hence "time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # ?ps)) = 1 + time (take_tm 7 ?ps) +
           time (find_closest_bf_tm p\<^sub>0 (val (take_tm 7 ?ps))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ?ps)"
[PROOF STATE]
proof (prove)
using 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))
[PROOF STEP]
by (auto simp: time_simps)
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... \<le> 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ?ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))
[PROOF STEP]
using time_take_tm[of 7 ?ps] time_find_closest_bf_tm[of p\<^sub>0 "val (take_tm 7 ?ps)"] *
[PROOF STATE]
proof (prove)
using this:
time (take_tm 7 (p\<^sub>2 # ps)) = min 7 (length (p\<^sub>2 # ps)) + 1
time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) \<le> length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) + 1
length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) \<le> 7

goal (1 subgoal):
 1. 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps))

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... \<le> 17 + 17 * (length ?ps) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1
[PROOF STEP]
using "3.IH"(1) C1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?vb = Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)); ?vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 ?vb); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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 ?vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. 17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
17 + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... = 17 * length (p\<^sub>0 # ?ps) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17 + 17 * length (p\<^sub>2 # ps) + 1 = 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
17 + 17 * length (p\<^sub>2 # ps) + 1 = 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
 2. \<not> ?P \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1

goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
assume C1: "\<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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
hence "time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # ?ps)) = 1 + time (take_tm 7 ?ps) +
           time (find_closest_bf_tm p\<^sub>0 (val (take_tm 7 ?ps))) + time (find_closest_pair_tm (p\<^sub>0, ?p\<^sub>1) ?ps)"
[PROOF STATE]
proof (prove)
using 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps))
[PROOF STEP]
by (auto simp: time_simps)
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) = 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... \<le> 17 + time (find_closest_pair_tm (p\<^sub>0, ?p\<^sub>1) ?ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps))
[PROOF STEP]
using time_take_tm[of 7 ?ps] time_find_closest_bf_tm[of p\<^sub>0 "val (take_tm 7 ?ps)"] *
[PROOF STATE]
proof (prove)
using this:
time (take_tm 7 (p\<^sub>2 # ps)) = min 7 (length (p\<^sub>2 # ps)) + 1
time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) \<le> length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) + 1
length (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))) \<le> 7

goal (1 subgoal):
 1. 1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + time (take_tm 7 (p\<^sub>2 # ps)) + time (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... \<le> 17 + 17 * (length ?ps) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1
[PROOF STEP]
using "3.IH"(2) C1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?vb = Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)); ?vc = Time_Monad.val (find_closest_bf_tm p\<^sub>0 ?vb); \<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 ?vc of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))\<rbrakk> \<Longrightarrow> time (find_closest_pair_tm (p\<^sub>0, ?vc) (p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. 17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
17 + time (find_closest_pair_tm (p\<^sub>0, Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps))))) (p\<^sub>2 # ps)) \<le> 17 + 17 * length (p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
have "... = 17 * length (p\<^sub>0 # ?ps) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17 + 17 * length (p\<^sub>2 # ps) + 1 = 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
17 + 17 * length (p\<^sub>2 # ps) + 1 = 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 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 Time_Monad.val (find_closest_bf_tm p\<^sub>0 (Time_Monad.val (take_tm 7 (p\<^sub>2 # ps)))) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1

goal (1 subgoal):
 1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)) \<le> 17 * length (p\<^sub>0 # p\<^sub>2 # ps) + 1

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) []) \<le> 17 * length [] + 1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_. time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) [uu_]) \<le> 17 * length [uu_] + 1
[PROOF STEP]
qed (auto simp: time_simps)


[STATEMENT]
lemma time_combine_tm:
  fixes ps :: "point list"
  shows "time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
obtain c\<^sub>0 c\<^sub>1 where c_def:
    "(c\<^sub>0, c\<^sub>1) = (if dist p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L < dist p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c\<^sub>0 c\<^sub>1. (c\<^sub>0, c\<^sub>1) = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(c\<^sub>0, c\<^sub>1) = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
let ?P = "(\<lambda>p. dist p (l, snd p) < dist c\<^sub>0 c\<^sub>1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
define ps' where "ps' = val (filter_tm ?P ps)"
[PROOF STATE]
proof (state)
this:
ps' = Time_Monad.val (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps)

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
note defs = c_def ps'_def
[PROOF STATE]
proof (state)
this:
(c\<^sub>0, c\<^sub>1) = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = Time_Monad.val (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps)

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
hence "time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = 1 + time (filter_tm ?P ps) +
        time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')"
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = Time_Monad.val (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps)

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = 1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')
[PROOF STEP]
by (auto simp: combine_tm.simps Let_def time_simps split: prod.split)
[PROOF STATE]
proof (state)
this:
time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = 1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = 1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
have "... = 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') = 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')
[PROOF STEP]
using time_filter_tm
[PROOF STATE]
proof (prove)
using this:
time (filter_tm ?P ?xs) = length ?xs + 1

goal (1 subgoal):
 1. 1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') = 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') = 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + time (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps) + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') = 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps')

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
have "... \<le> 3 + length ps + 17 * length ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') \<le> 3 + length ps + 17 * length ps'
[PROOF STEP]
using defs time_find_closest_pair_tm
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = Time_Monad.val (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, y) \<Rightarrow> (real_of_int x, 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))) ps)
time (find_closest_pair_tm (?c\<^sub>0, ?c\<^sub>1) ?ps) \<le> 17 * length ?ps + 1

goal (1 subgoal):
 1. 2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') \<le> 3 + length ps + 17 * length ps'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') \<le> 3 + length ps + 17 * length ps'

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 + length ps + time (find_closest_pair_tm (c\<^sub>0, c\<^sub>1) ps') \<le> 3 + length ps + 17 * length ps'

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
have "... \<le> 3 + 18 * length ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 + length ps + 17 * length ps' \<le> 3 + 18 * length ps
[PROOF STEP]
unfolding ps'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 + length ps + 17 * length (Time_Monad.val (filter_tm (\<lambda>x. dist (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) of (x, xa) \<Rightarrow> (real_of_int x, xa)) < dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps)) \<le> 3 + 18 * length ps
[PROOF STEP]
by (subst filter_eq_val_filter_tm, simp)
[PROOF STATE]
proof (state)
this:
3 + length ps + 17 * length ps' \<le> 3 + 18 * length ps

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps

goal (1 subgoal):
 1. time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) \<le> 3 + 18 * length ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma time_closest_pair_rec_tm_simps_1:
  assumes "length xs \<le> 3"
  shows "time (closest_pair_rec_tm xs) = 1 + time (length_tm xs) + time (mergesort_tm snd xs) + time (closest_pair_bf_tm xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (closest_pair_rec_tm xs) = 1 + time (length_tm xs) + time (mergesort_tm snd xs) + time (closest_pair_bf_tm xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

goal (1 subgoal):
 1. time (closest_pair_rec_tm xs) = 1 + time (length_tm xs) + time (mergesort_tm snd xs) + time (closest_pair_bf_tm xs)
[PROOF STEP]
by  (auto simp: time_simps length_eq_val_length_tm)


[STATEMENT]
lemma time_closest_pair_rec_tm_simps_2:
  assumes "\<not> (length xs \<le> 3)"
  shows "time (closest_pair_rec_tm xs) = 1 + (
    let (xs\<^sub>L, xs\<^sub>R) = val (split_at_tm (length xs div 2) xs) in
    let (ys\<^sub>L, p\<^sub>L) = val (closest_pair_rec_tm xs\<^sub>L) in
    let (ys\<^sub>R, p\<^sub>R) = val (closest_pair_rec_tm xs\<^sub>R) in
    let ys = val (merge_tm (\<lambda>p. snd p) ys\<^sub>L ys\<^sub>R) in
    time (length_tm xs) + time (split_at_tm (length xs div 2) xs) + time (closest_pair_rec_tm xs\<^sub>L) +
    time (closest_pair_rec_tm xs\<^sub>R) + time (merge_tm (\<lambda>p. snd p) ys\<^sub>L ys\<^sub>R) + time (combine_tm p\<^sub>L p\<^sub>R (fst (hd xs\<^sub>R)) ys)
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (closest_pair_rec_tm xs) = 1 + (let (xs\<^sub>L, xs\<^sub>R) = Time_Monad.val (split_at_tm (length xs div 2) xs); (ys\<^sub>L, p\<^sub>L) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>L); (ys\<^sub>R, p\<^sub>R) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>R); ys = Time_Monad.val (merge_tm snd ys\<^sub>L ys\<^sub>R) in time (length_tm xs) + time (split_at_tm (length xs div 2) xs) + time (closest_pair_rec_tm xs\<^sub>L) + time (closest_pair_rec_tm xs\<^sub>R) + time (merge_tm snd ys\<^sub>L ys\<^sub>R) + time (combine_tm p\<^sub>L p\<^sub>R (fst (hd xs\<^sub>R)) ys))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3

goal (1 subgoal):
 1. time (closest_pair_rec_tm xs) = 1 + (let (xs\<^sub>L, xs\<^sub>R) = Time_Monad.val (split_at_tm (length xs div 2) xs); (ys\<^sub>L, p\<^sub>L) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>L); (ys\<^sub>R, p\<^sub>R) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>R); ys = Time_Monad.val (merge_tm snd ys\<^sub>L ys\<^sub>R) in time (length_tm xs) + time (split_at_tm (length xs div 2) xs) + time (closest_pair_rec_tm xs\<^sub>L) + time (closest_pair_rec_tm xs\<^sub>R) + time (merge_tm snd ys\<^sub>L ys\<^sub>R) + time (combine_tm p\<^sub>L p\<^sub>R (fst (hd xs\<^sub>R)) ys))
[PROOF STEP]
apply (subst closest_pair_rec_tm.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> time (length_tm xs \<bind> (\<lambda>n. if n \<le> 3 then mergesort_tm snd xs \<bind> (\<lambda>ys. closest_pair_bf_tm xs \<bind> (\<lambda>p. return (ys, p))) else split_at_tm (n div 2) xs \<bind> (\<lambda>(xs\<^sub>L, xs\<^sub>R). closest_pair_rec_tm xs\<^sub>L \<bind> (\<lambda>(ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L). closest_pair_rec_tm xs\<^sub>R \<bind> (\<lambda>(ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R). merge_tm snd ys\<^sub>L ys\<^sub>R \<bind> (\<lambda>ys. combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (fst (hd xs\<^sub>R)) ys \<bind> (\<lambda>(p\<^sub>0, p\<^sub>1). return (ys, p\<^sub>0, p\<^sub>1))))))) \<bind> tick) = 1 + (let (xs\<^sub>L, xs\<^sub>R) = Time_Monad.val (split_at_tm (length xs div 2) xs); (ys\<^sub>L, p\<^sub>L) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>L); (ys\<^sub>R, p\<^sub>R) = Time_Monad.val (closest_pair_rec_tm xs\<^sub>R); ys = Time_Monad.val (merge_tm snd ys\<^sub>L ys\<^sub>R) in time (length_tm xs) + time (split_at_tm (length xs div 2) xs) + time (closest_pair_rec_tm xs\<^sub>L) + time (closest_pair_rec_tm xs\<^sub>R) + time (merge_tm snd ys\<^sub>L ys\<^sub>R) + time (combine_tm p\<^sub>L p\<^sub>R (fst (hd xs\<^sub>R)) ys))
[PROOF STEP]
by (auto simp del: closest_pair_rec_tm.simps
           simp add: time_simps length_eq_val_length_tm
              split: prod.split)


[STATEMENT]
lemma closest_pair_recurrence_nonneg[simp]:
  "0 \<le> closest_pair_recurrence n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> closest_pair_recurrence n
[PROOF STEP]
by (induction n rule: closest_pair_recurrence.induct) auto