[STATEMENT]
lemma closest_pair_rec_eq_val_closest_pair_rec_tm:
  "val (closest_pair_rec_tm xs) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
proof (induction rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys

goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
define n where "n = length xs"
[PROOF STATE]
proof (state)
this:
n = length xs

goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
obtain xs\<^sub>L xs\<^sub>R where xs_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 (n div 2) xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
(xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs

goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
note defs = n_def xs_def
[PROOF STATE]
proof (state)
this:
n = length xs
(xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs

goal (1 subgoal):
 1. \<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
 2. \<not> ?P \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
assume "n \<le> 3"
[PROOF STATE]
proof (state)
this:
n \<le> 3

goal (2 subgoals):
 1. ?P \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
 2. \<not> ?P \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<le> 3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n \<le> 3

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
using defs
[PROOF STATE]
proof (prove)
using this:
n \<le> 3
n = length xs
(xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
by (auto simp: length_eq_val_length_tm mergesort_eq_val_mergesort_tm
                     closest_pair_bf_eq_val_closest_pair_bf_tm closest_pair_rec.simps)
[PROOF STATE]
proof (state)
this:
Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs

goal (1 subgoal):
 1. \<not> n \<le> 3 \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n \<le> 3 \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
assume asm: "\<not> n \<le> 3"
[PROOF STATE]
proof (state)
this:
\<not> n \<le> 3

goal (1 subgoal):
 1. \<not> n \<le> 3 \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
have "length xs\<^sub>L < length xs" "length xs\<^sub>R < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs\<^sub>L < length xs &&& length xs\<^sub>R < length xs
[PROOF STEP]
using asm defs
[PROOF STATE]
proof (prove)
using this:
\<not> n \<le> 3
n = length xs
(xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs

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

goal (1 subgoal):
 1. \<not> n \<le> 3 \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
hence "val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L"
          "val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
length xs\<^sub>L < length xs
length xs\<^sub>R < length xs

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L &&& Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
length xs\<^sub>L < length xs
length xs\<^sub>R < length xs
\<forall>ys. length ys < length xs \<longrightarrow> Time_Monad.val (closest_pair_rec_tm ys) = closest_pair_rec ys

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L &&& Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L
Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R

goal (1 subgoal):
 1. \<not> n \<le> 3 \<Longrightarrow> Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L
Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
using asm defs
[PROOF STATE]
proof (prove)
using this:
Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L
Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R
\<not> n \<le> 3
n = length xs
(xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs

goal (1 subgoal):
 1. Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs
[PROOF STEP]
apply (subst closest_pair_rec.simps, subst closest_pair_rec_tm.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L; Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R; \<not> n \<le> 3; n = length xs; (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs; Time_Monad.val (closest_pair_rec_tm xs\<^sub>L) = closest_pair_rec xs\<^sub>L; Time_Monad.val (closest_pair_rec_tm xs\<^sub>R) = closest_pair_rec xs\<^sub>R; \<not> n \<le> 3; n = length xs; (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs\<rbrakk> \<Longrightarrow> Time_Monad.val (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) = (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))
[PROOF STEP]
by (auto simp del: closest_pair_rec_tm.simps
               simp add: Let_def length_eq_val_length_tm merge_eq_val_merge_tm
                         split_at_eq_val_split_at_tm combine_eq_val_combine_tm
               split: prod.split)
[PROOF STATE]
proof (state)
this:
Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Time_Monad.val (closest_pair_rec_tm xs) = closest_pair_rec xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_set_length_sorted_snd:
  assumes "(ys, p) = closest_pair_rec xs"
  shows "set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
proof (induction xs arbitrary: ys p rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> set x = set ys \<and> length x = length ys \<and> sorted_snd x); (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> set x = set ys \<and> length x = length ys \<and> sorted_snd x)
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> set x = set ys \<and> length x = length ys \<and> sorted_snd x); (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
let ?n = "length xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> set x = set ys \<and> length x = length ys \<and> sorted_snd x); (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
 2. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
 2. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
using "1.prems" sorted_snd_def
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3
(ys, p) = closest_pair_rec xs
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps

goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
by (auto simp: mergesort closest_pair_rec.simps)
[PROOF STATE]
proof (state)
this:
set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs \<le> 3

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[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> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
define P where "P = combine P\<^sub>L P\<^sub>R L YS"
[PROOF STATE]
proof (state)
this:
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSP\<^sub>L_def YSP\<^sub>R_def YS_def P_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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
have "length XS\<^sub>L < length xs" "length XS\<^sub>R < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length XS\<^sub>L < length xs &&& length XS\<^sub>R < length xs
[PROOF STEP]
using False defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
hence IH: "set XS\<^sub>L = set YS\<^sub>L" "set XS\<^sub>R = set YS\<^sub>R"
              "length XS\<^sub>L = length YS\<^sub>L" "length XS\<^sub>R = length YS\<^sub>R"
              "sorted_snd YS\<^sub>L" "sorted_snd YS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs

goal (1 subgoal):
 1. (set XS\<^sub>L = set YS\<^sub>L &&& set XS\<^sub>R = set YS\<^sub>R &&& length XS\<^sub>L = length YS\<^sub>L) &&& length XS\<^sub>R = length YS\<^sub>R &&& sorted_snd YS\<^sub>L &&& sorted_snd YS\<^sub>R
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs
\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> set x = set ys \<and> length x = length ys \<and> sorted_snd x)
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
have "set xs = set XS\<^sub>L \<union> set XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set XS\<^sub>L \<union> set XS\<^sub>R
[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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. set xs = set XS\<^sub>L \<union> set XS\<^sub>R
[PROOF STEP]
by (auto simp: set_take_drop split_at_take_drop_conv)
[PROOF STATE]
proof (state)
this:
set xs = set XS\<^sub>L \<union> set XS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
hence SET: "set xs = set YS"
[PROOF STATE]
proof (prove)
using this:
set xs = set XS\<^sub>L \<union> set XS\<^sub>R

goal (1 subgoal):
 1. set xs = set YS
[PROOF STEP]
using set_merge IH(1,2) defs
[PROOF STATE]
proof (prove)
using this:
set xs = set XS\<^sub>L \<union> set XS\<^sub>R
set (Common.merge ?f ?xs ?ys) = set ?xs \<union> set ?ys
set XS\<^sub>L = set YS\<^sub>L
set XS\<^sub>R = set YS\<^sub>R
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. set xs = set YS
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
set xs = set YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
have "length xs = length XS\<^sub>L + length XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length XS\<^sub>L + length XS\<^sub>R
[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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
hence LENGTH: "length xs = length YS"
[PROOF STATE]
proof (prove)
using this:
length xs = length XS\<^sub>L + length XS\<^sub>R

goal (1 subgoal):
 1. length xs = length YS
[PROOF STEP]
using IH(3,4) length_merge defs
[PROOF STATE]
proof (prove)
using this:
length xs = length XS\<^sub>L + length XS\<^sub>R
length XS\<^sub>L = length YS\<^sub>L
length XS\<^sub>R = length YS\<^sub>R
length (Common.merge ?f ?xs ?ys) = length ?xs + length ?ys
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
have SORTED: "sorted_snd YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_snd YS
[PROOF STEP]
using IH(5,6)
[PROOF STATE]
proof (prove)
using this:
sorted_snd YS\<^sub>L
sorted_snd YS\<^sub>R

goal (1 subgoal):
 1. sorted_snd YS
[PROOF STEP]
by (simp add: defs sorted_snd_def sorted_merge)
[PROOF STATE]
proof (state)
this:
sorted_snd YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
have "(YS, P) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, P) = 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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. (YS, P) = closest_pair_rec xs
[PROOF STEP]
by (auto simp: Let_def split: prod.split)
[PROOF STATE]
proof (state)
this:
(YS, P) = closest_pair_rec xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
hence "(ys, p) = (YS, P)"
[PROOF STATE]
proof (prove)
using this:
(YS, P) = closest_pair_rec xs

goal (1 subgoal):
 1. (ys, p) = (YS, P)
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
(YS, P) = closest_pair_rec xs
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. (ys, p) = (YS, P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(ys, p) = (YS, P)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(ys, p) = (YS, P)

goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
using SET LENGTH SORTED
[PROOF STATE]
proof (prove)
using this:
(ys, p) = (YS, P)
set xs = set YS
length xs = length YS
sorted_snd YS

goal (1 subgoal):
 1. set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set ys = set xs \<and> length ys = length xs \<and> sorted_snd ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_distinct:
  assumes "distinct xs" "(ys, p) = closest_pair_rec xs"
  shows "distinct ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct xs
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
proof (induction xs arbitrary: ys p rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> distinct x); distinct xs; (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> distinct ys
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> distinct x)
distinct xs
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> distinct x); distinct xs; (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> distinct ys
[PROOF STEP]
let ?n = "length xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys p. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> distinct x); distinct xs; (ys, p) = closest_pair_rec xs\<rbrakk> \<Longrightarrow> distinct ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> distinct ys
 2. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> distinct ys
 2. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3
distinct xs
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
by (auto simp: mergesort closest_pair_rec.simps)
[PROOF STATE]
proof (state)
this:
distinct ys

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs \<le> 3

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

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSP\<^sub>L_def YSP\<^sub>R_def YS_def P_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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
have "length XS\<^sub>L < length xs" "length XS\<^sub>R < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length XS\<^sub>L < length xs &&& length XS\<^sub>R < length xs
[PROOF STEP]
using False defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
have "distinct XS\<^sub>L" "distinct XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct XS\<^sub>L &&& distinct XS\<^sub>R
[PROOF STEP]
using "1.prems"(1) defs
[PROOF STATE]
proof (prove)
using this:
distinct xs
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs
distinct XS\<^sub>L
distinct XS\<^sub>R
[PROOF STEP]
have IH: "distinct YS\<^sub>L" "distinct YS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs
distinct XS\<^sub>L
distinct XS\<^sub>R

goal (1 subgoal):
 1. distinct YS\<^sub>L &&& distinct YS\<^sub>R
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
length XS\<^sub>L < length xs
length XS\<^sub>R < length xs
distinct XS\<^sub>L
distinct XS\<^sub>R
\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa. (x, xa) = closest_pair_rec ys \<longrightarrow> distinct x)
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
have "set XS\<^sub>L \<inter> set XS\<^sub>R = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set XS\<^sub>L \<inter> set XS\<^sub>R = {}
[PROOF STEP]
using "1.prems"(1) defs
[PROOF STATE]
proof (prove)
using this:
distinct xs
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. set XS\<^sub>L \<inter> set XS\<^sub>R = {}
[PROOF STEP]
by (auto simp: split_at_take_drop_conv set_take_disj_set_drop_if_distinct)
[PROOF STATE]
proof (state)
this:
set XS\<^sub>L \<inter> set XS\<^sub>R = {}

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set XS\<^sub>L \<inter> set XS\<^sub>R = {}

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
have "set XS\<^sub>L = set YS\<^sub>L" "set XS\<^sub>R = set YS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set XS\<^sub>L = set YS\<^sub>L &&& set XS\<^sub>R = set YS\<^sub>R
[PROOF STEP]
using closest_pair_rec_set_length_sorted_snd defs
[PROOF STATE]
proof (prove)
using this:
(?ys, ?p) = closest_pair_rec ?xs \<Longrightarrow> set ?ys = set ?xs \<and> length ?ys = length ?xs \<and> sorted_snd ?ys
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set XS\<^sub>L \<inter> set XS\<^sub>R = {}
set XS\<^sub>L = set YS\<^sub>L
set XS\<^sub>R = set YS\<^sub>R
[PROOF STEP]
have "set YS\<^sub>L \<inter> set YS\<^sub>R = {}"
[PROOF STATE]
proof (prove)
using this:
set XS\<^sub>L \<inter> set XS\<^sub>R = {}
set XS\<^sub>L = set YS\<^sub>L
set XS\<^sub>R = set YS\<^sub>R

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
hence DISTINCT: "distinct YS"
[PROOF STATE]
proof (prove)
using this:
set YS\<^sub>L \<inter> set YS\<^sub>R = {}

goal (1 subgoal):
 1. distinct YS
[PROOF STEP]
using distinct_merge IH defs
[PROOF STATE]
proof (prove)
using this:
set YS\<^sub>L \<inter> set YS\<^sub>R = {}
\<lbrakk>set ?xs \<inter> set ?ys = {}; distinct ?xs; distinct ?ys\<rbrakk> \<Longrightarrow> distinct (Common.merge ?f ?xs ?ys)
distinct YS\<^sub>L
distinct YS\<^sub>R
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. distinct YS
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
have "(YS, P) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, P) = 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, P\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, P\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
P = combine P\<^sub>L P\<^sub>R L YS

goal (1 subgoal):
 1. (YS, P) = closest_pair_rec xs
[PROOF STEP]
by (auto simp: Let_def split: prod.split)
[PROOF STATE]
proof (state)
this:
(YS, P) = closest_pair_rec xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
hence "(ys, p) = (YS, P)"
[PROOF STATE]
proof (prove)
using this:
(YS, P) = closest_pair_rec xs

goal (1 subgoal):
 1. (ys, p) = (YS, P)
[PROOF STEP]
using "1.prems"
[PROOF STATE]
proof (prove)
using this:
(YS, P) = closest_pair_rec xs
distinct xs
(ys, p) = closest_pair_rec xs

goal (1 subgoal):
 1. (ys, p) = (YS, P)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
(ys, p) = (YS, P)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> distinct ys
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(ys, p) = (YS, P)

goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
using DISTINCT
[PROOF STATE]
proof (prove)
using this:
(ys, p) = (YS, P)
distinct YS

goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
distinct ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_c0_c1:
  assumes "1 < length xs" "distinct xs" "(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs"
  shows "c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < length xs
distinct xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs

goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb); 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
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb)
1 < length xs
distinct 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> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb); 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
[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> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb); 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
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
 2. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

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

goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
using "1.prems"(1,2) closest_pair_bf_c0_c1
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
1 < length xs
distinct xs
\<lbrakk>1 < length ?ps; (?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf ?ps\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<in> set ?ps
\<lbrakk>1 < length ?ps; (?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf ?ps\<rbrakk> \<Longrightarrow> ?c\<^sub>1 \<in> set ?ps
\<lbrakk>1 < length ?ps; distinct ?ps; (?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf ?ps\<rbrakk> \<Longrightarrow> ?c\<^sub>0 \<noteq> ?c\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs \<le> 3

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have "1 < length XS\<^sub>L" "length XS\<^sub>L < length xs" "distinct XS\<^sub>L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length xs &&& distinct XS\<^sub>L
[PROOF STEP]
using False "1.prems"(2) defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
distinct xs
(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. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length xs &&& distinct XS\<^sub>L
[PROOF STEP]
by (auto simp: split_at_take_drop_conv)
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
hence "C\<^sub>0\<^sub>L \<in> set XS\<^sub>L" "C\<^sub>1\<^sub>L \<in> set XS\<^sub>L" and IHL1: "C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L

goal (1 subgoal):
 1. (C\<^sub>0\<^sub>L \<in> set XS\<^sub>L &&& C\<^sub>1\<^sub>L \<in> set XS\<^sub>L) &&& C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
distinct XS\<^sub>L
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb)
(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. (C\<^sub>0\<^sub>L \<in> set XS\<^sub>L &&& C\<^sub>1\<^sub>L \<in> set XS\<^sub>L) &&& C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>L \<in> set XS\<^sub>L
C\<^sub>1\<^sub>L \<in> set XS\<^sub>L
C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
hence IHL2: "C\<^sub>0\<^sub>L \<in> set xs" "C\<^sub>1\<^sub>L \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>L \<in> set XS\<^sub>L
C\<^sub>1\<^sub>L \<in> set XS\<^sub>L
C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L

goal (1 subgoal):
 1. C\<^sub>0\<^sub>L \<in> set xs &&& C\<^sub>1\<^sub>L \<in> set xs
[PROOF STEP]
using split_at_take_drop_conv in_set_takeD fst_conv defs
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>L \<in> set XS\<^sub>L
C\<^sub>1\<^sub>L \<in> set XS\<^sub>L
C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L
split_at ?n ?xs = (take ?n ?xs, drop ?n ?xs)
?x \<in> set (take ?n ?xs) \<Longrightarrow> ?x \<in> set ?xs
fst (?x1.0, ?x2.0) = ?x1.0
(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. C\<^sub>0\<^sub>L \<in> set xs &&& C\<^sub>1\<^sub>L \<in> set xs
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>L \<in> set xs
C\<^sub>1\<^sub>L \<in> set xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have "1 < length XS\<^sub>R" "length XS\<^sub>R < length xs" "distinct XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length xs &&& distinct XS\<^sub>R
[PROOF STEP]
using False "1.prems"(2) defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
distinct xs
(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. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length xs &&& distinct XS\<^sub>R
[PROOF STEP]
by (auto simp: split_at_take_drop_conv)
[PROOF STATE]
proof (state)
this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
hence "C\<^sub>0\<^sub>R \<in> set XS\<^sub>R" "C\<^sub>1\<^sub>R \<in> set XS\<^sub>R" and IHR1: "C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R

goal (1 subgoal):
 1. (C\<^sub>0\<^sub>R \<in> set XS\<^sub>R &&& C\<^sub>1\<^sub>R \<in> set XS\<^sub>R) &&& C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
distinct XS\<^sub>R
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> distinct ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> xa \<in> set ys \<and> xb \<in> set ys \<and> xa \<noteq> xb)
(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. (C\<^sub>0\<^sub>R \<in> set XS\<^sub>R &&& C\<^sub>1\<^sub>R \<in> set XS\<^sub>R) &&& C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>R \<in> set XS\<^sub>R
C\<^sub>1\<^sub>R \<in> set XS\<^sub>R
C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
hence IHR2: "C\<^sub>0\<^sub>R \<in> set xs" "C\<^sub>1\<^sub>R \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>R \<in> set XS\<^sub>R
C\<^sub>1\<^sub>R \<in> set XS\<^sub>R
C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R

goal (1 subgoal):
 1. C\<^sub>0\<^sub>R \<in> set xs &&& C\<^sub>1\<^sub>R \<in> set xs
[PROOF STEP]
using split_at_take_drop_conv in_set_dropD snd_conv defs
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>R \<in> set XS\<^sub>R
C\<^sub>1\<^sub>R \<in> set XS\<^sub>R
C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R
split_at ?n ?xs = (take ?n ?xs, drop ?n ?xs)
?x \<in> set (drop ?n ?xs) \<Longrightarrow> ?x \<in> set ?xs
snd (?x1.0, ?x2.0) = ?x2.0
(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. C\<^sub>0\<^sub>R \<in> set xs &&& C\<^sub>1\<^sub>R \<in> set xs
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>R \<in> set xs
C\<^sub>1\<^sub>R \<in> set xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[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> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have YS: "set xs = set YS" "distinct YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs = set YS &&& distinct 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
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
set xs = set YS
distinct YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have "C\<^sub>0 \<in> set xs" "C\<^sub>1 \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<in> set xs &&& C\<^sub>1 \<in> set xs
[PROOF STEP]
using combine_set IHL2 IHR2 YS defs
[PROOF STATE]
proof (prove)
using this:
(?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 \<Longrightarrow> ?c\<^sub>0 \<in> set ?ps \<and> ?c\<^sub>1 \<in> set ?ps \<or> ?c\<^sub>0 = ?p\<^sub>0\<^sub>L \<and> ?c\<^sub>1 = ?p\<^sub>1\<^sub>L \<or> ?c\<^sub>0 = ?p\<^sub>0\<^sub>R \<and> ?c\<^sub>1 = ?p\<^sub>1\<^sub>R
C\<^sub>0\<^sub>L \<in> set xs
C\<^sub>1\<^sub>L \<in> set xs
C\<^sub>0\<^sub>R \<in> set xs
C\<^sub>1\<^sub>R \<in> set xs
set xs = set YS
distinct 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. C\<^sub>0 \<in> set xs &&& C\<^sub>1 \<in> set xs
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set xs
C\<^sub>1 \<in> set xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set xs
C\<^sub>1 \<in> set xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have "C\<^sub>0 \<noteq> C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
using combine_c0_ne_c1 IHL1(1) IHR1(1) YS defs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p\<^sub>0\<^sub>L \<noteq> ?p\<^sub>1\<^sub>L; ?p\<^sub>0\<^sub>R \<noteq> ?p\<^sub>1\<^sub>R; distinct ?ps; (?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> ?c\<^sub>0 \<noteq> ?c\<^sub>1
C\<^sub>0\<^sub>L \<noteq> C\<^sub>1\<^sub>L
C\<^sub>0\<^sub>R \<noteq> C\<^sub>1\<^sub>R
set xs = set YS
distinct 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. C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<noteq> C\<^sub>1

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0 \<in> set xs
C\<^sub>1 \<in> set xs
C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set xs
C\<^sub>1 \<in> set xs
C\<^sub>0 \<noteq> C\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
using "1.prems"(3) *
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set xs
C\<^sub>1 \<in> set xs
C\<^sub>0 \<noteq> C\<^sub>1
(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. c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
by (metis Pair_inject)
[PROOF STATE]
proof (state)
this:
c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c\<^sub>0 \<in> set xs \<and> c\<^sub>1 \<in> set xs \<and> c\<^sub>0 \<noteq> c\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed