[STATEMENT]
lemma combine_eq_val_combine_tm:
  "val (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Time_Monad.val (combine_tm (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps) = combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps
[PROOF STEP]
by (auto simp: filter_eq_val_filter_tm find_closest_pair_eq_val_find_closest_pair_tm)


[STATEMENT]
lemma combine_set:
  assumes "(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"
  shows "(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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 \<in> set ps \<and> c\<^sub>1 \<in> set ps \<or> c\<^sub>0 = 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
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 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
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = (if dist p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L < dist p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

goal (1 subgoal):
 1. 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
[PROOF STEP]
define ps' where ps'_def: "ps' = filter (\<lambda>p. dist p (l, snd p) < dist C\<^sub>0' C\<^sub>1') ps"
[PROOF STATE]
proof (state)
this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

goal (1 subgoal):
 1. 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
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 where C_def: "(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. 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
[PROOF STEP]
note defs = C'_def ps'_def C_def
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'

goal (1 subgoal):
 1. c\<^sub>0 \<in> set ps \<and> c\<^sub>1 \<in> set ps \<or> c\<^sub>0 = 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
[PROOF STEP]
have "(C\<^sub>0 \<in> set ps' \<and> C\<^sub>1 \<in> set ps') \<or> (C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<in> set ps' \<and> C\<^sub>1 \<in> set ps' \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using C_def find_closest_pair_set
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> ?C\<^sub>0 \<in> set ?ps \<and> ?C\<^sub>1 \<in> set ?ps \<or> ?C\<^sub>0 = ?c\<^sub>0 \<and> ?C\<^sub>1 = ?c\<^sub>1

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

goal (1 subgoal):
 1. 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
[PROOF STEP]
hence "(C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps)\<or> (C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1')"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set ps' \<and> C\<^sub>1 \<in> set ps' \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using ps'_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set ps' \<and> C\<^sub>1 \<in> set ps' \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

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

goal (1 subgoal):
 1. 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
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. 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
[PROOF STEP]
have "C\<^sub>0 = c\<^sub>0" "C\<^sub>1 = c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
using assms 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
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'

goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
apply (auto split: if_splits prod.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b)\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 3. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b)\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
 4. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. 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
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<in> set 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
[PROOF STEP]
using C'_def
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<in> set ps \<and> C\<^sub>1 \<in> set ps \<or> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma combine_c0_ne_c1:
  assumes "p\<^sub>0\<^sub>L \<noteq> p\<^sub>1\<^sub>L" "p\<^sub>0\<^sub>R \<noteq> p\<^sub>1\<^sub>R" "distinct ps"
  assumes "(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"
  shows "c\<^sub>0 \<noteq> c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = (if dist p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L < dist p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
define ps' where ps'_def: "ps' = filter (\<lambda>p. dist p (l, snd p) < dist C\<^sub>0' C\<^sub>1') ps"
[PROOF STATE]
proof (state)
this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 where C_def: "(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
note defs = C'_def ps'_def C_def
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'

goal (1 subgoal):
 1. 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 defs find_closest_pair_c0_ne_c1[of C\<^sub>0' C\<^sub>1' ps'] assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'
\<lbrakk>C\<^sub>0' \<noteq> C\<^sub>1'; distinct ps'; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<noteq> ?C\<^sub>1
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

goal (1 subgoal):
 1. C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<noteq> C\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<noteq> C\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
have "C\<^sub>0 = c\<^sub>0" "C\<^sub>1 = c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
using assms defs
[PROOF STATE]
proof (prove)
using this:
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
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'

goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
apply (auto split: if_splits prod.splits)
[PROOF STATE]
proof (prove)
goal (16 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x1a \<noteq> x1; x1c \<noteq> x1b\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x1a \<noteq> x1; x2c \<noteq> x2b\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 3. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x2a \<noteq> x2; x1c \<noteq> x1b\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 4. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x2a \<noteq> x2; x2c \<noteq> x2b\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 5. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2); x1c \<noteq> x1b; x1a \<noteq> x1\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 6. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2); x1c \<noteq> x1b; x2a \<noteq> x2\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 7. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2); x2c \<noteq> x2b; x1a \<noteq> x1\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 8. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2); x2c \<noteq> x2b; x2a \<noteq> x2\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 9. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x1a \<noteq> x1; x1c \<noteq> x1b\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
 10. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); distinct ps; p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b); x1a \<noteq> x1; x2c \<noteq> x2b\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
A total of 16 subgoals...
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 \<noteq> c\<^sub>1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0 \<noteq> C\<^sub>1
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 \<noteq> C\<^sub>1
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma combine_dist:
  assumes "distinct ps" "sorted_snd ps" "set ps = ps\<^sub>L \<union> ps\<^sub>R"
  assumes "\<forall>p \<in> ps\<^sub>L. fst p \<le> l" "\<forall>p \<in> ps\<^sub>R. l \<le> fst p"
  assumes "sparse (dist p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L) ps\<^sub>L" "sparse (dist p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R) ps\<^sub>R"
  assumes "(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"
  shows "sparse (dist c\<^sub>0 c\<^sub>1) (set ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = (if dist p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L < dist p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
define ps' where ps'_def: "ps' = filter (\<lambda>p. dist p (l, snd p) < dist C\<^sub>0' C\<^sub>1') ps"
[PROOF STATE]
proof (state)
this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
define PS\<^sub>L where PS\<^sub>L_def: "PS\<^sub>L = { p \<in> ps\<^sub>L. dist p (l, snd p) < dist C\<^sub>0' C\<^sub>1' }"
[PROOF STATE]
proof (state)
this:
PS\<^sub>L = {p \<in> ps\<^sub>L. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
define PS\<^sub>R where PS\<^sub>R_def: "PS\<^sub>R = { p \<in> ps\<^sub>R. dist p (l, snd p) < dist C\<^sub>0' C\<^sub>1' }"
[PROOF STATE]
proof (state)
this:
PS\<^sub>R = {p \<in> ps\<^sub>R. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}

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

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
note defs = C'_def ps'_def PS\<^sub>L_def PS\<^sub>R_def C_def
[PROOF STATE]
proof (state)
this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
PS\<^sub>L = {p \<in> ps\<^sub>L. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
PS\<^sub>R = {p \<in> ps\<^sub>R. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have EQ: "C\<^sub>0 = c\<^sub>0" "C\<^sub>1 = c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
using defs assms(8)
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
PS\<^sub>L = {p \<in> ps\<^sub>L. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
PS\<^sub>R = {p \<in> ps\<^sub>R. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') 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

goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
apply (auto split: if_splits prod.splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); PS\<^sub>L = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>L \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; PS\<^sub>R = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>R \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); (c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b)\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); PS\<^sub>L = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>L \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; PS\<^sub>R = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>R \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); (c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 3. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>L = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>L = (x1a, x2a); PS\<^sub>L = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>L \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; PS\<^sub>R = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>R \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); (c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>R = (x1b, x2b); p\<^sub>0\<^sub>R = (x1c, x2c); dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b)\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
 4. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>C\<^sub>0' = (x1a, x2a); C\<^sub>1' = (x1, x2); p\<^sub>1\<^sub>R = (x1, x2); ps' = filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps; p\<^sub>0\<^sub>R = (x1a, x2a); PS\<^sub>L = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>L \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; PS\<^sub>R = {p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> (x1b, x2b) \<in> ps\<^sub>R \<and> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)}; (C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); (c\<^sub>0, c\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (filter (\<lambda>p. \<forall>x1b x2b. p = (x1b, x2b) \<longrightarrow> dist (real_of_int x1b, real_of_int x2b) (real_of_int l, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)) ps); p\<^sub>1\<^sub>L = (x1b, x2b); p\<^sub>0\<^sub>L = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) < dist (real_of_int x1a, real_of_int x2a) (real_of_int x1, real_of_int x2)\<rbrakk> \<Longrightarrow> C\<^sub>1 = c\<^sub>1
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have ps': "ps' = filter (\<lambda>p. l - dist C\<^sub>0' C\<^sub>1' < fst p \<and> fst p < l + dist C\<^sub>0' C\<^sub>1') ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps' = filter (\<lambda>p. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
[PROOF STEP]
using ps'_def dist_transform
[PROOF STATE]
proof (prove)
using this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
(dist (case ?p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (?l, snd ?p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < ?\<delta>) = (real_of_int ?l - ?\<delta> < real_of_int (fst ?p) \<and> real_of_int (fst ?p) < real_of_int ?l + ?\<delta>)

goal (1 subgoal):
 1. ps' = filter (\<lambda>p. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ps' = filter (\<lambda>p. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have ps\<^sub>L: "sparse (dist C\<^sub>0' C\<^sub>1') ps\<^sub>L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L
[PROOF STEP]
using assms(6,8) C'_def sparse_def
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L
(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
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
sparse ?\<delta> ?ps = (\<forall>p\<^sub>0\<in>?ps. \<forall>p\<^sub>1\<in>?ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> ?\<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)))

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L
[PROOF STEP]
apply (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<And>\<delta> ps. sparse \<delta> ps = (\<forall>p\<^sub>0\<in>ps. \<forall>p\<^sub>1\<in>ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> \<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))); \<forall>p\<^sub>0\<in>ps\<^sub>L. \<forall>p\<^sub>1\<in>ps\<^sub>L. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<not> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (c\<^sub>0, c\<^sub>1) = find_closest_pair (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l, real_of_int (snd p)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps); (a, b) \<in> ps\<^sub>L; (aa, ba) \<in> ps\<^sub>L; C\<^sub>0' = p\<^sub>0\<^sub>R; C\<^sub>1' = p\<^sub>1\<^sub>R; \<not> dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (real_of_int a, real_of_int b) (real_of_int aa, real_of_int ba)\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba. \<lbrakk>\<And>\<delta> ps. sparse \<delta> ps = (\<forall>p\<^sub>0\<in>ps. \<forall>p\<^sub>1\<in>ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> \<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))); \<forall>p\<^sub>0\<in>ps\<^sub>L. \<forall>p\<^sub>1\<in>ps\<^sub>L. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<not> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (c\<^sub>0, c\<^sub>1) = find_closest_pair (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (real_of_int l, real_of_int (snd p)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps); (a, b) \<in> ps\<^sub>L; (aa, ba) \<in> ps\<^sub>L; C\<^sub>0' = p\<^sub>0\<^sub>R; C\<^sub>1' = p\<^sub>1\<^sub>R; \<not> dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (real_of_int a, real_of_int b) (real_of_int aa, real_of_int ba)\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
hence PS\<^sub>L: "sparse (dist C\<^sub>0' C\<^sub>1') PS\<^sub>L"
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>L
[PROOF STEP]
using PS\<^sub>L_def
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L
PS\<^sub>L = {p \<in> ps\<^sub>L. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have ps\<^sub>R: "sparse (dist C\<^sub>0' C\<^sub>1') ps\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R
[PROOF STEP]
using assms(5,7) C'_def sparse_def
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>ps\<^sub>R. l \<le> fst p
sparse (dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R
(C\<^sub>0', C\<^sub>1') = (if dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) then (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
sparse ?\<delta> ?ps = (\<forall>p\<^sub>0\<in>?ps. \<forall>p\<^sub>1\<in>?ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> ?\<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)))

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R
[PROOF STEP]
apply (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>\<And>\<delta> ps. sparse \<delta> ps = (\<forall>p\<^sub>0\<in>ps. \<forall>p\<^sub>1\<in>ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> \<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))); \<forall>p\<in>ps\<^sub>R. l \<le> fst p; \<forall>p\<^sub>0\<in>ps\<^sub>R. \<forall>p\<^sub>1\<in>ps\<^sub>R. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (a, b) \<in> ps\<^sub>R; (aa, ba) \<in> ps\<^sub>R; C\<^sub>0' = p\<^sub>0\<^sub>L; C\<^sub>1' = p\<^sub>1\<^sub>L; \<not> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (real_of_int a, real_of_int b) (real_of_int aa, real_of_int ba)\<rbrakk> \<Longrightarrow> a = aa
 2. \<And>a b aa ba. \<lbrakk>\<And>\<delta> ps. sparse \<delta> ps = (\<forall>p\<^sub>0\<in>ps. \<forall>p\<^sub>1\<in>ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> \<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))); \<forall>p\<in>ps\<^sub>R. l \<le> fst p; \<forall>p\<^sub>0\<in>ps\<^sub>R. \<forall>p\<^sub>1\<in>ps\<^sub>R. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case p\<^sub>0\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>R of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (a, b) \<in> ps\<^sub>R; (aa, ba) \<in> ps\<^sub>R; C\<^sub>0' = p\<^sub>0\<^sub>L; C\<^sub>1' = p\<^sub>1\<^sub>L; \<not> dist (case p\<^sub>0\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1\<^sub>L of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (real_of_int a, real_of_int b) (real_of_int aa, real_of_int ba)\<rbrakk> \<Longrightarrow> b = ba
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
hence PS\<^sub>R: "sparse (dist C\<^sub>0' C\<^sub>1') PS\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>R
[PROOF STEP]
using PS\<^sub>R_def
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R
PS\<^sub>R = {p \<in> ps\<^sub>R. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "sorted_snd ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_snd ps'
[PROOF STEP]
using ps'_def assms(2) sorted_snd_def sorted_wrt_filter
[PROOF STATE]
proof (prove)
using this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
sorted_snd ps
sorted_snd ?ps = sorted_wrt (\<lambda>p\<^sub>0 p\<^sub>1. snd p\<^sub>0 \<le> snd p\<^sub>1) ?ps
sorted_wrt ?f ?xs \<Longrightarrow> sorted_wrt ?f (filter ?P ?xs)

goal (1 subgoal):
 1. sorted_snd ps'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sorted_snd ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sorted_snd ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "distinct ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ps'
[PROOF STEP]
using ps'_def assms(1) distinct_filter
[PROOF STATE]
proof (prove)
using this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
distinct ps
distinct ?xs \<Longrightarrow> distinct (filter ?P ?xs)

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "set ps' = PS\<^sub>L \<union> PS\<^sub>R "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ps' = PS\<^sub>L \<union> PS\<^sub>R
[PROOF STEP]
using ps'_def PS\<^sub>L_def PS\<^sub>R_def assms(3) filter_Un
[PROOF STATE]
proof (prove)
using this:
ps' = filter (\<lambda>p. dist (case p of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
PS\<^sub>L = {p \<in> ps\<^sub>L. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
PS\<^sub>R = {p \<in> ps\<^sub>R. dist (case case p of (x, y) \<Rightarrow> (real_of_int x, y) of (x, y) \<Rightarrow> (x, real_of_int y)) (case (l, snd p) of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))}
set ps = ps\<^sub>L \<union> ps\<^sub>R
set ?xs = ?A \<union> ?B \<Longrightarrow> set (filter ?P ?xs) = {x \<in> ?A. ?P x} \<union> {x \<in> ?B. ?P x}

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set ps' = PS\<^sub>L \<union> PS\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "0 \<le> dist C\<^sub>0' C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "\<forall>p \<in> set ps'. l - dist C\<^sub>0' C\<^sub>1' \<le> fst p \<and> fst p \<le> l + dist C\<^sub>0' C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using ps'
[PROOF STATE]
proof (prove)
using this:
ps' = filter (\<lambda>p. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps

goal (1 subgoal):
 1. \<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sorted_snd ps'
distinct ps'
set ps' = PS\<^sub>L \<union> PS\<^sub>R
0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
have *: "sparse (dist C\<^sub>0 C\<^sub>1) (set ps')"
[PROOF STATE]
proof (prove)
using this:
sorted_snd ps'
distinct ps'
set ps' = PS\<^sub>L \<union> PS\<^sub>R
0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps')
[PROOF STEP]
using find_closest_pair_dist[of ps' PS\<^sub>L PS\<^sub>R "dist C\<^sub>0' C\<^sub>1'" l C\<^sub>0' C\<^sub>1'] C_def PS\<^sub>L PS\<^sub>R
[PROOF STATE]
proof (prove)
using this:
sorted_snd ps'
distinct ps'
set ps' = PS\<^sub>L \<union> PS\<^sub>R
0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<lbrakk>sorted_snd ps'; distinct ps'; set ps' = PS\<^sub>L \<union> PS\<^sub>R; 0 \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<forall>p\<in>set ps'. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> real_of_int (fst p) \<and> real_of_int (fst p) \<le> real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<forall>p\<in>PS\<^sub>L. fst p \<le> l; \<forall>p\<in>PS\<^sub>R. l \<le> fst p; sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>L; sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>R; dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'\<rbrakk> \<Longrightarrow> sparse (dist (case ?C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps')
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>L
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) PS\<^sub>R

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps')
[PROOF STEP]
by (simp add: PS\<^sub>L_def PS\<^sub>R_def assms(4,5))
[PROOF STATE]
proof (state)
this:
sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps')

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "\<forall>p\<^sub>0 \<in> set ps. \<forall>p\<^sub>1 \<in> set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist p\<^sub>0 p\<^sub>1 < dist C\<^sub>0' C\<^sub>1' \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'
[PROOF STEP]
using set_band_filter ps' ps\<^sub>L ps\<^sub>R assms(3,4,5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?p\<^sub>0 \<in> set ?ps; ?p\<^sub>1 \<in> set ?ps; ?p\<^sub>0 \<noteq> ?p\<^sub>1; dist (case ?p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < ?\<delta>; set ?ps = ?ps\<^sub>L \<union> ?ps\<^sub>R; sparse ?\<delta> ?ps\<^sub>L; sparse ?\<delta> ?ps\<^sub>R; \<forall>p\<in>?ps\<^sub>L. fst p \<le> ?l; \<forall>p\<in>?ps\<^sub>R. ?l \<le> fst p; ?ps' = filter (\<lambda>p. real_of_int ?l - ?\<delta> < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int ?l + ?\<delta>) ?ps\<rbrakk> \<Longrightarrow> ?p\<^sub>0 \<in> set ?ps' \<and> ?p\<^sub>1 \<in> set ?ps'
ps' = filter (\<lambda>p. real_of_int l - dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < real_of_int (fst p) \<and> real_of_int (fst p) < real_of_int l + dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>L
sparse (dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps\<^sub>R
set ps = ps\<^sub>L \<union> ps\<^sub>R
\<forall>p\<in>ps\<^sub>L. fst p \<le> l
\<forall>p\<in>ps\<^sub>R. l \<le> fst p

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
have "dist C\<^sub>0 C\<^sub>1 \<le> dist C\<^sub>0' C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using C_def find_closest_pair_dist_mono
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0', C\<^sub>1') ps'
(?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps \<Longrightarrow> dist (case ?C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case ?c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

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

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

goal (1 subgoal):
 1. \<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
hence "sparse (dist C\<^sub>0 C\<^sub>1) (set ps)"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'

goal (1 subgoal):
 1. sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
using sparse_def *
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<^sub>0\<in>set ps. \<forall>p\<^sub>1\<in>set ps. p\<^sub>0 \<noteq> p\<^sub>1 \<and> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) < dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<longrightarrow> p\<^sub>0 \<in> set ps' \<and> p\<^sub>1 \<in> set ps'
sparse ?\<delta> ?ps = (\<forall>p\<^sub>0\<in>?ps. \<forall>p\<^sub>1\<in>?ps. p\<^sub>0 \<noteq> p\<^sub>1 \<longrightarrow> ?\<delta> \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)))
sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps')

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

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)

goal (1 subgoal):
 1. sparse (dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
[PROOF STEP]
using EQ
[PROOF STATE]
proof (prove)
using this:
sparse (dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) (set ps)
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_simps:
  assumes "n = length xs" "\<not> (n \<le> 3)"
  shows "closest_pair_rec xs = (
    let (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs in
    let (ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) = closest_pair_rec xs\<^sub>L in
    let (ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) = closest_pair_rec xs\<^sub>R in
    let ys = 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 STATE]
proof (prove)
goal (1 subgoal):
 1. 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))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n = length xs
\<not> n \<le> 3

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