[STATEMENT]
lemma reorder_cyclic_list:
  assumes  "hd l = s" "last l = s" "length l > 2" "sl + 1 < length l"
    "rel_chain l r"
  obtains l' :: "'a list"
  where "hd l' = l ! (sl + 1)" "last l' = l ! sl" "rel_chain l' r" "length l' = length l - 1"
    "\<forall> i. i + 1 < length l' \<longrightarrow>
     (\<exists> j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<noteq> []
[PROOF STEP]
using \<open>length l > 2\<close>
[PROOF STATE]
proof (prove)
using this:
2 < length l

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

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have  "length (tl l) > 1" "tl l \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < length (tl l) &&& tl l \<noteq> []
[PROOF STEP]
using \<open>length l > 2\<close>
[PROOF STATE]
proof (prove)
using this:
2 < length l

goal (1 subgoal):
 1. 1 < length (tl l) &&& tl l \<noteq> []
[PROOF STEP]
by (auto simp add: length_0_conv[THEN sym])
[PROOF STATE]
proof (state)
this:
1 < length (tl l)
tl l \<noteq> []

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?l' = "if sl = 0 then
                 tl l
             else
                 drop (sl + 1) l @ tl (take (sl + 1) l)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "hd ?l' = l ! (sl + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! (sl + 1)
[PROOF STEP]
proof (cases "sl > 0", simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < sl \<Longrightarrow> hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
 2. sl = 0 \<Longrightarrow> hd (tl l) = l ! Suc 0
[PROOF STEP]
show "hd (tl l) = l ! (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl l) = l ! Suc 0
[PROOF STEP]
using \<open>tl l \<noteq> []\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
tl l \<noteq> []
l \<noteq> []

goal (1 subgoal):
 1. hd (tl l) = l ! Suc 0
[PROOF STEP]
by (simp add: hd_conv_nth tl_nth)
[PROOF STATE]
proof (state)
this:
hd (tl l) = l ! Suc 0

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
[PROOF STEP]
assume "0 < sl"
[PROOF STATE]
proof (state)
this:
0 < sl

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
[PROOF STEP]
show "hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! (Suc sl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
[PROOF STEP]
using \<open>sl + 1 < length l\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l
l \<noteq> []

goal (1 subgoal):
 1. hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl
[PROOF STEP]
by (auto simp add: hd_append hd_drop_conv_nth)
[PROOF STATE]
proof (state)
this:
hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! Suc sl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! (sl + 1)

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! (sl + 1)

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "last ?l' = l ! sl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! sl
[PROOF STEP]
proof (cases "sl > 0", simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < sl \<Longrightarrow> last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
 2. sl = 0 \<Longrightarrow> last (tl l) = l ! 0
[PROOF STEP]
show "last (tl l) = l ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (tl l) = l ! 0
[PROOF STEP]
using \<open>l \<noteq> []\<close> \<open>last l = s\<close> \<open>hd l = s\<close> \<open>length l > 2\<close>
[PROOF STATE]
proof (prove)
using this:
l \<noteq> []
last l = s
hd l = s
2 < length l

goal (1 subgoal):
 1. last (tl l) = l ! 0
[PROOF STEP]
by (simp add: hd_conv_nth last_tl)
[PROOF STATE]
proof (state)
this:
last (tl l) = l ! 0

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
[PROOF STEP]
assume "sl > 0"
[PROOF STATE]
proof (state)
this:
0 < sl

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < sl
[PROOF STEP]
show "last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl"
[PROOF STATE]
proof (prove)
using this:
0 < sl

goal (1 subgoal):
 1. last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
[PROOF STEP]
using \<open>l \<noteq> []\<close> \<open>tl l \<noteq> []\<close> \<open>sl + 1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
0 < sl
l \<noteq> []
tl l \<noteq> []
sl + 1 < length l

goal (1 subgoal):
 1. last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl
[PROOF STEP]
by (auto simp add: last_append drop_Suc tl_take last_take_conv_nth tl_nth)
[PROOF STATE]
proof (state)
this:
last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
last (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! sl

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! sl

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "rel_chain ?l' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) r
[PROOF STEP]
proof (cases "sl = 0", simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sl = 0 \<Longrightarrow> rel_chain (tl l) r
 2. 0 < sl \<Longrightarrow> rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sl = 0

goal (2 subgoals):
 1. sl = 0 \<Longrightarrow> rel_chain (tl l) r
 2. 0 < sl \<Longrightarrow> rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
show "rel_chain (tl l) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (tl l) r
[PROOF STEP]
using \<open>rel_chain l r\<close>
[PROOF STATE]
proof (prove)
using this:
rel_chain l r

goal (1 subgoal):
 1. rel_chain (tl l) r
[PROOF STEP]
by (auto intro: rel_chain_tl)
[PROOF STATE]
proof (state)
this:
rel_chain (tl l) r

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
assume "sl > 0"
[PROOF STATE]
proof (state)
this:
0 < sl

goal (1 subgoal):
 1. 0 < sl \<Longrightarrow> rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
show  "rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r
[PROOF STEP]
proof (rule rel_chain_append)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_chain (drop (Suc sl) l) r
 2. rel_chain (tl (take (Suc sl) l)) r
 3. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
show "rel_chain (drop (Suc sl) l) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (drop (Suc sl) l) r
[PROOF STEP]
using \<open>rel_chain l r\<close>
[PROOF STATE]
proof (prove)
using this:
rel_chain l r

goal (1 subgoal):
 1. rel_chain (drop (Suc sl) l) r
[PROOF STEP]
by (auto intro: rel_chain_drop)
[PROOF STATE]
proof (state)
this:
rel_chain (drop (Suc sl) l) r

goal (2 subgoals):
 1. rel_chain (tl (take (Suc sl) l)) r
 2. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rel_chain (tl (take (Suc sl) l)) r
 2. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
show "rel_chain (tl (take (Suc sl) l)) r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_chain (tl (take (Suc sl) l)) r
[PROOF STEP]
using \<open>rel_chain l r\<close>
[PROOF STATE]
proof (prove)
using this:
rel_chain l r

goal (1 subgoal):
 1. rel_chain (tl (take (Suc sl) l)) r
[PROOF STEP]
by (auto intro: rel_chain_tl rel_chain_take)
[PROOF STATE]
proof (state)
this:
rel_chain (tl (take (Suc sl) l)) r

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
have "last (drop (sl + 1) l) = l ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (drop (sl + 1) l) = l ! 0
[PROOF STEP]
using \<open>sl + 1 < length l\<close> \<open>last l = s\<close> \<open>hd l = s\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l
last l = s
hd l = s
l \<noteq> []

goal (1 subgoal):
 1. last (drop (sl + 1) l) = l ! 0
[PROOF STEP]
by (auto simp add: hd_conv_nth)
[PROOF STATE]
proof (state)
this:
last (drop (sl + 1) l) = l ! 0

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last (drop (sl + 1) l) = l ! 0

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
have "sl > 0 \<longrightarrow> tl (take (sl + 1) l) \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []
[PROOF STEP]
using \<open>sl + 1 < length l\<close> \<open>l \<noteq> []\<close> \<open>tl l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l
l \<noteq> []
tl l \<noteq> []

goal (1 subgoal):
 1. 0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []
[PROOF STEP]
by (auto simp add: take_Suc)
[PROOF STATE]
proof (state)
this:
0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []
[PROOF STEP]
have "sl > 0 \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1"
[PROOF STATE]
proof (prove)
using this:
0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []

goal (1 subgoal):
 1. 0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1
[PROOF STEP]
using \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
0 < sl \<longrightarrow> tl (take (sl + 1) l) \<noteq> []
l \<noteq> []

goal (1 subgoal):
 1. 0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1
[PROOF STEP]
by (auto simp add: hd_conv_nth take_Suc tl_nth)
[PROOF STATE]
proof (state)
this:
0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
last (drop (sl + 1) l) = l ! 0
0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1
[PROOF STEP]
show "(last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r"
[PROOF STATE]
proof (prove)
using this:
last (drop (sl + 1) l) = l ! 0
0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
using \<open>rel_chain l r\<close> \<open>length l > 2\<close> \<open>sl > 0\<close>
[PROOF STATE]
proof (prove)
using this:
last (drop (sl + 1) l) = l ! 0
0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1
rel_chain l r
2 < length l
0 < sl

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
unfolding rel_chain_def
[PROOF STATE]
proof (prove)
using this:
last (drop (sl + 1) l) = l ! 0
0 < sl \<longrightarrow> hd (tl (take (sl + 1) l)) = l ! 1
\<forall>k<length l - 1. (l ! k, l ! (k + 1)) \<in> r
2 < length l
0 < sl

goal (1 subgoal):
 1. (last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) \<in> r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_chain (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) r

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_chain (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) r

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "length ?l' = length l - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = length l - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = length l - 1

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hd (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! (sl + 1)
last (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! sl
rel_chain (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) r
length (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = length l - 1
[PROOF STEP]
obtain l' where *: "l' = ?l'" "hd l' = l ! (sl + 1)" "last l' = l ! sl" "rel_chain l' r" "length l' = length l - 1"
[PROOF STATE]
proof (prove)
using this:
hd (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! (sl + 1)
last (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = l ! sl
rel_chain (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) r
length (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)) = length l - 1

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)); hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
hd l' = l ! (sl + 1)
last l' = l ! sl
rel_chain l' r
length l' = length l - 1

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have l'_l: "\<forall> i. i + 1 < length l' \<longrightarrow>
    (\<exists> j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i + 1 < length l' \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i + 1 < length l' \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
assume "i + 1 < length l'"
[PROOF STATE]
proof (state)
this:
i + 1 < length l'

goal (1 subgoal):
 1. \<And>i. i + 1 < length l' \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
show "\<exists> j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
proof (cases "sl = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sl = 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
sl = 0

goal (2 subgoals):
 1. sl = 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sl = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sl = 0

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>i + 1 < length l'\<close>
[PROOF STATE]
proof (prove)
using this:
sl = 0
i + 1 < length l'

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>l' = ?l'\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
sl = 0
i + 1 < length l'
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
l \<noteq> []

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
by (force simp add: tl_nth)
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal (1 subgoal):
 1. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
sl \<noteq> 0

goal (1 subgoal):
 1. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sl \<noteq> 0
[PROOF STEP]
have "length l' = length l - 1"
[PROOF STATE]
proof (prove)
using this:
sl \<noteq> 0

goal (1 subgoal):
 1. length l' = length l - 1
[PROOF STEP]
using \<open>l' = ?l'\<close> \<open>sl + 1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
sl \<noteq> 0
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
sl + 1 < length l

goal (1 subgoal):
 1. length l' = length l - 1
[PROOF STEP]
by (simp add: min_def)
[PROOF STATE]
proof (state)
this:
length l' = length l - 1

goal (1 subgoal):
 1. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length l' = length l - 1
[PROOF STEP]
have "i + 2 < length l"
[PROOF STATE]
proof (prove)
using this:
length l' = length l - 1

goal (1 subgoal):
 1. i + 2 < length l
[PROOF STEP]
using \<open>i + 1 < length l'\<close>
[PROOF STATE]
proof (prove)
using this:
length l' = length l - 1
i + 1 < length l'

goal (1 subgoal):
 1. i + 2 < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i + 2 < length l

goal (1 subgoal):
 1. sl \<noteq> 0 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
proof (cases "i + 1 < length (drop (sl + 1) l)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i + 1 < length (drop (sl + 1) l)

goal (2 subgoals):
 1. i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i + 1 < length (drop (sl + 1) l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i + 1 < length (drop (sl + 1) l)

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>sl \<noteq> 0\<close> \<open>l' = ?l'\<close>
[PROOF STATE]
proof (prove)
using this:
i + 1 < length (drop (sl + 1) l)
sl \<noteq> 0
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
by (force simp add: nth_append)
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal (1 subgoal):
 1. \<not> i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i + 1 < length (drop (sl + 1) l)

goal (1 subgoal):
 1. \<not> i + 1 < length (drop (sl + 1) l) \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
proof (cases "i + 1 > length (drop (sl + 1) l)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length (drop (sl + 1) l) < i + 1

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (drop (sl + 1) l) < i + 1
[PROOF STEP]
have "i + 1 > length l - (sl + 1)"
[PROOF STATE]
proof (prove)
using this:
length (drop (sl + 1) l) < i + 1

goal (1 subgoal):
 1. length l - (sl + 1) < i + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length l - (sl + 1) < i + 1

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
have
            "l' ! i = l ! Suc (i - (length l - Suc sl))"
            "l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
using \<open>i + 2 < length l\<close> \<open>sl + 1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
i + 2 < length l
sl + 1 < length l

goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
using \<open>i + 1 > length l - (sl + 1)\<close>
[PROOF STATE]
proof (prove)
using this:
i + 2 < length l
sl + 1 < length l
length l - (sl + 1) < i + 1

goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
using \<open>sl \<noteq> 0\<close> \<open>l' = ?l'\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
i + 2 < length l
sl + 1 < length l
length l - (sl + 1) < i + 1
sl \<noteq> 0
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
l \<noteq> []

goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
using tl_nth[of "take (sl + 1) l" "i - (length l - Suc sl)"]
[PROOF STATE]
proof (prove)
using this:
i + 2 < length l
sl + 1 < length l
length l - (sl + 1) < i + 1
sl \<noteq> 0
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
l \<noteq> []
take (sl + 1) l \<noteq> [] \<Longrightarrow> tl (take (sl + 1) l) ! (i - (length l - Suc sl)) = take (sl + 1) l ! (i - (length l - Suc sl) + 1)

goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
using tl_nth[of "take (sl + 1) l" "Suc i - (length l - Suc sl)"]
[PROOF STATE]
proof (prove)
using this:
i + 2 < length l
sl + 1 < length l
length l - (sl + 1) < i + 1
sl \<noteq> 0
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
l \<noteq> []
take (sl + 1) l \<noteq> [] \<Longrightarrow> tl (take (sl + 1) l) ! (i - (length l - Suc sl)) = take (sl + 1) l ! (i - (length l - Suc sl) + 1)
take (sl + 1) l \<noteq> [] \<Longrightarrow> tl (take (sl + 1) l) ! (Suc i - (length l - Suc sl)) = take (sl + 1) l ! (Suc i - (length l - Suc sl) + 1)

goal (1 subgoal):
 1. l' ! i = l ! Suc (i - (length l - Suc sl)) &&& l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))
[PROOF STEP]
by (auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
l' ! i = l ! Suc (i - (length l - Suc sl))
l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
have "Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1"
            "Suc (Suc i - (length l - Suc sl)) = (i + sl + 1 - length l + 1) + 1"
            "i + sl + 1 - length l + 1 + 1 < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1 &&& Suc (Suc i - (length l - Suc sl)) = i + sl + 1 - length l + 1 + 1 &&& i + sl + 1 - length l + 1 + 1 < length l
[PROOF STEP]
using \<open>sl + 1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l

goal (1 subgoal):
 1. Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1 &&& Suc (Suc i - (length l - Suc sl)) = i + sl + 1 - length l + 1 + 1 &&& i + sl + 1 - length l + 1 + 1 < length l
[PROOF STEP]
using \<open>i + 1 > length l - (sl + 1)\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l
length l - (sl + 1) < i + 1

goal (1 subgoal):
 1. Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1 &&& Suc (Suc i - (length l - Suc sl)) = i + sl + 1 - length l + 1 + 1 &&& i + sl + 1 - length l + 1 + 1 < length l
[PROOF STEP]
using \<open>i + 2 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
sl + 1 < length l
length l - (sl + 1) < i + 1
i + 2 < length l

goal (1 subgoal):
 1. Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1 &&& Suc (Suc i - (length l - Suc sl)) = i + sl + 1 - length l + 1 + 1 &&& i + sl + 1 - length l + 1 + 1 < length l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1
Suc (Suc i - (length l - Suc sl)) = i + sl + 1 - length l + 1 + 1
i + sl + 1 - length l + 1 + 1 < length l

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
have "l' ! i = l ! (i + sl + 1 - length l + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' ! i = l ! (i + sl + 1 - length l + 1)
[PROOF STEP]
using \<open>l' ! i = l ! Suc (i - (length l - Suc sl))\<close>
[PROOF STATE]
proof (prove)
using this:
l' ! i = l ! Suc (i - (length l - Suc sl))

goal (1 subgoal):
 1. l' ! i = l ! (i + sl + 1 - length l + 1)
[PROOF STEP]
by (subst \<open>Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1\<close>[THEN sym])
[PROOF STATE]
proof (state)
this:
l' ! i = l ! (i + sl + 1 - length l + 1)

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l' ! i = l ! (i + sl + 1 - length l + 1)

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
have "l' ! (i + 1) = l ! ((i + sl + 1 - length l + 1) + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)
[PROOF STEP]
using \<open>l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))\<close>
[PROOF STATE]
proof (prove)
using this:
l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))

goal (1 subgoal):
 1. l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)
[PROOF STEP]
by (subst \<open>Suc (Suc i - (length l - Suc sl)) = (i + sl + 1 - length l + 1) + 1\<close>[THEN sym])
[PROOF STATE]
proof (state)
this:
l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)

goal (2 subgoals):
 1. length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
 2. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l' ! i = l ! (i + sl + 1 - length l + 1)
l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l' ! i = l ! (i + sl + 1 - length l + 1)
l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>i + sl + 1 - length l + 1 + 1 < length l\<close>
[PROOF STATE]
proof (prove)
using this:
l' ! i = l ! (i + sl + 1 - length l + 1)
l' ! (i + 1) = l ! (i + sl + 1 - length l + 1 + 1)
i + sl + 1 - length l + 1 + 1 < length l

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length (drop (sl + 1) l) < i + 1

goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> length (drop (sl + 1) l) < i + 1
[PROOF STEP]
have "i + 1 = length l - sl - 1"
[PROOF STATE]
proof (prove)
using this:
\<not> length (drop (sl + 1) l) < i + 1

goal (1 subgoal):
 1. i + 1 = length l - sl - 1
[PROOF STEP]
using \<open>\<not> i + 1 < length (drop (sl + 1) l)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> length (drop (sl + 1) l) < i + 1
\<not> i + 1 < length (drop (sl + 1) l)

goal (1 subgoal):
 1. i + 1 = length l - sl - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i + 1 = length l - sl - 1

goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i + 1 = length l - sl - 1
[PROOF STEP]
have "length l - 1 = sl + i + 1"
[PROOF STATE]
proof (prove)
using this:
i + 1 = length l - sl - 1

goal (1 subgoal):
 1. length l - 1 = sl + i + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length l - 1 = sl + i + 1

goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length l - 1 = sl + i + 1
[PROOF STEP]
have "l ! Suc (sl + i) = last l"
[PROOF STATE]
proof (prove)
using this:
length l - 1 = sl + i + 1

goal (1 subgoal):
 1. l ! Suc (sl + i) = last l
[PROOF STEP]
using last_conv_nth[of l, THEN sym] \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
length l - 1 = sl + i + 1
l \<noteq> [] \<Longrightarrow> l ! (length l - 1) = last l
l \<noteq> []

goal (1 subgoal):
 1. l ! Suc (sl + i) = last l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l ! Suc (sl + i) = last l

goal (1 subgoal):
 1. \<not> length (drop (sl + 1) l) < i + 1 \<Longrightarrow> \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l ! Suc (sl + i) = last l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l ! Suc (sl + i) = last l

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>i + 1 = length l - sl - 1\<close>
[PROOF STATE]
proof (prove)
using this:
l ! Suc (sl + i) = last l
i + 1 = length l - sl - 1

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>l' = ?l'\<close> \<open>sl \<noteq> 0\<close> \<open>l \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
l ! Suc (sl + i) = last l
i + 1 = length l - sl - 1
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
sl \<noteq> 0
l \<noteq> []

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using tl_nth[of "take (sl + 1) l" 0]
[PROOF STATE]
proof (prove)
using this:
l ! Suc (sl + i) = last l
i + 1 = length l - sl - 1
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
sl \<noteq> 0
l \<noteq> []
take (sl + 1) l \<noteq> [] \<Longrightarrow> tl (take (sl + 1) l) ! 0 = take (sl + 1) l ! (0 + 1)

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
using \<open>hd l = s\<close> \<open>last l = s\<close>
[PROOF STATE]
proof (prove)
using this:
l ! Suc (sl + i) = last l
i + 1 = length l - sl - 1
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
sl \<noteq> 0
l \<noteq> []
take (sl + 1) l \<noteq> [] \<Longrightarrow> tl (take (sl + 1) l) ! 0 = take (sl + 1) l ! (0 + 1)
hd l = s
last l = s

goal (1 subgoal):
 1. \<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)
[PROOF STEP]
by (force simp add: nth_append hd_conv_nth)
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using * l'_l
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))
l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l))
hd l' = l ! (sl + 1)
last l' = l ! sl
rel_chain l' r
length l' = length l - 1
\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))

goal (1 subgoal):
 1. thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1)); l' = (if sl = 0 then tl l else drop (sl + 1) l @ tl (take (sl + 1) l)); hd l' = l ! (sl + 1); last l' = l ! sl; rel_chain l' r; length l' = length l - 1; \<forall>i. i + 1 < length l' \<longrightarrow> (\<exists>j. j + 1 < length l \<and> l' ! i = l ! j \<and> l' ! (i + 1) = l ! (j + 1))\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma linear_plus_norm:
  includes notation_norm
  assumes \<open>linear f\<close>
  shows \<open>\<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
text \<open>
  Explanation: For arbitrary \<^term>\<open>x\<close> and a linear operator \<^term>\<open>f\<close>,
  \<^term>\<open>norm (f \<xi>)\<close> is upper bounded by the maximum of the norms
  of the shifts of \<^term>\<open>f\<close> (i.e., \<^term>\<open>f (x + \<xi>)\<close> and \<^term>\<open>f (x - \<xi>)\<close>).
\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
have \<open>norm (f \<xi>) = norm ( (inverse (of_nat 2)) *\<^sub>R (f (x + \<xi>) - f (x - \<xi>)) )\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> = \<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel>
[PROOF STEP]
by (smt add_diff_cancel_left' assms diff_add_cancel diff_diff_add linear_diff midpoint_def
        midpoint_plus_self of_nat_1 of_nat_add one_add_one scaleR_half_double)
[PROOF STATE]
proof (state)
this:
\<parallel>f \<xi>\<parallel> = \<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>f \<xi>\<parallel> = \<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
have \<open>\<dots> = inverse (of_nat 2) * norm (f (x + \<xi>) - f (x - \<xi>))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel> = inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel>
[PROOF STEP]
using Real_Vector_Spaces.real_normed_vector_class.norm_scaleR
[PROOF STATE]
proof (prove)
using this:
\<parallel>?a *\<^sub>R ?x\<parallel> = \<bar>?a\<bar> * \<parallel>?x\<parallel>

goal (1 subgoal):
 1. \<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel> = inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel> = inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>(f (x + \<xi>) - f (x - \<xi>)) /\<^sub>R real 2\<parallel> = inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
have \<open>\<dots> \<le> inverse (of_nat 2) * (norm (f (x + \<xi>)) + norm (f (x - \<xi>)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel> \<le> inverse (real 2) * (\<parallel>f (x + \<xi>)\<parallel> + \<parallel>f (x - \<xi>)\<parallel>)
[PROOF STEP]
by (simp add: norm_triangle_ineq4)
[PROOF STATE]
proof (state)
this:
inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel> \<le> inverse (real 2) * (\<parallel>f (x + \<xi>)\<parallel> + \<parallel>f (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (real 2) * \<parallel>f (x + \<xi>) - f (x - \<xi>)\<parallel> \<le> inverse (real 2) * (\<parallel>f (x + \<xi>)\<parallel> + \<parallel>f (x - \<xi>)\<parallel>)

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
have \<open>\<dots> \<le>  max (norm (f (x + \<xi>))) (norm (f (x - \<xi>)))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real 2) * (\<parallel>f (x + \<xi>)\<parallel> + \<parallel>f (x - \<xi>)\<parallel>) \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inverse (real 2) * (\<parallel>f (x + \<xi>)\<parallel> + \<parallel>f (x - \<xi>)\<parallel>) \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>

goal (1 subgoal):
 1. \<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>f \<xi>\<parallel> \<le> max \<parallel>f (x + \<xi>)\<parallel> \<parallel>f (x - \<xi>)\<parallel>

goal:
No subgoals!
[PROOF STEP]
qed