[STATEMENT]
lemma time_closest_pair_rec_conv_closest_pair_recurrence:
  "time (closest_pair_rec_tm ps) \<le> closest_pair_recurrence (length ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
proof (induction ps rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys) \<Longrightarrow> real (time (closest_pair_rec_tm xs)) \<le> closest_pair_recurrence (length xs)
[PROOF STEP]
case (1 ps)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length ps \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys)

goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys) \<Longrightarrow> real (time (closest_pair_rec_tm xs)) \<le> closest_pair_recurrence (length xs)
[PROOF STEP]
let ?n = "length ps"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys) \<Longrightarrow> real (time (closest_pair_rec_tm xs)) \<le> closest_pair_recurrence (length xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length ps \<le> 3

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence "time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)"
[PROOF STATE]
proof (prove)
using this:
length ps \<le> 3

goal (1 subgoal):
 1. time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)
[PROOF STEP]
using time_closest_pair_rec_tm_simps_1
[PROOF STATE]
proof (prove)
using this:
length ps \<le> 3
length ?xs \<le> 3 \<Longrightarrow> time (closest_pair_rec_tm ?xs) = 1 + time (length_tm ?xs) + time (mergesort_tm snd ?xs) + time (closest_pair_bf_tm ?xs)

goal (1 subgoal):
 1. time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "closest_pair_recurrence ?n = 3 + ?n + mergesort_recurrence ?n + ?n * ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
length ps \<le> 3

goal (1 subgoal):
 1. closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "time (length_tm ps) \<le> 1 + ?n" "time (mergesort_tm snd ps) \<le> mergesort_recurrence ?n"
                  "time (closest_pair_bf_tm ps) \<le> 1 + ?n * ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (length_tm ps) \<le> 1 + length ps &&& real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps) &&& time (closest_pair_bf_tm ps) \<le> 1 + length ps * length ps
[PROOF STEP]
using time_length_tm[of ps] time_mergesort_conv_mergesort_recurrence[of snd ps] time_closest_pair_bf_tm[of ps]
[PROOF STATE]
proof (prove)
using this:
time (length_tm ps) = length ps + 1
real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps)
time (closest_pair_bf_tm ps) \<le> length ps * length ps + 1

goal (1 subgoal):
 1. time (length_tm ps) \<le> 1 + length ps &&& real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps) &&& time (closest_pair_bf_tm ps) \<le> 1 + length ps * length ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
time (length_tm ps) \<le> 1 + length ps
real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps)
time (closest_pair_bf_tm ps) \<le> 1 + length ps * length ps

goal (2 subgoals):
 1. length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
 2. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)
closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)
time (length_tm ps) \<le> 1 + length ps
real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps)
time (closest_pair_bf_tm ps) \<le> 1 + length ps * length ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (mergesort_tm snd ps) + time (closest_pair_bf_tm ps)
closest_pair_recurrence (length ps) = real (3 + length ps) + mergesort_recurrence (length ps) + real (length ps * length ps)
time (length_tm ps) \<le> 1 + length ps
real (time (mergesort_tm snd ps)) \<le> mergesort_recurrence (length ps)
time (closest_pair_bf_tm ps) \<le> 1 + length ps * length ps

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length ps \<le> 3

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
obtain XS\<^sub>L XS\<^sub>R where XS_def: "(XS\<^sub>L, XS\<^sub>R) = val (split_at_tm (?n div 2) ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>XS\<^sub>L XS\<^sub>R. (XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>XS\<^sub>L XS\<^sub>R. (XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
obtain YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L where CP\<^sub>L_def: "(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
obtain YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R where CP\<^sub>R_def: "(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm 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) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
define YS where "YS = val (merge_tm (\<lambda>p. snd p) YS\<^sub>L YS\<^sub>R)"
[PROOF STATE]
proof (state)
this:
YS = Time_Monad.val (merge_tm snd YS\<^sub>L YS\<^sub>R)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 where C\<^sub>0\<^sub>1_def: "(C\<^sub>0, C\<^sub>1) = val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) 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) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
note defs = XS_def CP\<^sub>L_def CP\<^sub>R_def YS_def C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have XSLR: "XS\<^sub>L = take (?n div 2) ps" "XS\<^sub>R = drop (?n div 2) ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. XS\<^sub>L = take (length ps div 2) ps &&& XS\<^sub>R = drop (length ps div 2) ps
[PROOF STEP]
using defs
[PROOF STATE]
proof (prove)
using this:
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

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

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence "length XS\<^sub>L = ?n div 2" "length XS\<^sub>R = ?n - ?n div 2"
[PROOF STATE]
proof (prove)
using this:
XS\<^sub>L = take (length ps div 2) ps
XS\<^sub>R = drop (length ps div 2) ps

goal (1 subgoal):
 1. length XS\<^sub>L = length ps div 2 &&& length XS\<^sub>R = length ps - length ps div 2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length XS\<^sub>L = length ps div 2
length XS\<^sub>R = length ps - length ps div 2

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence *: "(nat \<lfloor>real ?n / 2\<rfloor>) = length XS\<^sub>L" "(nat \<lceil>real ?n / 2\<rceil>) = length XS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L = length ps div 2
length XS\<^sub>R = length ps - length ps div 2

goal (1 subgoal):
 1. nat \<lfloor>real (length ps) / 2\<rfloor> = length XS\<^sub>L &&& nat \<lceil>real (length ps) / 2\<rceil> = length XS\<^sub>R
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
nat \<lfloor>real (length ps) / 2\<rfloor> = length XS\<^sub>L
nat \<lceil>real (length ps) / 2\<rceil> = length XS\<^sub>R

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "length XS\<^sub>L = length YS\<^sub>L" "length XS\<^sub>R = length YS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length XS\<^sub>L = length YS\<^sub>L &&& length XS\<^sub>R = length YS\<^sub>R
[PROOF STEP]
using defs closest_pair_rec_set_length_sorted_snd closest_pair_rec_eq_val_closest_pair_rec_tm
[PROOF STATE]
proof (prove)
using this:
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
Time_Monad.val (closest_pair_rec_tm ?xs) = closest_pair_rec ?xs

goal (1 subgoal):
 1. length XS\<^sub>L = length YS\<^sub>L &&& length XS\<^sub>R = length YS\<^sub>R
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
length XS\<^sub>L = length YS\<^sub>L
length XS\<^sub>R = length YS\<^sub>R

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence L: "?n = length YS\<^sub>L + length YS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L = length YS\<^sub>L
length XS\<^sub>R = length YS\<^sub>R

goal (1 subgoal):
 1. length ps = length YS\<^sub>L + length YS\<^sub>R
[PROOF STEP]
using defs XSLR
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L = length YS\<^sub>L
length XS\<^sub>R = length YS\<^sub>R
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)
XS\<^sub>L = take (length ps div 2) ps
XS\<^sub>R = drop (length ps div 2) ps

goal (1 subgoal):
 1. length ps = length YS\<^sub>L + length YS\<^sub>R
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length ps = length YS\<^sub>L + length YS\<^sub>R

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "1 < length XS\<^sub>L" "length XS\<^sub>L < length ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length ps
[PROOF STEP]
using False XSLR
[PROOF STATE]
proof (prove)
using this:
\<not> length ps \<le> 3
XS\<^sub>L = take (length ps div 2) ps
XS\<^sub>R = drop (length ps div 2) ps

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

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence "time (closest_pair_rec_tm XS\<^sub>L) \<le> closest_pair_recurrence (length XS\<^sub>L)"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length ps

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (length XS\<^sub>L)
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length ps
\<forall>ys. length ys < length ps \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys)

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (length XS\<^sub>L)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (length XS\<^sub>L)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence IHL: "time (closest_pair_rec_tm XS\<^sub>L) \<le> closest_pair_recurrence (nat \<lfloor>real ?n / 2\<rfloor>)"
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (length XS\<^sub>L)

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (length XS\<^sub>L)
nat \<lfloor>real (length ps) / 2\<rfloor> = length XS\<^sub>L
nat \<lceil>real (length ps) / 2\<rceil> = length XS\<^sub>R

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "1 < length XS\<^sub>R" "length XS\<^sub>R < length ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length ps
[PROOF STEP]
using False XSLR
[PROOF STATE]
proof (prove)
using this:
\<not> length ps \<le> 3
XS\<^sub>L = take (length ps div 2) ps
XS\<^sub>R = drop (length ps div 2) ps

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

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence "time (closest_pair_rec_tm XS\<^sub>R) \<le> closest_pair_recurrence (length XS\<^sub>R)"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length ps

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (length XS\<^sub>R)
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length ps
\<forall>ys. length ys < length ps \<longrightarrow> real (time (closest_pair_rec_tm ys)) \<le> closest_pair_recurrence (length ys)

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (length XS\<^sub>R)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (length XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence IHR: "time (closest_pair_rec_tm XS\<^sub>R) \<le> closest_pair_recurrence (nat \<lceil>real ?n / 2\<rceil>)"
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (length XS\<^sub>R)

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (length XS\<^sub>R)
nat \<lfloor>real (length ps) / 2\<rfloor> = length XS\<^sub>L
nat \<lceil>real (length ps) / 2\<rceil> = length XS\<^sub>R

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "(YS, C\<^sub>0, C\<^sub>1) = val (closest_pair_rec_tm ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = Time_Monad.val (closest_pair_rec_tm ps)
[PROOF STEP]
using False closest_pair_rec_simps defs
[PROOF STATE]
proof (prove)
using this:
\<not> length ps \<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) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = Time_Monad.val (closest_pair_rec_tm ps)
[PROOF STEP]
by (auto simp: Let_def length_eq_val_length_tm split!: prod.split)
[PROOF STATE]
proof (state)
this:
(YS, C\<^sub>0, C\<^sub>1) = Time_Monad.val (closest_pair_rec_tm ps)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence "length ps = length YS"
[PROOF STATE]
proof (prove)
using this:
(YS, C\<^sub>0, C\<^sub>1) = Time_Monad.val (closest_pair_rec_tm ps)

goal (1 subgoal):
 1. length ps = length YS
[PROOF STEP]
using closest_pair_rec_set_length_sorted_snd closest_pair_rec_eq_val_closest_pair_rec_tm
[PROOF STATE]
proof (prove)
using this:
(YS, C\<^sub>0, C\<^sub>1) = Time_Monad.val (closest_pair_rec_tm ps)
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
Time_Monad.val (closest_pair_rec_tm ?xs) = closest_pair_rec ?xs

goal (1 subgoal):
 1. length ps = length YS
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ps = length YS

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
hence combine_bound: "time (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 3 + 18 * ?n"
[PROOF STATE]
proof (prove)
using this:
length ps = length YS

goal (1 subgoal):
 1. time (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 3 + 18 * length ps
[PROOF STEP]
using time_combine_tm
[PROOF STATE]
proof (prove)
using this:
length ps = length YS
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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 3 + 18 * length ps
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 3 + 18 * length ps

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (split_at_tm (?n div 2) ps) +
              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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)
[PROOF STEP]
using time_closest_pair_rec_tm_simps_2[OF False] defs
[PROOF STATE]
proof (prove)
using this:
time (closest_pair_rec_tm ps) = 1 + (let (xs\<^sub>L, xs\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps); (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 ps) + time (split_at_tm (length ps div 2) ps) + 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))
(XS\<^sub>L, XS\<^sub>R) = Time_Monad.val (split_at_tm (length ps div 2) ps)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = Time_Monad.val (closest_pair_rec_tm XS\<^sub>L)
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^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)
(C\<^sub>0, C\<^sub>1) = Time_Monad.val (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)
[PROOF STEP]
by (auto simp del: closest_pair_rec_tm.simps simp add: Let_def split: prod.split)
[PROOF STATE]
proof (state)
this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (closest_pair_rec_tm ps) = 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "... \<le> 7 + 21 * ?n + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)
[PROOF STEP]
using time_merge_tm[of "(\<lambda>p. snd p)" YS\<^sub>L YS\<^sub>R] L combine_bound
[PROOF STATE]
proof (prove)
using this:
time (merge_tm snd YS\<^sub>L YS\<^sub>R) \<le> length YS\<^sub>L + length YS\<^sub>R + 1
length ps = length YS\<^sub>L + length YS\<^sub>R
time (combine_tm (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 3 + 18 * length ps

goal (1 subgoal):
 1. 1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)
[PROOF STEP]
by (simp add: time_length_tm time_split_at_tm)
[PROOF STATE]
proof (state)
this:
1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + time (length_tm ps) + time (split_at_tm (length ps div 2) ps) + 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 (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) (fst (hd XS\<^sub>R)) YS) \<le> 7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "... \<le> 7 + 21 * ?n + closest_pair_recurrence (nat \<lfloor>real ?n / 2\<rfloor>) +
              closest_pair_recurrence (nat \<lceil>real ?n / 2\<rceil>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)) \<le> real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)
[PROOF STEP]
using IHL IHR
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm XS\<^sub>L)) \<le> closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>)
real (time (closest_pair_rec_tm XS\<^sub>R)) \<le> closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)

goal (1 subgoal):
 1. real (7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)) \<le> real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)) \<le> real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (7 + 21 * length ps + time (closest_pair_rec_tm XS\<^sub>L) + time (closest_pair_rec_tm XS\<^sub>R)) \<le> real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
have "... = closest_pair_recurrence (length ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>) = closest_pair_recurrence (length ps)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> length ps \<le> 3

goal (1 subgoal):
 1. real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>) = closest_pair_recurrence (length ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (7 + 21 * length ps) + closest_pair_recurrence (nat \<lfloor>real (length ps) / 2\<rfloor>) + closest_pair_recurrence (nat \<lceil>real (length ps) / 2\<rceil>) = closest_pair_recurrence (length ps)

goal (1 subgoal):
 1. \<not> length ps \<le> 3 \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)

goal (1 subgoal):
 1. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem closest_pair_recurrence:
  "closest_pair_recurrence \<in> \<Theta>(\<lambda>n. n * ln n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closest_pair_recurrence \<in> \<Theta>(\<lambda>x. real x * ln (real x))
[PROOF STEP]
by (master_theorem) auto


[STATEMENT]
theorem time_closest_pair_rec_bigo:
  "(\<lambda>xs. time (closest_pair_rec_tm xs)) \<in> O[length going_to at_top]((\<lambda>n. n * ln n) o length)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)
[PROOF STEP]
have 0: "\<And>ps. time (closest_pair_rec_tm ps) \<le> (closest_pair_recurrence o length) ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ps. real (time (closest_pair_rec_tm ps)) \<le> (closest_pair_recurrence \<circ> length) ps
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ps. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
using time_closest_pair_rec_conv_closest_pair_recurrence
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm ?ps)) \<le> closest_pair_recurrence (length ?ps)

goal (1 subgoal):
 1. \<And>ps. real (time (closest_pair_rec_tm ps)) \<le> closest_pair_recurrence (length ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_rec_tm ?ps)) \<le> (closest_pair_recurrence \<circ> length) ?ps

goal (1 subgoal):
 1. (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)
[PROOF STEP]
using bigo_measure_trans[OF 0] bigthetaD1[OF closest_pair_recurrence] of_nat_0_le_iff
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>closest_pair_recurrence \<in> O(?f); \<And>x. x \<in> ?A \<Longrightarrow> 0 \<le> real (time (closest_pair_rec_tm x))\<rbrakk> \<Longrightarrow> (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially within ?A](?f \<circ> length)
closest_pair_recurrence \<in> O(\<lambda>x. real x * ln (real x))
(0::?'a) \<le> of_nat ?n

goal (1 subgoal):
 1. (\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (time (closest_pair_rec_tm x))) \<in> O[length going_to sequentially]((\<lambda>n. real n * ln (real n)) \<circ> length)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma time_closest_pair_conv_closest_pair_recurrence:
  "time (closest_pair_tm ps) \<le> closest_pair_time (length ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (time (closest_pair_tm ps)) \<le> closest_pair_time (length ps)
[PROOF STEP]
unfolding closest_pair_time_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (time (closest_pair_tm ps)) \<le> 1 + mergesort_recurrence (length ps) + closest_pair_recurrence (length ps)
[PROOF STEP]
proof (induction rule: induct_list012)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
case (3 x y zs)
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs)
real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
let ?ps = "x # y # zs"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
define xs where "xs = val (mergesort_tm fst ?ps)"
[PROOF STATE]
proof (state)
this:
xs = Time_Monad.val (mergesort_tm fst (x # y # zs))

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
have *: "length xs = length ?ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length (x # y # zs)
[PROOF STEP]
using xs_def mergesort(3)[of fst ?ps] mergesort_eq_val_mergesort_tm
[PROOF STATE]
proof (prove)
using this:
xs = Time_Monad.val (mergesort_tm fst (x # y # zs))
length (mergesort fst (x # y # zs)) = length (x # y # zs)
Time_Monad.val (mergesort_tm ?f ?xs) = mergesort ?f ?xs

goal (1 subgoal):
 1. length xs = length (x # y # zs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length xs = length (x # y # zs)

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
have "time (closest_pair_tm ?ps) = 1 + time (mergesort_tm fst ?ps) + time (closest_pair_rec_tm xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (closest_pair_tm (x # y # zs)) = 1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)
[PROOF STEP]
using xs_def
[PROOF STATE]
proof (prove)
using this:
xs = Time_Monad.val (mergesort_tm fst (x # y # zs))

goal (1 subgoal):
 1. time (closest_pair_tm (x # y # zs)) = 1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)
[PROOF STEP]
by (auto simp del: mergesort_tm.simps closest_pair_rec_tm.simps simp add: time_simps split: prod.split)
[PROOF STATE]
proof (state)
this:
time (closest_pair_tm (x # y # zs)) = 1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (closest_pair_tm (x # y # zs)) = 1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
have "... \<le> 1 + mergesort_recurrence (length ?ps) + time (closest_pair_rec_tm xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs))
[PROOF STEP]
using time_mergesort_conv_mergesort_recurrence[of fst ?ps]
[PROOF STATE]
proof (prove)
using this:
real (time (mergesort_tm fst (x # y # zs))) \<le> mergesort_recurrence (length (x # y # zs))

goal (1 subgoal):
 1. real (1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs))

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (1 + time (mergesort_tm fst (x # y # zs)) + time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs))

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
have "... \<le> 1 + mergesort_recurrence (length ?ps) + closest_pair_recurrence (length ?ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
using time_closest_pair_rec_conv_closest_pair_recurrence[of xs] *
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_rec_tm xs)) \<le> closest_pair_recurrence (length xs)
length xs = length (x # y # zs)

goal (1 subgoal):
 1. 1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 + mergesort_recurrence (length (x # y # zs)) + real (time (closest_pair_rec_tm xs)) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))

goal (3 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
 3. \<And>x y zs. \<lbrakk>real (time (closest_pair_tm zs)) \<le> 1 + mergesort_recurrence (length zs) + closest_pair_recurrence (length zs); real (time (closest_pair_tm (y # zs))) \<le> 1 + mergesort_recurrence (length (y # zs)) + closest_pair_recurrence (length (y # zs))\<rbrakk> \<Longrightarrow> real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))

goal (1 subgoal):
 1. real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real (time (closest_pair_tm (x # y # zs))) \<le> 1 + mergesort_recurrence (length (x # y # zs)) + closest_pair_recurrence (length (x # y # zs))

goal (2 subgoals):
 1. real (time (closest_pair_tm [])) \<le> 1 + mergesort_recurrence (length []) + closest_pair_recurrence (length [])
 2. \<And>x. real (time (closest_pair_tm [x])) \<le> 1 + mergesort_recurrence (length [x]) + closest_pair_recurrence (length [x])
[PROOF STEP]
qed (auto simp: time_simps)


[STATEMENT]
lemma find_closest_pair_code_dist_eq:
  assumes "\<delta> = dist_code c\<^sub>0 c\<^sub>1" "(\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) ps"
  shows "\<Delta> = dist_code C\<^sub>0 C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<delta> = dist_code c\<^sub>0 c\<^sub>1
(\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) ps

goal (1 subgoal):
 1. \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
proof (induction "(\<delta>, c\<^sub>0, c\<^sub>1)" ps arbitrary: \<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1 rule: find_closest_pair_code.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<And>\<delta> c\<^sub>0 c\<^sub>1 p \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) [p]\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 3. \<And>\<delta> c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<delta> \<le> xa; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<not> \<delta> \<le> xa; xa = dist_code p\<^sub>0 y; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (xa, p\<^sub>0, y) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
case (3 \<delta> c\<^sub>0 c\<^sub>1 p\<^sub>0 p\<^sub>2 ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps)); (?xa, ?y) = ?x; \<delta> \<le> ?xa; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (?\<Delta>, ?C\<^sub>0, ?C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?\<Delta> = dist_code ?C\<^sub>0 ?C\<^sub>1
\<lbrakk>?x = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps)); (?xa, ?y) = ?x; \<not> \<delta> \<le> ?xa; ?xa = dist_code p\<^sub>0 ?y; (?\<Delta>, ?C\<^sub>0, ?C\<^sub>1) = find_closest_pair_code (?xa, p\<^sub>0, ?y) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?\<Delta> = dist_code ?C\<^sub>0 ?C\<^sub>1
\<delta> = dist_code c\<^sub>0 c\<^sub>1
(\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>\<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<And>\<delta> c\<^sub>0 c\<^sub>1 p \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) [p]\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 3. \<And>\<delta> c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<delta> \<le> xa; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<not> \<delta> \<le> xa; xa = dist_code p\<^sub>0 y; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (xa, p\<^sub>0, y) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
obtain \<delta>' p\<^sub>1 where \<delta>'_def: "(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<delta>' p\<^sub>1. (\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (3 subgoals):
 1. \<And>\<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<And>\<delta> c\<^sub>0 c\<^sub>1 p \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) [p]\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 3. \<And>\<delta> c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<delta> \<le> xa; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<not> \<delta> \<le> xa; xa = dist_code p\<^sub>0 y; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (xa, p\<^sub>0, y) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
hence A: "\<delta>' = dist_code p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. \<delta>' = dist_code p\<^sub>0 p\<^sub>1
[PROOF STEP]
using find_closest_bf_code_dist_eq[of "take 7 (p\<^sub>2 # ps)"]
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
\<lbrakk>0 < length (take 7 (p\<^sub>2 # ps)); (?\<delta>, ?c) = find_closest_bf_code ?p (take 7 (p\<^sub>2 # ps))\<rbrakk> \<Longrightarrow> ?\<delta> = dist_code ?p ?c

goal (1 subgoal):
 1. \<delta>' = dist_code p\<^sub>0 p\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<delta>' = dist_code p\<^sub>0 p\<^sub>1

goal (3 subgoals):
 1. \<And>\<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<And>\<delta> c\<^sub>0 c\<^sub>1 p \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) [p]\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 3. \<And>\<delta> c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<delta> \<le> xa; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<And>x xa y \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf_code p\<^sub>0 (take 7 (v # va)); (xa, y) = x; \<not> \<delta> \<le> xa; xa = dist_code p\<^sub>0 y; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (xa, p\<^sub>0, y) (v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
proof (cases "\<delta> \<le> \<delta>'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<delta> \<le> \<delta>'

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
obtain \<Delta>' C\<^sub>0' C\<^sub>1' where \<Delta>'_def: "(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Delta>' C\<^sub>0' C\<^sub>1'. (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases4)
[PROOF STATE]
proof (state)
this:
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
note defs = \<delta>'_def \<Delta>'_def
[PROOF STATE]
proof (state)
this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
hence "\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
[PROOF STEP]
using "3.hyps"(1)[of "(\<delta>', p\<^sub>1)" \<delta>' p\<^sub>1] "3.prems"(1) True \<delta>'_def
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps)); (\<delta>', p\<^sub>1) = (\<delta>', p\<^sub>1); \<delta> \<le> \<delta>'; \<delta> = dist_code c\<^sub>0 c\<^sub>1; (?\<Delta>, ?C\<^sub>0, ?C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?\<Delta> = dist_code ?C\<^sub>0 ?C\<^sub>1
\<delta> = dist_code c\<^sub>0 c\<^sub>1
\<delta> \<le> \<delta>'
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. \<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
have "\<Delta> = \<Delta>'" "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> = \<Delta>' &&& C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using defs True "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<delta> \<le> \<delta>'
(\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<Delta> = \<Delta>' &&& C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps); \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> \<Delta> = \<Delta>'
 2. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps); \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0'
 3. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps); \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (2 subgoals):
 1. \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

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

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<delta> \<le> \<delta>'

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
obtain \<Delta>' C\<^sub>0' C\<^sub>1' where \<Delta>'_def: "(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Delta>' C\<^sub>0' C\<^sub>1'. (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases4)
[PROOF STATE]
proof (state)
this:
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
note defs = \<delta>'_def \<Delta>'_def
[PROOF STATE]
proof (state)
this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
hence "\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
[PROOF STEP]
using "3.hyps"(2)[of "(\<delta>', p\<^sub>1)" \<delta>' p\<^sub>1] A False \<delta>'_def
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps)); (\<delta>', p\<^sub>1) = (\<delta>', p\<^sub>1); \<not> \<delta> \<le> \<delta>'; \<delta>' = dist_code p\<^sub>0 p\<^sub>1; (?\<Delta>, ?C\<^sub>0, ?C\<^sub>1) = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?\<Delta> = dist_code ?C\<^sub>0 ?C\<^sub>1
\<delta>' = dist_code p\<^sub>0 p\<^sub>1
\<not> \<delta> \<le> \<delta>'
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. \<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
have "\<Delta> = \<Delta>'" "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> = \<Delta>' &&& C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using defs False "3.prems"(2)
[PROOF STATE]
proof (prove)
using this:
(\<delta>', p\<^sub>1) = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<not> \<delta> \<le> \<delta>'
(\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<Delta> = \<Delta>' &&& C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps); \<not> \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> \<Delta> = \<Delta>'
 2. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps); \<not> \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0'
 3. \<lbrakk>(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps); \<not> \<delta> \<le> \<delta>'; find_closest_bf_code p\<^sub>0 (p\<^sub>2 # take 6 ps) = (\<delta>', p\<^sub>1); (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. \<not> \<delta> \<le> \<delta>' \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Delta>' = dist_code C\<^sub>0' C\<^sub>1'
\<Delta> = \<Delta>'
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Delta> = dist_code C\<^sub>0 C\<^sub>1

goal (2 subgoals):
 1. \<And>\<delta> c\<^sub>0 c\<^sub>1 \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
 2. \<And>\<delta> c\<^sub>0 c\<^sub>1 p \<Delta> C\<^sub>0 C\<^sub>1. \<lbrakk>\<delta> = dist_code c\<^sub>0 c\<^sub>1; (\<Delta>, C\<^sub>0, C\<^sub>1) = find_closest_pair_code (\<delta>, c\<^sub>0, c\<^sub>1) [p]\<rbrakk> \<Longrightarrow> \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
qed auto