Theory Simplex.Rel_Chain
theory Rel_Chain
imports
Simplex_Auxiliary
begin
definition
rel_chain :: "'a list ⇒ ('a × 'a) set ⇒ bool"
where
"rel_chain l r = (∀ k < length l - 1. (l ! k, l ! (k + 1)) ∈ r)"
lemma
rel_chain_Nil: "rel_chain [] r" and
rel_chain_Cons: "rel_chain (x # xs) r = (if xs = [] then True else ((x, hd xs) ∈ r) ∧ rel_chain xs r)"
by (auto simp add: rel_chain_def hd_conv_nth nth_Cons split: nat.split_asm nat.split)
lemma rel_chain_drop:
"rel_chain l R ==> rel_chain (drop n l) R"
unfolding rel_chain_def
by simp
lemma rel_chain_take:
"rel_chain l R ==> rel_chain (take n l) R"
unfolding rel_chain_def
by simp
lemma rel_chain_butlast:
"rel_chain l R ==> rel_chain (butlast l) R"
unfolding rel_chain_def
by (auto simp add: butlast_nth)
lemma rel_chain_tl:
"rel_chain l R ==> rel_chain (tl l) R"
unfolding rel_chain_def
by (cases "l = []") (auto simp add: tl_nth)
lemma rel_chain_append:
assumes "rel_chain l R" "rel_chain l' R" "(last l, hd l') ∈ R"
shows "rel_chain (l @ l') R"
using assms
by (induct l) (auto simp add: rel_chain_Cons split: if_splits)
lemma rel_chain_appendD:
assumes "rel_chain (l @ l') R"
shows "rel_chain l R" "rel_chain l' R" "l ≠ [] ∧ l' ≠ [] ⟶ (last l, hd l') ∈ R"
using assms
by (induct l) (auto simp add: rel_chain_Cons rel_chain_Nil split: if_splits)
lemma rtrancl_rel_chain:
"(x, y) ∈ R⇧* ⟷ (∃ l. l ≠ [] ∧ hd l = x ∧ last l = y ∧ rel_chain l R)"
(is "?lhs = ?rhs")
proof
assume ?lhs
then show ?rhs
by (induct rule: converse_rtrancl_induct) (auto simp add: rel_chain_Cons)
next
assume ?rhs
then obtain l where "l ≠ []" "hd l = x" "last l = y" "rel_chain l R"
by auto
then show ?lhs
by (induct l arbitrary: x) (auto simp add: rel_chain_Cons, force)
qed
lemma trancl_rel_chain:
"(x, y) ∈ R⇧+ ⟷ (∃ l. l ≠ [] ∧ length l > 1 ∧ hd l = x ∧ last l = y ∧ rel_chain l R)" (is "?lhs ⟷ ?rhs")
proof
assume ?lhs
then obtain z where "(x, z) ∈ R" "(z, y) ∈ R⇧*"
by (auto dest: tranclD)
then obtain l where "l ≠ [] ∧ hd l = z ∧ last l = y ∧ rel_chain l R"
by (auto simp add: rtrancl_rel_chain)
then show ?rhs
using ‹(x, z) ∈ R›
by (rule_tac x="x # l" in exI) (auto simp add: rel_chain_Cons)
next
assume ?rhs
then obtain l where "1 < length l" "l ≠ []" "hd l = x" "last l = y" "rel_chain l R"
by auto
then obtain l' where
"l' ≠ []" "l = x # l'" "(x, hd l') ∈ R" "rel_chain l' R"
using ‹1 < length l›
by (cases l) (auto simp add: rel_chain_Cons)
then have "(x, hd l') ∈ R" "(hd l', y) ∈ R⇧*"
using ‹last l = y›
by (auto simp add: rtrancl_rel_chain)
then show ?lhs
by auto
qed
lemma rel_chain_elems_rtrancl:
assumes "rel_chain l R" "i ≤ j" "j < length l"
shows "(l ! i, l ! j) ∈ R⇧*"
proof (cases "i = j")
case True
then show ?thesis
by simp
next
case False
then have "i < j"
using ‹i ≤ j›
by simp
then have "l ≠ []"
using ‹j < length l›
by auto
let ?l = "drop i (take (j + 1) l)"
have "?l ≠ []"
using ‹i < j› ‹j < length l›
by simp
moreover
have "hd ?l = l ! i"
using ‹?l ≠ []› ‹i < j›
by (auto simp add: hd_conv_nth)
moreover
have "last ?l = l ! j"
using ‹?l ≠ []› ‹l ≠ []› ‹i < j› ‹j < length l›
by (cases "length l = j + 1") (auto simp add: last_conv_nth min_def)
moreover
have "rel_chain ?l R"
using ‹rel_chain l R›
by (auto intro: rel_chain_drop rel_chain_take)
ultimately
show ?thesis
by (subst rtrancl_rel_chain) blast
qed
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"
"∀ i. i + 1 < length l' ⟶
(∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1))"
proof-
have "l ≠ []"
using ‹length l > 2›
by auto
have "length (tl l) > 1" "tl l ≠ []"
using ‹length l > 2›
by (auto simp add: length_0_conv[THEN sym])
let ?l' = "if sl = 0 then
tl l
else
drop (sl + 1) l @ tl (take (sl + 1) l)"
have "hd ?l' = l ! (sl + 1)"
proof (cases "sl > 0", simp_all)
show "hd (tl l) = l ! (Suc 0)"
using ‹tl l ≠ []› ‹l ≠ []›
by (simp add: hd_conv_nth tl_nth)
next
assume "0 < sl"
show "hd (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! (Suc sl)"
using ‹sl + 1 < length l› ‹l ≠ []›
by (auto simp add: hd_append hd_drop_conv_nth)
qed
moreover
have "last ?l' = l ! sl"
proof (cases "sl > 0", simp_all)
show "last (tl l) = l ! 0"
using ‹l ≠ []› ‹last l = s› ‹hd l = s› ‹length l > 2›
by (simp add: hd_conv_nth last_tl)
next
assume "sl > 0"
then show "last (drop (Suc sl) l @ tl (take (Suc sl) l)) = l ! sl"
using ‹l ≠ []› ‹tl l ≠ []› ‹sl + 1 < length l›
by (auto simp add: last_append drop_Suc tl_take last_take_conv_nth tl_nth)
qed
moreover
have "rel_chain ?l' r"
proof (cases "sl = 0", simp_all)
case True
show "rel_chain (tl l) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_tl)
next
assume "sl > 0"
show "rel_chain (drop (Suc sl) l @ tl (take (Suc sl) l)) r"
proof (rule rel_chain_append)
show "rel_chain (drop (Suc sl) l) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_drop)
next
show "rel_chain (tl (take (Suc sl) l)) r"
using ‹rel_chain l r›
by (auto intro: rel_chain_tl rel_chain_take)
next
have "last (drop (sl + 1) l) = l ! 0"
using ‹sl + 1 < length l› ‹last l = s› ‹hd l = s› ‹l ≠ []›
by (auto simp add: hd_conv_nth)
moreover
have "sl > 0 ⟶ tl (take (sl + 1) l) ≠ []"
using ‹sl + 1 < length l› ‹l ≠ []› ‹tl l ≠ []›
by (auto simp add: take_Suc)
then have "sl > 0 ⟶ hd (tl (take (sl + 1) l)) = l ! 1"
using ‹l ≠ []›
by (auto simp add: hd_conv_nth take_Suc tl_nth)
ultimately
show "(last (drop (Suc sl) l), hd (tl (take (Suc sl) l))) ∈ r"
using ‹rel_chain l r› ‹length l > 2› ‹sl > 0›
unfolding rel_chain_def
by simp
qed
qed
moreover
have "length ?l' = length l - 1"
by auto
ultimately
obtain l' where *: "l' = ?l'" "hd l' = l ! (sl + 1)" "last l' = l ! sl" "rel_chain l' r" "length l' = length l - 1"
by auto
have l'_l: "∀ i. i + 1 < length l' ⟶
(∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1))"
proof (safe)
fix i
assume "i + 1 < length l'"
show "∃ j. j + 1 < length l ∧ l' ! i = l ! j ∧ l' ! (i + 1) = l ! (j + 1)"
proof (cases "sl = 0")
case True
then show ?thesis
using ‹i + 1 < length l'›
using ‹l' = ?l'› ‹l ≠ []›
by (force simp add: tl_nth)
next
case False
then have "length l' = length l - 1"
using ‹l' = ?l'› ‹sl + 1 < length l›
by (simp add: min_def)
then have "i + 2 < length l"
using ‹i + 1 < length l'›
by simp
show ?thesis
proof (cases "i + 1 < length (drop (sl + 1) l)")
case True
then show ?thesis
using ‹sl ≠ 0› ‹l' = ?l'›
by (force simp add: nth_append)
next
case False
show ?thesis
proof (cases "i + 1 > length (drop (sl + 1) l)")
case True
then have "i + 1 > length l - (sl + 1)"
by auto
have
"l' ! i = l ! Suc (i - (length l - Suc sl))"
"l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))"
using ‹i + 2 < length l› ‹sl + 1 < length l›
using ‹i + 1 > length l - (sl + 1)›
using ‹sl ≠ 0› ‹l' = ?l'› ‹l ≠ []›
using tl_nth[of "take (sl + 1) l" "i - (length l - Suc sl)"]
using tl_nth[of "take (sl + 1) l" "Suc i - (length l - Suc sl)"]
by (auto simp add: nth_append)
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"
using ‹sl + 1 < length l›
using ‹i + 1 > length l - (sl + 1)›
using ‹i + 2 < length l›
by auto
have "l' ! i = l ! (i + sl + 1 - length l + 1)"
using ‹l' ! i = l ! Suc (i - (length l - Suc sl))›
by (subst ‹Suc (i - (length l - Suc sl)) = i + sl + 1 - length l + 1›[THEN sym])
moreover
have "l' ! (i + 1) = l ! ((i + sl + 1 - length l + 1) + 1)"
using ‹l' ! (i + 1) = l ! Suc (Suc i - (length l - Suc sl))›
by (subst ‹Suc (Suc i - (length l - Suc sl)) = (i + sl + 1 - length l + 1) + 1›[THEN sym])
ultimately
show ?thesis
using ‹i + sl + 1 - length l + 1 + 1 < length l›
by force
next
case False
then have "i + 1 = length l - sl - 1"
using ‹¬ i + 1 < length (drop (sl + 1) l)›
by simp
then have "length l - 1 = sl + i + 1"
by auto
then have "l ! Suc (sl + i) = last l"
using last_conv_nth[of l, THEN sym] ‹l ≠ []›
by simp
then show ?thesis
using ‹i + 1 = length l - sl - 1›
using ‹l' = ?l'› ‹sl ≠ 0› ‹l ≠ []›
using tl_nth[of "take (sl + 1) l" 0]
using ‹hd l = s› ‹last l = s›
by (force simp add: nth_append hd_conv_nth)
qed
qed
qed
qed
then show thesis
using * l'_l
apply -
..
qed
end