[STATEMENT]
lemma find_closest_pair_c0_ne_c1:
  "c\<^sub>0 \<noteq> c\<^sub>1 \<Longrightarrow> distinct ps \<Longrightarrow> (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
proof (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 rule: find_closest_pair.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> x; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>0 # v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
case (3 c\<^sub>0 c\<^sub>1 p\<^sub>0 p\<^sub>2 ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>2 # ps); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<noteq> ?C\<^sub>1
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> ?x; distinct (p\<^sub>2 # ps); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<noteq> ?C\<^sub>1
c\<^sub>0 \<noteq> c\<^sub>1
distinct (p\<^sub>0 # p\<^sub>2 # ps)
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> x; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>0 # v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> x; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>0 # v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
hence "p\<^sub>1 \<in> set (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (p\<^sub>2 # ps)
[PROOF STEP]
using find_closest_bf_set[of "take 7 (p\<^sub>2 # ps)"] in_set_takeD
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
0 < length (take 7 (p\<^sub>2 # ps)) \<Longrightarrow> find_closest_bf ?p (take 7 (p\<^sub>2 # ps)) \<in> set (take 7 (p\<^sub>2 # ps))
?x \<in> set (take ?n ?xs) \<Longrightarrow> ?x \<in> set ?xs

goal (1 subgoal):
 1. p\<^sub>1 \<in> set (p\<^sub>2 # ps)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p\<^sub>1 \<in> set (p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> x; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>0 # v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
hence A: "p\<^sub>0 \<noteq> p\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 \<in> set (p\<^sub>2 # ps)

goal (1 subgoal):
 1. p\<^sub>0 \<noteq> p\<^sub>1
[PROOF STEP]
using "3.prems"(1,2)
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 \<in> set (p\<^sub>2 # ps)
c\<^sub>0 \<noteq> c\<^sub>1
distinct (p\<^sub>0 # p\<^sub>2 # ps)

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

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> x; distinct (v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1; c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>0 # v # va); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
proof (cases "dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
hence "C\<^sub>0' \<noteq> C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0' \<noteq> C\<^sub>1'
[PROOF STEP]
using "3.hyps"(1) "3.prems"(1,2) True p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); c\<^sub>0 \<noteq> c\<^sub>1; distinct (p\<^sub>2 # ps); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<noteq> ?C\<^sub>1
c\<^sub>0 \<noteq> c\<^sub>1
distinct (p\<^sub>0 # p\<^sub>2 # ps)
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

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

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0' \<noteq> C\<^sub>1'

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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 defs True "3.prems"(3)
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^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) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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 (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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 simp
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<noteq> C\<^sub>1

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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 (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
hence "C\<^sub>0' \<noteq> C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0' \<noteq> C\<^sub>1'
[PROOF STEP]
using "3.hyps"(2) "3.prems"(2) A False p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); p\<^sub>0 \<noteq> ?x; distinct (p\<^sub>2 # ps); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 \<noteq> ?C\<^sub>1
distinct (p\<^sub>0 # p\<^sub>2 # ps)
p\<^sub>0 \<noteq> p\<^sub>1
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

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

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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 defs False "3.prems"(3)
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 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) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> 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 simp
[PROOF STATE]
proof (state)
this:
C\<^sub>0 \<noteq> C\<^sub>1

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

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct []; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. \<lbrakk>c\<^sub>0 \<noteq> c\<^sub>1; distinct [uu_]; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 \<noteq> C\<^sub>1
[PROOF STEP]
qed auto


[STATEMENT]
lemma find_closest_pair_dist_mono:
  assumes "(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps"
  shows "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 assms
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps

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]
proof (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 rule: find_closest_pair.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<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))
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<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)); \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x 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) (p\<^sub>0 # v # va)\<rbrakk> \<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))
[PROOF STEP]
case (3 c\<^sub>0 c\<^sub>1 p\<^sub>0 p\<^sub>2 ps)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<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))
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> dist (case ?C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x 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) (p\<^sub>0 # p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<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))
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<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)); \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x 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) (p\<^sub>0 # v # va)\<rbrakk> \<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))
[PROOF STEP]
define p\<^sub>1 where p\<^sub>1_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<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))
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va C\<^sub>0 C\<^sub>1. \<lbrakk>\<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<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)); \<And>x C\<^sub>0 C\<^sub>1. \<lbrakk>x = find_closest_bf p\<^sub>0 (take 7 (v # va)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case x 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) (p\<^sub>0 # v # va)\<rbrakk> \<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))
[PROOF STEP]
show ?case
[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]
proof (cases "dist c\<^sub>0 c\<^sub>1 \<le> dist p\<^sub>0 p\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
case True
[PROOF STATE]
proof (state)
this:
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
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) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
hence "dist C\<^sub>0' C\<^sub>1' \<le> dist c\<^sub>0 c\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

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 "3.hyps"(1) True p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<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))
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (1 subgoal):
 1. dist (case C\<^sub>0' of (x, y) \<Rightarrow> (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 simp
[PROOF STATE]
proof (state)
this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
moreover
[PROOF STATE]
proof (state)
this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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 "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 True "3.prems"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^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) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1c, x2c), x1b, x2b) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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 (2 subgoals):
 1. dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<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))
 2. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
ultimately
[PROOF STATE]
proof (chain)
picking 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))
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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>0'
C\<^sub>1 = C\<^sub>1'

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 simp
[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. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
obtain C\<^sub>0' C\<^sub>1' where C'_def: "(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0' C\<^sub>1'. (C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
note defs = p\<^sub>1_def C'_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
hence "dist C\<^sub>0' C\<^sub>1' \<le> dist p\<^sub>0 p\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)

goal (1 subgoal):
 1. dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
[PROOF STEP]
using "3.hyps"(2) False p\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<lbrakk>?x = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> dist (case ?C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?x of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))

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

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
moreover
[PROOF STATE]
proof (state)
this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (1 subgoal):
 1. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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 "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 False "3.prems"(1)
[PROOF STATE]
proof (prove)
using this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0', C\<^sub>1') = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
apply (auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 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) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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'
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0', C\<^sub>1') = find_closest_pair ((x1a, x2a), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1a, x2a) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1a, x2a); c\<^sub>1 = (x1b, x2b); c\<^sub>0 = (x1c, x2c); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) \<le> 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. \<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (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]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'

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 False
[PROOF STATE]
proof (prove)
using this:
dist (case C\<^sub>0' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1' of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
\<not> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case p\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

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 simp
[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:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [] \<Longrightarrow> dist (case C\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) \<le> dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ C\<^sub>0 C\<^sub>1. (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_] \<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))
[PROOF STEP]
qed auto