[STATEMENT]
lemma find_closest_pair_code_eq:
  assumes "\<delta> = dist c\<^sub>0 c\<^sub>1" "\<delta>' = dist_code c\<^sub>0 c\<^sub>1"
  assumes "(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps"
  assumes "(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) ps"
  shows "C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<delta>' = dist_code c\<^sub>0 c\<^sub>1
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) ps
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) ps

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
proof (induction "(c\<^sub>0, c\<^sub>1)" ps arbitrary: \<delta> \<delta>' c\<^sub>0 c\<^sub>1 C\<^sub>0 C\<^sub>1 \<Delta>' 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 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = 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)); \<delta>' = dist_code p\<^sub>0 x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = 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)); ?\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); ?\<delta>' = dist_code 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); (?\<Delta>', ?C\<^sub>0', ?C\<^sub>1') = find_closest_pair_code (?\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 = ?C\<^sub>0' \<and> ?C\<^sub>1 = ?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)); ?\<delta> = 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)); ?\<delta>' = dist_code p\<^sub>0 ?x; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, ?x) (p\<^sub>2 # ps); (?\<Delta>', ?C\<^sub>0', ?C\<^sub>1') = find_closest_pair_code (?\<delta>', p\<^sub>0, ?x) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 = ?C\<^sub>0' \<and> ?C\<^sub>1 = ?C\<^sub>1'
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<delta>' = dist_code c\<^sub>0 c\<^sub>1
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = 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)); \<delta>' = dist_code p\<^sub>0 x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
obtain p\<^sub>1 \<delta>\<^sub>p' p\<^sub>1' where \<delta>\<^sub>p_def: "p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
    "(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p\<^sub>1 \<delta>\<^sub>p' p\<^sub>1'. \<lbrakk>p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps)); (\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surj_pair)
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = 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)); \<delta>' = dist_code p\<^sub>0 x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
hence A: "\<delta>\<^sub>p' = dist_code 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))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))

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

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

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = 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)); \<delta>' = dist_code p\<^sub>0 x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
have B: "p\<^sub>1 = p\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<^sub>1 = p\<^sub>1'
[PROOF STEP]
using "3.prems"(1,2,3) \<delta>\<^sub>p_def find_closest_bf_code_eq
[PROOF STATE]
proof (prove)
using this:
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<delta>' = dist_code c\<^sub>0 c\<^sub>1
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
\<lbrakk>0 < length ?ps; ?c = find_closest_bf ?p ?ps; (?\<delta>', ?c') = find_closest_bf_code ?p ?ps\<rbrakk> \<Longrightarrow> ?c = ?c'

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

goal (3 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 3. \<And>c\<^sub>0 c\<^sub>1 p\<^sub>0 v va \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<And>x \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' 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)); \<delta> = 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)); \<delta>' = dist_code p\<^sub>0 x; (C\<^sub>0, C\<^sub>1) = find_closest_pair (p\<^sub>0, x) (v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', p\<^sub>0, x) (v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'; \<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va); (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # v # va)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
proof (cases "\<delta> \<le> dist p\<^sub>0 p\<^sub>1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<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 (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
hence C: "\<delta>' \<le> \<delta>\<^sub>p'"
[PROOF STATE]
proof (prove)
using this:
\<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. \<delta>' \<le> \<delta>\<^sub>p'
[PROOF STEP]
by (simp add: "3.prems"(1,2) A B dist_eq_dist_code_le)
[PROOF STATE]
proof (state)
this:
\<delta>' \<le> \<delta>\<^sub>p'

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
obtain C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i' where \<Delta>\<^sub>i_def:
      "(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)"
      "(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'. \<lbrakk>(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps); (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
note defs = \<delta>\<^sub>p_def \<Delta>\<^sub>i_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
have "C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
[PROOF STEP]
using "3.hyps"(1)[of p\<^sub>1] "3.prems" True defs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p\<^sub>1 = 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 p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); ?\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); ?\<delta>' = dist_code 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); (?\<Delta>', ?C\<^sub>0', ?C\<^sub>1') = find_closest_pair_code (?\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 = ?C\<^sub>0' \<and> ?C\<^sub>1 = ?C\<^sub>1'
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<delta>' = dist_code c\<^sub>0 c\<^sub>1
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
\<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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)

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

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
have "C\<^sub>0 = C\<^sub>0\<^sub>i" "C\<^sub>1 = C\<^sub>1\<^sub>i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0\<^sub>i &&& C\<^sub>1 = C\<^sub>1\<^sub>i
[PROOF STEP]
using defs(1,3) True "3.prems"(1,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\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>2 # ps)
\<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))
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (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) (p\<^sub>0 # p\<^sub>2 # ps)

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0\<^sub>i &&& C\<^sub>1 = C\<^sub>1\<^sub>i
[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), x1a, x2a) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair ((x1c, x2c), x1a, x2a) (p\<^sub>2 # ps); find_closest_bf (x1b, x2b) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1b, x2b); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a) \<le> dist (real_of_int x1b, real_of_int x2b) (real_of_int x1, real_of_int x2); c\<^sub>1 = (x1a, x2a); c\<^sub>0 = (x1c, x2c); \<delta> = dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0\<^sub>i
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1c, x2c), x1a, x2a) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair ((x1c, x2c), x1a, x2a) (p\<^sub>2 # ps); find_closest_bf (x1b, x2b) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1b, x2b); dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a) \<le> dist (real_of_int x1b, real_of_int x2b) (real_of_int x1, real_of_int x2); c\<^sub>1 = (x1a, x2a); c\<^sub>0 = (x1c, x2c); \<delta> = dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1\<^sub>i
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = C\<^sub>0\<^sub>i
C\<^sub>1 = C\<^sub>1\<^sub>i

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = C\<^sub>0\<^sub>i
C\<^sub>1 = C\<^sub>1\<^sub>i

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

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

goal (2 subgoals):
 1. \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
C\<^sub>0 = C\<^sub>0\<^sub>i
C\<^sub>1 = C\<^sub>1\<^sub>i
\<Delta>' = \<Delta>\<^sub>i'
C\<^sub>0' = C\<^sub>0\<^sub>i'
C\<^sub>1' = C\<^sub>1\<^sub>i'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
C\<^sub>0 = C\<^sub>0\<^sub>i
C\<^sub>1 = C\<^sub>1\<^sub>i
\<Delta>' = \<Delta>\<^sub>i'
C\<^sub>0' = C\<^sub>0\<^sub>i'
C\<^sub>1' = C\<^sub>1\<^sub>i'

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

goal (1 subgoal):
 1. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<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. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
hence C: "\<not> \<delta>' \<le> \<delta>\<^sub>p'"
[PROOF STATE]
proof (prove)
using this:
\<not> \<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. \<not> \<delta>' \<le> \<delta>\<^sub>p'
[PROOF STEP]
by (simp add: "3.prems"(1,2) A B dist_eq_dist_code_le)
[PROOF STATE]
proof (state)
this:
\<not> \<delta>' \<le> \<delta>\<^sub>p'

goal (1 subgoal):
 1. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
obtain C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i' where \<Delta>\<^sub>i_def:
      "(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)"
      "(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>\<^sub>p', p\<^sub>0, p\<^sub>1') (p\<^sub>2 # ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'. \<lbrakk>(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps); (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>\<^sub>p', p\<^sub>0, p\<^sub>1') (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>\<^sub>p', p\<^sub>0, p\<^sub>1') (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
note defs = \<delta>\<^sub>p_def \<Delta>\<^sub>i_def
[PROOF STATE]
proof (state)
this:
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>\<^sub>p', p\<^sub>0, p\<^sub>1') (p\<^sub>2 # ps)

goal (1 subgoal):
 1. \<not> \<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)) \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
have "C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' \<and> C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
[PROOF STEP]
using "3.prems" "3.hyps"(2)[of p\<^sub>1] A B False defs
[PROOF STATE]
proof (prove)
using this:
\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))
\<delta>' = dist_code c\<^sub>0 c\<^sub>1
(C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) (p\<^sub>0 # p\<^sub>2 # ps)
\<lbrakk>p\<^sub>1 = 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 p\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); ?\<delta> = 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>' = dist_code p\<^sub>0 p\<^sub>1; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps); (?\<Delta>', ?C\<^sub>0', ?C\<^sub>1') = find_closest_pair_code (?\<delta>', p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)\<rbrakk> \<Longrightarrow> ?C\<^sub>0 = ?C\<^sub>0' \<and> ?C\<^sub>1 = ?C\<^sub>1'
\<delta>\<^sub>p' = dist_code p\<^sub>0 p\<^sub>1'
p\<^sub>1 = p\<^sub>1'
\<not> \<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))
p\<^sub>1 = find_closest_bf p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(\<delta>\<^sub>p', p\<^sub>1') = find_closest_bf_code p\<^sub>0 (take 7 (p\<^sub>2 # ps))
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair (p\<^sub>0, p\<^sub>1) (p\<^sub>2 # ps)
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = find_closest_pair_code (\<delta>\<^sub>p', p\<^sub>0, p\<^sub>1') (p\<^sub>2 # ps)

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

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

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

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0\<^sub>i &&& C\<^sub>1 = C\<^sub>1\<^sub>i
[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 ((x1b, x2b), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair ((x1b, x2b), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1b, x2b) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1b, x2b); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a) \<le> dist (real_of_int x1b, real_of_int x2b) (real_of_int x1, real_of_int x2); c\<^sub>1 = (x1a, x2a); c\<^sub>0 = (x1c, x2c); \<delta> = dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a)\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0\<^sub>i
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair ((x1b, x2b), x1, x2) (p\<^sub>2 # ps); p\<^sub>1 = (x1, x2); (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = find_closest_pair ((x1b, x2b), x1, x2) (p\<^sub>2 # ps); find_closest_bf (x1b, x2b) (p\<^sub>2 # take 6 ps) = (x1, x2); p\<^sub>0 = (x1b, x2b); \<not> dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a) \<le> dist (real_of_int x1b, real_of_int x2b) (real_of_int x1, real_of_int x2); c\<^sub>1 = (x1a, x2a); c\<^sub>0 = (x1c, x2c); \<delta> = dist (real_of_int x1c, real_of_int x2c) (real_of_int x1a, real_of_int x2a)\<rbrakk> \<Longrightarrow> C\<^sub>1 = C\<^sub>1\<^sub>i
[PROOF STEP]
by (metis Pair_inject)+
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = C\<^sub>0\<^sub>i
C\<^sub>1 = C\<^sub>1\<^sub>i

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>c\<^sub>0 c\<^sub>1 \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) []; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) []\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
 2. \<And>c\<^sub>0 c\<^sub>1 uu_ \<delta> \<delta>' C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>\<delta> = dist (case c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); \<delta>' = dist_code c\<^sub>0 c\<^sub>1; (C\<^sub>0, C\<^sub>1) = find_closest_pair (c\<^sub>0, c\<^sub>1) [uu_]; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<delta>', c\<^sub>0, c\<^sub>1) [uu_]\<rbrakk> \<Longrightarrow> C\<^sub>0 = C\<^sub>0' \<and> C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
qed auto


[STATEMENT]
lemma combine_code_dist_eq:
  assumes "\<delta>\<^sub>L = dist_code p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L" "\<delta>\<^sub>R = dist_code p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R"
  assumes "(\<delta>, c\<^sub>0, c\<^sub>1) = combine_code (\<delta>\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (\<delta>\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps"
  shows "\<delta> = dist_code c\<^sub>0 c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<delta>\<^sub>L = dist_code p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L
\<delta>\<^sub>R = dist_code p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R
(\<delta>, c\<^sub>0, c\<^sub>1) = combine_code (\<delta>\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (\<delta>\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps

goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
by (auto simp: find_closest_pair_code_dist_eq split: if_splits)


[STATEMENT]
lemma combine_code_eq:
  assumes "\<delta>\<^sub>L' = dist_code p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L" "\<delta>\<^sub>R' = dist_code p\<^sub>0\<^sub>R p\<^sub>1\<^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"
  assumes "(\<delta>', c\<^sub>0', c\<^sub>1') = combine_code (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps"
  shows "c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
obtain C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i' where \<Delta>\<^sub>i_def:
    "(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = (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))"
    "(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<Delta>\<^sub>i' C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'. \<lbrakk>(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = (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)); (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = (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))
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))

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

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1' where \<Delta>_def:
    "(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) ps'"
    "(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') ps''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) ps'; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') ps''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) ps'
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') ps''

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
note defs = \<Delta>\<^sub>i_def ps'_def \<Delta>_def
[PROOF STATE]
proof (state)
this:
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = (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))
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', 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\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
ps'' = filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) ps'
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') ps''

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
have *: "C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i'" "C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'" "\<Delta>\<^sub>i' = dist_code C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i' &&& C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i' &&& \<Delta>\<^sub>i' = dist_code C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'
[PROOF STEP]
using \<Delta>\<^sub>i_def assms(1,2,3,4) dist_eq_dist_code_lt
[PROOF STATE]
proof (prove)
using this:
(C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) = (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))
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
\<delta>\<^sub>L' = dist_code p\<^sub>0\<^sub>L p\<^sub>1\<^sub>L
\<delta>\<^sub>R' = dist_code p\<^sub>0\<^sub>R p\<^sub>1\<^sub>R
(c\<^sub>0, c\<^sub>1) = combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps
(\<delta>', c\<^sub>0', c\<^sub>1') = combine_code (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps
(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>2 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?p\<^sub>3 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = (dist_code ?p\<^sub>0 ?p\<^sub>1 < dist_code ?p\<^sub>2 ?p\<^sub>3)

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

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
hence "\<And>p. \<bar>fst p - l\<bar> < dist C\<^sub>0\<^sub>i C\<^sub>1\<^sub>i \<longleftrightarrow> (fst p - l)\<^sup>2 < \<Delta>\<^sub>i'"
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i'
C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
\<Delta>\<^sub>i' = dist_code C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'

goal (1 subgoal):
 1. \<And>p. (real_of_int \<bar>fst p - l\<bar> < dist (case C\<^sub>0\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = ((fst p - l)\<^sup>2 < \<Delta>\<^sub>i')
[PROOF STEP]
using dist_eq_dist_code_abs_lt
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i'
C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
\<Delta>\<^sub>i' = dist_code C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'
(\<bar>real_of_int ?c\<bar> < 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\<^sup>2 < dist_code ?p\<^sub>0 ?p\<^sub>1)

goal (1 subgoal):
 1. \<And>p. (real_of_int \<bar>fst p - l\<bar> < dist (case C\<^sub>0\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = ((fst p - l)\<^sup>2 < \<Delta>\<^sub>i')
[PROOF STEP]
by (metis (mono_tags) of_int_abs)
[PROOF STATE]
proof (state)
this:
(real_of_int \<bar>fst ?p - l\<bar> < dist (case C\<^sub>0\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = ((fst ?p - l)\<^sup>2 < \<Delta>\<^sub>i')

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
hence "ps' = ps''"
[PROOF STATE]
proof (prove)
using this:
(real_of_int \<bar>fst ?p - l\<bar> < dist (case C\<^sub>0\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = ((fst ?p - l)\<^sup>2 < \<Delta>\<^sub>i')

goal (1 subgoal):
 1. ps' = ps''
[PROOF STEP]
using ps'_def dist_fst_abs
[PROOF STATE]
proof (prove)
using this:
(real_of_int \<bar>fst ?p - l\<bar> < dist (case C\<^sub>0\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) = ((fst ?p - l)\<^sup>2 < \<Delta>\<^sub>i')
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\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y))) ps
ps'' = filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') 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)) = real_of_int \<bar>fst ?p - ?l\<bar>

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

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
hence "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
ps' = ps''

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using * find_closest_pair_code_eq \<Delta>_def
[PROOF STATE]
proof (prove)
using this:
ps' = ps''
C\<^sub>0\<^sub>i = C\<^sub>0\<^sub>i'
C\<^sub>1\<^sub>i = C\<^sub>1\<^sub>i'
\<Delta>\<^sub>i' = dist_code C\<^sub>0\<^sub>i' C\<^sub>1\<^sub>i'
\<lbrakk>?\<delta> = dist (case ?c\<^sub>0 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case ?c\<^sub>1 of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)); ?\<delta>' = dist_code ?c\<^sub>0 ?c\<^sub>1; (?C\<^sub>0, ?C\<^sub>1) = find_closest_pair (?c\<^sub>0, ?c\<^sub>1) ?ps; (?\<Delta>', ?C\<^sub>0', ?C\<^sub>1') = find_closest_pair_code (?\<delta>', ?c\<^sub>0, ?c\<^sub>1) ?ps\<rbrakk> \<Longrightarrow> ?C\<^sub>0 = ?C\<^sub>0' \<and> ?C\<^sub>1 = ?C\<^sub>1'
(C\<^sub>0, C\<^sub>1) = find_closest_pair (C\<^sub>0\<^sub>i, C\<^sub>1\<^sub>i) ps'
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') ps''

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

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

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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(3) defs(1,3,5)
[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\<^sub>i, C\<^sub>1\<^sub>i) = (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\<^sub>i of (x, y) \<Rightarrow> (real_of_int x, real_of_int y)) (case C\<^sub>1\<^sub>i 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\<^sub>i, C\<^sub>1\<^sub>i) ps'

goal (1 subgoal):
 1. C\<^sub>0 = c\<^sub>0 &&& C\<^sub>1 = c\<^sub>1
[PROOF STEP]
apply (auto simp: combine.simps split: prod.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e. \<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>1\<^sub>i = (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; C\<^sub>0\<^sub>i = (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>0\<^sub>R = (x1c, x2c); p\<^sub>1\<^sub>L = (x1d, x2d); p\<^sub>0\<^sub>L = (x1e, x2e); (if dist (real_of_int x1e, real_of_int x2e) (real_of_int x1d, real_of_int x2d) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) then ((x1e, x2e), x1d, x2d) else ((x1c, x2c), x1b, x2b)) = ((x1a, x2a), x1, x2); p\<^sub>1\<^sub>R = (x1b, x2b)\<rbrakk> \<Longrightarrow> C\<^sub>0 = c\<^sub>0
 2. \<And>x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e. \<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>1\<^sub>i = (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; C\<^sub>0\<^sub>i = (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>0\<^sub>R = (x1c, x2c); p\<^sub>1\<^sub>L = (x1d, x2d); p\<^sub>0\<^sub>L = (x1e, x2e); (if dist (real_of_int x1e, real_of_int x2e) (real_of_int x1d, real_of_int x2d) < dist (real_of_int x1c, real_of_int x2c) (real_of_int x1b, real_of_int x2b) then ((x1e, x2e), x1d, x2d) else ((x1c, x2c), x1b, x2b)) = ((x1a, x2a), x1, x2); p\<^sub>1\<^sub>R = (x1b, x2b)\<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 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C\<^sub>0 = c\<^sub>0
C\<^sub>1 = c\<^sub>1

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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(4) defs(2,4,6)
[PROOF STATE]
proof (prove)
using this:
(\<delta>', c\<^sub>0', c\<^sub>1') = combine_code (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) l ps
(\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') = (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R))
ps'' = filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps
(\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') 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. \<lbrakk>ps'' = filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') (filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps); (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) = (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i'); (\<delta>', c\<^sub>0', c\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') (filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps)\<rbrakk> \<Longrightarrow> C\<^sub>0' = c\<^sub>0'
 2. \<lbrakk>ps'' = filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps; (\<Delta>', C\<^sub>0', C\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') (filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps); (if \<delta>\<^sub>L' < \<delta>\<^sub>R' then (\<delta>\<^sub>L', p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) else (\<delta>\<^sub>R', p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R)) = (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i'); (\<delta>', c\<^sub>0', c\<^sub>1') = find_closest_pair_code (\<Delta>\<^sub>i', C\<^sub>0\<^sub>i', C\<^sub>1\<^sub>i') (filter (\<lambda>p. (fst p - l)\<^sup>2 < \<Delta>\<^sub>i') ps)\<rbrakk> \<Longrightarrow> C\<^sub>1' = c\<^sub>1'
[PROOF STEP]
by (metis prod.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 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
C\<^sub>0 = c\<^sub>0
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 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
C\<^sub>0 = c\<^sub>0
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 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_code_simps:
  assumes "n = length xs" "\<not> (n \<le> 3)"
  shows "closest_pair_rec_code xs = (
    let (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs in
    let l = fst (hd xs\<^sub>R) in
    let (ys\<^sub>L, p\<^sub>L) = closest_pair_rec_code xs\<^sub>L in
    let (ys\<^sub>R, p\<^sub>R) = closest_pair_rec_code xs\<^sub>R in
    let ys = merge snd ys\<^sub>L ys\<^sub>R in
    (ys, combine_code p\<^sub>L p\<^sub>R l ys)
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closest_pair_rec_code xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs; l = fst (hd xs\<^sub>R); (ys\<^sub>L, p\<^sub>L) = closest_pair_rec_code xs\<^sub>L; (ys\<^sub>R, p\<^sub>R) = closest_pair_rec_code xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine_code p\<^sub>L p\<^sub>R l 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_code xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (n div 2) xs; l = fst (hd xs\<^sub>R); (ys\<^sub>L, p\<^sub>L) = closest_pair_rec_code xs\<^sub>L; (ys\<^sub>R, p\<^sub>R) = closest_pair_rec_code xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine_code p\<^sub>L p\<^sub>R l ys))
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma closest_pair_rec_code_dist_eq:
  assumes "1 < length xs" "(ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs"
  shows "\<delta> = dist_code c\<^sub>0 c\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 < length xs
(ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs

goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
proof (induction xs arbitrary: ys \<delta> c\<^sub>0 c\<^sub>1 rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys \<delta> c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc); 1 < length xs; (ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc)
1 < length xs
(ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs

goal (1 subgoal):
 1. \<And>xs ys \<delta> c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc); 1 < length xs; (ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
let ?n = "length xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys \<delta> c\<^sub>0 c\<^sub>1. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc); 1 < length xs; (ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
proof (cases "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
 2. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
 2. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
hence "(\<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code xs"
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

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

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

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
 2. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code xs

goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
using "1.prems"(1) closest_pair_bf_code_dist_eq
[PROOF STATE]
proof (prove)
using this:
(\<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_bf_code xs
1 < length xs
\<lbrakk>1 < length ?ps; (?\<delta>, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf_code ?ps\<rbrakk> \<Longrightarrow> ?\<delta> = dist_code ?c\<^sub>0 ?c\<^sub>1

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
obtain XS\<^sub>L XS\<^sub>R where XS\<^sub>L\<^sub>R_def: "(XS\<^sub>L, XS\<^sub>R) = split_at (?n div 2) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>XS\<^sub>L XS\<^sub>R. (XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
define L where "L = fst (hd XS\<^sub>R)"
[PROOF STATE]
proof (state)
this:
L = fst (hd XS\<^sub>R)

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
obtain YS\<^sub>L \<Delta>\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L where YSC\<^sub>0\<^sub>1\<^sub>L_def: "(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>YS\<^sub>L \<Delta>\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L. (YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>L \<Delta>\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L. (YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
obtain YS\<^sub>R \<Delta>\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R where YSC\<^sub>0\<^sub>1\<^sub>R_def: "(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>YS\<^sub>R \<Delta>\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R. (YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>R \<Delta>\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R. (YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
define YS where "YS = merge (\<lambda>p. snd p) YS\<^sub>L YS\<^sub>R"
[PROOF STATE]
proof (state)
this:
YS = Common.merge snd YS\<^sub>L YS\<^sub>R

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
obtain \<Delta> C\<^sub>0 C\<^sub>1 where C\<^sub>0\<^sub>1_def: "(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Delta> C\<^sub>0 C\<^sub>1. (\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>\<Delta> C\<^sub>0 C\<^sub>1. (\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSC\<^sub>0\<^sub>1\<^sub>L_def YSC\<^sub>0\<^sub>1\<^sub>R_def YS_def C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
have "1 < length XS\<^sub>L" "length XS\<^sub>L < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>L &&& length XS\<^sub>L < length xs
[PROOF STEP]
using False "1.prems"(1) defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
1 < length xs
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
hence IHL: "\<Delta>\<^sub>L = dist_code C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs

goal (1 subgoal):
 1. \<Delta>\<^sub>L = dist_code C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc)
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
have "1 < length XS\<^sub>R" "length XS\<^sub>R < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length XS\<^sub>R &&& length XS\<^sub>R < length xs
[PROOF STEP]
using False "1.prems"(1) defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
1 < length xs
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
hence IHR: "\<Delta>\<^sub>R = dist_code C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs

goal (1 subgoal):
 1. \<Delta>\<^sub>R = dist_code C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R
[PROOF STEP]
using "1.IH" defs
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>R
length XS\<^sub>R < length xs
\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb xc. (x, xa, xb, xc) = closest_pair_rec_code ys \<longrightarrow> xa = dist_code xb xc)
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
have *: "(YS, \<Delta>, C\<^sub>0, C\<^sub>1) = closest_pair_rec_code xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, \<Delta>, C\<^sub>0, C\<^sub>1) = closest_pair_rec_code xs
[PROOF STEP]
using False closest_pair_rec_code_simps defs
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
\<lbrakk>?n = length ?xs; \<not> ?n \<le> 3\<rbrakk> \<Longrightarrow> closest_pair_rec_code ?xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (?n div 2) ?xs; l = fst (hd xs\<^sub>R); (ys\<^sub>L, p\<^sub>L) = closest_pair_rec_code xs\<^sub>L; (ys\<^sub>R, p\<^sub>R) = closest_pair_rec_code xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine_code p\<^sub>L p\<^sub>R l ys))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, \<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, \<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec_code XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(YS, \<Delta>, C\<^sub>0, C\<^sub>1) = closest_pair_rec_code xs

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
have "\<Delta> = dist_code C\<^sub>0 C\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta> = dist_code C\<^sub>0 C\<^sub>1
[PROOF STEP]
using combine_code_dist_eq IHL IHR C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<delta>\<^sub>L = dist_code ?p\<^sub>0\<^sub>L ?p\<^sub>1\<^sub>L; ?\<delta>\<^sub>R = dist_code ?p\<^sub>0\<^sub>R ?p\<^sub>1\<^sub>R; (?\<delta>, ?c\<^sub>0, ?c\<^sub>1) = combine_code (?\<delta>\<^sub>L, ?p\<^sub>0\<^sub>L, ?p\<^sub>1\<^sub>L) (?\<delta>\<^sub>R, ?p\<^sub>0\<^sub>R, ?p\<^sub>1\<^sub>R) ?l ?ps\<rbrakk> \<Longrightarrow> ?\<delta> = dist_code ?c\<^sub>0 ?c\<^sub>1
\<Delta>\<^sub>L = dist_code C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L
\<Delta>\<^sub>R = dist_code C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R
(\<Delta>, C\<^sub>0, C\<^sub>1) = combine_code (\<Delta>\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (\<Delta>\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

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

goal (1 subgoal):
 1. \<delta> = dist_code c\<^sub>0 c\<^sub>1
[PROOF STEP]
using "1.prems"(2) *
[PROOF STATE]
proof (prove)
using this:
(YS, \<Delta>, C\<^sub>0, C\<^sub>1) = closest_pair_rec_code xs
\<Delta> = dist_code C\<^sub>0 C\<^sub>1
(ys, \<delta>, c\<^sub>0, c\<^sub>1) = closest_pair_rec_code xs
(YS, \<Delta>, C\<^sub>0, C\<^sub>1) = closest_pair_rec_code xs

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

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

goal:
No subgoals!
[PROOF STEP]
qed