Quelle  Rel_Chain.thy

(* Authors: F. Maric, M. Spasic *)
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