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

goal (1 subgoal):
 1. ys = ys'
[PROOF STEP]
proof (induction xs arbitrary: ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1' rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>xa xb xc xd. (xa, xb, xc, xd) = closest_pair_rec_code ys \<longrightarrow> x = xa)); 1 < length xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs; (ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> ys = ys'
[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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>xa xb xc xd. (xa, xb, xc, xd) = closest_pair_rec_code ys \<longrightarrow> x = xa))
1 < length xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs

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

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> ys = ys'
 2. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
hence "ys = mergesort snd xs"
[PROOF STATE]
proof (prove)
using this:
length xs \<le> 3

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

goal (1 subgoal):
 1. ys = mergesort snd xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ys = mergesort snd xs

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> ys = ys'
 2. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = mergesort snd xs

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> ys = ys'
 2. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
have "ys' = mergesort snd xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys' = mergesort snd xs
[PROOF STEP]
using "1.prems"(3) closest_pair_rec_code.simps
[PROOF STATE]
proof (prove)
using this:
(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. ys' = mergesort snd xs
[PROOF STEP]
by (simp add: True)
[PROOF STATE]
proof (state)
this:
ys' = mergesort snd xs

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> ys = ys'
 2. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = mergesort snd xs
ys' = mergesort snd xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = mergesort snd xs
ys' = mergesort snd xs

goal (1 subgoal):
 1. ys = ys'
[PROOF STEP]
using "1.prems"(1)
[PROOF STATE]
proof (prove)
using this:
ys = mergesort snd xs
ys' = mergesort snd xs
1 < length xs

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

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

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

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
obtain YS\<^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' where YSC\<^sub>0\<^sub>1\<^sub>L_def:
      "(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L"
      "(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 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'. \<lbrakk>(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L YS\<^sub>L' \<Delta>\<^sub>L' C\<^sub>0\<^sub>L' C\<^sub>1\<^sub>L'. \<lbrakk>(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(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> ys = ys'
[PROOF STEP]
obtain YS\<^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' where YSC\<^sub>0\<^sub>1\<^sub>R_def:
      "(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R"
      "(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 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'. \<lbrakk>(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R YS\<^sub>R' \<Delta>\<^sub>R' C\<^sub>0\<^sub>R' C\<^sub>1\<^sub>R'. \<lbrakk>(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
(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> ys = ys'
[PROOF STEP]
define YS YS' where YS_def:
      "YS = merge (\<lambda>p. snd p) YS\<^sub>L YS\<^sub>R"
      "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
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
obtain C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1' where C\<^sub>0\<^sub>1_def:
      "(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS"
      "(\<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>C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS; (\<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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS; (\<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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> ys = ys'
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSC\<^sub>0\<^sub>1\<^sub>L_def YSC\<^sub>0\<^sub>1\<^sub>R_def YS_def C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> ys = ys'
[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, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> ys = ys'
[PROOF STEP]
hence IHL: "YS\<^sub>L = YS\<^sub>L'"
[PROOF STATE]
proof (prove)
using this:
1 < length XS\<^sub>L
length XS\<^sub>L < length xs

goal (1 subgoal):
 1. YS\<^sub>L = YS\<^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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>xa xb xc xd. (xa, xb, xc, xd) = closest_pair_rec_code ys \<longrightarrow> x = xa))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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\<^sub>L = YS\<^sub>L'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
YS\<^sub>L = YS\<^sub>L'

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

goal (1 subgoal):
 1. YS\<^sub>R = YS\<^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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>xa xb xc xd. (xa, xb, xc, xd) = closest_pair_rec_code ys \<longrightarrow> x = xa))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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\<^sub>R = YS\<^sub>R'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
YS\<^sub>R = YS\<^sub>R'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[PROOF STEP]
have "(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
[PROOF STEP]
using False closest_pair_rec_simps defs(1,2,3,5,7,9)
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
\<lbrakk>?n = length ?xs; \<not> ?n \<le> 3\<rbrakk> \<Longrightarrow> closest_pair_rec ?xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (?n div 2) ?xs; (ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) = closest_pair_rec xs\<^sub>L; (ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) = closest_pair_rec xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (fst (hd xs\<^sub>R)) ys))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> ys = ys'
[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(1,2,4,6,8,10)
[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> ys = ys'
[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> ys = ys'
[PROOF STEP]
have "YS = YS'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. YS = YS'
[PROOF STEP]
using IHL IHR YS_def
[PROOF STATE]
proof (prove)
using this:
YS\<^sub>L = YS\<^sub>L'
YS\<^sub>R = YS\<^sub>R'
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'

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

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

goal (1 subgoal):
 1. ys = ys'
[PROOF STEP]
by (metis "1.prems"(2,3) Pair_inject)
[PROOF STATE]
proof (state)
this:
ys = ys'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_rec_code_eq:
  assumes "1 < length xs"
  assumes "(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs"
  assumes "(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs"
  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:
1 < length xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
proof (induction xs arbitrary: ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1' rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe)); 1 < length xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs; (ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe))
1 < length xs
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs

goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe)); 1 < length xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs; (ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs\<rbrakk> \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
let ?n = "length xs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> 1 < length ys \<longrightarrow> (\<forall>x xa xb. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe)); 1 < length xs; (ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec xs; (ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code xs\<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 "?n \<le> 3")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
 2. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xs \<le> 3

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

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

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

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
 2. \<not> length xs \<le> 3 \<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>1) = closest_pair_bf xs

goal (2 subgoals):
 1. length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
 2. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
have "(\<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code xs
[PROOF STEP]
using "1.prems"(3) closest_pair_rec_code.simps
[PROOF STATE]
proof (prove)
using this:
(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 add: True)
[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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
 2. \<not> length xs \<le> 3 \<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, c\<^sub>1) = closest_pair_bf xs
(\<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
(\<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code xs

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
using "1.prems"(1) closest_pair_bf_code_eq
[PROOF STATE]
proof (prove)
using this:
(c\<^sub>0, c\<^sub>1) = closest_pair_bf xs
(\<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_bf_code xs
1 < length xs
\<lbrakk>1 < length ?ps; (?c\<^sub>0, ?c\<^sub>1) = closest_pair_bf ?ps; (?\<delta>', ?c\<^sub>0', ?c\<^sub>1') = closest_pair_bf_code ?ps\<rbrakk> \<Longrightarrow> ?c\<^sub>0 = ?c\<^sub>0' \<and> ?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 simp
[PROOF STATE]
proof (state)
this:
c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<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> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xs \<le> 3

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

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
obtain YS\<^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' where YSC\<^sub>0\<^sub>1\<^sub>L_def:
      "(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L"
      "(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 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'. \<lbrakk>(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>L C\<^sub>0\<^sub>L C\<^sub>1\<^sub>L YS\<^sub>L' \<Delta>\<^sub>L' C\<^sub>0\<^sub>L' C\<^sub>1\<^sub>L'. \<lbrakk>(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
obtain YS\<^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' where YSC\<^sub>0\<^sub>1\<^sub>R_def:
      "(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R"
      "(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 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'. \<lbrakk>(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>YS\<^sub>R C\<^sub>0\<^sub>R C\<^sub>1\<^sub>R YS\<^sub>R' \<Delta>\<^sub>R' C\<^sub>0\<^sub>R' C\<^sub>1\<^sub>R'. \<lbrakk>(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
(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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
define YS YS' where YS_def:
      "YS = merge (\<lambda>p. snd p) YS\<^sub>L YS\<^sub>R"
      "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
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> 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 C\<^sub>0\<^sub>1_def:
      "(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS"
      "(\<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>C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS; (\<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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>C\<^sub>0 C\<^sub>1 \<Delta>' C\<^sub>0' C\<^sub>1'. \<lbrakk>(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS; (\<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'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
note defs = XS\<^sub>L\<^sub>R_def L_def YSC\<^sub>0\<^sub>1\<^sub>L_def YSC\<^sub>0\<^sub>1\<^sub>R_def YS_def C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (state)
this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
hence IHL: "C\<^sub>0\<^sub>L = C\<^sub>0\<^sub>L'" "C\<^sub>1\<^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. C\<^sub>0\<^sub>L = C\<^sub>0\<^sub>L' &&& C\<^sub>1\<^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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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. C\<^sub>0\<^sub>L = C\<^sub>0\<^sub>L' &&& C\<^sub>1\<^sub>L = C\<^sub>1\<^sub>L'
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>L = C\<^sub>0\<^sub>L'
C\<^sub>1\<^sub>L = C\<^sub>1\<^sub>L'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
hence IHR: "C\<^sub>0\<^sub>R = C\<^sub>0\<^sub>R'" "C\<^sub>1\<^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. C\<^sub>0\<^sub>R = C\<^sub>0\<^sub>R' &&& C\<^sub>1\<^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. (x, xa, xb) = closest_pair_rec ys \<longrightarrow> (\<forall>x xc xd xe. (x, xc, xd, xe) = closest_pair_rec_code ys \<longrightarrow> xa = xd \<and> xb = xe))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>L', \<Delta>\<^sub>L', C\<^sub>0\<^sub>L', C\<^sub>1\<^sub>L') = closest_pair_rec_code XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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. C\<^sub>0\<^sub>R = C\<^sub>0\<^sub>R' &&& C\<^sub>1\<^sub>R = C\<^sub>1\<^sub>R'
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
C\<^sub>0\<^sub>R = C\<^sub>0\<^sub>R'
C\<^sub>1\<^sub>R = C\<^sub>1\<^sub>R'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
have "YS = YS'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. YS = YS'
[PROOF STEP]
using defs \<open>1 < length XS\<^sub>L\<close> \<open>1 < length XS\<^sub>R\<close> closest_pair_rec_ys_eq
[PROOF STATE]
proof (prove)
using this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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'
1 < length XS\<^sub>L
1 < length XS\<^sub>R
\<lbrakk>1 < length ?xs; (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec ?xs; (?ys', ?\<delta>', ?c\<^sub>0', ?c\<^sub>1') = closest_pair_rec_code ?xs\<rbrakk> \<Longrightarrow> ?ys = ?ys'

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
have "\<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'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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'
[PROOF STEP]
using defs \<open>1 < length XS\<^sub>L\<close> \<open>1 < length XS\<^sub>R\<close> closest_pair_rec_code_dist_eq
[PROOF STATE]
proof (prove)
using this:
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^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
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^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
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
YS' = Common.merge snd YS\<^sub>L' YS\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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'
1 < length XS\<^sub>L
1 < length XS\<^sub>R
\<lbrakk>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

goal (1 subgoal):
 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'
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<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'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
YS = YS'
\<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'
[PROOF STEP]
have "C\<^sub>0 = C\<^sub>0'" "C\<^sub>1 = C\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
YS = YS'
\<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'

goal (1 subgoal):
 1. C\<^sub>0 = C\<^sub>0' &&& C\<^sub>1 = C\<^sub>1'
[PROOF STEP]
using combine_code_eq IHL IHR C\<^sub>0\<^sub>1_def
[PROOF STATE]
proof (prove)
using this:
YS = YS'
\<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'
\<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; (?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\<rbrakk> \<Longrightarrow> ?c\<^sub>0 = ?c\<^sub>0' \<and> ?c\<^sub>1 = ?c\<^sub>1'
C\<^sub>0\<^sub>L = C\<^sub>0\<^sub>L'
C\<^sub>1\<^sub>L = C\<^sub>1\<^sub>L'
C\<^sub>0\<^sub>R = C\<^sub>0\<^sub>R'
C\<^sub>1\<^sub>R = C\<^sub>1\<^sub>R'
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS
(\<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. 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. \<not> length xs \<le> 3 \<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'
C\<^sub>1 = C\<^sub>1'

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
have "(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
[PROOF STEP]
using False closest_pair_rec_simps defs(1,2,3,5,7,9)
[PROOF STATE]
proof (prove)
using this:
\<not> length xs \<le> 3
\<lbrakk>?n = length ?xs; \<not> ?n \<le> 3\<rbrakk> \<Longrightarrow> closest_pair_rec ?xs = (let (xs\<^sub>L, xs\<^sub>R) = split_at (?n div 2) ?xs; (ys\<^sub>L, p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) = closest_pair_rec xs\<^sub>L; (ys\<^sub>R, p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) = closest_pair_rec xs\<^sub>R; ys = Common.merge snd ys\<^sub>L ys\<^sub>R in (ys, combine (p\<^sub>0\<^sub>L, p\<^sub>1\<^sub>L) (p\<^sub>0\<^sub>R, p\<^sub>1\<^sub>R) (fst (hd xs\<^sub>R)) ys))
(XS\<^sub>L, XS\<^sub>R) = split_at (length xs div 2) xs
L = fst (hd XS\<^sub>R)
(YS\<^sub>L, C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) = closest_pair_rec XS\<^sub>L
(YS\<^sub>R, C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) = closest_pair_rec XS\<^sub>R
YS = Common.merge snd YS\<^sub>L YS\<^sub>R
(C\<^sub>0, C\<^sub>1) = combine (C\<^sub>0\<^sub>L, C\<^sub>1\<^sub>L) (C\<^sub>0\<^sub>R, C\<^sub>1\<^sub>R) L YS

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

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

goal (1 subgoal):
 1. \<not> length xs \<le> 3 \<Longrightarrow> c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = 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(1,2,4,6,8,10)
[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> 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'
(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
(YS', \<Delta>', C\<^sub>0', C\<^sub>1') = closest_pair_rec_code xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C\<^sub>0 = C\<^sub>0'
C\<^sub>1 = C\<^sub>1'
(YS, C\<^sub>0, C\<^sub>1) = closest_pair_rec xs
(YS', \<Delta>', C\<^sub>0', C\<^sub>1') = closest_pair_rec_code xs

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

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' \<and> c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
by (metis Pair_inject)
[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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closest_pair_code_eq:
  "closest_pair ps = closest_pair_code ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closest_pair ps = closest_pair_code ps
[PROOF STEP]
proof (induction ps rule: induct_list012)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
case (3 x y zs)
[PROOF STATE]
proof (state)
this:
closest_pair zs = closest_pair_code zs
closest_pair (y # zs) = closest_pair_code (y # zs)

goal (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
obtain ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1' where *:
    "(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))"
    "(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ys c\<^sub>0 c\<^sub>1 ys' \<delta>' c\<^sub>0' c\<^sub>1'. \<lbrakk>(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs)); (ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases3)
[PROOF STATE]
proof (state)
this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))

goal (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))

goal (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
have "1 < length (mergesort fst (x # y # zs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length (mergesort fst (x # y # zs))
[PROOF STEP]
using length_mergesort[of fst "x # y # zs"]
[PROOF STATE]
proof (prove)
using this:
length (mergesort fst (x # y # zs)) = length (x # y # zs)

goal (1 subgoal):
 1. 1 < length (mergesort fst (x # y # zs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < length (mergesort fst (x # y # zs))

goal (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))
1 < length (mergesort fst (x # y # zs))
[PROOF STEP]
have "c\<^sub>0 = c\<^sub>0'" "c\<^sub>1 = c\<^sub>1'"
[PROOF STATE]
proof (prove)
using this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))
1 < length (mergesort fst (x # y # zs))

goal (1 subgoal):
 1. c\<^sub>0 = c\<^sub>0' &&& c\<^sub>1 = c\<^sub>1'
[PROOF STEP]
using closest_pair_rec_code_eq
[PROOF STATE]
proof (prove)
using this:
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))
1 < length (mergesort fst (x # y # zs))
\<lbrakk>1 < length ?xs; (?ys, ?c\<^sub>0, ?c\<^sub>1) = closest_pair_rec ?xs; (?ys', ?\<delta>', ?c\<^sub>0', ?c\<^sub>1') = closest_pair_rec_code ?xs\<rbrakk> \<Longrightarrow> ?c\<^sub>0 = ?c\<^sub>0' \<and> ?c\<^sub>1 = ?c\<^sub>1'

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 (3 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
 3. \<And>x y zs. \<lbrakk>closest_pair zs = closest_pair_code zs; closest_pair (y # zs) = closest_pair_code (y # zs)\<rbrakk> \<Longrightarrow> closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
c\<^sub>0 = c\<^sub>0'
c\<^sub>1 = c\<^sub>1'

goal (1 subgoal):
 1. closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
c\<^sub>0 = c\<^sub>0'
c\<^sub>1 = c\<^sub>1'
(ys, c\<^sub>0, c\<^sub>1) = closest_pair_rec (mergesort fst (x # y # zs))
(ys', \<delta>', c\<^sub>0', c\<^sub>1') = closest_pair_rec_code (mergesort fst (x # y # zs))

goal (1 subgoal):
 1. closest_pair (x # y # zs) = closest_pair_code (x # y # zs)
[PROOF STEP]
by (auto split: prod.splits)
[PROOF STATE]
proof (state)
this:
closest_pair (x # y # zs) = closest_pair_code (x # y # zs)

goal (2 subgoals):
 1. closest_pair [] = closest_pair_code []
 2. \<And>x. closest_pair [x] = closest_pair_code [x]
[PROOF STEP]
qed auto


[STATEMENT]
lemma mop_bef_length[simp]: "length (mopup_a n) = 4 * n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (mopup_a n) = 4 * n
[PROOF STEP]
by(induct n, simp_all)


[STATEMENT]
lemma mopup_a_nth:
  "\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) =
                             mopup_a (Suc q) ! ((4 * q) + x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>q < 0; x < 4\<rbrakk> \<Longrightarrow> mopup_a 0 ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
 2. \<And>n. \<lbrakk>\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x); q < Suc n; x < 4\<rbrakk> \<Longrightarrow> mopup_a (Suc n) ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
q < Suc n
x < 4

goal (2 subgoals):
 1. \<lbrakk>q < 0; x < 4\<rbrakk> \<Longrightarrow> mopup_a 0 ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
 2. \<And>n. \<lbrakk>\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x); q < Suc n; x < 4\<rbrakk> \<Longrightarrow> mopup_a (Suc n) ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
q < Suc n
x < 4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>q < n; x < 4\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
q < Suc n
x < 4

goal (1 subgoal):
 1. mopup_a (Suc n) ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
[PROOF STEP]
by(cases "q < n";cases "q = n", auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
mopup_a (Suc n) ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)

goal (1 subgoal):
 1. \<lbrakk>q < 0; x < 4\<rbrakk> \<Longrightarrow> mopup_a 0 ! (4 * q + x) = mopup_a (Suc q) ! (4 * q + x)
[PROOF STEP]
qed auto


[STATEMENT]
lemma fetch_bef_erase_a_o[simp]:
  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>
  \<Longrightarrow> (fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc) = (WB, s + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) s Oc = (WB, s + 1)
[PROOF STEP]
apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> (mopup_a n @ shift mopup_b (2 * n)) ! Suc (4 * q) = (WB, Suc (Suc (2 * q)))
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4*n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q); length (mopup_a n) = 4 * n\<rbrakk> \<Longrightarrow> (mopup_a n @ shift mopup_b (2 * n)) ! Suc (4 * q) = (WB, Suc (Suc (2 * q)))
 2. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> length (mopup_a n) = 4 * n
 3. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> mopup_a n ! Suc (4 * q) = (WB, Suc (Suc (2 * q)))
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(subgoal_tac "mopup_a n ! (4 * q + 1) =
                      mopup_a (Suc q) ! ((4 * q) + 1)",
      simp add: nth_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + 1) = mopup_a (Suc q) ! (4 * q + 1)
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(rule mopup_a_nth, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_bef_erase_a_b[simp]:
  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk>
   \<Longrightarrow>  (fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk) = (R, s + 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) s Bk = (R, s + 2)
[PROOF STEP]
apply(subgoal_tac "\<exists> q. s = 2*q + 1", auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> (mopup_a n @ shift mopup_b (2 * n)) ! (4 * q) = (R, Suc (Suc (Suc (2 * q))))
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4*n")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q); length (mopup_a n) = 4 * n\<rbrakk> \<Longrightarrow> (mopup_a n @ shift mopup_b (2 * n)) ! (4 * q) = (R, Suc (Suc (Suc (2 * q))))
 2. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> length (mopup_a n) = 4 * n
 3. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(auto simp: nth_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q) = (R, Suc (Suc (Suc (2 * q))))
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(subgoal_tac "mopup_a n ! (4 * q + 0) =
                       mopup_a (Suc q) ! ((4 * q + 0))",
      simp add: nth_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>q. \<lbrakk>Suc (2 * q) \<le> 2 * n; s = Suc (2 * q)\<rbrakk> \<Longrightarrow> mopup_a n ! (4 * q + 0) = mopup_a (Suc q) ! (4 * q + 0)
 2. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply(rule mopup_a_nth, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0\<rbrakk> \<Longrightarrow> \<exists>q. s = Suc (2 * q)
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_jump_over1_o:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc
  = (R, Suc (2 * n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc = (R, Suc (2 * n))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Oc = (R, Suc (2 * n))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_jump_over1_b:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk
 = (R, Suc (Suc (2 * n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk = (R, Suc (Suc (2 * n)))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (2 * n)) Bk = (R, Suc (Suc (2 * n)))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_aft_erase_a_o:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc
 = (WB, Suc (2 * n + 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc = (WB, Suc (2 * n + 2))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Oc = (WB, Suc (2 * n + 2))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_aft_erase_a_b:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk
  = (L, Suc (2 * n + 4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk = (L, Suc (2 * n + 4))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (Suc (Suc (2 * n))) Bk = (L, Suc (2 * n + 4))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_aft_erase_b_b:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (2*n + 3) Bk
  = (R, Suc (2 * n + 3))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 3) Bk = (R, Suc (2 * n + 3))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 3) Bk = (R, Suc (2 * n + 3))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 3 = Suc (2*n + 2)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 3 = Suc (2 * n + 2)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 2)) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (R, Suc (Suc (2 * n + 2)))
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 3 = Suc (2 * n + 2)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_aft_erase_c_o:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc
 = (WB, Suc (2 * n + 2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc = (WB, Suc (2 * n + 2))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Oc = (WB, Suc (2 * n + 2))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 4 = Suc (2 * n + 3)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 3) + 1) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (WB, Suc (2 * n + 2))
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 4 = Suc (2 * n + 3)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_aft_erase_c_b:
  "fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk
 = (R, Suc (2 * n + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk = (R, Suc (2 * n + 1))
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 4) Bk = (R, Suc (2 * n + 1))
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 4 = Suc (2*n + 3)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 4 = Suc (2 * n + 3)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 3)) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (R, Suc (2 * n + 1))
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 4 = Suc (2 * n + 3)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_left_moving_o:
  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc)
 = (L, 2*n + 6)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc = (L, 2 * n + 6)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Oc = (L, 2 * n + 6)
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 5 = Suc (2 * n + 4)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 4) + 1) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (L, 2 * n + 6)
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 5 = Suc (2 * n + 4)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_left_moving_b:
  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk)
  = (L, 2*n + 5)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk = (L, 2 * n + 5)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 5) Bk = (L, 2 * n + 5)
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 5 = Suc (2*n + 4)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 5 = Suc (2 * n + 4)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 4)) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (L, Suc (2 * n + 4))
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 5 = Suc (2 * n + 4)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_jump_over2_b:
  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk)
 = (R, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk = (R, 0)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Bk = (R, 0)
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 6 = Suc (2 * n + 5)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 5)) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (R, 0)
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 6 = Suc (2 * n + 5)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fetch_jump_over2_o:
  "(fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc)
 = (L, 2*n + 6)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc = (L, 2 * n + 6)
[PROOF STEP]
apply(subgoal_tac "length (mopup_a n) = 4 * n")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (mopup_a n) = 4 * n \<Longrightarrow> fetch (mopup_a n @ shift mopup_b (2 * n)) (2 * n + 6) Oc = (L, 2 * n + 6)
 2. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(subgoal_tac "2*n + 6 = Suc (2*n + 5)", simp only: fetch.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length (mopup_a n) = 4 * n; 2 * n + 6 = Suc (2 * n + 5)\<rbrakk> \<Longrightarrow> (case nth_of (mopup_a n @ shift mopup_b (2 * n)) (2 * (2 * n + 5) + 1) of None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i) = (L, Suc (2 * n + 5))
 2. length (mopup_a n) = 4 * n \<Longrightarrow> 2 * n + 6 = Suc (2 * n + 5)
 3. length (mopup_a n) = 4 * n
[PROOF STEP]
apply(auto simp: mopup_b_def nth_append shift.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_bef_erase_b_Bk_via_a_Oc[simp]:
  "\<lbrakk>mopup_bef_erase_a (s, l, Oc # xs) lm n ires\<rbrakk> \<Longrightarrow>
  mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mopup_bef_erase_a (s, l, Oc # xs) lm n ires \<Longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires
[PROOF STEP]
apply(auto simp: mopup_bef_erase_a.simps mopup_bef_erase_b.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ln m rn. \<lbrakk>l = Bk \<up> ln @ Bk # Bk # ires; Oc # xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> \<exists>m rn. xs = Oc \<up> m @ Bk # <drop (Suc s div 2) lm> @ Bk \<up> rn
[PROOF STEP]
by (metis cell.distinct(1) hd_append list.sel(1) list.sel(3) tl_append2 tl_replicate)


[STATEMENT]
lemma mopup_false1:
  "\<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0;  \<not> Suc s \<le> 2 * n\<rbrakk>
  \<Longrightarrow> RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < s; s \<le> 2 * n; s mod 2 = Suc 0; \<not> Suc s \<le> 2 * n\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(arith)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mopup_bef_erase_a_implies_two[simp]:
  "\<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0;
   mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk>
 \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires)  \<and>
     (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length lm; 0 < s; s \<le> 2 * n; s mod 2 = Suc 0; mopup_bef_erase_a (s, l, Oc # xs) lm n ires; r = Oc # xs\<rbrakk> \<Longrightarrow> (Suc s \<le> 2 * n \<longrightarrow> mopup_bef_erase_b (Suc s, l, Bk # xs) lm n ires) \<and> (\<not> Suc s \<le> 2 * n \<longrightarrow> mopup_jump_over1 (Suc s, l, Bk # xs) lm n ires)
[PROOF STEP]
apply(auto elim!: mopup_false1)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)
                    else Oc\<up>(Suc m) @ Bk # <lm>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <m # lm> = (if lm = [] then Oc \<up> Suc m else Oc \<up> Suc m @ Bk # <lm>)
[PROOF STEP]
by(cases lm, simp_all add: tape_of_list_def  tape_of_nat_def split: if_splits)


[STATEMENT]
lemma drop_tape_of_cons:
  "\<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>
[PROOF STEP]
using Suc_lessD append_Cons list.simps(2) Cons_nth_drop_Suc replicate_Suc tape_of_nl_cons
[PROOF STATE]
proof (prove)
using this:
Suc ?m < ?n \<Longrightarrow> ?m < ?n
(?x # ?xs) @ ?ys = ?x # ?xs @ ?ys
[] \<noteq> ?x21.0 # ?x22.0
?i < length ?xs \<Longrightarrow> ?xs ! ?i # drop (Suc ?i) ?xs = drop ?i ?xs
?x \<up> Suc ?n = ?x # ?x \<up> ?n
<?m # ?lm> = (if ?lm = [] then Oc \<up> Suc ?m else Oc \<up> Suc ?m @ Bk # <?lm>)

goal (1 subgoal):
 1. \<lbrakk>Suc q < length lm; x = lm ! q\<rbrakk> \<Longrightarrow> <drop q lm> = Oc # Oc \<up> x @ Bk # <drop (Suc q) lm>
[PROOF STEP]
by metis


[STATEMENT]
lemma erase2jumpover1:
  "\<lbrakk>q < length list;
             \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>
       \<Longrightarrow> <drop q list> = Oc # Oc \<up> (list ! q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < length list; \<forall>rn. <drop q list> \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(erule_tac x = 0 in allE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < length list; <drop q list> \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(cases "Suc q < length list")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>q < length list; <drop q list> \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>; Suc q < length list\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
 2. \<lbrakk>q < length list; <drop q list> \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(erule_tac notE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>q < length list; Suc q < length list\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>
 2. \<lbrakk>q < length list; <drop q list> \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(rule_tac drop_tape_of_cons, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < length list; <drop q list> \<noteq> Oc # Oc \<up> list ! q @ [Bk]; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(subgoal_tac "length list = Suc q", auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk><drop q list> \<noteq> Oc # Oc \<up> list ! q @ [Bk]; length list = Suc q\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
[PROOF STEP]
apply(subgoal_tac "drop q list = [list ! q]")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk><drop q list> \<noteq> Oc # Oc \<up> list ! q @ [Bk]; length list = Suc q; drop q list = [list ! q]\<rbrakk> \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q
 2. \<lbrakk><drop q list> \<noteq> Oc # Oc \<up> list ! q @ [Bk]; length list = Suc q\<rbrakk> \<Longrightarrow> drop q list = [list ! q]
[PROOF STEP]
apply(simp add: tape_of_nat_def tape_of_list_def replicate_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk><drop q list> \<noteq> Oc # Oc \<up> list ! q @ [Bk]; length list = Suc q\<rbrakk> \<Longrightarrow> drop q list = [list ! q]
[PROOF STEP]
by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI)


[STATEMENT]
lemma erase2jumpover2:
  "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>
  Oc # Oc \<up> (list ! q) @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk>
  \<Longrightarrow> RR"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(cases "Suc q < length list")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn; Suc q < length list\<rbrakk> \<Longrightarrow> RR
 2. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(erule_tac x = "Suc n" in allE, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Suc q < length list; <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> Suc n\<rbrakk> \<Longrightarrow> RR
 2. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(erule_tac notE, simp add: replicate_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Suc q < length list \<Longrightarrow> <drop q list> = Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list>
 2. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # <drop (Suc q) list> @ Bk \<up> rn; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(rule_tac drop_tape_of_cons, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # Bk \<up> rn; \<not> Suc q < length list\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(subgoal_tac "length list = Suc q", auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq> Oc # Oc \<up> list ! q @ Bk # Bk \<up> rn; length list = Suc q\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
apply(erule_tac x = "n" in allE, simp add: tape_of_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length list = Suc q; tape_of_nat_list (drop q list) \<noteq> Oc # Oc \<up> list ! q\<rbrakk> \<Longrightarrow> RR
[PROOF STEP]
by (metis append_Nil2 append_eq_conv_conj Cons_nth_drop_Suc lessI replicate_Suc tape_of_list_def tape_of_nl_cons)


[STATEMENT]
lemma mod_ex1: "(a mod 2 = Suc 0) = (\<exists> q. a = Suc (2 * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a mod 2 = Suc 0) = (\<exists>q. a = Suc (2 * q))
[PROOF STEP]
by arith